Перейти к основному контенту
Kontrol - formal verification tool based on Foundry and KEVM
Security & testing

Kontrol - formal verification tool based on Foundry and KEVM

Formal verification

Foundry · Обучение · Управление · Формальная верификация · Solidity · Верификация во время выполнения · Развертывание контрактов · Статический анализ

Социальные сети (opens in a new tab)runtimeverification/kontrol(118 ☆) (opens in a new tab)runtimeverification/optimism-ci(4 ☆) (opens in a new tab)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆) (opens in a new tab)runtimeverification/yearn-v3-term-vault(0 ☆) (opens in a new tab)runtimeverification/Depeg-swap(0 ☆) (opens in a new tab)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆) (opens in a new tab)

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

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

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

hax

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

Act

Act

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

Verifereum

Verifereum

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