At a glance
- By Q1 2027, any Cardano developer will be able to run automated formal verification on their smart contracts and spin up a fully pre-configured development environment with a single command -no formal methods background required.
- This proposal funds two workstreams: extending Blaster (our automated verification engine, already proven on production DApps) to full DApp-level verification across four new smart contract languages (besides Plinth, the new languages will be: Aiken, Scalus, Futura, and Pebble), and delivering a containerised developer environment that packages the full Cardano High Assurance toolkit at verified, compatible versions.
- The result: 20-50 active developers performing formal verification; 3-8 projects adopting end-to-end formal methods; 10-25 verified vulnerabilities discovered; and $10m-$50m in TVL from formally verified DApps.
- We lead delivery with six ecosystem partners (Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness Labs, and TxPipe), each owning defined components. Execution and long-term maintenance are distributed across the ecosystem.
- The treasury withdrawal of 13,078,578 ada is subject to DRep vote. Review the full proposal and vote on the Cardano governance portal.
Cardano was built for serious applications
Cardano was designed for applications where correctness matters: DeFi, identity, and financial infrastructure. The extended UTXO model and Plutus's functional foundations reflect that premise, with formal verification as a long-term goal.
That goal is now practical. This past cycle, we proved Blaster, our automated formal verification engine for Lean 4, can verify Cardano smart contracts at production scale. Running against Djed and USDCx , it proved the absence of common vulnerabilities automatically. The capability works. This proposal makes it shared infrastructure, available to every Cardano builder.
Why verification hasn't been within reach yet
Two things have kept formal verification out of most Cardano developers' hands.
- First: exposure. Blaster was designed from the start to remove the specialist barrier: it automates the proof work so developers don't need a formal methods background to use it. But until now, it's lived inside IO, used on our own DApps. Most Cardano developers haven't had a way to run it on their own contracts.
- Second: setup friction at the toolchain level. Of the tools in the Cardano High Assurance stack, only one requires Nix, and that's Plutus, specifically at install and deployment. Blaster and Plu-Stan don't. But because Plutus sits at the centre of the toolchain, the Nix barrier gates the whole environment in practice. Getting a full, reproducible setup running has historically meant deep Nix knowledge, and that's the point where developers drop off.
This proposal addresses both. We're handing over tools that work on day one, without prerequisites.
Blaster extends from single-contract verification to full DApp-level multi-script proof. We're integrating it into four smart contract languages (Aiken via Midgard Labs, Pebble via Harmonic Labs, Scalus via Lantr, and Futura via SAIB), so developers stay in their native environment. A Visual Studio Code extension brings visual counterexample exploration into the editor. A Common Vulnerability Library provides pre-built property templates for major DApp categories: DEXs, bridges, lending protocols, and NFT minting.
The Container-Based Developer Environment (CBDE) is the second tool. It packages the entire Plinth toolchain (compilers, formal verification, property-based testing, static analysis, and profiling) at verified, compatible versions, initialised with a single command. We'll make a pre-release (0.x) available to an initial cohort in Q4 2026. Version 1.0 ships in Q1 2027.
One verification core, four languages
Blaster runs on Untyped Plutus Core (UPLC), the universal compilation target for all Cardano smart contract languages. The investment serves the entire Cardano smart contract ecosystem all at once. It is not rebuilt per language. It is one verification engine, exposed across languages via the Universal Annotation Language: an open integration protocol any future Cardano language team can implement independently.
Every new language that integrates Blaster strengthens ecosystem-wide security. Every DApp shipped with a machine-checked correctness proof raises the baseline.
The ecosystem after this ships
Here's what Cardano looks like in Q3 2027:
A developer building a lending protocol runs one command. The full High Assurance toolchain (compilers, formal verification, property-based testing) is live in under a minute – no Nix configuration, no dependency setup. They write their first contract in Aiken and, before pushing to testnet, run Blaster directly from VS Code. The tool checks their contract against pre-built security properties for lending protocols from the Common Vulnerability Library (Double Satisfaction, Large Value Attack, Large Datum Attack) and produces a machine-checked proof that the contract behaves correctly across all inputs.
This is a mathematical guarantee independently verifiable using only the Lean proof kernel. It goes into the audit package. It gets cited in the DApp's documentation. It becomes part of why institutional partners are willing to commit capital to the protocol.
A second developer is working on an optimised version of an existing contract. They want to apply aggressive UPLC optimisations to reduce execution unit consumption. The equivalence checking tool formally proves that the optimised version is semantically identical to the original: not approximately the same, provably identical. They can ship the optimisation knowing exactly what they changed, and what they did not.
That's the outcome we're working towards: formally verified DApps that give institutional capital a basis for confidence it does not have today. This proposal advances Cardano's potential monthly active user growth and total value locked, two core 2030 KPIs, by making machine-checked security accessible to the full developer population and by making Cardano the provably safe choice for high-value DeFi deployment.
The developer onboarding tells a parallel story. Source documents in the proposal indicate attrition is currently 60–70%; CBDE targets <20%. We project a 3–5x increase in active Plinth developers within 12 months of the CBDE V1.0 release. More active developers means more DApps, more transactions, more users: compounding return on infrastructure that removes friction.
Formally verified DApps shift the conversation from 'we believe it is safe' to 'we can prove it'. This is not a claim. It is a proof term, replayable by anyone with access to the Lean kernel. In a sector where high-profile exploits routinely reset ecosystem trust overnight, verifiable safety is a durable advantage that compounds as more DApps carry it.
Built to last beyond a single funding cycle
The six-partner delivery model is structural. Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness Labs, and TxPipe each own defined work packages and are responsible for the long-term maintenance of their components. The Universal Annotation Language means any future Cardano language can integrate Blaster without our involvement. The CBDE community beta in Q1 2027, with at least five external developers using the environment for real-world development, ensures the V1.0 release reflects actual usage, not our internal assumptions.
All funds are disbursed via Intersect's TRSC/PSSC framework, with a five-member Oversight Committee (Sundae Labs, Cardano Foundation, Dquadrant, Xerberus, NMKR) verifying key administrative actions on-chain. Third-party assurance sign-off is required before every payment. Any undisbursed funds return to the Cardano treasury at the end of the delivery period, with a public reconciliation report.
The treasury withdrawal of 13,078,578 ada funds a nine-month programme from Q3 2026 to Q1 2027, with 86% of the budget going directly to engineering and delivery teams across all six partner organisations.
Your vote, your call
DReps: the full proposal is live on the Cardano governance portal. Review the roadmap, budget, risk register, and the accountability structure. Then vote.
A Yes vote means: by Q1 2027, machine-checked smart contract security is standard infrastructure on Cardano, available to every builder, in every smart contract language, from a one-command setup.
