Verifereum

KEVM je spustitelná sémantika EVM v K-frameworku: namiřte ji na bajtkód, když potřebujete provádění s kontrolou shody, symbolické zkoumání, uvažování o gasu nebo důkazy, které přesně sledují pravidla Etherea.

hax je nástroj pro vysoce spolehlivé překlady velké podmnožiny jazyka Rust do formálních jazyků, jako jsou F* nebo 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.