A STARK proof of Bitcoin's UTXO set with circuits proven in Lean

An independent developer has built a STARK prover for Bitcoin consensus as a side project, generating a 1.6 MB proof that validates header chains, block data replaying from block 935,001 to 972,500, and the resulting UTXO set. The project uses Stwo circle STARKs through a Zig port, with circuits written and proven in Lean 4 and verified in a browser in about half a second. The author is seeking feedback and hardening attempts for the implementation. Open article →