Verifereum

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 ist ein Tool für hochsichere Übersetzungen einer großen Teilmenge von Rust in formale Sprachen wie F* oder Rocq.

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.