Paper 2024/1768

Programmable Bitcoin Verification via Synthesis-Aided Lifting

Abstract

A new wave of proposals, such as covenants (OP_CHECKTEMPLATEVERIFY), the reactivation of OP_CAT, and BitVM-style fraud proofs, promises to turn Bitcoin into a settlement layer for decentralised finance. These projects must be expressed in Bitcoin script, a stack language with no loops or recursion; practical applications therefore expand into megabytes of unrolled opcodes whose slightest error can freeze or steal funds. Existing verification tools collapse under the resulting explosion of constraints. We present bitguard, the first scalable verifier for programmable-Bitcoin artifacts. Inspired by recent advances in program lifting and synthesis, bitguard automatically (i) lifts raw script into a semantics-preserving, register-based DSL and (ii) detects repetitive slices that mimic batch operations (map, fold, filter, Merkle-proof checks). Each slice is replaced with a single higher-order combinator whose behavior is captured by an axiom, shrinking downstream SMT constraints by orders of magnitude. A counter-example-guided inductive synthesis loop ensures every transformed fragment remains equivalent to its original script. Evaluated on 104 real-world benchmarks, including full BitVM2 prover–verifier pairs, bitguard automatically verifies 88% of the cases in an average of 23.57s, outperforms direct SMT encodings by up to two orders of magnitude, and uncovers 5 previously unknown vulnerabilities. These results demonstrate that synthesis-aided lifting with axiomatized batch combinators delivers practical, rigorous assurance for the emerging ecosystem of programmable Bitcoin.