Cardano High Assurance | Momentum 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 High Assurance

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.

"Formal verification used to require a PhD and three months of setup. We are collapsing that to an afternoon with a container image and an AI assistant. The math stays rigorous. The experience becomes human."

Stefano LeoneInitiative Owner

"The Cardano ecosystem needs more than audits; it needs verification tooling that every developer can reach for in their own workflow. Blaster does exactly that by making automated formal verification a first-class part of building on Cardano, and at No.Witness Labs we see it as foundational to the next generation of high-assurance DApps, which is why we're contributing to the DevX and Generic Security Properties work packages."

Jonathan RodriguezCo-Founder, No.Witness Labs

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

Formal verification directly addresses the security risk that deters institutional capital from committing to Cardano DApps. As the Common Vulnerability Library and language integrations make verification accessible to the majority of Cardano developers, the cumulative effect on DApp security creates a defensible basis for TVL growth.

The equivalence checking tool enables developers to apply aggressive optimizations with proof that behavior is unchanged, improving effective throughput per block without requiring protocol-level parameter changes. CBDE directly converts the current setup barrier into a 60-second initialization, targeting a significant reduction in developer onboarding attrition.

This initiative directly supports the 2030 Ecosystem KPIs for MAU and Monthly Transactions, while enabling improvements in TVL, Revenue/Adoption, and Throughput Capacity.

Governance links

Formal treasury proposal

The on-chain submission, read the full proposal text and rationale.

View the formal proposal

Join the Conversation

Ask questions, share views, and follow the community debate.

X Spaces