Zum Hauptinhalt springen
Sicherheit & Testing

Certora Prover

Formale Verifikation

Auf GitHub ansehen (öffnet in einem neuen Tab)

Nächstes ansehen

Kontrol - formal verification tool based on Foundry and KEVM

Über 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

  • Formale Verifikation
  • Verifikation
  • Sicherheit

RepositoryCertora

Info

Typ
Formale Verifikation
GitHub-Sterne
339
Lizenz
GPL-3.0
Eintrag überprüft
September 2026

Ähnliche Tools

K Semantics of the Ethereum Virtual Machine (EVM)

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.

hax

hax

hax ist ein Tool für hochsichere Übersetzungen einer großen Teilmenge von Rust in formale Sprachen wie F* oder Rocq.

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.