Act

KEVM est la sémantique exécutable du framework K de l'EVM : pointez-le vers le bytecode lorsque vous avez besoin d'une exécution vérifiée en termes de conformité, d'une exploration symbolique, d'un raisonnement sur le gaz ou de preuves qui suivent de près les règles d'Ethereum.

hax est un outil pour les traductions à haute assurance d'un grand sous-ensemble de Rust vers des langages formels tels que F* ou 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.