Last updated 5 months ago
Despite ongoing work on Cardano-focused formal verification tools in Lean4, there is still no framework that enables writing and compiling smart contracts directly within Lean4.
Build a Lean4-native framework that provides macros, DSLs, and UPLC tooling for writing, optimizing, and verifying Cardano smart contracts directly within Lean4.
Please provide your proposal title
Smart Contract Development in Lean4
Enter the amount of funding you are requesting in ADA
189000
Please specify how many months you expect your project to last
9
Please indicate if your proposal has been auto-translated
No
Original Language
en
What is the problem you want to solve?
Despite ongoing work on Cardano-focused formal verification tools in Lean4, there is still no framework that enables writing and compiling smart contracts directly within Lean4.
Supporting links
Does your project have any dependencies on other organizations, technical or otherwise?
No
Describe any dependencies or write 'No dependencies'
Cardano suite necessary for developing smart contract will be bootstrapped from scratch in Lean4.
Will your project's outputs be fully open source?
Yes
Please provide details on the intellectual property (IP) status of your project outputs, including whether they will be released as open source or retained under another licence.
Project will be fully opensourced. It will be published on github under BSD-Clause3 license
Please choose the most relevant theme and tag related to the outcomes of your proposal
Developer Tools
Describe what makes your idea innovative compared to what has been previously launched in the market (whether by you or others).
We have similar eDSLs implemented in Haskell, like Plutarch, and full languages such as Plinth. However, there is no smart contract framework that is integrated into a general-purpose theorem prover like Lean4. This integration is fundamentally innovative because it unifies contract authoring, code generation, and formal verification in a single environment. Developers can define high-level logic, inspect the generated UPLC, prove properties about their contracts, and maintain correctness as the code evolves—all within Lean’s interactive proof and metaprogramming ecosystem. This approach brings the rigor of formal methods directly into everyday smart contract engineering, enabling safer, more transparent, and more reliable Cardano applications than what is possible with existing toolchains
Describe what your prototype or MVP will demonstrate, and where it can be accessed.
https://github.com/SeungheonOh/Moist
I've created a very simple prototype for creating UPLC program in Lean4. This demonstrates how Lean4's amazing LSP can help achieve interactive development experience for Cardano smart contract.
Describe realistic measures of success, ideally with on-chain metrics.
By the last milestone, I will have a fully functional smart contract written in the Lean4 framework deployed on the Cardano mainnet to demonstrate end-to-end correctness, compatibility, and real-world usability. Additional success metrics include the generation of valid UPLC artifacts, reproducible builds via the Lean4 pipeline, verified contract serialization matching ledger standards, and community developers successfully using the framework to compile and deploy their own example scripts.
Please describe your proposed solution and how it addresses the problem
This proposal introduces a Lean4-native smart contract framework that exploits Lean’s macro system, elaborator extensions, partial evaluation engine, and reflection APIs to create a fully programmable pipeline from high-level DSL constructs to raw UPLC. The framework enables fine-grained manipulation of UPLC terms, symbolic execution for correctness, customizable domain-specific syntax via macro_rules, automated property-based test generation, and predictable compilation pathways. By embedding Cardano smart contract development directly into Lean4’s metaprogramming ecosystem, the system delivers both low-level control and high-level expressiveness, filling a critical gap in the current Cardano tooling landscape and enabling developers to reason about contracts using the same mechanisms that produce their executable UPLC.
Because all smart contract development occurs within Lean4, developers can implement, test, optimize, and formally verify contracts using a unified environment and shared semantics. This tight integration eliminates the friction between code and proofs, enabling seamless refinement, interactive theorem proving, symbolic reasoning, and correctness-by-construction workflows. As a result, contract development becomes more rigorous, repeatable, and auditable, with a drastically reduced risk of divergence between specification and implementation.
Moreover, Lean4’s rich development environment—including its powerful LSP features, real-time type and value introspection, interactive reduction displays, and immediate feedback loops—provides an exceptionally smooth and enjoyable developer experience. These capabilities allow smart contract developers to explore contract behavior live, inspect generated UPLC, debug transformations, and rapidly iterate on DSL extensions with full visibility into the compilation process. The combination of Lean4’s ergonomics and Cardano-specific infrastructure dramatically enhances productivity and lowers the barrier to building safe, high-assurance smart contracts.
Please define the positive impact your project will have on the wider Cardano community
This project will meaningfully expand Cardano’s developer ecosystem by introducing the first smart contract framework fully integrated into Lean4, a modern proof assistant and metaprogramming environment. By unifying contract implementation, testing, symbolic execution, and formal verification within a single toolchain, the framework dramatically lowers the barrier to producing high-assurance Cardano smart contracts.
Developers will gain access to powerful capabilities that are currently unavailable in any Cardano-native tooling: interactive theorem proving tied directly to executable UPLC, automated correctness checks, predictable compilation pipelines, customizable DSLs, and deep introspection of generated code. This empowers teams building financial, governance, DeFi, and infrastructure applications to achieve higher security guarantees with less friction and fewer external tools.
The Lean4-based workflow also encourages best practices across the ecosystem. New developers can learn smart contract development through a guided, interactive environment with instant feedback. Experienced developers can build reusable verified libraries, contribute new DSL extensions, and collaborate more effectively via Lean’s structured proof ecosystem.
By bridging the gap between formal methods research and practical Cardano engineering, this project strengthens the reliability, auditability, and long-term sustainability of Cardano’s smart contract ecosystem. It positions Cardano as the leading platform for rigorously verified decentralized applications and opens the door for academic, industrial, and open-source communities to converge around a shared, formally grounded development experience.
What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?
Seungheon is an experienced developer specializing in Cardano smart contracts and smart contract framework design. He previously maintained Plutarch, a Haskell eDSL for Cardano smart contract development, and now works on the Plutus Core team at IOG, where he contributes new features to Plinth and leads maintenance and optimization of the Haskell implementation of the CEK machine.
His deep background in strongly typed functional programming, compiler construction, and UPLC semantics provides a natural foundation for work in Lean4, whose dependent type theory and metaprogramming model share conceptual parallels with advanced Haskell techniques. This familiarity positions him well to build a Lean4-based smart contract framework informed by both practical Cardano engineering and modern proof-oriented tooling.
Milestone Title
Core UPLC Representation
Milestone Outputs
Implement core UPLC AST types in Lean4 (DeBruijn, AST nodes, builtins).
Define serialization/deserialization (CBOR-compatible) for UPLC terms.
Build foundational macro utilities for constructing UPLC-safe Lean syntax.
Set up project scaffolding, CI, documentation, test suite, and code quality tools.
Validate correctness by round-trip tests and equivalence tests with Plutus Core reference implementation.
Acceptance Criteria
UPLC AST in Lean4 matches Plutus Core specification.
CBOR round-trip (serialize to deserialize to serialize) is identical to reference implementation.
Basic macro constructors produce syntactically valid UPLC
Evidence of Completion
Public GitHub repo with AST modules, macro utilities, and CBOR codec
Test logs comparing Lean4 UPLC encoding with Plutus Core reference
Delivery Month
1
Cost
37000
Progress
20 %
Milestone Title
High-Level eDSL Construction
Milestone Outputs
Design user-friendly syntax for building UPLC terms.
Implement high-level eDSL primitives (lam, app, arithmetic, lists, bytearrays, etc.).
Add elaborator extensions to enforce scoping and structural correctness.
Provide initial example scripts written in Lean4.
Acceptance Criteria
Users can write UPLC expressions in Lean using idiomatic syntax.
Example eDSL contracts transforms cleanly into raw UPLC encoded in specified flat encoding.
At least 5 example contracts compile to valid UPLC.
Evidence of Completion
Example directory with scripts and CI-verified compiled UPLC artifacts.
Documentation describing syntax rules and macros.
Golden tests demonstrating correct elaboration into UPLC.
Delivery Month
2
Cost
38000
Progress
40 %
Milestone Title
Builtin Functions, Data Encoding, and Golden-File Testing
Milestone Outputs
Implement the full suite of UPLC builtin functions in Lean4, mirroring the Plutus Core specification (arithmetic, bytestring ops, hashing, crypto, list utilities, etc.).
Define Lean4-side encoders for Cardano Data (constructors, integers, bytestrings, lists, maps).
Build data schemas for datum, redeemer, and script context structures.
Create golden-file testing infrastructure:
snapshot UPLC output
snapshot serialized bytes
detect regressions automatically
Add compatibility tests by comparing serialized outputs with reference files from Plutus Core tooling
Acceptance Criteria
All relevant UPLC builtins are represented correctly in Lean4 and serialize to valid UPLC.
Golden tests run in CI and detect changes in structure or serialization.
Reference tests confirm compatibility with Plutus Core serialization.
Evidence of Completion
Lean modules defining all supported builtins and data constructors.
Golden test outputs stored under version control.
CI logs showing stable snapshots and regression detection.
Documentation describing builtin semantics and encoding layer.
Delivery Month
4
Cost
38000
Progress
60 %
Milestone Title
Contract Compilation Layer, Optimization Passes, and Cardano Integration
Milestone Outputs
Provide structural correctness checks (scope correctness, well-formedness).
Implement basic syntactic optimization passes
Define reusable contract templates: spending validator, minting policy, staking script
Implement strong typing for datum/redeemer/context bindings based on Milestone 3 encoders.
Integrate output with Plinth, Cardano CLI, and text-envelope format.
Acceptance Criteria
Users can write full Cardano contracts in Lean4 and generate valid UPLC.
Optimization produces structurally smaller UPLC terms.
Generated scripts serialize to text envelopes compatible with other Cardano projects.
All contract templates compile without errors and produce correct serialized artifacts.
Evidence of Completion
Example contracts in repo (validator, minting policy, staking script).
Golden test fixtures for post-optimization UPLC and envelope bytes.
Docs explaining the compilation pipeline and optimization passes.
Delivery Month
6
Cost
38000
Progress
80 %
Milestone Title
Developer Experience, Documentation, and v1 Public Release
Milestone Outputs
Write full documentation:
eDSL reference
builtin function reference
data encoding cookbook
contract templates
Add developer tooling:
UPLC pretty-print preview panel
debugging helpers for DSL expansion
Produce onboarding materials for Haskell/Plutus developers transitioning to Lean4.
Publish a v1 “starter kit” (example repo, templates, scaffolding project).
Prepare the v1 stable release.
Acceptance Criteria
Documentation is fully sufficient for a new user to write a contract and compile it to UPLC.
At least three complete example contracts included and verified to serialize correctly.
v1 is released publicly and includes stable APIs.
Evidence of Completion
Public documentation site (GitHub Pages or equivalent).
Example repositories demonstrating end-to-end workflows.
GitHub v1.0 release tag with binaries, docs, release notes, and templates.
Close out report and video demo for community.
Delivery Month
8
Cost
38000
Progress
100 %
Please provide a cost breakdown of the proposed work and resources
The budget primarily supports developer labor, intensive DSL design work, builtin implementation, data encoding research, documentation, tooling integration, and comprehensive testing infrastructure .
How does the cost of the project represent value for the Cardano ecosystem?
The proposed budget delivers exceptional value by producing foundational infrastructure that dramatically improves the safety, reliability, and accessibility of Cardano smart contract development. A Lean4-based UPLC eDSL becomes a long-lived asset for the ecosystem: it enables high-assurance contract development, lowers audit and debugging costs, and bridges formal verification research directly into real-world Cardano engineering. By investing once in this framework, the community gains reusable tooling, safer contract patterns, better developer onboarding, and a modern, verifiable development pipeline that will serve teams across DeFi, governance, and infrastructure for years. The cost reflects the highly specialized engineering effort required, yet the resulting platform reduces future development overheads ecosystem-wide, making it a high-leverage, high-impact investment for Cardano.
I confirm that evidence of prior research, whitepaper, design, or proof-of-concept is provided.
Yes
I confirm that the proposal includes ecosystem research and uses the findings to either (a) justify its uniqueness over existing solutions or (b) demonstrate the value of its novel approach.
Yes
I confirm that the proposal demonstrates technical capability via verifiable in-house talent or a confirmed development partner (GitHub, LinkedIn, portfolio, etc.)
Yes
I confirm that the proposer and all team members are in good standing with prior Catalyst projects.
Yes
I confirm that the proposal clearly defines the problem and the value of the on-chain utility.
Yes
I confirm that the primary goal of the proposal is a working prototype deployed on at least a Cardano testnet.
Yes
I confirm that the proposal outlines a credible and clear technical plan and architecture.
Yes
I confirm that the budget and timeline (≤ 12 months) are realistic for the proposed work.
Yes
I confirm that the proposal includes a community engagement and feedback plan to amplify prototype adoption with the Cardano ecosystem.
Yes
I confirm that the budget is for future development only; excludes retroactive funding, incentives, giveaways, re-granting, or sub-treasuries.
Yes
I Agree
Yes
Seungheon is the only participant who will develop, produce documents, create tests, and write examples.
github.com/SeungheonOh