Always secure and safer than ever, thanks to next-level smart contract verification on Cardano

It is now possible to formally verify smart contracts at the exact level they execute on Cardano nodes – working directly with Untyped Plutus Core (UPLC) rather than reasoning over abstract models or surface loop. 

By directly targeting UPLC, contracts can be verified regardless of the source language, including Plinth, Aiken, Plutarch, or any future language that targets the Plutus Core compilation pipeline.

Such a degree of proof automation and analysis at the UPLC level has never been achieved before on Cardano. 

This approach closes a significant gap in smart contract assurance. Instead of assuming that compilers preserve semantics (ie, even after several optimization passes) or that verification at the source code/model level catches all issues, anyone can directly verify the actual compiled (or even deployed) bytecode. 

As indicated in the first blog post in this series, the properties are expected to be annotated at the surface language level. And the transpiler produces the corresponding UPLC code and Lean4 formalization. 

Input | Output Engineering (IOE)’s formal verification tool not only automatically proves the correctness of smart contracts and ensures the absence of security vulnerabilities, but also provides the ability to generate concrete counterexamples. When a property is violated, the tool identifies the specific datum, redeemer, and script context that triggered the issue. Conversely, when a property is proven to hold, it delivers mathematical certainty about the behavior of the deployed contract, regardless of the original source language.

The verification gap

Every Cardano smart contract compiles down to UPLC before execution. Yet, formal verification has traditionally operated at higher abstraction levels – checking models of contracts rather than the contracts themselves.

This creates a blind spot where compiler transformations, optimization passes, and subtle semantic shifts can introduce issues that model abstraction and source-code level verification miss. The previous post in this series explained how the team’s tool can automatically discover bugs in smart contracts by verifying their behavior in Lean4. This post explains how the capability has been extended to work directly with the code that actually runs on-chain.

Building UPLC execution in Lean4

To formally verify Cardano contracts, it was necessary to faithfully reimplement UPLC and its execution semantics from scratch in Lean4. This involved building a comprehensive encoding of Plutus Core types and terms, a complete implementation of the CEK (Control Evaluation Kontinuation) machine (with a simplified cost model for now), and all the various built-ins, while staying as close as possible to the Haskell implementation.

The CEK machine is the virtual machine that evaluates UPLC code during on-chain validation. Reimplementing it in Lean4 enables formal reasoning about exactly how smart contracts execute, step by step, during actual validation.

Automatic transpilation from any UPLC source

The tool includes a command that automatically transpiles raw UPLC, regardless of its origin, into the Lean4 UPLC representation. As a result, there is no need for users to create separate models or manually translate their smart contracts into Lean4. 

Concrete counterexamples from failed properties

One of the core strengths of this formal verification tool is its ability not only to prove properties but also to find concrete counterexamples for violated properties.

When verifying properties over UPLC code, the tool does not merely perform an induction step through the CEK machine interactively. Instead, it systematically simplifies the CEK step function by applying a set of optimization rules, producing a compact and semantically equivalent representation of the contract’s behavior with respect to a specified script budget.

def step (Sigma : State) : State :=
  match Sigma with
  | s; ρ ▷ u(var x) => s ◁ ρ⟦x⟧ If x is bound in ρ
  | s; ρ ▷ u(con T c) => s ◁ v⟨con T c⟩
  | s; ρ ▷ u(lam x, M) => s ◁ v⟨lam x, M, ρ⟩
  | s; ρ ▷ u(delay M) => s ◁ v⟨delay M, ρ⟩
  | s; ρ ▷ u(force M) =>  (@f(force ⎵) ⋅ s); ρ ▷ M
  | s; ρ ▷ u[M ∘_ N] => (@f[⎵ (N, ρ)] ⋅ s); ρ ▷ M
  | s; ρ ▷ u(constr i (M ⋅ Ms)) => (@f(constr i, [] ⎵ (Ms, ρ)) ⋅ s); ρ ▷ M
  | s; ρ ▷ u(constr i []) => s ◁ v⟨constr i, []⟩
  | s; ρ ▷ u(case N, Ms) => (@f(case ⎵ (Ms, ρ)) ⋅ s); ρ ▷ N
  | s; ρ ▷ u(builtin b) => s ◁ v⟨builtin b, [], α(b)⟩
  | s; ρ ▷ u(error) => ◆
  | [] ◁ V => ▢ V
  | (@f[⎵ (M, ρ)] ⋅ s) ◁ V => (@f[V ⎵] ⋅ s); ρ ▷ M
  | (@f[v⟨lam x, M, ρ⟩ ⎵] ⋅ s) ◁ V => s; ρ⟦x ↦ V⟧ ▷ M
  | (@f[⎵ V] ⋅ s) ◁ v⟨lam x, M, ρ⟩ => s; ρ⟦x ↦ V⟧ ▷ M
  | (@f[v⟨builtin b, Vs, ι ⊙ η⟩ ⎵] ⋅ s) ◁ V =>
(s ◁ v⟨builtin b, Vs :⋅ V, η⟩) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[⎵ V] ⋅ s) ◁ v⟨builtin b, Vs, ι ⊙ η⟩ =>
(s ◁ v⟨builtin b, Vs :⋅ V, η⟩) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[v⟨builtin b, Vs, a[ι]⟩ ⎵] ⋅ s) ◁ V =>
(Eval_CEK(s, b, Vs :⋅ V)) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[⎵ V] ⋅ s) ◁ v⟨builtin b, Vs, a[ι]⟩ =>
(Eval_CEK(s, b, Vs :⋅ V)) If ι ∈ 𝓤 ∪ 𝓥
  | (@f(force ⎵) ⋅ s) ◁ v⟨delay M, ρ⟩ => s; ρ ▷ M
  | (@f(force ⎵) ⋅ s) ◁ v⟨builtin b, Vs, ι ⊙ η⟩ =>
(s ◁ v⟨builtin b, Vs, η⟩) If ι ∈ 𝓠
  | (@f(force ⎵) ⋅ s) ◁ v⟨builtin b, Vs, a[ι]⟩ =>
(Eval_CEK(s, b, Vs)) If ι ∈ 𝓠
  | (@f(constr i, Vs ⎵ (M ⋅ Ms, ρ)) ⋅ s) ◁ V =>
(@f(constr i, Vs :⋅ V ⎵ (Ms, ρ)) ⋅ s); ρ ▷ M
  | (@f(constr i, Vs ⎵ ([], ρ)) ⋅ s) ◁ V => s ◁ v⟨constr i, Vs :⋅ V⟩
  | (@f(case ⎵ (Ms, ρ)) ⋅ s) ◁ v⟨constr i, Vs⟩ => unfoldCase s i Ms Vs ρ
  | _ => ◆

The end result is a highly optimized and simplified satisfiability modulo theories (SMT) formula that captures the contract’s behavior across all possible inputs. The tool’s pre-processing phase attempts to fully resolve the CEK machine’s evaluation and reduction rules in the final formula according to the provided UPLC program. In essence, what remains is a direct logical constraint over the inputs and outputs, derived from the UPLC built-ins referenced in the code. However, a minimal portion of the CEK formulation may still appear in the final solution, particularly when script budget computation depends on the values of certain UPLC built-in datatypes. 

When a property is violated, the SMT solver produces a counterexample that corresponds to one execution of the smart contract on a given set of inputs. Unlike other formal method techniques, this is not merely a failed proof. The tool returns a concrete datum, redeemer, and script context that leads to the property violation.

Below is an example of a UPLC program that adds two integers, showing how execution can be simplified: 

(program 1.1.0 (lam x (lam y [[(builtin addInteger) y] x] )))

The team built the necessary tool to read the UPLC file and load it as a Lean definition. We also defined a lot of useful library functions to help evaluate the result of evaluation and returning it into a user-friendly type (Bool, Integer, Pairs, etc)

#import_uplc "Tests/addInteger.uplc" addInteger

def executeAdd (x : Integer) (y : Integer) : Option Int :=
 executeIntProgram addInteger (intArgs2 x y) 20

From that point, we can evaluate the UPLC program on some inputs, with the default Lean eval function:

#eval executeAdd 55 110

You can also use our tool #solve to formally prove the correctness of this program:

#solve [∀ (x y : Integer), executeAdd x y = some (x + y)]

In order to prove this correctness, this program needs to go through the CEK step function 20 times, which would make simple unrolling very inefficient. Instead, proving that addInteger does add the two inputs produce the following SMT query through our tool produces the following SMT query:

; Setting the solver call
(set-option :print-success true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi true)

; Type declaration
(declare-fun @isInt ( Int) Bool)

; Variable declaration
(declare-const $0 Int)
(declare-const $1 Int)
(declare-const $2 Int)

; Option declaration
(declare-datatype @Option (par ( |@α|) ( (Option.none )
 (Option.some  (Option.some.1 |@α|)))))

; Program and specification 
(define-fun @isOption._uniq.32834 ((@x (@Option  Int))) Bool (ite (is-Option.some @x) (@isInt (Option.some.1 @x)) true))

(assert (not (=> (@isInt $0) (=> (@isInt $1) (=> (@isInt $2) (=> (not (< $0 0)) (=> (= ((as Option.some (@Option  Int)) $2) ((as Option.some (@Option  Int)) (+ $0 $1))) (= $2 (+ $0 $1)))))))))

As one can see, the program and specification, even if it goes through 20 iterations of the CEK step function, has been reduced to just $0 + $1 by all our powerful optimization rules.

Verifying compiled code, not just surface logic

Having a formal verification tool that directly targets UPLC code allows proving properties on the exact code representation executed on the Cardano blockchain. As such, this approach does not rely on assumptions made at the surface language level, nor on trusting that compilation correctly preserves semantics.

Instead, the tool verifies how the actual compiled validator behaves, along with all compiler optimizations. This provides strong assurance that the compiled contract behaves correctly (ie, not just the surface code), and that transformation and compiler optimizations have not introduced any bugs.

We tested our tool on a project that is currently running on Cardano’s mainnet. As we did for the addInteger example, we can import the produced UPLC code with a simple command:

#import_uplc "Tests/Smt/Benchmarks/UPLC/Examples/Onchain/processSCOrder.uplc" processSCOrder
#prep_uplc "compiledProcessSCOrder" processSCOrder [ProcessSCInput] orderInputToParams 1000000

The processSCOrder function is not a simple one, it’s more than 1,500 lines of prettified UPLC code. We then allow up to 1,000,000 executions through the CEK step function.

We can then start writing in Lean4 the 14 requirements the developing team already had:

def sto7_part1 (x : ProcessSCInput) : Prop :=
  isBuySCOrder x →
  validOrderInput x →
  x.state.crN_RC = 0 →
  successfulOrderImpliesPredicate (fromHaltState $ compiledProcessSCOrder x) (validBuySC x)

#solve [ ∀ (x : ProcessSCInput), sto7_part1 x ]

The tool outputs: ✅ Valid for all of them. Each SMT model is around 60 lines of SMTLib2 thanks to the preprocessing and optimization step. The proof time for those 14 specifications is around 10 seconds on a regular laptop.

If we change slightly the code to make it different from the correct implementation, the tool reports a bug for a specific value:

 x:=
   scMinRatio : 5/2
   scMinOperatorFee : 1
   scMaxOperatorFee : 3
   scOperatorFeeRatio : 4/4
   scBaseFeeBSC : 2/1
   scBaseFeeSSC : 0/3
   nbTokens : 1
   totalPrice : 4
   orderSubmitter : 7
   orderRate : 1/2
   orderTimeStamp : 13
   orderTxOutRef : 9
   adaAtOrderUtxo : 11
   minAdaTransfer : 3
   state : ComputeReserve.mk 19 5 0

The developer can then replay this counterexample, fix the bug, and relaunch the proof to see if the fixed version now matches the expected behavior.

Practical implications

This capability enables developers to catch subtle bugs in their contracts regardless of the input language, as long as it complies to UPLC. The verification process is completely automatic and works with real, deployed contracts. 

Looking forward, the tool could be used to verify that surface code and compiled code are semantically equivalent, hence providing mathematical proof that the compiler preserves intended behaviors. The tool can also be used to prove the equivalence of two different UPLC scripts with very minimal need for formalization from the user. 

While work on this tool is still early, it is already being tested. In a future blog post, we will show how this is used internally for the proof of a DApp running on mainnet.

Extending to multi-transaction scenarios

So far, the focus has been on single transactions, verifying properties of individual contract executions in isolation. However, many smart contract bugs – and most real business logic – arise from multi-step interactions, where datum evolves across multiple blocks or epochs.

Think about common examples from tutorials: auctions, escrow contracts, and other protocols where business logic requires multiple transactions from different stakeholders.

In the next post in this series, the team will introduce a state machine model for verifying smart contract behavior across multiple transactions and blocks. It will show how the blockchain state and ledger rules were modeled and present new techniques for verifying execution traces, from finite sequences to unbounded executions.