Working formalization
Lean Miniscript
A Lean 4 model connecting Miniscript validation, typing, compilation, and Bitcoin Script behavior.
Selected work
Formal models, proof-oriented tools, and compact explanations of the boundaries they aim to verify.
Working formalization
A Lean 4 model connecting Miniscript validation, typing, compilation, and Bitcoin Script behavior.