Certora Prover

KEVM — это исполняемая семантика EVM на базе K-framework: используйте ее с байт-кодом, когда вам нужно выполнение с проверкой соответствия, символьное исследование, анализ газа или доказательства, которые строго следуют правилам Эфириума.

hax — это инструмент для высоконадежной трансляции большого подмножества Rust в формальные языки, такие как F* или Rocq.

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

Act — это декларативный язык спецификаций Эфириума и набор инструментов для описания всех вариантов поведения EVM-программы, чтобы SMT-решатели, системы автоматического доказательства теорем или инструменты экономического анализа могли делать выводы о корректности на уровне байт-кода и совместимости стимулов, включая автоматические доказательства уточнения для конкретных реализаций.

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Verifereum подключает смарт-контракты Эфириума к доказательству теорем на базе HOL4, чтобы вы могли добиваться очень строгих гарантий корректности, когда автоматизированных подходов SMT недостаточно.