LLMs verify Bitcoin’s core math
Summary
- LLMs turn formal verification into a practical shield for Bitcoin’s protocol.
- A database 'seek compaction' bug thrashed disks for months.
- Parallel UTXO fetching triples sync speeds on slow drives.
Large language models are no longer just chatbots - they’re proving Bitcoin’s mathematical foundations. Keegan’s BTC Verified project uses LLMs to automate proofs in Lean 4, transforming formal verification from academic exercise into deployable engineering. The goal: build compounding proof capital, a durable, citable body of Bitcoin’s invariants that survives developer turnover.
LLMs act as 'chainsaws' in this workflow - handling rote logic so humans can focus on high-level design. Lean 4’s rigid checks make it ideal for reinforcement learning, letting models correct errors in real time. This isn’t about replacing developers; it’s about scaling trust. As Keegan notes, it’s the difference between checking 3+5=8 and proving addition for all numbers.
"LLMs are chainsaws for proof engineering - doing the tedious work so humans can focus on the big picture."
- Keegan, Bitcoin Optech
Meanwhile, a performance tweak in Bitcoin Core backfired. Increasing LevelDB file sizes to 32MB and flushing hourly was meant to speed sync and reduce data loss. But Andrew revealed it triggered 'seek compaction' - a feature that rewrote 15GB of data every hour. Random Bitcoin hashes forced disk-wide seeks, turning efficiency gains into thrashing.
The fix? Disable seek compaction. Backported to versions 29, 30, and 31, it underscores a harsh truth: even mature databases behave unpredictably under Bitcoin’s unique IO load. Optimization has costs - and they’re paid in disk cycles.
"We optimized for the wrong thing. The hardware assumptions didn’t hold."
- Andrew, Bitcoin Optech
Now, syncing is getting faster again. Andrew’s parallel UTXO prefetching system deploys a 'clerk' thread to scan inputs and dispatch up to eight 'helpers' to cache data ahead of validation. On high-latency systems, IBD speeds tripled. Even laptops see 35% gains. It turns block validation from stuttering ping-pong into a smooth assembly line.
Source Intelligence
- Deep dive into what was said in the episodes
Bitcoin Optech: Newsletter #414 Recap • Jul 21
- Keegan's BTC Verified project aims to apply formal verification using Lean 4 to the Bitcoin protocol, building a living body of knowledge to crystallize understanding and evaluate changes.
- Keegan notes that while proof assistants like Lean 4 are not designed for efficient execution, they are crucial for high-stakes projects where cost of failure is extremely high, such as the Bitcoin protocol.
- Andrew reports that Bitcoin Core releases 29.4, 30.3, and 31.1 fix a long-standing LevelDB bug that caused excessive disk I/O from repeated chain state compactions.
- The LevelDB bug worsened in Bitcoin Core 29 due to increasing the default file size from 2 MB to 32 MB, leading to 15 GB of read/write I/O per compaction; this was exacerbated in version 30 by hourly chain state flushes.
- The primary cause of the LevelDB issue was the 'seek compaction' feature, which prematurely compacted files after frequent reads, even if they were not full; the fix involved disabling this feature.
- Andrew's PR 35295 significantly speeds up Initial Block Download (IBD) and steady-state block validation by parallelizing UTXO lookups from disk using worker threads, preventing the validation thread from waiting on single reads.
- Bitcoin Core 35209, included in recent maintenance releases, provides a cleaner fix for CVE-2024-52911, addressing a vulnerability that could cause a remote crash by accessing freed memory during specially crafted block validation.
- Andrew's PR 35568 disables bloom filters in the TXO Spender Index, saving disk space and time because the index's iterator-based lookup pattern does not benefit from bloom filters designed for point reads.
- Bitcoin Core PR 34897 prevents index inconsistencies during unclear shutdowns by ensuring indexes like CoinStats never get ahead of the chain state's last durable UTXO flush.
- Bitcoin Core PR 35406 adds a limit of 10,000 transactions to the tracking queue for private broadcast, preventing resource exhaustion if transactions are not relayed due to policy differences or poor connectivity.
- Bitcoin Core PR 35380 extends the LibBitcoin Kernel API to expose transaction inputs, witness stacks, and script sig data, facilitating silent payment scanners in retrieving public keys.
- BIP54, the consensus cleanup proposal, had its rationale section updated to include discussions regarding the D64 byte mitigation and alternative proposals, documenting community review.
- LND PR 10962 fixes an issue where the RBF Cooperative Close Flow could accidentally spend overlay assets during fee bumping by making auxiliary channels incompatible with this flow.
- LND PR 10897 ensures that low-Bitcoin-value UTXOs representing high-value overlay assets are not skipped during fee rate increases, by recognizing them as auxiliary channel outputs and including them in sweeps.
- BIN 20250003 has been assigned to BIP442 (OP_PER_COMMIT) in the Bananas repository, which serves as an alternative for standardizing and publishing documents and activating soft forks on Bitcoin Inquisition's signet.
Also from this episode: (3)
Coding (1)
- Formal verification employs dependent type theory in interactive theorem provers like Lean 4, enabling proofs that software behaves properly for all inputs, unlike property testing which only checks sampled points.
Models (1)
- LLMs significantly reduce the effort required for proof engineering by generating proofs that are mechanically verifiable, allowing human experts to focus on precise specification of correctness.
AI Infrastructure (1)
- Andrew's IBD optimization makes systems at least 50% faster, with network-connected storage like AWS seeing up to three times faster IBD, and typical performance gains around 35% on standard hardware.