Why verify the mainnet consensus rules

Bitcoin nodes must agree on which blocks are valid and on the spendable outputs that a valid block creates. A discrepancy in an arithmetic boundary, script operation, or historical exception can change that decision. This mission targets all Bitcoin mainnet consensus rules, including their historical applicability, through a source-linked Lean 4 development. BIP68 relative sequence locks are the first component, not the completion criterion.

The implementation reference is Bitcoin Core revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, with unmodified mainnet parameters. Freezing the revision makes the target reviewable; future protocol changes require an explicit scope revision. Historical coverage means the pinned implementation's treatment of blocks at historical heights, including exceptions. Reproducing every obsolete software release is a separate question. Validation source, mainnet parameters.

The specification developed over multiple generations: the original proof-of-work chain design, later script and duplicate-transaction rules, relative locks, witness transactions, and Taproot. These layers remain relevant together. Existing Lean work on absolute transaction lock time provides a potential reusable starting point; it does not discharge relative locks or whole-system correctness. Original design, BIP68, existing lock-time formalization.

Blocks, histories, and validation outcomes

A chain state contains a validated ancestor history and a UTXO set, the outputs currently available to spend, including their values, scripts, creation heights, and coinbase status. A candidate block contains a header and an ordered transaction list. An explicit time input represents the local clock used when checking a newly received header. A consensus specification states validity and state transitions independently of the translated implementation.

The executable model must cover the complete validation path. Calling ConnectBlock alone is insufficient: header and contextual checks occur elsewhere. The full-validation setting enables proof-of-work, commitment, and script checks; assumed-valid shortcuts are not evidence of those checks. Temporary future-time failures must remain distinguishable from permanent invalidity. Validation entry points and caller contracts.

Whole-consensus target and component milestones

Write $R(S)$ for independently specified reachability from mainnet genesis, $C(S,B,t)$ for the source-linked validation outcome, and $V(S,B,t)$ for declarative admissibility at the supplied time. The intended acceptance theorem is

$$\forall S,B,t,\quad R(S)\Longrightarrow \bigl(C(S,B,t)\text{ accepts}\iff V(S,B,t)\bigr).$$

For every accepted block, the implementation and specification must also agree on the resulting ledger state:

$$C(S,B,t)=\operatorname{Accept}(S') \Longrightarrow S'=\operatorname{ApplySpec}(S,B).$$

The target additionally requires correct genesis initialization, interpretation of serialized data, historical rule selection, and state restoration across disconnect/reconnect operations. The candidate block is not assumed valid. A classification contract must account for time-dependent rejection without permanently invalidating an otherwise eligible header.

These formulas are the goal contract to formalize, not existing Lean declarations. A complete concrete definition of the history, specification, executable validation pipeline, and state correspondence must precede the overarching theorem. The main theorem is BitcoinBlock.acceptance of component mission 13, the formalization of the acceptance contract above, to be selected once that mission is published; BitcoinBlock.apply_spec is the state-transition contract. Selecting the BIP68 theorem as the main theorem would incorrectly allow a partial result to complete this mission.

The component program covers:

1. Data representation, serialization, hashes, finite-width arithmetic, and source coverage.
2. BIP68, including sequence decoding, threshold accumulation, output heights, bounds, and the caller bridge.
3. Transaction structure, duplicate inputs, amount ranges, UTXO availability, maturity, fees, subsidy, and coinbase rewards.
4. Absolute lock time, median-time-past calculation and selection, and script-level lock checks.
5. Header validity, compact targets, proof of work, retargeting, and cumulative work.
6. Block structure, Merkle mutation detection, witness commitments, weight, and signature-operation limits.
7. Legacy Script and P2SH, signature encodings, signature hashes, and exact ECDSA verification behavior.
8. SegWit version-zero execution and signing rules, Taproot, Schnorr verification, and Tapscript.
9. Historical flags, activation boundaries, genesis behavior, and named block exceptions.
10. Full validation composition, ledger updates, reorganization correctness, and closure of the source-coverage audit.

Ledger-safety corollaries

The overarching equivalence and state-transition theorems must yield the following named results, each stated as its own milestone once the ledger model exists:

1. No value creation by a transaction. An accepted ordinary transaction consumes available outputs, leaves unrelated outputs unchanged, and does not increase total ledger value.
2. Block value bound. An accepted block increases total ledger value by at most its subsidy; fees only move value between outputs.
3. Issuance bound. Repeated valid extensions from genesis keep cumulative issuance below 21 million BTC, accounting for the subsidy schedule, unclaimed coinbase value, unspendable outputs, output-key overwrites, and the historical duplicate-coinbase exceptions.

Reuse and modeling notes

Existing Lean work in btc-verified documents proofs for serialization, Merkle properties, UTXO accounting, and transaction checks, and lists BIP68 relative locks and full block composition as outstanding. Those modules are candidates for reuse after their representations and assumptions are audited against the pinned revision; their documentation has not been independently built or audited here. Documented coverage

The BIP68 model uses natural-number subtraction, so $h-1$ truncates to $0$ and matches the source's $\max(h-1,0)$. The sequence-seconds mask-and-shift stays below $2^{25}$ and cannot overflow a 32-bit word. Real chains have monotone median-time-past; the component theorems deliberately do not assume it, so they hold for the weaker model.

Concrete hash and signature-verification semantics are required for the final result on purpose: functional correctness needs them, while cryptographic hardness and unforgeability are separate projects with computational assumptions. Because the full scope is large, the BIP68 component, UTXO accounting, and the Merkle and serialization layers are each suitable as an independently reviewable sub-mission feeding this umbrella goal.

The BIP68 component is published as its own mission, BIP68 Relative Lock-Time: Bitcoin Core Sequence Locks Agree with the Specification, whose two definitions and five open theorems are referenced here rather than re-declared. Its four supporting statements are component milestones of this mission; its goal theorem BitcoinBIP68.core_correct is a component result, not this mission's goal. The other areas are roadmap obligations pending concrete formalization, not already linked theorem milestones.

Component missions

The roadmap areas are being delivered as separately reviewable missions whose published theorems this mission references:

1. BIP68 relative lock-time — goal BitcoinBIP68.core_correct (proved): the Core sequence-lock helpers decide exactly the BIP68 condition. Area 2.
2. Block subsidy and the 21 million bound — goal BitcoinSubsidy.issuance_bound: cumulative GetBlockSubsidy stays below MAX_MONEY at every height. Area 3 (issuance).
3. Proof of work: compact targets and retargeting — goal BitcoinPow.nextWork_permitted: CalculateNextWorkRequired always passes PermittedDifficultyTransition, with exact characterizations of SetCompact/GetCompact overflow and rounding. Area 5.
4. Merkle root and the CVE-2012-2459 mutation check — goal BitcoinMerkle.dup_block: duplicating an aligned trailing block of $2^k$ leaves preserves the root and is detected. Area 6 (Merkle).
5. UTXO accounting and the ledger supply bound — goal BitcoinUtxo.ledger_bound: from an empty ledger, accepted blocks (with CheckTransaction, BIP30, CheckTxInputs, fee accumulation and the coinbase bound) hold at most the summed subsidies; with milestones tx_conservation (no value creation) and block_bound. Area 3 (accounting) and the three ledger-safety corollaries above.
6. Block headers: median time past and the contextual rules — goal BitcoinHeader.mtp_mono_chain: along any chain obeying time-too-old, the median time past is non-decreasing; with the characterization of ContextualCheckBlockHeader and the BIP34/66/65 version floors. Area 4 (median-time-past) and the header part of area 5.
7. Soft-fork activation: script flags by height — goal BitcoinActivation.flags_mono: GetBlockScriptFlags is monotone in height for ordinary blocks, with the activation order, the two hash-keyed exception blocks, and the CSV lock-time flag. Area 9 (historical flags and named exceptions).
8. Script: CScriptNum, the legacy interpreter, and the P2PKH template — goal BitcoinScript.p2pkh_correct: against the transcribed EvalScript (full non-push opcode table of SigVersion::BASE, element/operation/stack limits, disabled opcodes) and VerifyScript for plain output scripts, DUP HASH160 <h> EQUALVERIFY CHECKSIG succeeds exactly when the key hashes to $h$ and the signature verifies, for every oracle; with the CScriptNum round-trip and minimality, the CastToBool characterization, the CVE-2010-5137 rule and the 201-operation limit. Area 7 (legacy Script), with hashes, signature checking and lock-time checks as oracle parameters.
9. Serialization, CompactSize, SHA-256d/Hash160, weights, the genesis block — goal BitcoinSer.block_roundtrip: the block, transaction and header encodings round-trip for well-formed values, with concrete SHA-256 and RIPEMD-160, the CompactSize canonical form, GetSerializeSize-based weights, and the genesis hash and merkle root by kernel evaluation. Area 1.
10. Signatures: strict DER, sighash (legacy and BIP143), secp256k1 ECDSA and BIP340 Schnorr, concrete P2PKH — goal BitcoinSig.derEncode_complete: IsValidSignatureEncoding accepts exactly the canonical encodings, with the exact SignatureHash quirks (SIGHASH_SINGLE bug, FindAndDelete), the field and group arithmetic of secp256k1, and the Script mission's P2PKH theorem instantiated with the real checker. Area 7 (signatures) and part of area 8 (BIP143).
11. VerifyScript: P2SH, native and wrapped SegWit v0, unknown witness versions — goal BitcoinVerify.p2wpkh_correct: the dispatch of VerifyScript/VerifyWitnessProgram/ExecuteWitnessScript, with the four spending templates characterized two-directionally and the malleability and upgrade rules as universal statements. Area 8 (SegWit v0) and BIP16.
12. Taproot: key path, script-path commitment, BIP341 sighash, Tapscript rules — goal BitcoinTaproot.keypath_correct: the version-1 branch, the tagged hashes, the merkle path, the tweak check, SignatureHashSchnorr, CheckSchnorrSignature, and the BIP342 interpreter rules, closing the script layer with no parameter left. Area 8 (Taproot, Schnorr, Tapscript).
13. Block validation composed — goal BitcoinBlock.acceptance: the executable validation path C(S, B, t) (AcceptBlockHeader, CheckBlock, ContextualCheckBlock, ConnectBlock, with GetBlockScriptFlags, BIP30 history, IsBIP30Repeat, undo data) composed from the component missions' functions, the declarative V(S, B, t) and ApplySpec(S, B), and the proofs of R(S) ⟹ (C accepts ⟺ V) and C = Accept(S') ⟹ S' = ApplySpec(S, B), together with the exact classification of temporary future-time rejections, the well-formedness of reachable states, strictly increasing chain work, and DisconnectBlock restoring the ledger. Area 10 and the remaining parts of area 9 (genesis, BIP30 exceptions). Its goal theorem is the intended main theorem of this mission once published.

Each is parametric where the layer below is not yet formalized (an abstract hash type for Merkle, an abstract subsidy function for the ledger bound, abstract transaction ids, an oracle for the hash, signature and lock-time primitives of Script), so that composing them is a matter of instantiation. Missions 9–13 perform that instantiation: the composition in mission 13 uses the concrete hashes, signatures, scripts, subsidy, difficulty, median time, activation flags and BIP68 functions of the published missions, with no parameter left abstract. Two technical notes for solvers of the remaining areas: the platform rejects proofs that use bv_decide, because its certificate relies on Lean.ofReduceBool; bit-level facts must be proved through BitVec.toNat and the Nat bitwise lemmas. And the BIP68 equivalence core_correct holds without its admissibility and overflow hypotheses, since Lean's integers are unbounded; those hypotheses are what the separate bounds theorem needs to justify the fixed-width reading of the source.

What completion would establish

Completion would give kernel-checked acceptance and state-transition results for a concrete Lean rendering of the pinned mainnet validation rules. Both acceptance of valid candidates and rejection of invalid candidates matter. The source-to-Lean correspondence must be documented and independently reviewed; a proof about manually transcribed Lean code alone is not a proof about a compiled Bitcoin Core binary.

The current BIP68 statements have independent read-backs and compiled locally with intentional open proof placeholders. Previous differential checks exercised 2,014 cases against extracted Core helper bodies. Those checks provide evidence about that component only; they neither prove its universal theorems nor validate the broader mission. No whole-consensus correctness proof is claimed.

Existing Formalpedia definitions and proofs should be reused after their assumptions and representations have been checked. Generic Merkle-tree or signature results cannot be treated as Bitcoin-specific theorems without a correspondence result.

Why composition and historical behavior are difficult

Local helper contracts leave premises for callers to establish. For BIP68, these include input heights, ancestor clocks, activation flags, coinbase exclusion, and arithmetic bounds. Completing the helper proof does not establish those premises for block validation.

Historical behavior is not captured by a single table of activation heights. The pinned implementation contains script-flag exceptions indexed by block hash and special duplicate-coinbase handling. Its genesis transaction is not connected to the spendable ledger. These cases must be represented explicitly. Flag selection, connection, and disconnection.

Script correctness also depends on execution version, exact byte encodings, signature-message construction, and rules for unknown or reserved features. Mempool policy flags must not accidentally become consensus requirements. Script interpreter.

Formalization scope and completion criteria

All mainnet consensus branches reachable under the fixed parameters are in scope, across historical heights and admissible alternative histories. This includes formerly external BIP68 caller responsibilities. The top-level result must discharge component premises or expose a genuine source limitation; assuming successful validation, defining the specification by calling the implementation, or leaving unimplemented rules behind always-true predicates is unacceptable.

The full development must supply concrete hash and signature-verification semantics. Conditional intermediate lemmas are welcome, but unresolved crypto-verification or script oracles do not satisfy the final goal. Functional correctness does not require proving cryptographic hardness. Machine bounds must be justified; cases that reveal undefined source arithmetic are findings, not cases to hide through convenient hypotheses.

The core target uses full validation from genesis. Equivalence of caches or optional validation shortcuts requires separate justification if incorporated. Networking, wallet behavior, relay policy, miner incentives, and compiler correctness are outside this consensus-rule target. Cumulative-work comparison and valid reorganization are included; universal agreement on arrival-order tie-breaking is not asserted.

Completion requires the concrete global theorem, all necessary component proofs without proof holes or custom correctness axioms, historical boundary coverage, source correspondence review, and a branch-level inventory with no unexplained consensus omissions. The roadmap is an initial decomposition, not a claim that the source inventory is already exhaustive. The comprehensive goal must be formalized and audited before this proposal is ready for submission.

Selected references

• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. Paper.
• Bitcoin Core contributors. Bitcoin Core mainnet validation implementation, pinned revision reviewed 2026. Source.
• Mark Friedenbach, BtcDrak, Nicolas Dorier, and kinoshitajona. BIP68: Relative lock-time using consensus-enforced sequence numbers, Bitcoin Improvement Proposals, 2015. Specification.
• Bitcoin Improvement Proposal authors. Consensus specifications and their historical context, collection at revision 100ba872c808946155b1eeb8c4568058f2eea0a7. Collection.
• ProofOfKeags contributors. btc-verified: Absolute transaction lock time, pinned revision reviewed 2026. Lean development.