A formal, adversarial, and invariant-driven treatment of what it actually takes to make Bitcoin quantum-safe at the consensus level — not at the wallet level, not at the "just use a post-quantum signature" level, but at the level where it matters: the state machine.
This repository contains:
- A research paper that models Bitcoin's consensus layer as a labeled transition system and proves, under explicit axioms, what protocol-level quantum safety requires and why it cannot be achieved without hard trade-offs.
- A Rust reference implementation of the PQ witness protocol (SegWit v2, ML-DSA-44 FIPS 204) with an explicit FIPS 205 SLH-DSA-128s fallback profile that is dimensioned but not consensus-enabled until a verifier/refinement boundary exists.
- Coq mechanized artifacts for the spend predicate, cryptographic suite profile/activation boundary, UTXO transition, cost model, sighash model, txid preimage transcript, executable structural block-application semantics, structural PO-6 UTXO-domain preservation, total-value non-increase, legacy-output non-increase after announcement, and freeze-policy/frozen-count non-increase after cutover, Coq-extracted/Rust PQ profile refinement, Coq-extracted/Rust sighash transcript refinement, Coq-extracted/Rust txid/UTXO structural transition/final-state refinement, a CoqExtractedTransitionKernel/Rust
TransitionKernelper-case report-refinement adapter boundary for future Coq-first extracted transition cores, Coq-extracted/Rust PO-6 invariant witness refinement, bounded PO-8 extraction evidence, Kani source-level bounded Rust refinement harnesses for the witness parser, PO-5 structural transition functions, and transition-kernel adapter, runtime txid/UTXO-store refinement validation, and compiled-artifact translation validation for each proof boundary. - TLA+ model-checked specifications of UTXO transitions (58,237 states, zero invariant violations).
This is not a proposal. This is not a BIP. This is a formal framework for reasoning about Bitcoin under quantum adversaries, with a reference implementation that demonstrates feasibility.
| Result | Theorem | Formal artifact |
|---|---|---|
| Invariant preservation | Thm 3, 4 | TLA+/TLC (2 models, zero violations) + Coq structural UTXO-domain, value, migration, and freeze theorems/refinement witnesses |
| Authorization reduction | Thm 5 | Game-hopping, tight, QROM-valid |
| Replay exclusion | Thm 6 | Sighash commitment assumption (PO-4 verified Coq model + transcript refinement + Rust PBT) |
| Suite activation boundary | Profile invariant | Coq PQProfile.v + Coq-extracted/Rust pq_profile.rs profile refinement + release-binary certificate |
| Network resilience | Thm 7 | Trace model with union bound |
| Impossibility of free migration | Thm 8, 9 | TLC counterexample |
| Spend predicate correctness | PO-1,2,3 | Coq (strengthened to full witness identity) |
| Transition determinism | PO-5 | Coq + Coq-extracted/Rust txid and structural transition refinement |
| Cost boundedness | PO-7 | Coq (exact equality: Cost = weight) |
| PO | Property | Status | Artifact |
|---|---|---|---|
| PO-1 | Spend predicate totality | Verified | Coq SpendPredPQ.v |
| PO-2 | Spend predicate determinism | Verified | Coq SpendPredPQ.v |
| PO-3 | Parse canonicality | Verified (strengthened) | Coq SpendPredPQ.v |
| PO-4 | Sighash commitment | Verified model + transcript refinement + executable evidence | Coq SighashV2.v under SHA-256 collision-resistance axiom + Coq-extracted/Rust preimage transcript refinement + Rust PBT |
| PO-5 | Transition determinism | Verified model + txid/transition refinement + bounded source-level/runtime evidence | Coq UTXOTransitions.v + Coq TxidPreimage.v + Coq-extracted/Rust txid, structural transition/final-state, and CoqExtractedTransitionKernel per-case report refinement over edge-case matrices + Kani bounded valid_tx_structural/delta_tx/valid_block_structural/structural block-application/TransitionKernel adapter harnesses + release txid/store/transition-kernel refinement validation |
| PO-6 | Invariant preservation | Model-checked + structural Coq invariant theorems + operational refinement evidence | TLA+/TLC + Coq domain/value/migration/freeze invariant theorems + Coq-extracted/Rust invariant witnesses + release-binary certificate |
| PO-7 | Cost boundedness | Verified | Coq UTXOTransitions.v |
| PO-8 | Implementation correspondence | Bounded extraction + source-level + compiled-artifact evidence | Coq VarintConcrete.v concrete canonicality/injectivity + exhaustive u16 varint refinement + witness-level consensus-domain refinement matrix + executable consensus-size guard + extracted serializer + 7 golden vectors + Kani harnesses over src/encoding.rs + release-binary refinement validation + Rust PBT |
| Profile | Cryptographic suite activation | Verified profile boundary + extraction/release evidence | Coq PQProfile.v proves ML-DSA-44/FIPS 204 is the only consensus-enabled tracked scheme; Coq-extracted/Rust profile summaries and scripts/verification/verify_pq_profile_refinement.sh require pq_profile.rs release binaries to preserve that activation boundary |
The detailed status ledger, including assumptions and residual proof gaps, is
maintained in PROOF_OBLIGATIONS.md.
├── paper/
│ ├── main.tex # Paper source (LaTeX)
│ ├── refs.bib # Bibliography
│ └── Makefile # Build via pdflatex + bibtex
├── src/ # Rust reference implementation
│ ├── lib.rs # Public API, ValidTx, DeltaTx, ValidBlock
│ ├── types.rs # Core types: Commitment, Transaction, UtxoSet
│ ├── encoding.rs # Varint, witness serialize/parse (single + multisig)
│ ├── spend_pred.rs # SpendPred_PQ (single-sig + multisig, FIPS 204)
│ ├── pq_profile.rs # FIPS 204/FIPS 205 suite profile and consensus activation guard
│ ├── sighash.rs # Sighash v2 transcript/preimage construction with BIP 340-style tagged hashes
│ ├── kani_proofs.rs # Source-level bounded PO-8 parser and PO-5 transition harnesses
│ ├── transition_core.rs # PO-5 structural TransitionKernel adapter boundary
│ ├── migration.rs # Migration_Controller (3-phase state machine)
│ ├── weight.rs # Weight_Accountant, block cost invariant
│ ├── freeze.rs # Freeze_Enforcer for unmigrated outputs
│ ├── params.rs # Consensus parameters (C_MAX, witness sizes)
│ └── tests/mod.rs # Core property-based and adversarial tests
├── tests/
│ └── integration.rs # 4 end-to-end integration tests
├── formal/
│ ├── coq/
│ │ ├── SpendPredPQ.v # PO-1, PO-2, PO-3 (varint model)
│ │ ├── UTXOTransitions.v # PO-5, PO-7 (UTXO model, cost model, structural validators)
│ │ ├── VarintConcrete.v # PO-8 (compact-size varint through 0xFD/u16)
│ │ ├── SighashV2.v # PO-4 verified model + extractable transcript function
│ │ ├── TxidPreimage.v # PO-5 txid preimage transcript + shape injectivity
│ │ ├── PQProfile.v # Cryptographic suite profile, witness cap, and activation invariants
│ │ ├── extraction/ # Coq extraction drivers + PO-4/PO-5/PO-8 refinement harnesses
│ │ └── Makefile
│ └── tla/
│ ├── BitcoinPQ.tla # Single-input model (492 states)
│ ├── BitcoinPQ.cfg
│ ├── BitcoinPQ_Migration.cfg # Migration dilemma counterexample
│ ├── BitcoinPQMulti.tla # Multi-input model (58,237 states)
│ ├── BitcoinPQMulti.cfg
│ ├── BitcoinPQMulti_Freeze.cfg
│ └── Makefile
├── models/
│ ├── state-machine.md # State machine model summary
│ └── invariants.md # Invariant catalog
├── PROOF_OBLIGATIONS.md # Authoritative proof-status ledger
├── scripts/
│ └── verification/ # Extraction, refinement, and release-certificate entrypoints
│ ├── build_extraction.sh
│ ├── compare_vectors.py
│ ├── compare_transition_kernel_refinement.py
│ ├── compare_transition_invariant_refinement.py
│ ├── verify_source_refinement.sh
│ ├── verify_compiled_refinement.sh
│ ├── verify_sighash_refinement.sh
│ ├── verify_txid_refinement.sh
│ ├── verify_transition_refinement.sh
│ ├── verify_transition_kernel_refinement.sh
│ ├── verify_transition_invariant_refinement.sh
│ ├── verify_runtime_refinement.sh
│ └── verify_pq_profile_refinement.sh
├── Cargo.toml
├── CITATION.cff
└── LICENSE
| Tool | Version | Purpose |
|---|---|---|
| Rust | 1.70+ | Reference implementation |
| Kani | 0.67.0 | Source-level bounded Rust refinement harnesses |
| Rocq/Coq | 8.18+ or 9.x | Mechanized proofs |
| Java | 17+ | TLC model checker |
| TeX Live | 2024+ | Paper compilation |
# Build
cargo build
# Run the full Rust test suite
cargo test
# Lint
cargo clippy
# Install Kani once, if needed
cargo install --locked kani-verifier --version 0.67.0
# Run source-level bounded parser and transition refinement harnesses
bash ./scripts/verification/verify_source_refinement.shThe implementation uses the fips204 crate for NIST FIPS 204 ML-DSA-44 signatures (not the pre-standard Dilithium2). src/pq_profile.rs makes the cryptographic agility boundary executable: ML-DSA-44/FIPS 204 is the only consensus-enabled tracked scheme today, while SLH-DSA-128s/FIPS 205 is a standards-aligned hash-based fallback profile that fits the witness cap but is rejected by consensus until a deployed verifier and refinement artifacts exist. The spend predicate checks this activation guard before invoking expensive signature verification, and multisig rejects committed keys outside the active consensus profile to avoid algorithm-confusion. The Kani harnesses verify the deployed Rust parser source over bounded symbolic byte arrays and check that the allocation-free layout parser, public parse_witness, consensus-domain parser, trace instrumentation, and canonicality predicates remain aligned. They also verify bounded source-level PO-5 transition behavior through the explicit structural Rust entrypoints: valid_tx_structural, delta_tx removal/preservation/insertion/empty/full-spend-create cases, valid_block_structural empty/sequential/rejection cases, structural block-application final-state projection, and the TransitionKernel adapter report/projection boundary. Under cfg(kani), txids use a deterministic bounded structural model and UTXO sets use a fixed-capacity finite map. The runtime path exposes a domain-separated, self-delimiting txid_preimage, computes compute_txid as SHA-256 of that transcript, exposes apply_block_transitions_structural/validate_and_apply_block_structural for PO-5 structural refinement, exposes transition_core::TransitionKernel as the thin adapter boundary for future verified/extracted transition cores, exposes full apply_block_transitions/validate_and_apply_block for operational consensus validation with PQ witness checks, and exposes deterministic UTXO snapshots through an explicit UtxoStore extensional contract.
scripts/verification/verify_txid_refinement.sh validates the optimized txid preimage binary against the Coq-extracted txid transcript summary. scripts/verification/verify_runtime_refinement.sh validates the optimized release binary against independent references for txid preimage/SHA-256 wiring and runtime UtxoSet insert/get/remove/delta_tx behavior. The compiled-refinement scripts are run after scripts/verification/build_extraction.sh: scripts/verification/verify_compiled_refinement.sh validates optimized release binaries against the generated Coq-extracted PO-8 summaries, scripts/verification/verify_sighash_refinement.sh validates the optimized Rust sighash transcript generator against the Coq-extracted PO-4 transcript summary, scripts/verification/verify_txid_refinement.sh validates the optimized Rust txid preimage generator against the Coq-extracted txid summary, and scripts/verification/verify_transition_refinement.sh validates the optimized Rust structural UTXO transition/final-state refinement generator against the Coq-extracted PO-5 transition/final-state summary.
scripts/verification/verify_transition_kernel_refinement.sh validates the optimized DeployedTransitionKernel report generator against the Coq-extracted CoqExtractedTransitionKernel oracle's per-case structured witnesses. scripts/verification/compare_transition_kernel_refinement.py emits semantic diffs by case name and report/final-state field on mismatch. scripts/verification/verify_transition_invariant_refinement.sh validates the optimized PO-6 invariant witness generator against Coq-extracted UTXO-domain preservation, total-value non-increase, legacy-output non-increase after announcement, and freeze-policy/frozen-count non-increase after cutover witnesses, including explicit fresh-id/collision-boundary non-applicability cases. scripts/verification/verify_pq_profile_refinement.sh validates the optimized PQ profile generator against the Coq-extracted profile/activation summary. The release scripts emit certificates with toolchain, source, lockfile, binary, and generated-output hashes. This is translation validation and runtime refinement evidence, not a proof of rustc, LLVM, SHA-256 primitive correctness, FIPS 204/FIPS 205 primitive security, PQ witness cryptographic verification, or store backend internals.
cd formal/coq
# Compile all core modules
make
# Build bounded PO-8 extraction artifacts and compare with Rust
cd ../..
./scripts/verification/build_extraction.sh
# Validate compiled release examples against Coq-extracted refinement summaries
./scripts/verification/verify_compiled_refinement.sh
# Validate compiled sighash transcript construction against Coq extraction
./scripts/verification/verify_sighash_refinement.sh
# Validate compiled txid preimage construction against Coq extraction
./scripts/verification/verify_txid_refinement.sh
# Validate compiled UTXO transition behavior against Coq extraction
./scripts/verification/verify_transition_refinement.sh
# Validate compiled TransitionKernel report behavior against Coq extraction
./scripts/verification/verify_transition_kernel_refinement.sh
# Validate compiled PO-6 UTXO-domain/value/migration/freeze invariant witnesses against Coq extraction
./scripts/verification/verify_transition_invariant_refinement.sh
# Validate compiled txid and runtime UTXO-store behavior against deterministic references
./scripts/verification/verify_runtime_refinement.sh
# Validate compiled PQ suite profile behavior against Coq extraction
./scripts/verification/verify_pq_profile_refinement.sh
# Clean build artifacts
cd formal/coq
make cleanRequires Coq 8.18+ or Rocq 9.x. The imports use From Coq Require Import which is compatible with both. PQProfile.v proves the tracked FIPS 204/FIPS 205 suite profile invariants: ML-DSA-44 serializes to a 3738-byte single-signature witness, SLH-DSA-128s serializes to a 7892-byte fallback-profile witness, both fit the 16000-byte cap, the primary and fallback schemes use distinct assumption families, and only ML-DSA-44 is consensus-enabled while SLH-DSA-128s lacks a deployed verifier. scripts/verification/build_extraction.sh now also compares the Coq-extracted PQ profile/activation summary against Rust's pq_profile.rs summary. VarintConcrete.v proves the compact-size varint axioms for the modeled range 0..=65535, proves concrete witness canonicality/injectivity for the bounded parser/serializer, proves that the protocol witness cap MAX_WITNESS_SIZE = 16000 remains inside that range, proves that the consensus-domain parser equals the byte-level parser below the cap and rejects above it, and prints representative Compute values. SighashV2.v proves the modeled Sighash v2 commitment property under the SHA-256 collision-resistance axiom and exposes sighash_preimage_from_hashes, which separates deterministic transcript assembly from the cryptographic hash assumption for extraction. TxidPreimage.v mechanizes the domain-separated txid transcript and proves injectivity over the committed TxidShape projection: version, input outpoints, outputs, and locktime. UTXOTransitions.v proves PO-5/PO-7 model properties, exposes structural valid_tx, valid_block, migration/freeze, delta_tx, block-application final-state transformers, domain/value/migration/freeze invariant observers, and cost functions for extraction, proves that optional final-state block application is equivalent to the boolean block validator, proves apply_valid_block_structural_preserves_domain_nodup, proves apply_valid_block_structural_preserves_total_value, proves apply_valid_block_structural_legacy_count_nonincreasing_after_announcement, proves apply_valid_block_structural_inputs_pq_after_cutover, and proves apply_valid_block_structural_frozen_count_nonincreasing_after_cutover. scripts/verification/build_extraction.sh generates seven bounded witness vectors from the Coq-extracted serializer and compares them byte-for-byte against the Rust generator; it exhaustively compares Coq-extracted varint encode/decode behavior against Rust over every modeled value 0..=65535 plus canonical rejection cases; it compares extracted witness serialize/parse/consensus-domain parse/canonicality behavior plus parser decision traces against Rust over a deterministic boundary/rejection matrix and 111,111 symbolic bounded witnesses; it compares the Coq-extracted sighash preimage transcript summary against Rust's deployed transcript construction; it compares Coq-extracted txid preimage summaries against Rust's deployed txid_preimage; it compares the Coq-extracted UTXO transition/final-state summary against Rust's deployed structural transition entrypoints, migration, freeze, block-application, and cost functions over deterministic structural edge-case matrices; it compares CoqExtractedTransitionKernel structural transaction/block reports against Rust DeployedTransitionKernel reports as per-case JSON witnesses over the same projection boundary; and it compares Coq-extracted PO-6 UTXO-domain/value/migration/freeze invariant witnesses against Rust structural final-state invariant observations, including explicit rejected-block and fresh-id boundary cases. scripts/verification/verify_source_refinement.sh then verifies five Kani harnesses over the Rust source-level witness parser plus twenty-one bounded PO-5 transition harnesses over valid_tx_structural, delta_tx, valid_block_structural, structural block application, and the TransitionKernel adapter boundary. scripts/verification/verify_compiled_refinement.sh builds the release PO-8 refinement executables and validates their generated outputs against the same Coq-extracted summaries. scripts/verification/verify_sighash_refinement.sh separately builds the release sighash refinement executable and validates its output against the Coq-extracted transcript summary. scripts/verification/verify_txid_refinement.sh builds the release txid refinement executable and validates its output against the Coq-extracted txid summary. scripts/verification/verify_transition_refinement.sh builds the release structural transition refinement executable and validates its output against the Coq-extracted transition/final-state summary. scripts/verification/verify_transition_kernel_refinement.sh builds the release TransitionKernel report executable and validates its per-case output against the Coq-extracted transition-kernel oracle witnesses, with semantic diffs produced by scripts/verification/compare_transition_kernel_refinement.py on mismatch. scripts/verification/verify_transition_invariant_refinement.sh builds the release PO-6 invariant witness executable and validates its per-case output against the Coq-extracted invariant witness JSON, with semantic diffs produced by scripts/verification/compare_transition_invariant_refinement.py on mismatch. scripts/verification/verify_runtime_refinement.sh validates the release txid/runtime-store refinement executable against independent deterministic references and emits a txid/store certificate. scripts/verification/verify_pq_profile_refinement.sh validates the release PQ profile executable against the Coq-extracted profile summary and emits a dedicated certificate. Rust separately implements and tests the 0xFE and 0xFF CompactSize ranges; those ranges are outside the current Coq proof boundary for general-purpose CompactSize, and are rejected by the executable consensus-domain witness parser while the witness cap remains below 65535.
cd formal/tla
# Download TLC if not present
curl -sL -o tla2tools.jar \
"https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar"
# Check structural invariants — single-input model (should PASS)
make check
# Result: 492 states, 260 distinct, zero violations
# Check structural invariants — multi-input model (should PASS)
make check-multi
# Result: 58,237 states, 6,365 distinct, zero violations
# Check migration dilemma — single-input (should FAIL with counterexample)
make check-migration
# Check freeze enforcement — multi-input (should FAIL with counterexample)
make check-multi-freeze
# Run all passing checks
make check-allcd paper
make # or: pdflatex main.tex && bibtex main && pdflatex main.tex && pdflatex main.tex
make cleanThe table groups security-relevant test intent. cargo test -- --list is the
authoritative source for the exact current test-case count.
| Category | Count | Description |
|---|---|---|
| Encoding unit tests | 75 | Varint, witness serialize/parse, consensus-domain guard, multisig encoding |
| Spend predicate tests | 18 | SpendPred_PQ single-sig + multisig with real ML-DSA-44 plus reserved-profile rejection |
| PQ suite profile tests | 7 | FIPS 204/FIPS 205 profile metadata, witness sizes, cap fit, activation guard, assumption-family diversity |
| Sighash tests | 27 | Tagged hashes, transcript layout, field coverage, domain separation |
| Migration tests | 24 | Phase transitions, boundary conditions, freeze |
| Freeze tests | 13 | Frozen-output detection and mixed-input rejection |
| Weight tests | 25 | Cost function, block invariant, budget exclusion |
| Validation tests | 26 | ValidTx, structural/full transition boundary, DeltaTx, ValidBlock, block application, txid preimage |
| Transition kernel adapter tests | 5 | TransitionKernel reports, block projection, pure-copy delta adapter |
| Property-based tests | 34 | Core protocol, PO-4, PO-8, migration, cost, and parser properties |
| PO-8 correspondence | 25 named tests + extraction matrix | Varint axioms, parse injectivity, consensus-domain guard, trace alignment, bounded golden vectors |
| Source-level refinement | 26 | 5 Kani symbolic bounded harnesses over Rust witness parser/layout/canonicality + 21 bounded PO-5 transition harnesses over valid_tx_structural, delta_tx, valid_block_structural, structural block application, and TransitionKernel adapter projection |
| Compiled-artifact refinement | 7 | Release-binary validation against Coq-extracted PO-8, PO-4 transcript, PO-5 txid, transition, TransitionKernel per-case report witnesses, PO-6 UTXO-domain/value/migration/freeze invariant witnesses, plus runtime txid/store references |
| Consensus parameter guards | 1 | MAX_WITNESS_SIZE <= u16::MAX formal-domain guard |
| Adversarial boundary | 4 | Cross-input replay, cross-tx replay, commitment binding, block-budget exclusion |
| Integration tests | 4 | Full migration, mixed blocks, multisig, activation |
@article{giovani2026bitcoin,
author = {Mayckon Giovani},
title = {Toward Protocol-Level Quantum Safety in Bitcoin:
A Formal, Adversarial, and Invariant-Driven Treatment},
year = {2026},
note = {Preprint, with Coq-mechanized proofs and TLA+ model checking}
}Mayckon Giovani
MIT License. See LICENSE for details.