Verifereum

KEVM è la semantica eseguibile del K-framework dell'EVM: puntalo al bytecode quando hai bisogno di un'esecuzione con controllo di conformità, esplorazione simbolica, ragionamento sul gas o prove che seguono da vicino le regole di Ethereum.

hax è uno strumento per traduzioni ad alta garanzia di un ampio sottoinsieme di Rust in linguaggi formali come F* o 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.