Home

Formal reasoning for Bitcoin spending conditions

Lean Miniscript

Lean Miniscript is a Lean 4 project building a machine-checked link between Miniscript’s type system, its compiler, and the behavior of the Bitcoin Script it produces.

View repository

01

Project overview

A Lean model of typed Miniscript and the Script it compiles to

Lean Miniscript formalizes both sides of the compiler boundary in Lean 4. It models Miniscript syntax, validation, and types; a compiler from core expressions to Bitcoin Script; and the stack behavior of the Script instructions that compiler produces.

The central proof goal is to show that a well-typed Miniscript expression compiles to Script whose execution respects the behavior promised by its type. The project therefore connects a readable spending condition to the lower-level program a Bitcoin node ultimately evaluates.

Miniscript

A typed structure for composing Script

Miniscript gives a composable subset of Bitcoin Script a readable expression form and a type system. Wallet software can analyze a Miniscript expression, reason about possible spending paths, and compile it to Script.

Bitcoin Script

The program Bitcoin nodes execute

Bitcoin Script is a low-level, stack-based language used to enforce spending conditions. Signatures, timelocks, and branch choices ultimately have to succeed as Script under the transaction context.

Try the relationship

Miniscript playground

Choose an example, then change the spending data available to it.

Spending rule

Any two of A, B, and C can authorize a spend.

Miniscript

multi(2,A,B,C)

Bitcoin Script

2 A B C 3 CHECKMULTISIG

Schematic

Available spending data

Illustrative check: ready

Two primary signatures are available: A and B.

This interaction illustrates spending paths. It does not execute Bitcoin Script, run the compiler, or invoke the Lean model.

02

How a Miniscript expression becomes Bitcoin Script

Compiler walkthrough

The compiler expands one constructor at a time

Using the recovery policy from above, the surface shorthand is first expanded into core syntax. The compiler then walks the core tree: each constructor contributes a fixed instruction pattern, and the nested results are concatenated into one list.

surface expression → core syntax → instruction list
01 · Simplified Miniscript

Readable policy structure

or_i(multi(2,A,B,C), and_v(v:older(DELAY),pk(R)))
02 · Core syntax

Explicit constructor tree

  • .or_i
    • .multi 2 [A, B, C]
    • .and_v
      • .v
        • .older DELAY
      • .c
        • .pk_k R

The readable pk(R) shorthand becomes the explicit core wrapper .c (.pk_k R).

03 · Recursive compile

Each node contributes a local instruction shape

.or_i x y OP_IF · compile x · OP_ELSE · compile y · OP_ENDIF
.multi 2 [A,B,C] PUSH 2 · PUSH A · PUSH B · PUSH C · PUSH 3 · OP_CHECKMULTISIG
.and_v x y compile x · compile y
.v (.older DELAY) PUSH DELAY · OP_CHECKSEQUENCEVERIFY · OP_VERIFY
.c (.pk_k R) PUSH R · OP_CHECKSIG
04 · Modeled Bitcoin Script

Nested results flatten into one list

03

Lean in the pipeline

What Lean models and checks

Lean formalizes the core expression, its validation and type, the compiler that emits Script instructions, and an execution model for those instructions. This lets the project ask whether the compiled Script has the stack behavior recorded by Miniscript’s type system.

Shared Lean value

m : CoreFragment

Lean stores the expression as a tree built from keys, timelocks, wrappers, and connectives. Both statements below use this same m.

1 · Static checks about m

Validate the expression and assign its type

  1. Validate WellFormed ctx m

    Checks whether the expression is allowed for these keys, timelocks, thresholds, and Script context.

  2. Type HasType m ty

    Assigns a MiniType named ty, whose base type and modifiers summarize stack use and composition rules.

Type summary: ty records what the expression consumes from the stack, what it leaves behind, and how it can be combined with other expressions.

2 · Compiled execution of m

Compile the same expression and evaluate its Script

  1. Compile compile m

    Recursively turns the core expression into a modeled Bitcoin Script instruction list.

  2. Evaluate Eval (compile m) … result

    Uses the stacks, flags, and transaction context to determine the Script result.

Behavior: result records what the compiled Script actually does.

A concrete check

What Lean can say about multi(2,A,B,C)

Miniscript expression multi(2,A,B,C)
Core syntax .multi 2 [A, B, C]
Static check before compilation

WellFormed

Checks the expression and its context, not the signatures or runtime outcome.

  • legacy multisig is permitted
  • 1 ≤ 2 ≤ 3
  • key count and keys are valid
What type does Lean assign?

HasType

Base type B, with the modeled n d u s modifiers.

Modeled Bitcoin Script 2 A B C 3 CHECKMULTISIG

Possible CHECKMULTISIG outcomes

  • Enough matching signatures and a valid dummytrue on the stack · spend accepted
  • Signatures do not meet the thresholdfalse on the stack · spend rejected
  • Invalid legacy dummyScript error · spend rejected

What Lean lets us check: compiling multi(2,A,B,C) must not weaken its 2-of-3 requirement or change its expected stack behavior. This becomes a precise statement that Lean can prove and recheck whenever the model changes.

04

Why soundness matters

Why prove that the type matches the compiled Script?

Miniscript’s type system describes a spending condition before execution, but the Bitcoin network enforces only the compiled Script. The soundness proof is needed to show that compilation does not weaken or change the stack behavior recorded by the type.

A 2022 rust-miniscript security advisory documented a concrete mismatch: the type system said that a satisfied d: child produced exactly 1, but some compiled Scripts could leave another true value.

What happened when the type and the compiled Script disagreed

Miniscript type says

A satisfied d: child contributes exactly 1 to a threshold.

Compiled Script can actually leave

Where MINIMALIF is not a consensus rule, the child can retain another true value such as 2.

05

What Lean adds

What can Lean Miniscript help us do?

Lean gives the project precise definitions of Miniscript syntax, typing, compilation, and Script execution, together with a language for stating how they should agree.

  1. 01

    Make the compiler pipeline precise

    Define Miniscript syntax, typing, compilation, and Script execution so that every step has an exact meaning.

  2. 02

    Verify and improve compiler rules

    For a supported case, prove the current rule correct or show that a smaller, optimized Script sequence preserves the same Miniscript behavior.

  3. 03

    Get immediate feedback on changes

    As the model changes, Lean rechecks the affected examples and proofs and shows what no longer holds.