- 1. Headline (요약 제안): 에이다 고신뢰 도구 보급에 대한 제안 2. Body (상세 요약): 에이다의 핵심 강점인 보안과 정확성을 전문가 영역에서 모든 개발자의 영역으로 확장하기 위한 제안임 .

- 첫 번째 작업은 IO의 오픈 소스 자동 형식 검증 도구인 Blaster를 단일 스크립트에서 DApp 수준의 전체 검증으로 확장하는 것임 .

- Blaster는 Aiken, Pebble, Scalus, Futura 언어와 통합되어 개발 도구 체인에서 직접 검증을 수행할 수 있도록 지원함 .

- 시각적 반례 탐색을 지원하는 VS Code 확장 프로그램과 보안 템플릿을 포함한 공통 취약점 라이브러리, UPLC 최적화를 위한 등가성 확인 도구를 제공함 .

- 두 번째 작업은 고신뢰 도구 모음을 단일 명령으로 설정할 수 있는 CBDE를 구축하여 환경 설정 시간을 단축함 .

- DeFi 사용자는 수학적으로 검증된 DApp을 사용하게 되며, 개발자는 실용적인 고신뢰 엔지니어링 기반을 갖추게 됨 .

- IO, Lantr, Harmonic Labs, SAIB, Midgard Labs, TxPipe, No.Witness Labs가 협력하여 개발 및 유지보수를 분담함 .

- Intersect가 마일스톤에 따라 자금을 집행하며, 총 예산 요청액은 ₳13.08M임 .

- 3. Glossary (주석): ■ 주석 *Formal Verification: 프로그램의 정확성을 수학적으로 증명하는 기술 **Blaster: IO에서 개발한 오픈 소스 자동 형식 검증 도구 ***DApp: 탈중앙화 애플리케이션 ****UPLC: 에이다 스마트 계약의 하위 수준 실행 언어 *****CBDE: 컨테이너 기반 개발 환경 ******DeFi: 탈중앙화 금융

- 에이다 고보증 개발 환경에 대한 제안 에이다 스마트 계약 개발자를 위해 자동화된 형식 검증 도구와 사전 설정된 개발 환경을 제공하고자 함 .

- 현재 개발자는 계약 코드 작성 전 환경 설정에 많은 시간을 소비하며, 이는 협업 시 일관성 없는 결과로 이어질 수 있음 .

- 형식 검증 도구인 Blaster는 현재 내부 전문가 위주로 사용되나, 이를 전체 생태계로 확장할 필요가 있음 .

- 첫 번째 작업은 Blaster를 공개 도구로 전환하여 전체 DApp 수준의 검증과 4개의 신규 언어를 지원하는 것임 .

- 여기에는 VS Code 확장 프로그램, 취약점 라이브러리, UPLC 프로그램 간의 의미적 동일성을 증명하는 도구가 포함됨 .

- 두 번째 작업은 Plinth 툴체인이 포함된 컨테이너 기반 개발 환경(CBDE)을 구축하여 단일 명령으로 설정을 완료하는 것임 .

- Blaster는 모든 언어의 공통 컴파일 대상인 UPLC에서 작동하므로 생태계 전반에 걸친 투자의 효율성이 높음 .

- Lantr, Harmonic Labs, SAIB 등 여러 파트너와의 협업을 통해 도구의 개발과 장기적인 유지보수를 수행함 .

- ■ 주석 *Formal Verification: 수학적 명세를 통해 소프트웨어의 오류 없음을 증명하는 방법임 **Nix: 재현 가능한 빌드 환경을 구축하기 위한 패키지 관리 도구임 ***DApp: 블록체인 기반의 탈중앙화 애플리케이션임 ****UPLC: 에이다 스마트 계약의 최종 실행 형태인 Untyped Plutus Core임 *****CLI: 명령어를 직접 입력하여 프로그램을 제어하는 인터페이스임 ******Plinth: 에이다 스마트 계약 개발 및 검증을 지원하는 통합 프레임워크임

- 에이다 검증 및 개발 환경에 대한 제안 에이다의 보안성과 정확성은 기관 도입 및 고가치 DeFi를 위한 핵심 차별화 요소임 .

- 자동화된 형식 검증 도구와 보안 속성 라이브러리를 통해 모든 DApp이 높은 수준의 보증을 달성하게 했음 .

- CBDE는 복잡한 Nix 설정을 60초 초기화로 단축하여 개발자 진입 장벽을 낮췄음 .

- 이 제안은 TVL 증가, 월간 트랜잭션 확대, 활성 사용자 수(MAU) 성장을 목표로 했음 .

- Blaster 도구는 Lean4 기반의 자동 형식 검증 백엔드로 연구 우수성에 기여했음 .

- 2026년 3분기부터 2027년 2분기까지 단계별 로드맵을 통해 도구와 프레임워크를 출시했음 .

- 총 예산은 ₳13.07M이며, Blaster와 CBDE 두 가지 작업 스트림으로 나뉨 .

- Intersect와 법적 계약을 체결하고 스마트 계약 기반의 투명한 자금 관리를 수행했음 .

- ■ 주석 *DeFi: 탈중앙화 금융 **DApp: 탈중앙화 애플리케이션 ***Formal Verification: 형식 검증 (수학적 증명을 통한 소프트웨어 검증) ****UPLC: Untyped Plutus Core (에이다 스마트 계약 실행 언어) *****TVL: 총 예치 자산 ******MAU: 월간 활성 사용자 수 *******Nix: 패키지 관리 및 빌드 시스템 ********CBDE: Cardano Blockchain Development Environment (에이다 블록체인 개발 환경) *********TRSC: Treasury Reserve Smart Contract (재무 예비비 스마트 계약) **********PSSC: Project-Specific Smart Contract (프로젝트 전용 스마트 계약)

**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

***As an experienced Cardano smart contract developer, interested in software quality and correctness, I want access to automated formal verification tools and a fully pre-configured development environment, so that I can prove the correctness of my contracts and begin building in minutes, without becoming an expert in Nix configuration or formal methods.***

**Opportunity:** The Cardano ecosystem has always positioned itself as the blockchain for serious applications: financial systems, identity management, DeFi protocols, and use cases where correctness is essential. Delivering on this promise depends on two capabilities that would benefit from further development to fully support the developer community.

First, the **developer environments**. Developers, including experienced engineers, spend significant time configuring the different tools and libraries they need before their first line of contract code. This becomes more pronounced in collaborative settings, where environment differences can lead to inconsistent behavior, failed tests, and deployment discrepancies. Improving access to the various high-assurance tools built by IO ensures that all developers can benefit from them.

Second, **formal verification**. Blaster, IO's automated formal verification tool for Lean 4, has already proven correctness properties for production DApps’ scripts, including Djed and USDCx, and demonstrated the ability to prove the absence of common Cardano vulnerabilities in a fully automated fashion.

Blaster is currently used primarily within IO and benefits from specialist expertise. The tool can currently operate on each individual script of a DApp. It is currently delivered as a CLI tool and will get a tight integration with the Plinth framework in Q3 2026. Modern developer experience relies on extensions or language server protocols, and the landscape of programming languages for Cardano smart contracts is ever-expanding.

**Solution:** This proposal funds two tightly complementary workstreams under the Cardano High Assurance umbrella.

1. Workstream 1 delivers **Blaster** as an open tool, extending it from single-contract to full DApp-level verification, making it compatible with four new smart contract languages, delivering a Visual Studio Code extension with visual counterexample exploration, and inlined information at the source code level, building a Common Vulnerability Library with pre-built property templates for major protocol categories, and delivering an equivalence checking tool that formally proves two UPLC programs are semantically identical. The work is structured as a technical collaboration: Lantr (Scalus), Harmonic Labs (Pebble), SAIB (Futura), Midgard Labs, IO (Aiken), No.Witness Labs and TxPipe (proof reconstruction and vulnerability library) each contribute to different components of the proposal, distributing delivery and long-term maintenance responsibilities across the ecosystem.
2. Workstream 2 delivers the **Developer Environments for the High Assurance Toolkit**. First, a single-command, pre-configured Container-Based Developer Environment (CBDE) that includes the complete Plinth toolchain (compilers, libraries, property-based testing, static analysis, formal verification, and profiling) at verified, compatible versions. CBDE becomes the unified hub for the entire High Assurance toolkit. Second, integrating the different IO’s High assurance tools into \`cardano-init\` if funded in Developer Experience proposal, with each tool's preconfiguration and templates for an easy start.

**Why now:** Blaster's 2025/26 cycle demonstrated that automated formal verification of a single Cardano smart contract is feasible at production scale, with the work on Djed and USDCx. A key technical aspect is that Blaster operates on Untyped Plutus Core (UPLC), the common compilation target of all Cardano smart contract languages, which means that investment in the verification core can support the broader ecosystem simultaneously. This creates an opportunity to extend to public infrastructure that supports unified alignment across ecosystem tools and workflows. On the developer experience side, setup complexity remains a measurable factor in developer onboarding. Reducing friction with CBDE for a fully packaged Plinth framework and with `cardano-init` for a more à la carte environment would help more developers progress from initial setup to deploying their first verified contract.

**Ecosystem Collaboration:** Lantr; Harmonic Labs; SAIB; Midgard Labs; TxPipe; No.Witness Labs

### Proposed Value Delivered (Why)

Cardano's reputation for security and correctness is its primary differentiator for institutional adoption and high-value DeFi. Without accessible formal verification, DApps are delivered based on testing, auditor and manual reviews.

The automated formal verification tool for Cardano smart contracts, coupled with a set of predefined security properties and accessibility to most surface programming languages, means that every DApp and protocol will be able to achieve a level of assurance currently inaccessible without a significant budget.

An integration since the early phases of the developer journey in `cardano-init` means we’re capturing developers from the start, so that automated formal verification is a natural component of a DApp, and not an addition when the protocol has already been implemented. We will also deliver the formal verification of TWAG 1’s ready-to-audit examples, based on the defined Common security property library.

For users seeking the upper echelon of high assurance, a more reliable, controlled development environment through CBDE would support developer progression from initial setup to the first deployment of their verified protocol.

#### KPIs

| Core Cardano 2030 KPIs (Adoption) | Alignment | KPI Alignment Narrative |
| :---- | :---- | :---- |
| **TVL** | **Yes: Partially** | Formal verification directly addresses the security risk that deters institutional capital from committing to Cardano DApps. A formally verified DApp provides a machine-checked correctness guarantee that no testing or manual review can match. As the Common Vulnerability Library and language integrations make this accessible to the majority of Cardano developers, the cumulative effect on DApp security quality creates a defensible basis for institutional TVL inflow. A measurable impact on total value locked (TVL) is likely to emerge over a 12–18-month period, reflecting the time it takes for verified DApps to move from development to production. |
| **Monthly Transactions** | **Yes: Partially** | The equivalence checking tool enables developers to apply aggressive UPLC optimizations with a machine-checked proof that behavior is unchanged. This improves throughput utilization per transaction and reduces the cost barrier for high-frequency on-chain activity. Additionally, by converting more developers through the onboarding funnel (via CBDE) and enabling them to build production-quality DApps faster, this proposal increases the number of active DApps contributing to monthly transaction volume. |
| **Monthly Active Users (MAU)** | **Yes: Fully** | CBDE directly converts the current multi-day Nix setup barrier into a 60-second initialization. Source documents indicate that developer onboarding attrition currently runs at 60–70%; CBDE targets a reduction to under 20%. We expect a 3–5x increase in the number of active Plinth developers within 12 months of the CBDE release. Blaster's language integrations extend this effect to the full developer population. More active developers translates directly to more production DApps and MAU growth through the standard builder-to-user multiplier. |

#### Additional KPIs

| Additional Cardano 2030 KPIs (Adoption) | Alignment | KPI Alignment Narrative |
| :---- | :---- | :---- |
| **Reliability: Monthly Uptime (6 epochs)** | N/A | |
| **Operational Resilience: Voting Power Distribution of Controlling Stake** | N/A | |
| **Operational Resilience: Alternative Full Node Clients** | N/A | |
| **Revenue / Adoption: Annual Protocol Revenue** | **Yes: Partially** | More active developers producing more DApps creates more on-chain transactions and fee revenue. The equivalence checker's enablement of UPLC optimizations reduces per-transaction cost without reducing fee income. The overall security improvements to Cardano DApps reduce the likelihood of high-profile exploits that drain TVL and suppress user activity. |
| **Governance: DRep Participation Rate** | N/A | |
| **Scalability: Throughput Capacity per day** | **Yes: Partially** | The equivalence checking tool enables aggressive UPLC optimizations, reducing execution unit consumption per transaction. Cheaper, more optimized contracts improve effective throughput utilization per block without requiring protocol-level parameter changes. This is a complementary capacity lever, not a substitute for Leios. |

#### Pillars

| Cardano 2030 Pillars | Alignment | Pillar Alignment Description |
| :---- | :---- | :---- |
| **Pillar 1: Infrastructure & Research Excellence** | **Yes: Fully** | Lean-Blaster is, to the best of the team's knowledge, the best automated formal verification backend for Lean4, surpassing existing tools such as lean-auto and lean-smt on neutral benchmarks. Delivering it as shared Cardano public infrastructure, with formal UPLC semantics, a CEK machine formalization, and the Universal Annotation Language is a direct contribution to research excellence. The DApp proof framework extends this to protocol-level security properties. |
| **Pillar 2: Adoption & Utility** | **Yes: Fully** | CBDE eliminates the primary barrier to developer adoption by converting a multi-day setup process into a 60-second initialization. Blaster's language integrations and the VS Code extension make formal verification accessible to developers regardless of their formal methods background. The pre-configured quality assurance toolchain makes enterprise-grade security the default development workflow, not an optional expert add-on. |
| **Pillar 3: Governance** | N/A | |
| **Pillar 4: Community & Ecosystem Growth** | **Yes: Fully** | The formal verification workstream is structured as a consortium: Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness Labs and TxPipe contribute defined work packages, each with its own developer communities. The Universal Annotation Language and open integration protocol lower the barrier for any future language team to integrate Blaster, creating a self-reinforcing ecosystem effect. CBDE's community beta process (Q1 2027\) directly cultivates community involvement in shaping the V1.0 release. |
| **Pillar 5: Ecosystem Sustainability & Resilience** | **Yes: Partially** | Formally verified smart contracts reduce the probability of exploits that drain TVL, erode user trust, and damage Cardano's institutional reputation. By delivering Blaster as shared public infrastructure, with the collaboration model distributing maintenance responsibility across multiple stakeholders, this proposal ensures the verification layer persists independently of any single team's funding cycle. CBDE expands the developer base beyond the narrow group currently able to navigate Nix complexity. |

### Deliverables & Roadmap

| Sequence | Item Description |
| :---- | :---- |
| **Q3 2026** | **CBDE: Solution Design and Tool Inventory.** Architectural design for the containerized environment. Inventory of all High Assurance tools and compilers (Plinth, Plutarch, Aiken, AFV tool, Lean-Blaster, Property-Based Testing tool, Transaction Monitoring System, Plutus Static Analyzer) and analysis of integration requirements, dependency constraints, and containerization approach. Audit readiness assessment. |
| **Q4 2026** | **CBDE: Environment Setup and Tool Encapsulation.** Container runtime configured with verified, compatible versions of all identified tools and compilers. All High Assurance tools are operational within the containerized environment. Initial internal testing. Pre-release (0.x) available for an initial cohort of internal users. |
| **Q4 2026** | **Formal verification: Equivalence Checking Tool.** Backend capability and CLI for formal proof that two UPLC programs are semantically equivalent. Enables post-audit UPLC optimizations and cross-compiler verification. Integrated into CI/CD pipelines. Tutorial examples covering both correct and incorrect optimizations. |
| **Q4 2026** | **Formal verification: VS Code Extension V1.** Extension in the official Visual Studio Marketplace supporting single smart contract verification, tool parameterization, execution trace visualization, and Lean 4 proof output for power users. Directly installable; example runs on installation. |
| **Q1 2027** | **CBDE: Community Beta, Feedback Management, and V1.0 Preparation.** Minimum five external community members using CBDE for real-world development over 1–2 months. Feedback and bug items are captured in a prioritized product backlog. Critical and high-impact items addressed in preparation for V1.0. |
| **Q1 2027** | **Formal verification: Language Integrations – Aiken, Pebble, Scalus, Futura.** Blaster integrated as a formal verification backend into four smart contract languages via a property-based testing framework or a full Universal Annotation Language path. Counterexample replay in each developer's native environment. Delivered with Midgard Labs (Aiken), Harmonic Labs (Pebble), Lantr (Scalus), SAIB (Futura). |
| **Q2 2027** | **CBDE: V1.0 Release and Documentation.** Version 1.0 is released to the community with comprehensive how-to-set-up and how-to-use guides. All tools accessible, properly configured, and documented for use without specialist environment knowledge. |
| **Q2 2027** | **Formal verification: VS Code Extension V2.** Extension updated for multi-contract interactions, complex multi-transaction trace visualization (EUTXO graph view), CBOR-level counterexample export for emulator/testnet replay, and LLM-friendly counterexample format for AI-assisted debugging. |
| **Q2 2027** | **Formal verification: DApp Proof Framework.** Blaster extended from single-contract to multi-script DApp-level verification. An extended ledger state supporting multi-script execution. Universal Annotation Language extended to express protocol-wide invariants, unique contract instances, and user role distinctions. Demonstrated on TWAG 1 examples. |
| **Q2 2027** | **Formal verification: Common Vulnerability Library.** Publicly accessible library of ready-made property templates for major DApp categories (DEXs, bridges, lending, NFT minting). Initial coverage: Double Satisfaction, Large Value Attack, Large Datum Attack. Open contribution process. Produced with auditing partners. |
| **Q2 2027** | **Formal verification: Proof Reconstruction Module.** Optimization and rewriting of step proofs, reconstructed as Lean 4 proof terms, replayable using only the Lean kernel, removing Blaster from the trusted codebase for this scope. Enables faster replay of the optimization and rewriting steps. Delivered with TxPipe. |

#### Resources

The outlined roadmap will be co-developed by engineers across Midgard Labs, No.Witness Labs, TxPipe, and IO. It will also fund and support integration across the system by organizations such as Harmonic Labs, Lantr, and SAIB

* Workstream 1 Blaster: Formal methods, Architect, Frontend, Software, and Product
* Workstream 2 CBDE: Site Reliability Engineering, Software, and Product

#### Budget

**Total Treasury Ask:** ₳13,078,578

* Workstream 1 Blaster: ₳10,112,037
* Workstream 2 CBDE: ₳2,966,541

| Funding Distribution | | |
| ----- | ----: | :---: |
| **Development** | ₳11,247,577 | 86% |
| **Infrastructure** | ₳130,786 | 1% |
| **Security & Audits** | ₳130,786 | 1% |
| **Legal & Compliance** | ₳130,786 | 1% |
| **Engagement & Ecosystem support** | ₳784,715 | 6% |
| **Operations & Delivery** | ₳392,357 | 3% |
| **Governance** | ₳130,786 | 1% |
| **Others** | ₳130,786 | 1% |

**Pricing Principles**: IO is requesting funding in ada and has provided USD figures as a reference. A portion of the funding shall be specifically tied to demonstrating measurable impact on Cardano's KPIs and pillars

* **Personnel & Delivery:** Majority of costs needed to fund the delivery resources across both workstreams, including IO internal team members and technical collaboration partner contributions
* **Ecosystem support, Audit, Assurance & Contingency**: Leadership, ecosystem, and delivery to support execution and wider alignment. Independent work assurance and audits, plus contingency to account for complexities during execution

#### Risks

| Type | Description | Likelihood | Severity / Impact |
| :---- | :---- | :---- | :---- |
| **Technical** | Scaling Blaster's optimization pipeline from single-contract to multi-script DApp-level verification proves harder than anticipated, requiring additional research iterations. | **Medium** | High: Could delay the DApp proof framework. Mitigation: remaining work packages (language integrations, equivalence checker, VS Code extension, vulnerability library) are not blocked and can deliver value independently. |
| **Community / Ecosystem** | One or more technical collaborators (Lantr, Harmonic Labs, SAIB, Midgard Labs, No.Witness labs TxPipe) fail to deliver their work package on time, blocking language integration or vulnerability library milestones. | **Medium** | High: Language integration milestones are on the critical path for ecosystem-wide adoption. Mitigation: the IO team has direct involvement in each integration and can absorb partial scope if a partner falls short. |
| **Process** | Key Formal Methods engineers are pulled into other higher-priority IO work, reducing engineering capacity below the required 15 person-months for the verification core. | **Medium** | High: The DApp proof framework and proof reconstruction work packages are dependent on a small number of specialists. Mitigation |
| **Community / Ecosystem** | Without dedicated promotion and developer outreach, Blaster and CBDE see low adoption despite on-time delivery, undermining KPI alignment claims on MAU and protocol revenue. | **Medium** | High: Both tools require community visibility to convert delivery into adoption. Mitigation: coordination required with Developer Experience Initiative and IO communications. |
| **Community/Ecosystem** | Developer Experience is not funded, and `cardano-init` is not delivered. | **Medium** | Low: The different templates will be delivered via dedicated repositories rather than integrated into a CLI tool. Users will be invited to the Blaster repository to use those templates. Discoverability of the High Assurance tool will be impacted, but mitigated with proper communication and marketing |
| **Community/Ecosystem** | Developer Experience is not funded, and the ready-to-audit examples are not delivered | **Medium** | Low: The examples used in Blaster will be drawn from other sources, reducing the overall value but still demonstrating Blaster's value.Mitigation: We could even go a step further and implement fixes on the chosen examples so that they pass formal verification. |

### Additional Information

**Known Limitations:** Blaster proof reconstruction scope for this cycle is limited to the optimization and rewriting steps – Z3 proof reconstruction is planned for the future roadmap. CBDE V1.0 will deliver a pre-release (0.x) at the end of Q4 2026 for an initial user cohort; general availability is planned for Q2 2027. The intent layer for the equivalence checker is not required to be open and permissionless at this stage.

**Benefit Dependencies:** Community visibility and developer outreach are required to convert tool delivery into measurable MAU and KPI impact. Neither is funded within this proposal; coordination with the Developer Experience Initiative (CBU Proposal 1\) and IO communications is required. Auditing firm participation in the Common Vulnerability Library is important for the library's credibility and adoption.

**Release / Solution Readiness:** CBDE 0.x pre-release: end of Q4 2026.
Blaster equivalence checking tool and VS Code Extension V1: Q4 2026.
Language integrations (Aiken, Pebble, Scalus, Futura): Q1/Q2 2027.
CBDE V1.0, VS Code Extension V2, DApp proof framework, proof reconstruction module, and Common Vulnerability Library: Q2 2027.
All AFV deliverables mainnet-ready.

### **Treasury Governance & Compliance**

#### **Contract Management**

A written off-chain Legal Contract will be created between Input Output and the Cardano Development Holdings (CDH), as mandated by the Constitution, and will be administered by Intersect. This will include details of the project delivery schedule and dispute resolution.

##### Project Delivery

All milestones, acceptance criteria, payment amounts and expected delivery dates will be agreed between the Input Output and Intersect, acting on behalf of the CDH. Input Output will deliver according to the agreed-upon project schedule within the Legal Contract, of which the necessary information will be made public via the budget management platform via transaction metadata.

Defined by the milestones within a Legal Contract, Input Output will submit and attest milestone acceptance to the community, Intersect or 3rd Party Assurer.

Project progress will be monitored via Intersect's delivery assurance function which will be communicated to the community.

Acceptance of the work will be supported by a 3rd Party Assurer, who will be responsible for reviewing and signing off the work completed at each project milestone against the corresponding milestone deliverables detailed within the Legal Contract. This work is funded from a portion of this treasury withdrawal.

#### **Auditable Accounts & Fund Delegation**

##### Budget Management Tooling

To administrate treasury funds on-chain, Intersect will utilize the treasury management smart contract framework developed by Sundae Labs. The smart contracts have been extensively tested including audits from TxPipe and MLabs.

Final mainnet validation test can be seen via the Disburse action within transaction: 0f591dc544ae14102dbb4a74d5311a6acffc1772b163d8b7a9656b9525950b17

This withdrawal will utilise Intersect’s 2025 treasury reserve contract with address being: stake17xzc8pt7fgf0lc0x7eq6z7z6puhsxmzktna7dluahrj6g6ghh5qjr
Funds will later be migrated to a 2026 treasury reserve contract once established.

##### Budget Management Specifics

Intersect will utilize a single Treasury Reserve Smart Contract (TRSC), with many Project-Specific Smart Contracts (PSSC), managed by Intersect. Intersect's management consists of three 'admin' and two Intersect 'leadership' roles. An Oversight Committee consisting of five external, independent third-party entities will provide checks and balances on Intersect, and safeguard against errors and unilateral control. The administration of both TRSC and PSSCs will be managed by Intersect, with external oversight on certain actions from the Oversight Committee.

The 2025 TRSC Oversight Committee consists of Sundae Labs, Cardano Foundation, Dquadrant, Xerberus and NMKR. Their role is to independently verify key administrative actions using on-chain logic, ensuring accuracy and consistency without exercising discretion over governance decisions.

For all details on Intersect's configuration please see the Smart Contract Guide on the knowledgebase.

The high level permissions are as follows:

* TRSC Fund and PSSC Modify
* Two of the three Intersect admins, two of the five trusted entities and one of the two Intersect leadership sign-off must authorize
* TRSC Disperse
* Two of three Intersect admins, three of five trusted entities and two of two Intersect leadership sign-off must authorize
* TRSC Pause and Resume
* Two of three Intersect admins, and one of two Intersect leadership sign-off must authorize
* TRSC Sweep
* One of three Intersect admins, and one of two Intersect leadership sign-off must authorize
* TRSC Reorganize
* Two of three Intersect admins and three of five trusted entities must authorize

##### Processes

Upon enactment of this governance action, funding for this project will be directed into the TRSC's stake account. All instances of TRSC and PSSC can not be staked with a SPO and will be delegated to the auto-abstain predefined DRep. From here funds will be withdrawn into a UTxO remaining at the TRSC.

When a 2026 TRSC is established, the funding for this project will be migrated via the ‘disburse’ action.

When the Legal contract is prepared and Input Output is ready, funding for this project will be transferred using the Fund action to a PSSC. All milestones will be outlined within the metadata.

A dashboard will be available for the community to audit the TRSC or PSSC and track metrics related to this withdrawn ada as well as being immutably verifiable on chain.

#### **Funding Denomination**

All amounts in this proposal are denominated in ada (₳). The total treasury ask is ₳13,078,578 USD figures ($3,138,859) are provided for reference only and are based on an ADA/USD rate of 0.24.

#### **Refund Conditions**

All funds not disbursed by the end of the delivery period will be returned to the Cardano Treasury. A final reconciliation will be published as part of the oversight reporting cycle. In the event of partial delivery or scope reduction, unspent funds associated with cancelled or reduced deliverables will be returned proportionally.

#### **Prior Treasury Receipts**

IO and its affiliated entities has been accountable for delivery of work funded by the Cardano Treasury. The total funds allocated has been ₳130,708,860 across a number of projects within Treasury Smart Contract, to date IOG has withdrawn ₳78,459,777.

| Workstream | Ada received | % of allocation | Corresponding Governance Action |
| :---: | :---: | :---: | :---: |
| Blockfrost | ₳1,137,500 | 88% | 8ad3d454f3496a35cb0d07b0fd32f687f66338b7d60e787fc0a22939e5d8833e#2 |
| Catalyst | ₳3,095,400 | 60% *\* | 8ad3d454f3496a35cb0d07b0fd32f687f66338b7d60e787fc0a22939e5d8833e#23 |
| IOE | ₳47,159,487 | 49% | 8ad3d454f3496a35cb0d07b0fd32f687f66338b7d60e787fc0a22939e5d8833e#1 |
| IOR | ₳26,840,000 | 100% | 8ad3d454f3496a35cb0d07b0fd32f687f66338b7d60e787fc0a22939e5d8833e#32 |
| Governance | ₳227,390 | 38% | 8ad3d454f3496a35cb0d07b0fd32f687f66338b7d60e787fc0a22939e5d8833e#22 |

*\*Note: for Catalyst this only reflects the workstream that focuses on the Hermes Infrastructure and UX/UI improvements, not the execution and operation of Funds 14-16. Per [Info Action](https://explorer.cardano.org/governance-action/gov_action1k5vwlfrxtyusd2ec37tckd54gjvqn2kd72xj4t6wkkapdv7zfg0qq468n2r) this is in the process of transitioning to Cardano Foundation.

#### **Net Change Limit Compliance**

The requested amount does not at time of submission, on its own or in aggregate, breach the applicable [350M Net Change Limit](https://explorer.cardano.org/governance-action/gov_action1m3xx08yv788vfxqh6nfvrjtvmqpwezsy0ggaczctkyjmttc2wmxsq4jsr7q) covering Epoch 613 to Epoch 713.

In accordance with the guardrail *TREASURY-02a*, this withdrawal does not exceed the NCL at the moment of submission.

#### **Audit & Oversight**

Audit and oversight costs are included within the overhead applied to this proposal. The Intersect administration fee covers administrative oversight and is reflected within the cost of this proposal. Independent oversight will be provided through Intersect and technically capable third-party, including reporting obligations and milestone-based disbursement controls.

#### **Standardized Format & Immutable Hosting**

Upon finalization, this proposal will be hosted on IPFS in an immutable format. The blake2b-256 hash of the document will be provided for on-chain reference and verification.