IO: Cardano High Assurance Technical Collaboration
**Proposal as pdf: [https://ipnso-com.ipns.dweb.link/?cid=QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A](https://ipnso-com.ipns.dweb.link/?cid=QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A)** Cardano's strongest differentiator is its focus on security and correctness, but the tools that deliver on that promise have so far been the domain of auditors and formal methods experts. This proposal lowers the barrier: it brings automated formal verification, and the full high-assurance toolkit, within reach of every Cardano developer. Two workstreams deliver this. The first extends Blaster, IO's open-source automated formal verification tool, from single-script verification to full DApp-level verification. Blaster has already been used to prove correctness properties on production DApps including Djed and USDCx, and has received strong feedback from the Cardano developer community. Today, extending those results to an entire DApp requires manually decomposing properties and verifying each script in isolation. This proposal removes that manual work by automating verification at the DApp level. It also connects Blaster to four smart contract languages (Aiken, Pebble, Scalus, and Futura), so developers can invoke verification directly from their native toolchain. It delivers a VS Code extension with visual counterexample exploration and inline verification feedback, creates a Common Vulnerability Library with ready-made security templates for major DApp categories, and adds an equivalence checking tool that formally proves two UPLC programs are semantically identical, enabling safe and aggressive optimization. The second workstream delivers a Container-Based Developer Environment (CBDE) that packages the complete high-assurance toolkit into a single-command setup, compressing environment configuration from days into one click. The outcome is a stronger foundation for everyone who depends on Cardano: DeFi users get DApps whose correctness has been mathematically proven, developers get tools that make high-assurance engineering practical, and the ecosystem gets a toolkit maintained collectively by multiple teams. The work is structured as a technical collaboration: IO, Lantr, Harmonic Labs, SAIB, Midgard Labs, TxPipe, and No.Witness Labs each contribute defined components, distributing delivery and long-term maintenance across the ecosystem. Intersect administers funds via milestone-based disbursement with independent oversight, and unspent funds return to the Treasury. **Treasury Ask:** ₳13,078,578
Reasoning
Written after the vote was cast
What this asks for, and from whom
Input Output asked for 13,080,000 ADA for the Cardano High Assurance Technical Collaboration.
What would have to be true for this to be a good use of treasury funds
Formal methods and high assurance engineering are the reason I have backed this chain since 2017. The academic, peer-reviewed approach is Cardano's actual differentiator against chains that ship fast and get exploited.
What specifically concerns me
High assurance work is expensive and its payoff is invisible when it works. Nobody throws a parade for the exploit that never happened. That makes it easy to underfund and easy to overspend on, and hard to audit either way.
What I am asking of the proposer if this passes
It was enacted. Publish what the assurance work covers and what it found. Verification results that stay internal are worth a fraction of verification results the ecosystem can point to when someone asks why Cardano is different.