A library of standardized, reusable smart contracts for Cardano.
ContractsLibrary provides battle-tested, ready-to-use contract implementations, shipped as on-chain + off-chain pairs with a decoupled formal spec and machine-checked formal proofs. The goal is to reduce the time and risk of building on Cardano, especially for developers new to the ecosystem.
The EVM ecosystem matured in part because OpenZeppelin gave developers vetted, reusable contracts. Cardano lacks an equivalent: teams repeatedly re-implement the same primitives (vesting, escrow, token standards, AMMs), each time re-incurring design and security risk.
Existing Cardano libraries operate at a lower level of abstraction (on-chain utilities and generic patterns). ContractsLibrary operates at the use-case level: complete contracts, both on-chain and off-chain. We are very grateful to and stand on the shoulders of libraries like vodka and Anastasia Labs' design-patterns.
Every contract supports a layered consumption model:
- Use: Supply parameters to a finished contract and ship.
- Compose: Import lower-level validation functions and off-chain helpers to build something new.
- Fork: Copy the module(s) and modify for your needs.
You can choose how you want to use this library depending on your needs. While the packages are pre-release (not yet published to a registry), consume the library by cloning it:
- Use — drive a finished contract through its off-chain builders. Each contract ships transaction builders under
offchain/; for linear vesting seeoffchain/meshjs/lib(buildLockTx/buildClaimTx/buildCancelTx) and its README. - Compose — import the parameterized on-chain predicates from
onchain/lib/<contract>/and the off-chain helpers to build something new, instead of the ready-made validator. - Fork — copy the contract's
onchain/,offchain/, andspecs/modules and modify them for your needs.
Start from the contract's spec to understand the behavior, then pick a layer above. Compiled blueprints live in onchain/plutus.json.
Each contract ships as four parts:
| Part | Location | Role |
|---|---|---|
| On-chain | onchain/ |
Aiken validation logic the ledger enforces. The only part that carries security. |
| Off-chain | offchain/ |
Transaction builders developers call. The primary developer-facing API. |
| Spec | specs/ |
Implementation-independent description of behavior. The source of truth. |
| Formal proofs | formal/ |
Machine-checked Lean 4 proofs about the spec (completeness, soundness, robustness). |
Validators are written as well-behaved predicates that avoid global assumptions about transaction shape, so contracts compose freely in shared transactions. See docs/ARCHITECTURE.md for the composability rules.
onchain/ Aiken workspace (lib/<contract>/, validators/)
offchain/
meshjs/ MeshJS implementations
tx3/ Tx3 implementations
specs/ decoupled per-contract specifications
formal/ Lean 4 proofs of the specs (Lean-Blaster / Z3)
docs/ PRD, ARCHITECTURE, contributor docs
The full, status-tracked catalog lives in the PRD. Current In progress, Ready-to-audit, or Audited/Verified contracts:
| Contract | Category | Status | Spec |
|---|---|---|---|
| Linear vesting | DeFi | In progress | spec |
More candidates (escrow, AMM, CIP-68, programmable tokens, multisig, DAO, …) are explored and triaged in the PRD.
The on-chain layer is an Aiken workspace:
cd onchain
aiken build # compile validators
aiken check # run testsThe off-chain layer provides TypeScript builders (MeshJS) and Tx3 implementations under offchain/.
- Product Requirements (PRD) — what we ship, goals, catalog.
- Architecture — composability conventions every contract follows.
- Formal proofs — machine-checked Lean 4 proofs of the
specs, plus the build pipeline and
blastertractability notes.
This is how ContractsLibrary relates to other libraries in the ecosystem:
flowchart TB
A["<b>Cardano Foundation Templates</b><br/>end-to-end dApps that might consume these contracts"]
L["<b>ContractsLibrary</b><br/>complete use-case contracts, on-chain + off-chain"]
P["<b>Primitives</b><br/>low-level on-chain building blocks.<br/><i>design-patterns · merkle patricia forestry</i>"]
A --> L --> P
style L fill:#0033ad,stroke:#001f6b,color:#fff
- Below (design-patterns, merkle patricia forestry) are lower-level building blocks (stake validators, batching, linked lists, authenticated key/value stores) that a contract may compose with, and in some cases depend on, rather than complete use cases.
- Above (Cardano Foundation templates) are end-to-end examples that wire finished contracts into working applications.