- 에이다 스마트 계약 강화에 대한 제안 본 제안은 언어 기능, 형식적 정확성, 개발자 경험이라는 세 가지 핵심 영역에서 에이다의 스마트 계약 플랫폼을 강화하는 것을 목표로 함 .

- 스크립트 비용 절감과 표현력 향상을 위해 Plutus 언어에 새로운 구문 형태와 프리미티브를 추가하여 더 효율적인 계약 패턴을 구현함 .

- 노드 다양성 증가에 대응하여 형식 명세, 적합성 테스트, 구조화된 보안 검토를 통해 시스템의 정확성을 지원함 .

- 설정 마찰을 줄이고 오류 보고를 개선하며 접근성을 높이기 위해 컴파일러와 툴링 경험을 개선함 .

- 이러한 작업은 Plutus 사용 비용을 낮추고 신뢰도를 높이며 개발자 채택을 용이하게 하여 에이다 생태계의 기반을 공고히 함 .

- Input Output 및 VacuumLabs와의 기술 협력을 통해 Plutus 관리 책임을 전문 팀들에 분산함 .

- Intersect가 마일스톤 기반 스마트 계약을 통해 자금을 관리하며 독립적인 감독을 수행하고 미사용 자금은 국고로 반환함 .

- 요청 예산은 총 ₳11.87M임 .

- ■ 주석 *Plutus: 에이다 블록체인에서 스마트 계약을 작성하기 위한 프로그래밍 언어 **Smart Contract: 블록체인 네트워크에서 조건이 충족되면 자동으로 실행되는 디지털 계약 ***Primitive: 프로그래밍 언어에서 제공하는 가장 기초적인 데이터 단위나 연산 기능 ****Node: 블록체인 네트워크를 유지하고 데이터를 검증하는 개별 컴퓨터 서버 *****Treasury: 에이다 생태계의 지속 가능한 발전을 위해 비축된 국고 자금

- 에이다 플루투스 플랫폼 개선에 대한 제안 에이다 스마트 컨트랙트 개발자를 위해 효율적이고 검증된 플루투스 플랫폼을 구축하고자 함 .

- 플루투스의 실행 효율성과 표현력을 높여 온체인 실행 비용을 절감할 계획임 .

- CIP-0156 및 CIP-0168 도입을 통해 리스트 및 다중 자산 연산 효율을 개선함 .

- 보안상 이점 없이 지연을 초래하는 스코프 체크를 제거하여 검증 오버헤드를 줄임 .

- 형식 검증과 보안 감사를 강화하여 노드 다양성 환경에서도 정확성을 보장함 .

- 속성 기반 테스트 프레임워크를 도입하고 메타이론의 공식화를 확장함 .

- 컴파일러 아키텍처를 개선하여 명확한 오류 메시지를 제공하고 개발 환경 설정을 간소화함 .

- Nix나 C 라이브러리 의존성을 제거하여 신규 개발자의 진입 장벽을 낮춤 .

- Van Rossem 하드포크 이후 Dijkstra 하드포크를 준비하며 적기에 기능을 확장함 .

- Input | Output과 VacuumLabs의 협업을 통해 핵심 인프라의 분산된 소유 모델을 실현함 .

- ■ 주석 *Plutus: 에이다 스마트 컨트랙트의 기반이 되는 프로그래밍 언어 및 플랫폼임 **UPLC: Untyped Plutus Core의 약자로 플루투스의 실행 모델임 ***CIP: Cardano Improvement Proposal의 약자로 에이다 개선 제안임 ****Formal Verification: 프로그램이 명세대로 작동함을 수학적으로 증명하는 과정임 *****Nix: 소프트웨어 배포 및 패키지 관리를 위한 도구임 ******Agda: 메타이론 공식화에 사용되는 증명 보조 도구임 *******Hard Fork: 블록체인의 기존 규칙을 근본적으로 변경하는 업데이트임 ********Poseidon: 영지식 증명에 최적화된 해시 함수임

- 에이다 플랫폼 기능 강화에 대한 제안 에이다 스마트 컨트랙트 플랫폼의 언어 기능 확장과 실행 비용 절감을 통해 사용자 수익성과 체인 경쟁력을 높임 .

- 보안 감사와 공식 검증을 통해 노드 다양성 확장에 따른 안정적인 기반을 마련함 .

- 개발자 도구 및 경험 개선으로 진입 장벽을 낮추고 더 많은 개발자가 컨트랙트를 배포할 수 있도록 지원함 .

- VacuumLabs와의 협업은 에이다 핵심 인프라가 특정 조직이 아닌 다양한 전문가 팀에 의해 유지 관리됨을 의미함 .

- 자본 효율성 개선과 보안 강화를 통해 TVL을 증대시키고 금융 프로토콜의 매력도를 높임 .

- 실행 비용 절감으로 트랜잭션 단가를 낮추어 어플리케이션 설계의 유연성을 확보하고 거래량을 늘림 .

- 개발자 온보딩 경로를 단순화하여 활성 사용자 수와 DApp 생태계 확장을 도모함 .

- 속성 기반 적합성 테스트 프레임워크를 통해 대체 노드 클라이언트 개발을 지원하고 네트워크 복원력을 강화함 .

- 2026년 3분기부터 2027년 2분기까지 UPLC 기능 확장, 보안 감사, 컴파일러 개선 등 단계별 로드맵을 실행함 .

- 총 예산은 ₳11.8M이며, 이 중 86%를 개발에 투입하고 나머지는 인프라, 보안, 운영 등에 배정함 .

- Intersect와 법적 계약을 체결하고 스마트 컨트랙트를 활용하여 투명하게 예산을 관리 및 집행함 .

- ■ 주석 *Plutus: 에이다의 스마트 컨트랙트 프로그래밍 언어임 .

- **UPLC: Untyped Plutus Core의 약자로 Plutus의 하위 수준 실행 언어임 .

- ***TVL: Total Value Locked의 약자로 블록체인 내 총 예치 자산 규모임 .

- ****MAU: Monthly Active Users의 약자로 월간 활성 사용자 수임 .

- *****CIP: Cardano Improvement Proposal의 약자로 에이다 개선 제안임 .

- ******GHC: Glasgow Haskell Compiler의 약자로 Haskell 언어 컴파일러임 .

- *******Agda: 프로그램의 정확성을 증명하기 위해 사용하는 정식 검증 도구임 .

- ********AST: Abstract Syntax Tree의 약자로 소스 코드의 구조를 트리 형태로 표현한 것임 .

- *********SNARK: 간결하고 비대화적인 영지식 증명 기술임 .

- **********DRep: Delegate Representative의 약자로 에이다 거버넌스의 위임 대표자임 .

- ***********SPO: Stake Pool Operator의 약자로 에이다 스테이크 풀 운영자임 .

- ************IPFS: InterPlanetary File System의 약자로 분산형 파일 시스템임 .

**Proposal as pdf: [https://ipnso-com.ipns.dweb.link/?cid=Qmd7G7L6xinunTLU9JorPLYyFCLGRarXEn7RngdNYgNH3B](https://ipnso-com.ipns.dweb.link/?cid=Qmd7G7L6xinunTLU9JorPLYyFCLGRarXEn7RngdNYgNH3B)**

This proposal strengthens Cardano’s smart contract platform across three critical and closely connected areas: language capabilities, formal correctness, and developer experience. It funds targeted expansion to the Plutus language with new syntactic forms and new primitives to reduce script costs, improve expressiveness, and unlock more efficient contract patterns; formal specification, conformance testing, and structured security review to support correctness as node diversity grows; and a better compiler and tooling experience that lowers setup friction, improves error reporting, and makes smart contract development more accessible. Together, these workstreams make Plutus cheaper to use, more trustworthy to build on, and easier for developers to adopt, helping Cardano support a broader range of applications while also providing stronger foundations for alternative node implementations and other ecosystem tooling.

This is a technical collaboration with Input Output and VacuumLabs, distributing Plutus stewardship across expert teams. Intersect administers funds via milestone-based smart contracts with independent oversight. All unspent funds return to the Treasury.

**Treasury Ask:** ₳11,877,575

***As a smart contract developer building on Cardano, whether authoring decentralized finance (DeFi) protocols, zero-knowledge (ZK) applications, or high-assurance infrastructure, I want a Plutus platform that compiles cleanly, runs efficiently, and carries formal correctness guarantees, so that I can spend my time building valuable applications with greater clarity and consistency across tools and specifications.***

**Opportunity:** Plutus, a compact lambda-calculus-based language executed by Cardano nodes, serves as the foundation of all Cardano smart contracts. Its quality and capabilities directly influence what developers can build, how quickly they can build it, and how much confidence they can place in the results. There are three interconnected areas where further improvements would strengthen Plutus’s ability to fulfill this role.

***Plutus execution efficiency and expressiveness.*** On-chain execution costs are critical to Cardano's competitiveness. Targeted expansion of Plutus capabilities and primitives can deliver meaningful reductions in script size and execution budget. Extending casing to cover the built-in Data type would let scripts efficiently pattern-match on Data, a ubiquitous type in validators. Implementing the ratified CIP-0156 (multiIndexArray) and the forthcoming CIP-0168 (additional Value functions) would turn common list and multi-asset operations into single, cheap built-ins rather than verbose on-chain loops. Removing the scope check, which currently adds roughly 25% to script preparation time without providing a security benefit, could free up significant validation overhead. Finally, a systematic exploration of laziness in UPLC would address a fundamental expressiveness gap that today forces developers into less modular or less efficient code patterns.

***Formal verification, conformance, and security.*** As node diversity becomes a reality, the correctness guarantees must keep pace. The Plutus metatheory currently lacks formalization for many built-in functions, and conformance testing falls back to the Haskell reference implementation. Extending the metatheory to cover programmatic builtins and enriching the conformance test suite with a property-based testing framework would help close this gap. Meanwhile, continuous security auditing of the evaluator and costing code would proactively surface correctness and denial-of-service risks before they reach production.

***Developer experience and tooling***. The smart contract developer experience would benefit from a compiler architecture that produces clear, source-level error messages and eliminates the need for boilerplate and compiler-specific extensions. Beyond that, broader compiler version support and a simpler project setup that does not require Nix or native C library dependencies would make the user experience significantly simpler and more attractive, allowing a new developer to install, build, and write their first contract without friction.

**Solution:** This proposal funds three workstreams that together address all three areas.

**Workstream 1. Plutus capabilities and primitives:** extends the UPLC execution model, set of built-in functions, and expressiveness. It delivers support for casing on the built-in Data type, significantly reducing execution costs for most contracts due to the ubiquity of Data; an investigation and CIP or report on removing the redundant scope check (which adds approximately 25% overhead to script preparation); a SNARK-friendly Poseidon hash function CIP and C bindings conditional on benchmarks; implementation of the already-ratified multiIndexArray builtin (CIP-0156); and implementation of additional BuiltinValue functions for multi-asset operations (CIP-0168). It also delivers a CIP exploring laziness and memoization in UPLC, opening the design space for contract patterns that are modular, reusable, and less repetitive - patterns that are currently difficult or impossible to express.

**Workstream 2. Formal specification, correctness, and security:** strengthens the formal foundations of the Plutus platform. This stream delivers a property-based conformance testing framework, extending the current 1,982-test suite with randomly generated programs, which supports node diversity by enabling alternative Plutus evaluators to verify correctness against the canonical implementation; a systematic security and correctness audit of the security-critical code (such as the Plutus evaluator and costing); and formalization of programmatic built-in types and functions in the Plutus metatheory (Agda), making the metatheory an authoritative, executable specification for the covered built-ins rather than a partial formalization that falls back to the Haskell implementation.

**Workstream 3. Developer experience:** introduces a new compiler and optimizer architecture that improves code optimization, delivers clearer source-level error messages, and reduces boilerplate. It also simplifies setting up the development environment, removing the need for tools like Nix or manual dependency installation.

**Why now:** The Plutus team has completed development for the upcoming Van Rossem hard fork. This creates a natural window until the next hard fork, allowing Plutus to further extend its capabilities. Changes that require a hard fork, such as removing the scope check, need to be completed in time for the Dijkstra hard fork. At the same time, it is important to continue building on the developer experience and usability improvements we made over the past year, as further enhancements in this area are critical to Cardano’s adoption. Finally, as Cardano adoption increases and node diversity becomes a reality, the cost of any correctness or security issue is amplified. Investing in formal specification, cross-implementation conformance, and structured auditing now is significantly more cost-effective than responding to incidents in production.

**Co-venture with VacuumLabs:** This proposal is structured as a deliberate co-venture between Input | Output and VacuumLabs, a specialist firm with deep expertise in formal methods, security-critical Haskell development, and Cardano infrastructure. The partnership is planned and purposeful. Both organizations are investing in Plutus as shared public infrastructure for the Cardano ecosystem. This distributed ownership model reflects what a maturing ecosystem looks like: core infrastructure maintained by a consortium of expert teams, not dependent on any single contributor.

### Proposed Value Delivered (Why)

Together, these workstreams enhance Cardano’s smart contract platform across three mutually reinforcing dimensions. Expanded language capabilities and lower execution costs directly translate into better returns for users and a more competitive offering relative to other chains. Formal verification, conformance testing, and continuous security auditing ensure that these gains rest on a sound foundation, which is increasingly important as node diversity expands. Tooling and developer-experience improvements lower the barrier to entry, allowing new developers to start building without friction and broadening the pool of people who write and deploy contracts.

The VacuumLabs co-venture signals that this is an ecosystem effort rather than a proprietary IO initiative. Cardano's core infrastructure benefits from being maintained and evolved across a broad contributor base of expert teams rather than a single organization. This distributed ownership model is a direct contribution to Pillar 5 (Ecosystem Sustainability and Resilience) and is the kind of structural outcome the Cardano 2030 Vision is designed to produce.

#### KPIs

| KPI | Alignment | KPI Alignment Narrative |
| :---- | :---- | :---- |
| **TVL** | **Yes: Partially** | Capital follows trust. Formal specification of Plutus primitives, cross-implementation conformance testing, and continuous security auditing all reduce the probability of exploits or consensus failures that could put locked funds at risk. At the same time, cheaper on-chain operations improve capital efficiency for financial protocols, making Cardano a more attractive venue for deploying liquidity than chains with higher execution costs or weaker correctness guarantees. |
| **Monthly Transactions** | **Yes: Fully** | Lower execution costs make transactions cheaper for users and open up application designs that were previously uneconomical. When builtins handle common operations like multi-asset comparisons or multi-index lookups in a single, cheap call rather than verbose on-chain loops, protocols can offer smaller minimum trade sizes and more frequent automated actions such as liquidations, rebalancing, and oracle updates, all of which increase transaction volume. |
| **Monthly Active Users (MAU)** | **Yes: Fully** | Simplifying the developer toolchain directly reduces the drop-off rate for new developers attempting their first Cardano application. A smoother onboarding path means more developers ship contracts, which in turn means more user-facing DApps, and ultimately, more people transacting on-chain regularly. |

#### Additional KPIs

| KPI | Alignment | KPI Alignment Narrative |
| :---- | :---- | :---- |
| **Reliability: Monthly Uptime (6 epochs)** | **Yes: Partially** | Several of these workstreams directly reduce the risk of unplanned downtime or degraded network performance. Removing the scope check eliminates unnecessary validation overhead; continuous security auditing is explicitly designed to catch subtle evaluator and costing bugs; formalizing built-in semantics and expanding conformance testing ensure that all node implementations agree on script execution, preventing unintended forks. |
| **Operational Resilience: Voting Power Distribution of Controlling Stake** | N/A | |
| **Operational Resilience: Alternative Full Node Clients** | **Yes: Partially** | The property-based conformance testing framework is a direct enabler of alternative node client development. Extending conformance testing to property-based tests that cover a wide program space gives alternative implementers far greater confidence that their evaluator agrees with the canonical implementation across edge cases. The Agda formalization provides an authoritative, implementation-independent specification that alternative node builders can test against. |
| **Revenue / Adoption: Annual Protocol Revenue** | **Yes: Partially** | A more capable and developer-friendly platform draws new protocols and use cases to Cardano, expanding fee-generating activities. Improved uptime and stronger correctness guarantees also matter here indirectly since they improve trust. |
| **Governance: DRep Participation Rate** | N/A | |
| **Scalability: Throughput Capacity per day** | **Yes: Partially** | Workstream 1 is directly related to this. By reducing the resources consumed per script execution, more transactions can fit into the same block. |

#### Pillars

| KPI | Alignment | KPI Alignment Narrative |
| :---- | :---- | :---- |
| **Pillar 1: Infrastructure and Research Excellence** | **Yes: Fully** | Formalizing Plutus's built-in semantics, building a property-based conformance framework, and improving the compiler advance the state of the art in how production blockchain contract logic is specified, verified, and compiled. They position Cardano's smart-contract infrastructure as among the most rigorously specified and tested in the industry. |
| **Pillar 2: Adoption and Utility** | **Yes: Fully** | A frictionless developer toolchain brings more builders to the platform. Cheaper on-chain execution unlocks applications that may be uneconomical today, expanding what Cardano is useful for. Stronger correctness and security guarantees give both developers and users the confidence to commit capital and build businesses on top of the platform. |
| **Pillar 3: Governance** | N/A | |
| **Pillar 4: Community and Ecosystem Growth** | **Yes: Partially** | The property-based conformance framework is designed for collaboration with teams building alternative evaluators, strengthening ties across the node-diversity ecosystem. Implementing ratified CIPs like CIP-0156 and CIP-0168 demonstrates that community-driven governance translates into timely delivery, reinforcing trust in the process. |
| **Pillar 5: Ecosystem Sustainability and Resilience** | **Yes: Fully** | Continuous security auditing and formal specification reduce the likelihood of costly incidents that erode trust and drain community resources. The VacuumLabs technical collaboration distributes Plutus maintenance expertise across multiple organizations, directly reducing the risk of a single point of failure in tooling stewardship. This distributed ownership model is a structural contribution to Pillar 5 and reflects the Cardano 2030 Vision for a resilient, multi-steward ecosystem. |

### Deliverables and Roadmap

| Sequence | Item Description |
| :---- | :---- |
| **Q3 2026** | WS1: UPLC Built-in Casing on Data, Phase 1. UPLC evaluation semantics extended to support built-in casing on the Data type. Conformance test cases for new evaluation rules and AST nodes. Benchmark results published. |
| **Q3 2026** | WS1: multiIndexArray Built-in (CIP-0156). multiIndexArray built-in implemented per CIP-0156 in both Plutus Core and Plinth. Cost model benchmarked and integrated. Hard fork ready. |
| **Q3 2026** | WS1: Additional BuiltinValue Functions (CIP-0168), Phase 1. CIP-0168 approach finalized. Initial implementations of policies, restrictValueTo, and filterOutPolicies built-ins in Plutus Core and Plinth. Unit tests complete. |
| **Q3 2026** | WS2: Security Audit, Evaluator Review begins. Structured manual review of the Plutus evaluator implementation initiated. Review notes and documented reasoning about evaluator behavior. |
| **Q3 2026** | WS3: Untangling Plinth Dependencies, Analysis. Full dependency analysis of Plinth native C library dependencies (blst, secp256k1). GitHub issue documenting all dependency paths and removal assessment. |
| **Q3 2026** | WS3: GHC Plinth Backend, Proof of Concept, and Feature Parity. Standalone Plinth compiler achieving feature parity with the existing GHC plugin-based compiler. Binary distributions for major platforms (Windows x86_64, macOS aarch64, Linux). Installable via a single command. |
| **Q3 2026** | WS3: Multi-Version GHC Support. Plinth compiler extended to support two concurrent major GHC versions. All tests compile and pass under both versions. Compatibility layer merged into the Plinth repository with updated documentation. |
| **Q4 2026** | WS1: Built-in Casing on Data, Plinth Support. Support for new Data casing semantics added to Plinth. Execution unit benchmark results published. |
| **Q4 2026** | WS1: Scope Check Investigation, Semantic Analysis, and Performance Comparison. Deep analysis of CEK interpreter code paths for open terms. Performance measurements with and without scope check across a range of programs. GitHub documentation of semantic consequences. |
| **Q4 2026** | WS1: Additional BuiltinValue Functions, Cost Models, and assetCount. Cost models for policies, restrictValueTo, filterOutPolicies benchmarked and integrated. assetCount built-in implemented. Conformance tests, metatheory updates, and user documentation delivered. |
| **Q4 2026** | WS1: SNARK-Friendly Hash Function, CIP and Benchmarks. Basic C bindings for Poseidon hash function implemented and benchmarked. CIP for SNARK-friendly built-in submitted. Conditional on benchmark results. |
| **Q4 2026** | WS2: Plutus Conformance Property Tests, Interface Design, and Initial Implementation. Community-informed interface design for property-based conformance testing. Framework implemented and tested with at least one alternative UPLC evaluator. Initial property tests running. |
| **Q4 2026** | WS2: Formalize Plutus Primitives, Agda Denotations. Agda denotations for the target list of programmatic built-in types and functions implemented. Invariants proved. Code available in the Plutus metatheory repository. Covers: BuiltinUnit, BuiltinInteger, BuiltinBool, BuiltinByteString, BuiltinList, BuiltinPair, BuiltinData, BuiltinString, BuiltinArray, BuiltinValue. |
| **Q4 2026** | WS2: Security Audit, Evaluator Review Complete. Systematic review of Plutus evaluator semantics and invariants complete. Potential issues documented; relevant GitHub issues opened. |
| **Q4 2026** | WS3: GHC Plinth Backend, Improved Error Messages, and Reduced Boilerplate. INLINEABLE pragma no longer required across modules. All compilation errors traceable to Haskell source locations. Testsuite for cross-module usability and source-location errors delivered. |
| **Q4 2026** | WS3: Untangling Plinth Dependencies, Implementation. Plinth decoupled from UPLC evaluator and native C library dependencies. Users can set up a Plinth environment like a standard Haskell project, without Nix or additional steps. Merged pull requests in the Plutus repository. |
| **Q1 2027** | WS1: Scope Check Investigation, CIP, or Report. CIP submitted if investigation indicates scope check removal is viable and beneficial; or a report explaining why removal is not advisable, with technical and performance evidence. |
| **Q1 2027** | WS2: Plutus Conformance Property Tests, Full Suite Ported. All relevant property tests from the Plutus repository ported to the new conformance framework. Multiple external tools are able to run the full suite. |
| **Q1 2027** | WS2: Formalize Plutus Primitives, Integration. Agda built-in implementations integrated into Plutus metatheory conformance test machinery. Performance report produced; any issues documented. |
| **Q1 2027** | WS2: Security Audit, Costing Review, and Final Report. Systematic audit of costing logic complete. Written audit report with all findings, risk assessments, and recommendations delivered. |
| **Q1 2027** | WS3: GHC Plinth Backend, Reduced Boilerplate, and Improved Frontend. Mandatory Plinth-specific GHC extensions and flags no longer required. Unsupported Haskell features detected before reaching GHC Core, with errors referencing Haskell source only. Full testsuite updated. |
| **Q1 2027** | WS3: Laziness and Memoization in UPLC, Evaluation and Prototyping. Candidate approaches to laziness and memoization in UPLC surveyed and evaluated. Security, semantic, and costing implications analyzed. Feasibility prototypes delivered. External researcher collaboration (Philip Wadler). |
| **Q2 2027** | WS1: Laziness and Memoization in UPLC, CIP Submitted. CIP describing the proposed laziness and memoization design opened for community discussion, structured similarly to CIP-0152 (Modules in UPLC). |
| **Q2 2027** | WS1: multiIndexArray and BuiltinValue Functions, Verification and Documentation Complete. Conformance tests, end-to-end tests, metatheory updates, Plutus Core specification updates, and user documentation complete for all delivered built-ins. |
| **Q2 2027** | WS2: Formalize Plutus Primitives, Conformance Harness (if required). If performance issues arose in Q1, the metatheory is refactored to abstract over built-in type representation. New Agda vs. Haskell conformance test harness added. Literate Agda documentation deployed at https://plutus.cardano.intersectmbo.org/metatheory/latest/. |

#### Resources

**Workstream 1: Plutus Developer Experience**

* 2 Compiler engineers (GHC backend and frontend work)
* 1 Compiler engineer (multi-version GHC support, Plinth dependency decoupling)
* 1 Language engineer (laziness and memoization investigation and CIP)

**Workstream 2: UPLC Capabilities and Platform Primitives**

* 1 Compiler and language engineer (built-in casing on Data),
* 1 Language engineer (scope check investigation)
* 1 Cryptography engineer (SNARK-friendly hash, Poseidon C bindings)
* 1 Language engineer (multiIndexArray CIP-0156 and BuiltinValue CIP-0168)

**Workstream 3: Formal Specification, Correctness, and Security**

* 1 Language and formal methods engineer (conformance property tests framework)
* 1 Security and language engineer (Plutus evaluator and costing audit)
* 1 Formal methods engineer (Agda formalization of Plutus primitives)

#### Budget

**Total Treasury Ask:** ₳11,877,575

| Funding Distribution | | |
| ----- | ----: | :---: |
| **Development** | ₳10,214,715 | 86% |
| **Infrastructure** | ₳118,776 | 1% |
| **Security & Audits** | ₳118,776 | 1% |
| **Legal & Compliance** | ₳118,776 | 1% |
| **Engagement & Ecosystem support** | ₳712,655 | 6% |
| **Operations & Delivery** | ₳356,327 | 3% |
| **Governance** | ₳118,776 | 1% |
| **Others** | ₳118,776 | 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 and Delivery:** Majority of costs needed to fund the delivery resources across the IO internal team members and VacuumLabs co-proposer contributions across all three workstreams
* **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 | The scope check investigation may conclude that removal requires bigger changes to the interpreter than anticipated. The deliverable is a CIP or report, either way; the risk is to the scope of the conclusion, not the existence of the deliverable. | Medium | Low: Time-boxed to one engineer for six months regardless of outcome. |
| Technical | Built-in casing on Data requires costing changes that allow non-constant operations on Case nodes. Costing discrepancies may require additional iterations. | Medium | Low: Core functionality is not blocked; costing can be resolved iteratively. |
| Technical | Poseidon hash C binding implementation is conditional on benchmark results. If benchmarks do not meet the threshold, implementation does not proceed. | Medium | Low: CIP is delivered regardless; only the C binding is conditional. |
| Technical | Scaling the property-based conformance test framework to run thousands of test cases against external tools within reasonable time is an open engineering challenge. | Medium | Medium: Could limit practical utility for frequent CI use. Mitigation: interface design phase (Q3 2026\) addresses this with community input before implementation commits to an architecture. |
| Technical | The Agda formalization may reveal that specific built-ins do not warrant formalization due to language limitations or unforeseen problems. | Low | Low: A report detailing the issue and proposed future solutions is an acceptable substitute output. |
| Community / Ecosystem | GHCup support is needed for the smoothest Plinth binary distribution experience. A fallback installation script is available if GHCup support is not ready in time. | Low / Medium | Low: Fallback script allows installation without GHCup; the effect is cosmetic rather than functional. |
| Community / Ecosystem | CIP-0168 (BuiltinValue functions) is not yet ratified (PR #1090). A material specification change after implementation begins could require rework. | Low | High: Implementation tracks the PR closely; any changes are assessed before incorporation. |

#### Additional Information

**Benefit Dependencies:** Realizing the cost and size reductions from Workstream 1 requires the corresponding hard fork to activate the new UPLC features on mainnet. The benefits of the property-based conformance framework depends on engagement from teams building alternative node clients.

**Release and Solution Readiness:** Plutus language and built-in extensions (casing on Data, multiIndexArray, and the additional BuiltinValue functions) are delivered as production-ready code and require a hard fork for activation on mainnet, with Dijkstra as the target. The scope check investigation and the laziness investigation are delivered as CIPs or technical reports; any subsequent implementation depends on community consensus and is out of scope for this proposal. The SNARK-friendly hash builtin is delivered as a CIP, with C bindings shipped conditional on benchmark results. The property-based conformance testing framework is released independently of the node and available for immediate use by alternative node implementers. The Agda formalization of programmatic built-ins ships as part of the Plutus metatheory, and will be used in conformance testing. The security and correctness audit is delivered as a written report with findings and recommendations. Developer experience and usability improvements from Workstream 3 are production-ready on delivery and can be adopted immediately by developers without waiting for a hard fork or any other governance or protocol-level change.

**Demos and Assets:** Plutus repository: [https://github.com/IntersectMBO/plutus](https://github.com/IntersectMBO/plutus) | Plutus Core formal spec: [https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf](https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf) | Metatheory: [https://plutus.cardano.intersectmbo.org/metatheory/latest/](https://plutus.cardano.intersectmbo.org/metatheory/latest/)

### **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](https://admin-services.docs.intersectmbo.org/governance/smart-contracts) 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 ₳11,877,575. USD figures ($2,850,618) are provided for reference only, 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.