跳至主要內容
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 框架可執行語意：當您需要一致性檢查執行、符號探索、燃料推論或密切追蹤以太坊規則的證明時，可以將其指向位元組碼。

hax

hax 是一個工具，用於將大部分 Rust 高保證地翻譯成 F* 或 Rocq 等形式化語言。

Act

Act

Act 是以太坊的宣告式規範語言和工具鏈，用於描述 EVM 程式的所有行為，以便 SMT 求解器、定理證明器或經濟分析工具能夠推論位元組碼層級的正確性和誘因相容性，包括針對具體實作的自動精煉證明。

Verifereum

Verifereum

Verifereum 將以太坊智能合約連接到由 HOL4 支援的定理證明，因此當自動化 SMT 方法不足時，您可以追求非常強大的正確性聲明。