跳至主要內容
安全性與測試

Kontrol - formal verification tool based on Foundry and KEVM

形式化驗證

在 GitHub 上查看 (在新分頁開啟)X 上的 Kontrol - formal verification tool based on Foundry and KEVM (在新分頁開啟)

查看下一個

Act

關於 Kontrol - formal verification tool based on Foundry and KEVM

Kontrol 將 Foundry 屬性測試提升為由 KEVM 支援的證明，因此您可以追求形式化保證，而所需的手寫規範工作比單獨使用原始 KEVM 更少。

標籤

  • Foundry
  • 教育
  • 治理
  • 形式化驗證
  • Solidity
  • 執行階段驗證
  • 合約部署
  • 靜態分析

儲存庫runtimeverification

資訊

類型
形式化驗證
GitHub 星數
127
授權條款
BSD-3-Clause
資訊審查日期
2026年6月

類似工具

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM 是 EVM 的 K 框架可執行語意：當您需要一致性檢查執行、符號探索、燃料推論或密切追蹤以太坊規則的證明時，可以將其指向位元組碼。

hax

hax

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

Certora Prover

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.