Безпека та тестування

Certora Prover

Формальна верифікація

Формальна верифікація · Верифікація · Безпека

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.

Пов'язані ресурси

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM — це виконувана семантика EVM у K-framework: вкажіть їй на байт-код, коли вам потрібне виконання з перевіркою відповідності, символьне дослідження, міркування щодо газу або доведення, які тісно відстежують правила Етеріуму.

hax

hax — це інструмент для високонадійних перекладів великої підмножини Rust на формальні мови, такі як F* або Rocq.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol перетворює тести властивостей Foundry на доведення на базі KEVM, щоб ви могли досягати формальних гарантій з меншим обсягом написаних вручну специфікацій, ніж при використанні лише чистого KEVM.

Act

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

Certora AutoProver

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

Verifereum підключає смарт-контракти Етеріуму до доведення теорем на базі HOL4, щоб ви могли прагнути до дуже сильних заяв про правильність, коли автоматизованих підходів SMT недостатньо.