Btc-verified October Update: Connecting Map to Territory
In briefbtc-verified October Update: Matching a Formal Model to Bitcoin Core's Real Behavior
SummaryThe btc-verified project builds a minimal formal model of Bitcoin consensus in Lean. This post describes using the libbitcoinkernel interface and differential fuzzing, in the style of bitcoinfuzz, to check whether the model matches Bitcoin Core on transaction parsing, serialization, and transaction-local checks. Nine kernel functions are currently backed by the Lean implementation.