IO: Cardano High Assurance Technical Collaboration

{
  "schema_version": "1.2.0",
  "id": "onchain-io-cardano-high-assurance",
  "ingestion": {
    "ingested_at": "2026-05-11T15:50:00Z",
    "ingested_by": "claude-opus-4.7",
    "source_documents": [
      "https://www.cardanocube.com/governance/gov_actions/gov_action1w0shrfxqwv95kk0v4cn34wylz25a2cmqkq5jpc0e2yrahhqava3q2yd5rxu",
      "https://ipnso-com.ipns.dweb.link/?cid=QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A"
    ],
    "extraction_notes": "Part of IO 2026 portfolio (tx ref #5). Yes 434.04M — highest Yes in the IO batch so far, suggesting DReps view formal verification as more clearly IO-appropriate than DevEx. Consortium of 7 orgs (IO, Lantr, Harmonic Labs, SAIB, Midgard Labs, TxPipe, No.Witness Labs). Duration is 12 months (Q3 2026 – Q2 2027). Proposal explicitly notes dependency on DevEx Initiative being funded (for cardano-init integration) — risk flagged with low severity mitigation. Also explicitly names No.Witness Labs as a consortium member — notable given their parallel proposals in this corpus (Lean 4 auditor training, Evolution SDK). DevEx Initiative is also in this corpus and currently failing — that dependency risk is live."
  },
  "source": {
    "channels": [
      "onchain"
    ],
    "hydra_id": null,
    "onchain_tx_hash": "73e171a4c0730b4b59ecae271ab89f12a9d56360b02920e1f95107dbdc1d6762",
    "onchain_action_id": "gov_action1w0shrfxqwv95kk0v4cn34wylz25a2cmqkq5jpc0e2yrahhqava3q2yd5rxu"
  },
  "identity": {
    "title": "IO: Cardano High Assurance Technical Collaboration",
    "proposer_name": "Input Output (IO)",
    "proposer_id": "io-research",
    "proposer_type": "coalition",
    "proposer_url": "https://www.iog.io",
    "doxxed": true,
    "primary_contact": "Stefano Leone; Romain Soulat (named in Momentum portfolio overview)",
    "team_size_disclosed": null,
    "team_size_disclosed_note": "7-org consortium: IO (lead), Lantr (Scalus integration), Harmonic Labs (Pebble), SAIB (Futura), Midgard Labs (Aiken), TxPipe (proof reconstruction + vulnerability library), No.Witness Labs (vulnerability library). WS1 Blaster ₳10.1M, WS2 CBDE ₳2.97M."
  },
  "classification": {
    "official_pillar_primary": [
      "Infrastructure & Research Excellence",
      "Adoption & Utility"
    ],
    "official_pillar_secondary": [
      "Community & Ecosystem Growth",
      "Ecosystem Sustainability & Resilience"
    ],
    "official_pillar_confidence": "stated",
    "working_category_suggestion": "Tooling/DevEx",
    "working_category_confidence": "high",
    "tags": [
      "formal-verification",
      "blaster",
      "lean4",
      "uplc",
      "aiken",
      "pebble",
      "scalus",
      "futura",
      "vscode-extension",
      "cbde",
      "developer-environment",
      "smart-contract-security",
      "vulnerability-library",
      "equivalence-checking",
      "consortium"
    ]
  },
  "ask": {
    "ada_amount": 13078578,
    "ada_amount_note": "WS1 Blaster ₳10,112,037 + WS2 CBDE ₳2,966,541. Budget: Development ₳11,247,577 (86%), Engagement ₳784,715 (6%), Operations ₳392,357 (3%), remainder spread across Infrastructure/Security/Legal/Governance/Others at 1% each.",
    "usd_amount": 3138859,
    "usd_peg_price": 0.24,
    "pegged": true,
    "currency_basis": "usd_pegged",
    "usd_peg_vs_market": "conservative",
    "implied_buffer_pct": -8,
    "duration_months": 12,
    "milestone_count": 11,
    "milestone_payments_disclosed": false,
    "milestone_schedule_disclosed": "names_only",
    "raw_ask_text": "Total Treasury Ask: ₳13,078,578. USD figures ($3,138,859) are provided for reference only, based on an ADA/USD rate of 0.24. Workstream 1 Blaster: ₳10,112,037. Workstream 2 CBDE: ₳2,966,541."
  },
  "treasury_return": {
    "has_return_clause": true,
    "mechanisms": [
      {
        "type": "unspent_funds",
        "trigger": "Funds undisbursed at end of delivery period OR partial delivery / scope reduction",
        "deadline": "End of delivery period (Q2 2027)",
        "excluded_costs": [],
        "estimated_return_pct": null,
        "estimated_return_pct_note": "Proportional to undelivered scope"
      }
    ],
    "treasury_favourability": "moderate",
    "treasury_favourability_confidence": "high",
    "treasury_favourability_note": "Standard IO 2026 proportional return language. ADA-denominated. No revenue share. Moderate because the proportional partial-delivery clause is substantive, but no upside mechanism.",
    "treasury_favourability_set_by": "ai",
    "raw_return_text": "All funds not disbursed by the end of the delivery period will be returned to the Cardano Treasury. In the event of partial delivery or scope reduction, unspent funds associated with cancelled or reduced deliverables will be returned proportionally."
  },
  "lifecycle": {
    "pipeline_state": "onchain_live",
    "hydra_submitted_at": null,
    "hydra_close_at": null,
    "hydra_support_pct": null,
    "onchain_submitted_at": "2026-04-22T00:00:00Z",
    "onchain_vote_close_at": "2026-05-24T00:00:00Z",
    "onchain_result": null,
    "status_last_checked_at": "2026-05-11T15:50:00Z"
  },
  "links": {
    "hydra_url": null,
    "adastat_url": null,
    "ipfs_cid": "QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A",
    "ipfs_gateway_url": "https://ipnso-com.ipns.dweb.link/?cid=QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A",
    "github_url": null,
    "website_url": "https://www.iog.io",
    "forum_thread_url": null,
    "other": [
      {
        "label": "IO Momentum portfolio overview",
        "url": "https://momentum.cardano.iog.io/"
      }
    ]
  },
  "content": {
    "abstract": "Two workstreams: (1) Blaster — IO's automated formal verification tool extended from single-script to full DApp-level verification, integrated into Aiken/Pebble/Scalus/Futura via Universal Annotation Language, VS Code extension with counterexample exploration, Common Vulnerability Library, equivalence checking tool. 7-org consortium delivery. (2) CBDE — Container-Based Developer Environment packaging the complete High Assurance toolkit (Plinth, Plutarch, Aiken, Lean-Blaster, property testing, static analysis) into a single-command setup.",
    "problem_statement": "Cardano's security differentiator is undermined by tool accessibility: formal verification is only within reach of auditors and formal methods experts. Developer environment setup takes days. Blaster currently works per-script only. No Common Vulnerability Library for DApp categories.",
    "proposed_solution": "WS1: Blaster extended to DApp-level verification, 4 language integrations (Aiken/Pebble/Scalus/Futura via Universal Annotation Language), VS Code extension v1+v2, equivalence checking tool, Common Vulnerability Library (DEXs/bridges/lending/NFT), Proof Reconstruction Module (removes Blaster from trusted codebase). WS2: CBDE 0.x pre-release Q4 2026, V1.0 Q2 2027 with community beta. Both integrate into cardano-init if DevEx Initiative funded.",
    "deliverables": [
      "Blaster: Equivalence Checking Tool (CLI + backend, Q4 2026)",
      "Blaster: VS Code Extension V1 — single contract verification, trace visualization (Q4 2026)",
      "Blaster: Language integrations — Aiken, Pebble, Scalus, Futura (Q1-Q2 2027)",
      "Blaster: VS Code Extension V2 — multi-contract, EUTXO graph, LLM-friendly counterexample format (Q2 2027)",
      "Blaster: DApp Proof Framework — multi-script DApp-level verification (Q2 2027)",
      "Blaster: Common Vulnerability Library — DEX/bridge/lending/NFT templates, open contribution (Q2 2027)",
      "Blaster: Proof Reconstruction Module — removes Blaster from trusted codebase (Q2 2027)",
      "CBDE: Solution Design and Tool Inventory (Q3 2026)",
      "CBDE: Environment Setup and Tool Encapsulation — 0.x pre-release (Q4 2026)",
      "CBDE: Community Beta + Feedback Management (Q1 2027)",
      "CBDE: V1.0 Release + Documentation (Q2 2027)"
    ],
    "milestones": [
      {
        "name": "CBDE Solution Design (Q3 2026)",
        "deliverable": "Architecture + tool inventory + containerization approach",
        "ada_release": null,
        "deadline": "2026-09-30"
      },
      {
        "name": "CBDE Tool Encapsulation + Equivalence Checker + VS Code V1 (Q4 2026)",
        "deliverable": "CBDE 0.x pre-release; Equivalence checker CLI; VS Code Extension V1",
        "ada_release": null,
        "deadline": "2026-12-31"
      },
      {
        "name": "Language Integrations + CBDE Beta (Q1 2027)",
        "deliverable": "Aiken/Pebble/Scalus/Futura integrations; CBDE community beta",
        "ada_release": null,
        "deadline": "2027-03-31"
      },
      {
        "name": "Full Release (Q2 2027)",
        "deliverable": "CBDE V1.0; VS Code V2; DApp Proof Framework; Common Vulnerability Library; Proof Reconstruction Module",
        "ada_release": null,
        "deadline": "2027-06-30"
      }
    ],
    "team": [
      {
        "name": "Stefano Leone",
        "role": "IO lead",
        "background": "Named in IO Momentum portfolio as co-lead"
      },
      {
        "name": "Romain Soulat",
        "role": "IO co-lead",
        "background": "Named in IO Momentum portfolio as co-lead"
      },
      {
        "name": "Lantr",
        "role": "Scalus language integration",
        "background": null
      },
      {
        "name": "Harmonic Labs",
        "role": "Pebble language integration",
        "background": null
      },
      {
        "name": "SAIB",
        "role": "Futura language integration",
        "background": null
      },
      {
        "name": "Midgard Labs",
        "role": "Aiken integration",
        "background": null
      },
      {
        "name": "TxPipe",
        "role": "Proof reconstruction + vulnerability library",
        "background": null
      },
      {
        "name": "No.Witness Labs",
        "role": "Vulnerability library",
        "background": "Same entity as two Hydra proposals in this corpus (Lean 4 auditor training, Evolution SDK)"
      }
    ],
    "risks_disclosed": [
      "Technical (Medium/High): DApp-level multi-script verification harder than anticipated — delays DApp proof framework but does not block other workstreams",
      "Ecosystem (Medium/High): Consortium partner delays — IO can absorb partial scope",
      "Process (Medium/High): Key Formal Methods specialists pulled to other IO work",
      "Ecosystem (Medium/High): Low adoption without dedicated outreach — depends on DevEx Initiative coordination",
      "Ecosystem (Medium/Low): DevEx Initiative not funded — cardano-init integration falls back to dedicated repositories"
    ]
  },
  "metadata": {
    "open_source": "yes",
    "open_source_url": null,
    "has_prior_funding": true,
    "prior_funding_sources": [
      "IO prior treasury allocations (same as other IO 2026 proposals)"
    ],
    "has_prior_delivery": true,
    "prior_delivery_evidence": "Blaster has already verified production DApps including Djed and USDCx. Lean-Blaster described as surpassing lean-auto and lean-smt on neutral benchmarks.",
    "admin_model": "intersect",
    "administrator_name": "Intersect",
    "oversight_committee": [
      "Sundae Labs",
      "Cardano Foundation",
      "DQuadrant",
      "Xerberus",
      "NMKR"
    ],
    "administration_fee_pct": 3,
    "duplicate_of_existing_solution": {
      "value": "no",
      "confidence": "high",
      "set_by": "ai"
    },
    "duplicate_notes": "Blaster is the only automated formal verification tool operating at UPLC level on Cardano. The Lean 4 auditor training proposal (No.Witness Labs, in this corpus) uses Lean 4 + Blaster for education — complementary, not competing. The Common Vulnerability Library fills a gap (Anastasia Labs design-patterns library exists but is not formal-verification-based)."
  },
  "relationships": {
    "bundle_with": [
      "onchain-cardano-vision-2026",
      "onchain-io-developer-experience-initiative",
      "onchain-io-ensurable-cardano-maintenance",
      "onchain-io-consensus-initiative",
      "onchain-io-cardano-upgrades",
      "onchain-io-midgard-l2"
    ],
    "supersedes": [],
    "competes_with": [],
    "depends_on": [
      "onchain-io-developer-experience-initiative"
    ],
    "notes": "Explicitly depends on DevEx Initiative for cardano-init integration (low-severity fallback if not funded). No.Witness Labs is a consortium member here AND has two separate Hydra proposals in the corpus (Lean 4 auditor training uses Blaster; Evolution SDK). Combined No.Witness Labs exposure across 3 proposals: ₳618K + ₳1.44M + share of ₳13.08M = substantial. Worth tracking per proposer_id in dashboard."
  },
  "community_signals": {
    "comment_count": 0,
    "notable_objections": [],
    "notable_endorsements": [],
    "forum_thread_urls": [],
    "live_voting_state": {
      "as_of": "2026-05-11",
      "drep_yes_ada": 434040000,
      "drep_no_ada": 5360000000,
      "drep_explicit_no_ada": 76080000,
      "drep_no_confidence_ada": 201000000,
      "drep_not_voted_ada": 5080000000,
      "drep_total_active_stake_ada": 14940000000,
      "cc_yes": 1,
      "cc_no": 0,
      "cc_not_voted": 6,
      "interpretation": "FAILING but highest Yes in IO batch (434M). Low Explicit No (76M) — opposition is mainly abstention/non-vote. DReps appear broadly sympathetic to formal verification but still not voting Yes at required threshold."
    }
  },
  "ecosystem_demand": {
    "evidence_level": "moderate",
    "evidence_level_confidence": "high",
    "evidence_level_set_by": "ai",
    "active_users_known": true,
    "active_users_examples": [
      {
        "name": "Djed (Coti)",
        "kind": "user",
        "url": null
      },
      {
        "name": "USDCx",
        "kind": "user",
        "url": null
      },
      {
        "name": "Midgard Labs",
        "kind": "integrator",
        "url": null
      },
      {
        "name": "No.Witness Labs",
        "kind": "integrator",
        "url": null
      },
      {
        "name": "TxPipe",
        "kind": "integrator",
        "url": null
      }
    ],
    "developer_demand_signals": [
      "Blaster already used on production DApps (Djed, USDCx) — demonstrated real demand",
      "Developer onboarding attrition cited at 60-70% currently; CBDE targets under 20%",
      "7-org consortium willing to contribute pro-bono development work signals ecosystem demand",
      "Cardano's positioning as 'blockchain for correctness' creates structural demand for formal verification"
    ],
    "adoption_risk_notes": "Demand is real and growing. Risk is adoption gap between tool delivery and developer uptake — proposal explicitly flags this and notes it depends on DevEx Initiative coordination for discovery. The 12-month delivery window runs to Q2 2027, which is longer than most proposals in this corpus."
  },
  "incumbents": {
    "has_existing_solution": "no",
    "has_existing_solution_confidence": "high",
    "has_existing_solution_set_by": "ai",
    "existing_solutions": [
      {
        "name": "lean-auto / lean-smt",
        "url": null,
        "status": "maintained",
        "overlap": "partial",
        "notes": "General Lean 4 automation tools. Proposal claims Lean-Blaster surpasses both on neutral benchmarks for Cardano use cases."
      },
      {
        "name": "Anastasia Labs design-patterns",
        "url": "https://github.com/Anastasia-Labs/design-patterns",
        "status": "maintained",
        "overlap": "partial",
        "notes": "Reusable smart contract patterns library — not formal-verification-based. Complementary to the Common Vulnerability Library deliverable."
      }
    ],
    "differentiation_claim": "Blaster is the only automated formal verification tool that operates at UPLC level (the common compilation target of all Cardano smart contract languages), enabling verification across Aiken/Pebble/Scalus/Futura simultaneously. No other tool delivers DApp-level multi-script formal verification on Cardano.",
    "differentiation_credibility": "high"
  },
  "risk_flags": {
    "aggressive_peg": false,
    "self_administered_no_oversight": false,
    "incumbent_already_delivering": false,
    "no_evidence_of_demand": false,
    "competes_with_in_batch": false,
    "concentration_risk": true,
    "failing_live_vote": true
  },
  "risk_flags_note": "concentration_risk: IO portfolio bundle + No.Witness Labs appears as consortium member here AND has 2 separate Hydra proposals. failing_live_vote: Yes 434M vs No 5.36B, expires May 24.",
  "_meta": {
    "title": "IO: Cardano High Assurance Technical Collaboration",
    "proposer": "Input Output (IO)"
  }
}