Certora AutoProver

hax — это инструмент для высоконадежной трансляции большого подмножества Rust в формальные языки, такие как F* или 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.

Kontrol преобразует тесты свойств Foundry в доказательства на базе KEVM, чтобы вы могли получать формальные гарантии с меньшим объемом ручного написания спецификаций, чем при использовании только чистого KEVM.