跳转到主要内容
安全与测试

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 框架可执行语义：当你需要一致性检查执行、符号探索、Gas 推理或密切跟踪以太坊规则的证明时，可以将其指向字节码。

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.