Passer au contenu principal
Sécurité et tests

K Semantics of the Ethereum Virtual Machine (EVM)

Vérification formelle

Voir sur GitHub (s'ouvre dans un nouvel onglet)K Semantics of the Ethereum Virtual Machine (EVM) sur X (s'ouvre dans un nouvel onglet)

Voir le suivant

hax

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

Tags

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

Dépôtruntimeverification

Informations

Type
Vérification formelle
Étoiles GitHub
595
Licence
BSD-3-Clause
Fiche révisée
juin 2026

Outils similaires

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.

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.