メインコンテンツへスキップ
セキュリティとテスト

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.