Zum Hauptinhalt springen
Sicherheit & Testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formale Verifikation

Auf GitHub ansehen (öffnet in einem neuen Tab)K Semantics of the Ethereum Virtual Machine (EVM) auf X (öffnet in einem neuen Tab)

Nächstes ansehen

hax

Über K Semantics of the Ethereum Virtual Machine (EVM)

KEVM ist die ausführbare K-Framework-Semantik der EVM: Wenden Sie sie auf Bytecode an, wenn Sie konformitätsgeprüfte Ausführung, symbolische Erkundung, Gas-Analysen oder Beweise benötigen, die den Regeln von Ethereum genau folgen.

Tags

  • Sicherheit
  • Bildung
  • Analytics
  • Formale Verifikation
  • Symbolische Ausführung
  • Debugging-Tools
  • Laufzeitverifikation
  • Vyper

Repositoryruntimeverification

Info

Typ
Formale Verifikation
GitHub-Sterne
595
Lizenz
BSD-3-Clause
Eintrag überprüft
Juni 2026

Ähnliche Tools

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 hebt Foundry-Eigenschaftstests in KEVM-gestützte Beweise, sodass Sie formale Garantien mit weniger handgeschriebener Spezifikationsarbeit als mit reinem KEVM allein anstreben können.

Act

Act

Act ist Ethereums deklarative Spezifikationssprache und Toolchain zur Beschreibung aller Verhaltensweisen eines EVM-Programms, sodass SMT-Solver, Theorembeweiser oder wirtschaftliche Analysetools über die Korrektheit auf Bytecode-Ebene und die Anreizkompatibilität nachdenken können, einschließlich automatischer Verfeinerungsbeweise gegen konkrete Implementierungen.