Lean Miniscript

A Lean 4 model connecting typed Miniscript to the Bitcoin Script it compiles.

GitHub repository

Introduction

How does a plain-language spending rule become Bitcoin Script?

We use MiniscriptA typed structure for composing and analyzing spending conditions. to describe Bitcoin spending conditions in a structured form. Miniscript tools can analyze this structure and compile it into the lower-level Bitcoin ScriptThe stack program that Bitcoin nodes execute. that nodes execute.

The same rule in three forms The meaning should stay the same while its representation changes.

Plain language

The spending condition stated without implementation details.

Two of the three signers must approve the spend.

Structured Miniscript

A readable form that software can analyze and compose.

multi(2,A,B,C)

Modeled Bitcoin Script

Execution consumes the input stack and leaves a Boolean result on top.

Compiled Script
2ABC3CHECKMULTISIG
Input stack
0sigAsigC
Result stack
true

Compilation

A compiler turns Miniscript into Bitcoin Script

Bitcoin nodes do not execute Miniscript directly. A compiler, usually part of wallet or library software, translates it into the ordered Bitcoin Script instructions they execute.

Compilation example: two ways to authorize a spend Use any two of A, B, and C. Alternatively, after a delay, use recovery key R.

1 · Miniscript input

Expression or_i(primary, recovery)
Primary // Any two of A, B, and C multi(2, A, B, C)
Recovery // After DELAY, use key R and_v(v:older(DELAY), pk(R))

2 · Compiler rules

or_i(X, Z)==>IF X ELSE Z ENDIF
multi(k, keys)==>k keys n CHECKMULTISIG
v:older(n)==>n CHECKSEQUENCEVERIFY VERIFY
pk(key)==>key CHECKSIG

3 · Bitcoin Script output

IF // Primary path 2 A B C 3 CHECKMULTISIG ELSE // Recovery path DELAY CHECKSEQUENCEVERIFY VERIFY R CHECKSIG ENDIF

The verification problem

How do we know the compiled Script still means the same thing?

The compiler has produced a Script. However, can we trust its translation? It is easy to assume that the output means the same thing as the Miniscript input. If the translation is wrong, the compiled Script could allow an extra spending case or produce different stack behavior.

Correct compilation preserves behavior For every supported expression, the Miniscript model and compiled Script must agree under the same input and transaction conditions.

Miniscript expects

  • Primary2-of-3 from A/B/Ctrue
  • RecoveryR after DELAYtrue
  • Otherwiseanything elserejected

Must match

expected(m)
=
execute(compile(m)) same input · same transaction

Compiled Script produces

  • Primary2 valid signaturestrue
  • RecoveryDELAY + signature Rtrue
  • Otherwiseanything elserejected

When compilation is faulty and allows more than Miniscript describes

Correct compilation keeps the two behavior sets equal. Faulty compilation can add a result that Miniscript never accounted for.

Faulty compilation enlarges the behavior set The extra region is where an assumption made by another expression can fail.
Compiled Script behavior
Behavior described by Miniscript Expected results
Extra result
Potential failure Extra result can lead to unexpected outcomes.

Concrete example A 2022 rust-miniscript security advisory documented this kind of mismatch: a satisfied d: child was typed as leaving exactly 1, while some compiled Scripts could leave another true value where MINIMALIF was not a consensus rule.

Lean for formal verification

Turn compiler correctness into a mathematical proof goal

Turn compiler correctness into a Lean theorem Define the expression, its compilation, and its execution. Then prove the expected and actual outcomes match.
1

Expression

Define the Miniscript model

m : CoreFragment Represent expressions, then assign each well-typed expression its expected stack behavior.
2

Translation

Model the compiler

compile m Specify the Script instructions emitted for each constructor.
3

Execution semantics

Define Script execution

Eval (compile m) … result Relate the initial stacks and transaction context to the resulting stacks—or failure.
4

Theorem target

Show the behaviors agree

expected = actual The general proof for every supported expression is still in progress.

The central goal is a theorem about every supported Miniscript expression. If Lean assigns an expression a type, evaluating its compiled Script must have the stack behavior recorded by that type. Proving this constructor by constructor rules out compilation steps that introduce results the type system did not account for.

Why it matters

How could Lean Miniscript help wallet and library developers?

Lean Miniscript gives wallet and library developers a way to check what a Miniscript compiler does instead of simply trusting its output. It is verification infrastructure, not a wallet feature by itself.

  1. Understand the compiler output

    Follow each Miniscript constructor into the Bitcoin Script instructions it produces. This makes the compiler easier to review and debug.

  2. Catch mistakes early

    For supported constructors, Lean checks that the generated Script follows the BIP 379 scheme. This can reveal translation mistakes before compiled policies reach users.

  3. Keep the checks up to date

    As implementations add constructors, optimizations, or Script contexts, their rules and proofs can be added to the same model. A general type-soundness proof is still in progress.