btc-verified: formalizing the Bitcoin protocol

The project, available at btc-verified, leverages the mathematical rigor provided by Lean4 and the comprehensive library of mathematical facts from mathlib. This initiative is particularly focused on addressing and resolving factual disputes within design discussions about Bitcoin, rather than debates centered on the value or ethical considerations of the protocol.

Formal Verification, a method superior to traditional testing and informal debate, offers precise definitions and proofs of how Bitcoin operates, including its properties and expected behaviors. This approach allows for a clear understanding of what statements about Bitcoin's functionality are actually true and why. Using Lean4, which supports Dependent Type Theory, enhances the ability to make specific logical assertions about the software. Such detailed specification is crucial because programming languages like C++ may not provide sufficient certainty over claims about the protocol due to their relatively weaker type systems.

An intriguing initial result from this project pertains to the non-malleability (or injectivity) of the Merkle Root in relation to its tree, a fundamental aspect of Bitcoin's architecture. This property ensures that each Merkle Root corresponds uniquely to a Merkle Tree accepted by the network, critical for the integrity and security of block transactions. The project repository outlines both the theoretical basis for this property and practical implementations that mirror those used by Bitcoin Core, showing that under certain assumptions, these implementations can be proven equivalent.

Despite these advancements, the project acknowledges its limitations, notably that it cannot serve as a definitive guide to Bitcoin Core's behavior. Any divergence between the model used in btc-verified and the actual operations of Bitcoin Core means the formal verifications may not directly translate to real-world scenarios. Additionally, while the project does not make normative assertions about how Bitcoin should function, it does offer insights into the descriptive accuracy of the protocol as it currently stands or under hypothetical modifications.

This work represents a blend of theoretical computer science and practical application, aiming to refine our understanding of Bitcoin's underlying mechanics and potentially streamline future developments and optimizations within its ecosystem. As such, it holds promise for contributing valuable clarity to discussions about Bitcoin’s technical foundations. If interested in further exploring or discussing this endeavor, feedback and engagement with the project are encouraged.