Summary:
- For the first time, Cardano smart contracts can be mathematically verified end-to-end, automatically. Developers can confirm their contracts behave correctly using the languages they already work with.
- This expands what's possible for developer assurance on Cardano. What previously required deep specialist expertise can now be run on any contract written in Plinth, Aiken, or Plutarch, using Lean 4.
- Two new open-source libraries make it possible. PlutusCoreBlaster captures how Cardano runs smart contracts, and CardanoLedgerAPIBlaster captures how Cardano validates transactions. Together, they give the Blaster theorem prover everything it needs to reason about real contracts.
- The team demonstrated the full pipeline on a known practice contract from a public security challenge. Blaster automatically generated a complete script context showing how the contract could be exploited.
- Both libraries are open source on GitHub and ready to use today, the result of years of work by IO's Cardano High Assurance and formal methods teams.
- Development continues into 2026 under the Cardano High Assurance proposal.
For the first time, the full chain from a high-level smart contract source language to a machine-checked property is open to Cardano developers. Write your validator in Plinth, Aiken, or Plutarch, compile it to Untyped Plutus Core (UPLC), import the result into Lean 4, state the properties you care about, and call Blaster. The proof either goes through, or you get back a concrete script context that shows exactly where it does not.
This is a new capability for the Cardano ecosystem, built by IO’s Cardano High Assurance team in close collaboration with the formal methods team. It opens the door to assurance work that was previously out of reach for everyday smart contract development, without forcing developers to leave the languages they already use.
What are the new Lean 4 formalizations?
Two pieces complete the pipeline.
The first is PlutusCoreBlaster, a Lean 4 formalization of Plutus Core, the language that runs on Cardano. At its core, the library provides machine-checked definitions of every built-in function in the Plutus Core specification: integer and bytestring arithmetic, string operations, booleans, lists, pairs, and the universal Data type. On top sits a complete model of UPLC, including inductive term types (variables, lambdas, applications, builtins, constructors, case expressions), two CEK machines, one with a step counter and one with full cost-model integration, and the two serialization formats Plutus uses in practice: CBOR and hex encoding. Any UPLC program can be imported from textual UPLC, CBOR, double CBOR, and other supported formats, with correctness theorems written against its actual execution.
A second major component is the standalone Cryptograph library, which formalizes the cryptographic primitives Plutus exposes as built-ins. Hash functions covered include SHA-256, SHA-512, SHA3-256, Blake2b-224, Blake2b-256, Keccak-256, and RIPEMD-160, each verified with NIST-sourced test vectors. Elliptic-curve coverage spans Secp256k1 (ECDSA and Schnorr signature verification, Jacobian-coordinate point arithmetic, SEC1 compression) and Ed25519 (EdDSA verification, extended-coordinate arithmetic, Curve25519 field). The implementation passes 100% of the conformance tests, with the exception of newly added types and built-ins, which are work in progress.
Check out the repository here.
The other piece is CardanoLedgerAPIBlaster, a Lean 4 formal model of the Cardano Ledger API, the typed interface that Plutus validators see at script execution time. The library is structured around the three API generations: V1, V2, and V3. All major ledger types are defined: addresses with payment and staking credentials, multi-asset Value as a sorted list of currency-symbol and token-name pairs, the full TxInfo transaction view, ScriptContext and ScriptPurpose hierarchies, POSIX time ranges, and certificate types that grow from version to version.
At the heart of the library sits a set of decidable boolean predicates that encode the Cardano ledger’s validation rules: a runnable formal specification of what the ledger accepts. We did not reimplement the Agda specification, but the one used by the node, since some design choices made there enable script optimizations. Capturing those was essential for avoiding spurious counterexamples. The predicates cover input and output validity, datum-witness bookkeeping, withdrawal and signer sortedness, minted-value structure, and the transaction-balance equation. Spending, minting, rewarding, certifying, voting, and proposing script purposes each get their own top-level validity predicate composed from these primitives. An IsData typeclass bridges arbitrary Lean types to Plutus’s on-chain Data representation.
Learn more about CardanoLedgerAPIBlaster here.
How this fits with prior work
Earlier in the program, the Cardano HA team shipped Lean-blaster, an application-agnostic automated theorem proving backend for Lean 4. It already lets anyone use Lean to prove math theorems, with the Cardano application in mind: support was scoped to the types and constructions that actually appear in Cardano smart contracts, with no extra weight from constructions that never will. The two new libraries supply the missing Cardano-specific layer, taking Blaster from a general theorem prover to an end-to-end verification tool for live smart contracts.
The demo
To exercise the pipeline end-to-end, the team imported the Invariant0’s Capture-the-Flag challenge’s `nft_sell` contract from UPLC, formalized its specification, expressed its properties in Lean 4, and ran Blaster. Blaster automatically generated a full, ledger-rules-compliant script context that demonstrates a double-satisfaction pattern, showing the entire flow working in practice: from compiled UPLC, through formal properties, to a concrete and ledger-valid counterexample.
The path from source code to verified property is now a single sequence: write your validator in Plinth, Aiken, or Plutarch, compile it, import the resulting UPLC into Lean 4, state your properties, and run Blaster.
Where this goes next
Scalability work continues, and coverage will keep growing as new Plutus features land. The pipeline as it stands today already enables anyone working on Plinth, Aiken, or Plutarch contracts to bring formal methods directly into their workflow, with no separate smart contract model.
A big shoutout to Mark Petruska and Alasdair Hill the entire High Assurance team – present and past members of the High Assurance team – and to Jean Frédéric Etienne and William DeMeo of the formal methods team, whose work together made this possible.
Learn more
This work continues under the 2025 Cardano High Assurance initiative and this year’s proposal. Read more about the 2026 proposal here and see how the program develops formal methods, tooling, and assurance for the Cardano ecosystem.
