btc-verified

Machine-checked components of the Bitcoin protocol, in Lean 4.

Consensus code is the kind of software testing alone cannot secure: every node must reach the same verdict on every byte, a divergence between implementations is a chain split, and the failures that matter are exactly the inputs no test suite thought to include. This repository builds Bitcoin's core in a proof assistant instead — the data structures, their serialization, the hash commitments that link them, the ledger they act on, and, ahead, the validity rules, the monetary guarantee, and fork choice — so that the properties Bitcoin depends on are theorems a machine re-checks on every build, not claims a reader has to take on trust.

The repo grows as small "proof leaves": each module builds cleanly, states exactly what it proves, and makes the next claim easier to state. The proofs stay anchored to the real network — the verified decoders and computable hashes run against actual mainnet blocks at build time, and an axiom audit fails CI if any headline theorem depends on an unproved assumption.

The ambition, laid out in the roadmap below, is machine-checked proofs of the guarantees Bitcoin is valued for: that its rules cap issuance below 21 million coins, and that the fork-choice rule selects the valid chain backed by the most work.

Current proof leaves

What is proved so far, by directory. Each directory's README carries the precise checked claims, theorem by theorem; each line here is the plain statement of what stands.

Serialize/ — Every encoder/decoder pair carries machine-checked proofs that decoding inverts encoding and that each value has exactly one accepted encoding, including Bitcoin's CompactSize integers.
Crypto/ — A computable SHA-256 checked against published test vectors, and Bitcoin's merkle tree with proofs of exactly what a merkle root does and does not commit to, including the defense against the CVE-2012-2459 duplication attack.
Transaction/ — Bitcoin transactions, legacy and SegWit, with verified serialization in both directions and proofs that transaction ids are binding commitments to the transaction.
Block/ — Every byte of a block parses through a verified codec (checked against real mainnet blocks), block hashes are proved binding, and a chain's tip hash provably commits to the entire history behind it.
Script/ — Bitcoin Script programs modeled as the raw bytes consensus actually validates, with the boundary between parsing and execution drawn where the protocol draws it.
Chainstate/ — The set of spendable coins and the single action every transaction performs on it, with the accounting identity the supply-limit theorem will be built on.
Impl/ — Functions transcribed from Bitcoin Core's own source code and proved to satisfy the specification, starting with its merkle-root computation.
BitVM/ — An abstract model of BitVM's bit commitments, with a proof that equivocating on a committed bit yields a hash collision.

Roadmap

The trail toward the larger artifacts is tracked as GitHub milestones, in dependency order. Each milestone page states its claims precisely and tracks the work items; in outline:

Consensus guards: transaction and block validity — Write down the rules that decide whether a transaction or block is valid, and prove that every valid block updates the set of spendable coins exactly as specified.
The supply limit theorem — Prove that under those validity rules, the total number of bitcoins that can ever exist stays below 21 million.
Proof of work and cumulative work — Define what it means for a block to prove work — the hash target its header must meet — and prove how that work adds up along a chain.
The block tree and fork choice — Prove that when competing chains exist, Bitcoin's rule for choosing between them selects the valid chain backed by the most total work.
The Core transcription track — Translate consensus-critical functions from Bitcoin Core's actual source code into Lean and prove they satisfy the specification, as is already done for its merkle-root computation.
Script: tokenization and the execution core — Build a verified interpreter for the core of Bitcoin's Script language, and prove the standard payment types accept exactly the spends that present a correct signature.
ByteArray transport and the full-chain demo — Make the verified components efficient enough for real use, and demonstrate it by checking actual Bitcoin mainnet history with them.

Build

With Nix, enter the development shell first:

nix develop

lake exe cache get   # fetch the mathlib cache (first build only)
lake build           # the library, plus the golden vectors and axiom audit
lake test            # block 481824 through the block codec (fetched on first run)
lake lint

lake build also elaborates Tests/: golden vectors that run the verified decoder over real mainnet bytes (the first Bitcoin payment, the SegWit activation coinbase, the first SegWit spend, the genesis block, block 170, and the genesis → block 1 chain link) and an axiom audit that fails the build if any headline theorem depends on sorry or an unexpected axiom. lake test decodes the full SegWit activation block, fetching it from a block explorer on first run and caching it locally (it is public chain data, so it is not committed). See CONTRIBUTING.md for the contribution workflow.

License

Licensed under the Apache License, Version 2.0 — matching the Lean and Mathlib ecosystem this builds on, and carrying an explicit patent grant. See LICENSE.

About

btc-verified is built by Keagan McClelland (@ProofOfKeags, proofofkeags.com) — an independent Bitcoin/Lightning engineer working toward verified cores for the protocol's correctness-critical surfaces.

The thesis behind the work — why AI-assisted authorship is making formal verification the defensible posture for protocol engineering, rather than a luxury — is laid out in Formal Vibefication.