Перейти до основного вмісту
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 недостатньо.