Passer au contenu principal
Sécurité et tests

Certora AutoProver

Vérification formelle

Voir sur GitHub (s'ouvre dans un nouvel onglet)

Voir le suivant

K Semantics of the Ethereum Virtual Machine (EVM)

À propos de Certora AutoProver

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Tags

  • Vérification formelle
  • Vérification

DépôtCertora

Informations

Type
Vérification formelle
Étoiles GitHub
17
Licence
GPL-3.0
Fiche révisée
septembre 2026

Outils similaires

hax

hax

hax est un outil pour les traductions à haute assurance d'un grand sous-ensemble de Rust vers des langages formels tels que F* ou Rocq.

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol élève les tests de propriétés de Foundry en preuves soutenues par KEVM afin que vous puissiez rechercher des garanties formelles avec moins de travail de spécification manuelle que le KEVM brut seul.