In September 2018, Bitcoin Core developers discovered that a software bug could allow a miner to create coins outside Bitcoin’s authorized issuance schedule.
The rule was clear. The software enforcing it had a flaw.
That distinction should matter to everyone who owns bitcoin.
The vulnerability, CVE-2018-17144, involved spending the same transaction input twice. Under certain conditions, affected versions could mishandle that duplication and allow inflation. Developers released a fix. At the time of their public disclosure, they reported being unaware of attempts to exploit it.
The incident exposed a gap between a monetary rule and the software responsible for applying it.
You can agree on the rules and still write code that breaks them.
I keep coming back to that sentence because so much of the conversation about Bitcoin skips over it.
We can debate the next halving, institutional demand, or how many coins will remain available to buy. All of those discussions depend on something more basic: the software checking the ledger must correctly distinguish what is allowed from what is forbidden.
Even when someone deliberately gives it the strangest input they can construct.
The U.S. government spends more on debt interest than on national defense. The era of independent central banking is over—welcome to the age of Fiscal Dominance.
“There will only ever be 21 million bitcoin.”
It is probably Bitcoin’s most effective sentence. Short enough to remember. Powerful enough to change how someone thinks about money.
But the number does not enforce itself.
Independent nodes enforce the rules that constrain issuance. A miner can propose a block claiming an excessive reward; a node correctly applying Bitcoin’s rules rejects it. That rejection is part of what makes the monetary promise credible.
The difficult question is how we establish that the software keeps making the right decision, including in cases its authors never thought to test.
On October 19, 2026, independent Bitcoin engineer Keagan McClelland published an update on ** btc-verified**, his project to formalize Bitcoin protocol components in Lean, a system for machine-checked proofs.
He reported 100,000 differential fuzz executions with no observed disagreement between his implementation and Bitcoin Core for the selected behaviors being compared.
That is useful progress. It is also a limited result: the campaign covered a subset of transaction-related behavior, not the entire consensus system.
The larger ambition is to establish stronger guarantees about the rules Bitcoin actually enforces.
And here the story gets interesting.
Before a mathematical proof can tell us something about Bitcoin, researchers must establish that the thing they have modeled actually behaves like Bitcoin.
A beautifully constructed model can leave out an awkward detail. A proof can be impeccable while the connection to the software remains incomplete.
You can prove your model correct and still be wrong about Bitcoin.
McClelland had already encountered a small example of that problem. His original model made an assumption so reasonable that most readers would probably make it too.
The assumption was wrong for the behavior he was trying to reproduce.
Understanding why gives us a much better way to judge claims about Bitcoin’s security—and a clearer view of the work behind its scarcity.
Below, I’ll unpack that example, explain what the 100,000 tests establish, and give you three questions to ask whenever someone says Bitcoin has been “mathematically proved secure.”
Subscribe for free to continue reading and receive In Bitcoin We Trust in your inbox. This article is free for subscribers.
