A new era of smart contract verification on Cardano

On Cardano, smart contracts are written in powerful surface languages, such as Plinth, Aiken, and Plu–ts, among others. These contracts control real, valuable assets. If they fail, funds could be stolen or permanently locked.

Input | Output (IO) is developing a new tool to bring formal verification to Cardano smart contracts. While existing tools in the ecosystem – based on systems like Agda, Rocq (formerly Coq), and other proof assistants – offer strong guarantees, they typically require expert knowledge to use. This new tool combines the power of the Lean4 proof system and SMT solvers, such as Z3, to automatically check that contracts behave as intended. The goal is to eliminate the need for developers to write any formal proofs themselves.

What makes this tool a game changer is its complete automation: no manual proofs, no expert intervention. You simply click a button and get formal verification. This means you can integrate it directly into your CI/CD pipeline and formally verify your contracts on every commit – instantly, continuously, and affordably. The tool remains under development and will be made available in due course.

Why formal verification?

Tests only cover the cases or scenarios that you can think of. Property-based testing helps a lot, but still leaves most of the test space unchecked. Furthermore, a comprehensive test suite, with multiple scenarios and attacks exploration, generally requires significant development effort and can be difficult to maintain when the number and complexity of the test objectives are quite significant.

Formal verification lets you state properties about your contract and then prove they’re indeed always true. Some formal verification techniques can generate a counterexample when a property is not verified. Existing formal verification tools in the ecosystem may offer strong guarantees of security and correctness, but often rely on developing models in a different language and require very niche expertise. Their complexity, lack of automation, and inability to generate reusable counterexamples make them inaccessible to most developers.

What we are aiming for

IO’s automated formal verification tool aims to verify smart contracts by:

1. Automatically transpiling from the surface programming language (Plinth, Aiken, Plu-ts, UPLC, etc) to the internal representation in Lean4 to create a faithful semantic model.
2. Translating contract properties as Lean theorems. The contract properties will be specified in a Universal Annotation Language, allowing cross-language specification.
3. Transforming and simplifying the Lean representation and theorems to tractable, but equivalent, SMT queries.
4. Passing this representation to powerful SMT solvers (eg, Z3, CVC5).
5. Returning either: a replayable proof that the property holds, a replayable counterexample showing a concrete execution trace that leads to an issue, or a proof obligation for a specialist to solve manually if the solver cannot decide.

The tool is being designed to minimize the need for expert intervention by embedding extensive optimizations, simplifications, and Cardano-specific knowledge into its core.

Development status

Currently, we have a strong version of the reasoning core. A lot of very specialized optimization, simplification, and normalization rewriting rules have been implemented that show we can scale up to realistic Cardano smart contract functions. We’ve taken into account a lot of the high-level language features offered by the surface languages, ensuring that using our tool will not restrict what the developers can use from their favourite programming languages.

We’ve built the translation to the SMT backend that transforms those Lean4 goals to SMT queries and a mechanism to bring the counterexamples back to Lean.

A simple example

We currently do not have a transpiler from any programming language to Lean4, but we can still demonstrate our tool on Lean4 examples. We manually translated a vesting example from VacuumLabs' capture-the-flag to Lean4.

The following validator verifies that funds locked at the vesting contract can only be spent when the expected beneficiary has signed the transaction and that the vesting time has elapsed.

def validator : Demo -> VestingDatum -> VestingRedeemer -> ScriptContext -> Bool :=
    fun demo datum _ sc =>
        let transaction := sc.transaction;
        let purpose := sc.purpose;
        let signatories := transaction.signatories;
        let v_range := transaction.validity_range
        (purpose == Purpose.Spending) && (containsKey signatories datum.beneficiary demo) && (timeHasElapsed v_range datum.lock_until)

Two helper functions are used. The helper function containsKey only verifies that the beneficiary key is in a given list. It is defined as follows:

def containsKey : List VerificationKeyHash -> VerificationKeyHash -> Bool :=
   fun keys key =>
   match keys with
   | [] => false
   | k :: ks => if k == key then true else containsKey ks key

The helper function timeHasElapsed checks that the vesting time has passed. It is defined as follows:

def timeHasElapsed : ValidityRange -> POSIXTime -> Bool :=
    fun range time =>
        range.upper_bound >= time.time

This closely mirrors what a developer could have written using any of Cardano’s smart contract programming languages.

To validate that the code is in conformance with the expected requirements, a tester (or even a developer) would typically need to write several nominal and edge case scenarios.

Using our approach, they are only required to specify the intended behaviours (ie, properties to be satisfied).

The expected behavior can be expressed as a theorem in Lean4. At this stage, the language is still not so user-friendly (but we’ll work on that!):

theorem only_accept_if_signatory_and_time_elapsed :
    ∀ (datum: VestingDatum) (redeemer: VestingRedeemer) (scriptContext : ScriptContext) (time: POSIXTime),


    (isValidCtx scriptContext time) →  
    (validator  datum redeemer scriptContext) →


    (scriptContext.transaction.signatories.contains datum.beneficiary
    &&
    time.time ≥ datum.lock_until.time)

The theorem simply states that: no matter the datum, the redeemer, or the script context, if the current time time is within the validity range and the validator returns true, then the following conditions must be satisfied: 

1. The transaction signatory contains the beneficiary that is in the datum
2. The current time is greater than the time specified in the datum.

Our tool then automatically translates this into an SMT query (which is not supposed to be read by the developers) and sends it to an SMT solver.

The SMT solver then reports that the theorem is Falsified! The tool produces the following test case (slightly cleaned up for readability):

❌ Falsified
Counterexample:
 - datum:
{ lock_until: 1,
	  Beneficiary: 0}
 - time:
0
 - scriptContext:
{ …
  purpose: Spending,
	  …
  signatories: [0],
  …
  validity_range : [0, 11798],
  …}
 - redeemer: 8335

This counterexample shows that the test of timeHasElapsed predicate is wrong. Indeed, a high enough upper bound of the validity range (eg, 11798, which is a bit of an overkill by the solver) is sufficient for the beneficiary to unlock the funds, even if the time has not actually passed (here time is still at 0, while the lock is until 1).

We can even replay this scenario, where the upper bound is set very high, in the VacuumLabs example, to solve this capture-the-flag!

What’s next

This is the first post of an upcoming series. In the next one, we’ll dive deeper and show how we can automatically prove UPLC code with a reimplementation of the CEK machine and Plutus Core in Lean4. We’ll demonstrate this mechanism on production code, and we will show how this tool can also be used to formally prove optimizations done at the code level.