Passer au contenu principal
Sécurité et tests

Certora Prover

Vérification formelle

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

Voir le suivant

Kontrol - formal verification tool based on Foundry and KEVM

À propos de 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.

Tags

  • Vérification formelle
  • Vérification
  • Sécurité

DépôtCertora

Informations

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

Outils similaires

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM est la sémantique exécutable du framework K de l'EVM : pointez-le vers le bytecode lorsque vous avez besoin d'une exécution vérifiée en termes de conformité, d'une exploration symbolique, d'un raisonnement sur le gaz ou de preuves qui suivent de près les règles d'Ethereum.

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.

Act

Act

Act est le langage de spécification déclarative et la chaîne d'outils d'Ethereum pour décrire tous les comportements d'un programme EVM afin que les solveurs SMT, les démonstrateurs de théorèmes ou les outils d'analyse économique puissent raisonner sur l'exactitude au niveau du bytecode et la compatibilité des incitations, y compris les preuves de raffinement automatique par rapport aux implémentations concrètes.