{"repo":"ProofOfKeags/btc-verified","free":true,"listed":false,"github":"https://github.com/ProofOfKeags/btc-verified","clone":"git clone https://github.com/ProofOfKeags/btc-verified.git","description":"Verified Bitcoin protocol components in Lean 4 — serialization, txids, and merkle commitments checked against real mainnet blocks.","language":"Lean","stars":17,"topics":["bitcoin","bitcoin-protocol","formal-methods","formal-verification","lean","lean4","theorem-proving"],"license":"Apache-2.0","category":"blockchain-web3","readme_excerpt":"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 state","default_branch":null,"files":null,"tree":[],"storefront":"/r/ProofOfKeags","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/ProofOfKeags/btc-verified/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}