Proposal as pdf: 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