Cardano Treasury

IO: Cardano High Assurance Technical Collaboration (1of2)

IO: Cardano High Assurance Technical Collaboration (1of2): $495K paid of $1.24M from Cardano's treasury, through Intersect Treasury Contracts 2, in 7 payments. The next payment unlocks 28 Feb 2027.

Approved by IO: Cardano High Assurance Technical Collaboration.

About the project

This Statement of Work delivers the Cardano High Assurance (HA) across 2 workstreams. 1. Automated formal verification toolkit, gives devs and auditors the means to: formally verify their smart contract development, reuse a library of generic properties according to the type of DApp being developed, verify semantic equivalence between smart contract codes. Includes 2 versions of a Visual Studio Code extension for Blaster, and integration of Blaster into 4 surface language developer environments: Aiken, Futura, Pebble, and Scalus. Delivered with named ecosystem partners (Harmonic Labs, Lantr, Midgard Labs, No.Witness Labs, SAIB, and TxPipe). 2. A Container-Based Development Environment provides a complete containerised HA development environment for Plinth: the Aiken, Plutarch and Plinth compilers, static analysis tools, Property-based testing frameworks, and an automated formal reasoning tool (Blaster), released to the community as a stable version 1.0.

Payments

  1. m-0: M1.1 Milestone 0 - Project kickoff & Blaster Integration — $495K, Paid 19 Aug 2026
  2. m-1: M2.1 Milestone 1 - Equivalence checking tool as Lean library — $160K, Scheduled, unlocks 28 Feb 2027
  3. m-2: M2.2 Milestone 2 - Proof reconstruction module — $160K, Scheduled, unlocks 29 Jul 2027
  4. m-3: M2.3 Milestone 3 - VS Code extension Release 1 — $160K, Scheduled, unlocks 28 Feb 2027
  5. m-4: M2.4 Milestone 4 - VS Code extension Release 2 — $90.5K, Scheduled, unlocks 29 Jul 2027
  6. m-5: M2.5 Milestone 5 - DApp proof framework — $90.5K, Scheduled, unlocks 29 Jul 2027
  7. m-6: M2.6 Milestone 6 - Generic set of high level security properties — $90.5K, Scheduled, unlocks 29 Jul 2027