Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

Sécurité · Éducation · Analyse · Vérification formelle · Exécution symbolique · Outils de débogage · Vérification à l'exécution · Vyper

Réseaux sociaux runtimeverification/evm-semantics(586 ☆)

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.

Related resources

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.

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 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.

Verifereum

Verifereum connecte les contrats intelligents Ethereum à la démonstration de théorèmes soutenue par HOL4 afin que vous puissiez viser des affirmations d'exactitude très fortes lorsque les approches SMT automatisées ne suffisent pas.