Cardano高保証
Cardano上で安全かつ検証可能なスマートコントラクト開発のための自動形式検証と統合開発者ツールキットを提供します。
The team behind the initiative
The opportunity
Cardano has already proven that automated formal verification works at production scale. Blaster, IO’s formal verification tool for Lean 4, has proven correctness properties for production DApps including Djed and USDCx, and demonstrated the ability to detect common Cardano vulnerabilities in a fully automated fashion. That is a genuine competitive advantage, and this initiative is about extending it to every developer in the ecosystem.
Two capabilities are ready to scale. First, formal verification itself: Blaster currently operates on individual scripts and benefits from specialist expertise. The opportunity is to extend it to full DApp-level verification, integrate it across multiple smart contract languages, and make it accessible through familiar developer tools like VS Code. Second, the developer environment: experienced engineers still spend significant time configuring tools and libraries before writing their first line of contract code. A containerized, pre-configured environment eliminates that friction and brings the full high-assurance toolkit within reach from day one.
The Initiative
Cardano高保証
This proposal funds two tightly complementary workstreams under the Cardano High Assurance umbrella.
- Workstream 1: Blaster Formal Verification. Extends Blaster from single-contract to full DApp-level verification. Integrates formal verification into four smart contract languages: Aiken (with Midgard Labs), Pebble (with Harmonic Labs), Scalus (with Lantr), and Futura (with SAIB). Delivers a Visual Studio Code extension with visual counterexample exploration, a Common Vulnerability Library with pre-built property templates for major DApp categories, an equivalence checking tool that formally proves two UPLC programs are semantically identical, and a proof reconstruction module (with TxPipe and No.Witness Labs) that removes Blaster from the trusted codebase.
- Workstream 2: Developer Environments for the High Assurance Toolkit. Delivers a single-command, pre-configured Container-Based Developer Environment (CBDE) that includes the complete Plinth toolchain: compilers, libraries, property-based testing, static analysis, formal verification, and profiling, all at verified, compatible versions. Also integrates IO’s high-assurance tools into cardano-init (if funded in TWGA 1), with each tool’s preconfiguration and templates for an easy start.
The formal verification workstream is structured as a consortium. Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness Labs, and TxPipe each contribute defined work packages, distributing delivery and long-term maintenance responsibilities across the ecosystem. IO brings deep protocol knowledge and Blaster’s verification core; each partner brings dedicated operational focus and their own developer communities.
Treasury ask: ₳13,078,578
Who is building
This initiative is led by Stefano Leone and Romain Soulat at Input Output, working alongside a consortium of ecosystem collaborators: Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness Labs, and TxPipe.
Expected outcomes
- Automated formal verification extended from single contracts to full DApp-level protocol verification, with proven correctness properties accessible to developers across Aiken, Pebble, Scalus, and Futura.
- A VS Code extension that brings formal verification directly into the developer’s IDE, with visual counterexample exploration and source-level verification feedback.
- An equivalence checking tool that lets developers apply aggressive UPLC optimizations with machine-checked proof that behavior is unchanged, improving throughput utilization per transaction.
- A Common Vulnerability Library with ready-made property templates for major DApp categories, including DEXs, lending protocols, and bridges, produced in collaboration with auditing partners.
- A containerized developer environment (CBDE) that converts the current multi-day setup process into a 60-second initialization, with the complete Plinth toolchain pre-configured and ready to use.
Ecosystem Impact
形式検証は、機関投資家の資本がCardano dAppにコミットすることを妨げるセキュリティリスクを直接対処します。共通脆弱性ライブラリと言語統合がCardano開発者の大多数に検証をアクセス可能にするにつれて、dAppセキュリティへの累積効果がTVL成長のための防御可能な基盤を生み出します。
等価チェックツールにより、開発者は動作が変わらないという証明を持って積極的な最適化を適用でき、プロトコルレベルのパラメータ変更なしにブロックあたりの実効スループットを改善します。CBDEは現在のセットアップ障壁を直接60秒の初期化に変換し、開発者のオンボーディング離脱の大幅な削減を目指します。
この取り組みはMAUと月間トランザクションの2030エコシステムKPIを直接サポートし、TVL、収益/採用、スループット能力の改善を可能にします。
Governance links
Formal treasury proposal
The on-chain submission, read the full proposal text and rationale.
View the formal proposalJoin the Conversation
Ask questions, share views, and follow the community debate.
X Spaces