From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Wed, 01 Jul 2026 14:24:10 -0700 Received: from mail-oo1-f58.google.com ([209.85.161.58]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wf2Pg-0007hD-Qm for bitcoindev@gnusha.org; Wed, 01 Jul 2026 14:24:10 -0700 Received: by mail-oo1-f58.google.com with SMTP id 006d021491bc7-6a0e3320c53sf1269831eaf.0 for ; Wed, 01 Jul 2026 14:24:08 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1782941038; cv=pass; d=google.com; s=arc-20260327; b=qmM/wTAcI8+sfy78REv1LsKVb7Ol3VCFaqjq/tNjixAulw+ad/ae/0BYHN7Xs//QsO Lx0sKyqmu/WVZENrTSjYDzIWI1zZz1dU+LuYaiCWdwdNNzwO1OZ3J5DRWeAzsVa2wmgU avUsV4BPwozkhKx6yUgfdMljrw5mSIeDYoLSaRMXpFKTcJLiVdOugUCpZLigLLrCjM+E AbeLZ4qKz0NJd3936+f3RE9CDMP8N6qJ/2tD8WOn+/paw4S7LmTeHZGrKyZ61ilo+bX8 v0sfOZSk4nduuSwIknBs1Ki9yHJCKPZPOr5H6112cwrOg9IQy/xMs8nR/hz/HsKxZ7xv OTcg== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=RSY2OcPmze6InnaJcCHVkZZj6aoaBBujEn+LfKLNeAM=; fh=tU/2zsko9FJuw5fUM8PrHbVC05vhryfHDzwDOkiq63c=; b=DAtelZs0pYcjpQwiRq6AZ6IuNVosSuIuJrxaCPqYeSiwJNpjhkW3faLK4mDO7S8FSa 11abG9B98T3ln2eS/wTZMPPQggbccfysR2mUNQhcmszZw48blgJ4fMPeyhiSgo4wDzpk K0WgiRsQMQJdHIvLOlsLZLnrROPKc6rf6G8FZ8bMZMQobi3LPLyFYl2JpqvU3Z7juz3S 1UFY1OX0eXft2ID5clfTMBsdIVTe/HPpb1dgn1KwgKqyLJT8b5D5BmakekSZPeWkwGJ0 OpDi/MRFN6BxoNwHuGnh2IYOz+GQ+JyB3fd9jZlYE0qaG+Vwi9WJz1FTP/OGNH19yM4R t1Kw==; darn=gnusha.org ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=PE20WnPZ; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::f2c as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1782941038; x=1783545838; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=RSY2OcPmze6InnaJcCHVkZZj6aoaBBujEn+LfKLNeAM=; b=btruTjRrb8jpLbC1HW6plIjD3PTSgafHg7tu2GOTCNkc+EchuYpf86477NGdmwomza qhc5hUtYkNEj78BSNKQD5elrTlV2syJ8cTB8FccDGWiQqaYtZk/wrfW1TMCa8ZzPcbL2 CVa3WLGSzxibDUspxlWoXrnEznEIh31jAqCxy8FMw0Bw++KZxb1TfDISuzHYh5zTJ523 k/Zc2XxIHAmPUth01CtANk1fpjDDWuWuhhPuI/n2E/UJchGT5G2frk77jvEAJYJUDp0y UB3NWUjpeaGPvd7qrBnttnwEp4JXylvvx+4+A5P+ZBtdW0lZNLAgjoYfBndYTAnuMCdY ULNw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20251104; t=1782941038; x=1783545838; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=RSY2OcPmze6InnaJcCHVkZZj6aoaBBujEn+LfKLNeAM=; b=WkwmAJ11oxO0vHjeDG5oINbRn0pPEw2owVj37Vk/7SXBDlK8pSmKGsySb3PLA1Zci7 3+nfddWCIci4M5x052J+EvUGL+kmidepC1hG5V9U145E2YNHWnv6AyttEUsTAqBXP73f V/K/QA8bTDyLtts7Z2ErFrxqr7hYf9ew62dzyQk0w2e+G7ttteYiuxntLgssfHdgYphv KFqrDdF9T6UlJhCRxUYEms62QdQOzXXtQuTQ0o3ybI+x7eAvkjAhKT60m0bPk5tH43Gm 9xfOBywUPrqtqUjmfzOG+Kih0qHsbcwG7i049HdAeg8rEwo1bwkfNR/DiEkXoXLnfBtj hHog== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1782941038; x=1783545838; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :x-gm-gg:x-beenthere:x-gm-message-state:sender:from:to:cc:subject :date:message-id:reply-to; bh=RSY2OcPmze6InnaJcCHVkZZj6aoaBBujEn+LfKLNeAM=; b=jH584i53MUvrBQ8Nl4xFIDhiVL6Vyk+m85JsfBJ7Vt4tDAk1kjijq+hKD7BUWvtA0H NchpxRH5/KM/TOWRwOJ5WNaVsxp+1N/qaZiyAE/KChFHDcGiFuKejuDp7dQt/1/bSiw/ SAGU7lC2s1iATN8pR4t0UH0roywer4leESvbg7brbH7jwDZ5eBuwnpVHJQWs0UmWNXDt IzwZUZZKuAyh4s0qePhcT9/bn44ziPFGfmkBpqAxhlJ+Sa4FtP/1dOgs087rW2alVsug mWNh7vH7fAHmozQCY6VdLQ54yJ7xH33DfkmiGgX5BFW1nnWKlQPcAf7RrF2QuyvV5aoy tzkQ== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=3; AFNElJ/gGHxPRJa+x+MoKHrNzJY6nRWe8fOPiY7WgesKGX/MjiNO7pHkSyPx6frRrAYft4V/OJO+OBoWs0xO@gnusha.org X-Gm-Message-State: AOJu0YzOGLfPXeGWClK840VfMQo6pCLQy2ERgp8D5Tcf4NtT1shDtPW3 VhNIKMFTQyM3W5IOJzjLZwL03AFjbsWazIO+zWri5kLUBWCqUn4zeOAk X-Received: by 2002:a05:6820:1748:b0:6a1:13ac:2ac9 with SMTP id 006d021491bc7-6a309a11fa6mr2053747eaf.21.1782941038334; Wed, 01 Jul 2026 14:23:58 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AX0PUUdjJm1BEItCA74/MiUlOa5KhYiMRjGTyIhfPHFrHLJEBQ==" Received: by 2002:a4a:e902:0:b0:6a0:dfb6:7175 with SMTP id 006d021491bc7-6a1b5e9a9a1ls1233880eaf.2.-pod-prod-01-us; Wed, 01 Jul 2026 14:23:52 -0700 (PDT) X-Received: by 2002:a05:6808:1995:b0:496:6b1:cc77 with SMTP id 5614622812f47-4960efa735emr2526158b6e.32.1782941032106; Wed, 01 Jul 2026 14:23:52 -0700 (PDT) Received: by 2002:a05:6808:889c:b0:495:e116:a399 with SMTP id 5614622812f47-495e116a489msb6e; Wed, 1 Jul 2026 14:07:18 -0700 (PDT) X-Received: by 2002:a05:6a20:9185:b0:3bf:9e25:1a0f with SMTP id adf61e73a8af0-3bfed0f5b68mr3496160637.11.1782940037989; Wed, 01 Jul 2026 14:07:17 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1782940037; cv=pass; d=google.com; s=arc-20260327; b=Tj5tUhF1UhGOyH3Zd9Lg/0fvfhsxHGfbW24+RTgSUeoXEYqOVGtlANJwdarnw3lupq Kbyw68ya4sd93wWAASR4cc2uM+2YdpKQnCc7az/k1OWwuHxi/T30mrUU4tMjpyLLHb08 5BnGF3gqyYTVBx1DgbUAUUhBwCRHxIWTXXiK26oa1nmhmVQJrsU82CD0zuMc9+dN9D5d XlHzYfqaPDvwss80sEU836rwKZggSgAK730gMyZupWHc0YxjZXwojBWaC58CO+wEMezP +z+iPjrDChtq28gokQ7x4ec8toqsC7uqULz9+PZ81nIOqW8X0Jhw0IFSSj0fJ74yLLeD trKw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=WpblWPM5kdUjw5WxfXL6WytPvfemvpvPknR82crhcLU=; fh=DMP0F9ULS1guKiqimntQRCN8ZraraesEgQuVcn7F0Z0=; b=IgFhsC93kuaHnBKXQ+3zLkJxsiy1A+XJLMiEDOtZa5MlmpTsDXmYGRIRyry4rrsrF7 LYwtkYLcxrpeePAJhdF/2ZjOd+yFa6Xi5DigU/8I/gNCN3n7E0TGyZVd8y6QF5E6Au7H OwonK4ExJks1/OlowZ1zyS0JYDudlRyCnTAGmWf4QBVHhFDZP/CMtG/Nvob/AITM2Jgp 91iySBK2APYlOStZRxgclqkABL3rJ96ZXhksC32+r9C30Uz35vf6Gh2hWY6iFGbr0OwI 0D1j/FfolJl3L61cJTstmg54z5IAidDSVs2bY/wQuJeRJZcM6voHkkoY6qlWgz8w3nFR io+Q==; dara=google.com ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=PE20WnPZ; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::f2c as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Received: from mail-qv1-xf2c.google.com (mail-qv1-xf2c.google.com. [2607:f8b0:4864:20::f2c]) by gmr-mx.google.com with ESMTPS id 41be03b00d2f7-c9e8ba40818si29236a12.0.2026.07.01.14.07.17 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 01 Jul 2026 14:07:17 -0700 (PDT) Received-SPF: pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::f2c as permitted sender) client-ip=2607:f8b0:4864:20::f2c; Received: by mail-qv1-xf2c.google.com with SMTP id 6a1803df08f44-8eabb1a9378so8332096d6.1 for ; Wed, 01 Jul 2026 14:07:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1782940037; cv=none; d=google.com; s=arc-20260327; b=pyeQ6AfRQZa1kfa3nmUPHqpVCmv5hf5j2eEpsjuV2R/DiyLw+HHv9QyeSNMgFSS5ZY g2AgaEqNnh5m0GkPuHT9wXaqJ6V7i1IRig1QWz2APx1EfxSVAr92r1AInPbBq2ikuWPT N+Wf802O/Wng+05I2nUYzkwZJD9LxPXNtx//q7q2fsW5jL2sQ8+UdZKB9OF0GTyyl5sU xsH0LjuJ0Xm+dRqZdBHTtAt68Sr8efIf0kGHIpGKgnce1VE8e4t22+N1lzm5RzesRiRn VLW2r7OVtdbXfnTKePSprzG5MpUfNJ0kcqo2L62iNETT8ULqeGR+AxH5UN58dWc/uB9F HTPg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20260327; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=WpblWPM5kdUjw5WxfXL6WytPvfemvpvPknR82crhcLU=; fh=DMP0F9ULS1guKiqimntQRCN8ZraraesEgQuVcn7F0Z0=; b=J8tRV849gthRIeiY1zZj5zoUVYY1ft6IcqVQci8UnAC2e9i1Mnkk2IwFQxIIUTF1Ap qRnqNsFWONHmJbKKAJbSZQmtXZEluOOt2Y7iCeTmquf84K/o0zuiAAfincP/L7BqlqEc ymyYGMLtSOhASYh86CPL/EaJkf86eGNH5h9upVyWIbQjAIu9EXZI3FYjycSJegkmZ7jX nmvgJCAe6fC6IC7F6paeZbUHFryHQhBgnPsFs2wjyzEfXn3Ae/upoT/CYBbUSv2UmYlT GfLHa1oR+Cjj/2rC4xOhOVkfqjAxcqWveFWbCb62VfcmwWZUAiZo91n1b6AEUvWE0P83 T4gA==; dara=google.com ARC-Authentication-Results: i=1; mx.google.com; arc=none X-Gm-Gg: AfdE7cmpMD4xOnKfDe9LQkc8Ca+ixMzwaWyzELH7PIz+99Q/KbscJJqYK+SGZWeSBTb 9J8+xS8CdR+WUsa4yWsoJTYPEhmRRaEkjpvXnHdesdWg/VfRbEoL+B2OmCAS0TPLzRCQ04x4aCp nvYbq7sXZgJyCQeADPFZJX1KcrRchqLPOQ84QDhk5bu5ESYLUN7aid2gWF0V+08mBiEv80ZlwdK P8YUM5rydra/DnlzP+gKX+pcsG4kGFlw5dRRifqJBUmFGeAnavgBYPr7c00lzRejmFvmaBtcaP6 H4C1ybaqweMNbP5ztuRjBlKFjSDqeqrN6vxSx3jhxU23XdrxoTHBNWYu+3E= X-Received: by 2002:a05:6214:202e:b0:8dc:e5b9:1f72 with SMTP id 6a1803df08f44-8f3c90f29c8mr50794826d6.33.1782940036817; Wed, 01 Jul 2026 14:07:16 -0700 (PDT) MIME-Version: 1.0 From: Keagan McClelland Date: Wed, 1 Jul 2026 15:07:05 -0600 X-Gm-Features: AVVi8CfQ4lxOZGPSFvoewbVJ4Co8pe8kO4hTTaZGSmo_bSxuc_c69lRLrGJfWc8 Message-ID: Subject: [bitcoindev] btc-verified: formalizing the Bitcoin protocol To: Bitcoin Development Mailing List Content-Type: multipart/alternative; boundary="0000000000008ce69b06559313f0" X-Original-Sender: keagan.mcclelland@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20251104 header.b=PE20WnPZ; arc=pass (i=1); spf=pass (google.com: domain of keagan.mcclelland@gmail.com designates 2607:f8b0:4864:20::f2c as permitted sender) smtp.mailfrom=keagan.mcclelland@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com; dara=pass header.i=@googlegroups.com Precedence: list Mailing-list: list bitcoindev@googlegroups.com; contact bitcoindev+owners@googlegroups.com List-ID: X-Google-Group-Id: 786775582512 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , X-Spam-Score: -0.5 (/) --0000000000008ce69b06559313f0 Content-Type: text/plain; charset="UTF-8" Esteemed colleagues, Today I'd like to share something I've been working on for the last month or so. I have been attempting to define the Bitcoin protocol in Lean4 and have gotten to a point where I can point to an interesting result in an attempt to demonstrate the type of value that something like this can provide. If you wish to jump immediately to the repository, you can find it here: https://github.com/ProofOfKeags/btc-verified # Background For the uninitiated, Formal Verification is a practice in software development that gives greater assurances than typical testing procedures or forum arguments on how various schemes, protocols, and implementations behave. When we argue about how Bitcoin is designed or how it ought to be designed, engineers will make statements of fact about how the system works, but depending on how much effort is put into the presentation of that argument, it can be difficult to tell if a statement is true, or if it is, why it is true. By formally specifying these statements of fact on how the Bitcoin protocol works we can be precise about what we are saying, what properties we have, what properties we want, and whether the system actually delivers those properties or not. Normal programming languages do this to an extent, and indeed one of the best ways to settle a dispute is to look at how the code is implemented. However, the nature of C++ can make it difficult to get certainty over certain claims about the behavior of the protocol due to its type system being comparatively weak when judged against the tools typically tasked with this responsibility. If you want to be able to make specific arbitrary logical statements about Bitcoin or any other software you typically need to specify it in a language with a Dependent Type Theory. The class of tools used for this is called an Interactive Theorem Prover (ITP). There are many, but the one I chose for this project is Lean4 due to its recent momentum and its corpus of mathematical facts defined in the open source "mathlib" which ends up being a useful piece of infrastructure to rely on when you start wanting to ask deeper questions about the protocol and don't want to have to rederive all mathematical knowledge from scratch. # Goals Like most open source work this is to scratch a personal itch of mine, but I do think that it has the ability to help settle disputes of fact (as opposed to disputes of value) when we have design discussions suggesting changes to how the system works. Consider bip340 (schnorr). In that BIP it makes the claims that Schnorr signatures are "provably secure ", "non-malleable ", and "linear ". In that BIP it has good citations about the evidence for the claim of "provably secure" and prose definitions of what those claims are trying to say, but what's cool is that these are all statements that have precise mathematical formulations that can be written down, verified, and later reused in other arguments that rest on those assumptions. At it's best, this project would be able to help document the set of interlocking behaviors in the protocol that allow us to sleep easy about how it works, know where the holes are (yes there are some), and waste less energy arguing about what *is*, and save all of our arguments for what *ought*. # Initial Result Like software, this process of formal verification requires building the protocol up from scratch, and so most of the value still lies in the future, but an interesting first result I stumbled on is related to the Merkle Tree and Root construction inside of Bitcoin blocks. One of the important properties we rely on in Bitcoin is that a Merkle Root *uniquely* identifies the Merkle Tree from which it is derived. This property is usually stated as "non-malleability" and to some may be more easily understood as "injectivity" of the inverse relation. However you wish to name it, we rely on the idea that for an arbitrary Merkle Root, I should only be able to show you a single Merkle Tree that has that root that would be accepted by the Bitcoin network. Bitcoin Core does this check via the (poorly named) "mutation check" in ComputeMerkleRoot . This computation that Bitcoin Core has a primary design goal of being efficient to compute, as indeed these types of computations can be expensive during IBD and being smart about how to compute them has a real impact on users running the software in normal operations. However, it is not obvious from the C++ code why this check is there or why it's important. The prose description at the top of the file does a decent job of trying to close that gap but still leaves a lot to be desired in terms of understanding how the check fixes the flaw mentioned. btc-verified instead specifies a notion of Canonicality , a check that determines whether a tree is defined in its "most reduced form", and a simple algorithm for computing the merkle root. Then it specifies the more memory efficient algorithm used by Core and proves the equivalence of those algorithms for all possible merkle trees. With this equivalence in hand, we can then show that the structure of this computation combined with a canonicality assumption built from Core's "mutation check" implies that a merkle root identifies a merkle tree or we have a sha256 collision . This type of result allows us to think about Bitcoin's properties compositionally in a way that stays faithful to the implementation itself. # Limitations Before any of you get out your pitchforks, let me discuss a bit about what this project does not claim, because claiming certainty where it doesn't exist is what inevitably gets us in trouble. For obvious reasons this implementation, at any time, can diverge from how Bitcoin Core works and as such should not be used as a final arbiter of how the Bitcoin protocol works. However, it does have the ability to tell us what properties are provably true under the model of implementation specified in btc-verified. Additionally, like in the example above, we can specify Bitcoin Core's actual semantics (along with alternative implementations such as btcd ) and prove equivalence to a less computationally efficient but correct-by-construction representation of the same ideas that is more suitable for this type of reasoning. *This repository is structurally incapable of giving guarantees about Bitcoin Core's behavior.* There is a camp of people that says that the Bitcoin Core codebase IS the spec. I have always hated that this is true, but in 2026 it is an accurate statement and safe bet for anyone writing production systems. That said, Bitcoin Core's code is generally not useful as a specification as the requirements are very often obscured by optimization decisions. As such there is still utility in this type of a project where we can map out the architecture of the protocol's soundness more cleanly. # Disclaimers 1. This is a brand new project and should be treated as a curious "science project" with all of the positive and negative connotations associated with that term. 2. I am NOT a seasoned professional at formal verification. I have had a pet-interest in this level of rigor in reasoning about the correctness of systems, but the tools and techniques are new to me. Those who have worked with me before know that I have been circling these ideas for the better part of a decade, but I am still just a software engineer with math envy and a reading habit. 3. 100% of the code in this repository is authored by AI. However, I have personally laid eyes on every line of code in this repository and have interactively guided decisions at every step along the way. 4. The proof bodies themselves, while they pass the lean kernel, leave a lot to be desired in terms of their legibility. Whether I put work into making the proofs themselves easier to digest will depend on whether there is appetite for being able to read them as opposed to just knowing that the statements are provable and have been verified by the Lean4 kernel. 5. This project doesn't offer much in terms of normative claims about how the Bitcoin protocol SHOULD work and what tradeoffs are desirable, however, I think it has the potential to offer a lot in terms of settling disputes about descriptive claims on how either the current protocol works, how a hypothetical change to the protocol would affect invariants we've come to rely on, or which parts of various implementations are load bearing or not. # One More Thing I think the most exciting aspect of this type of work is that since Lean4 is capable of generating working C code, at a sufficient level of maturity, it can make things like libbitcoinkernel a formally verified piece of common infrastructure that also discharge skepticism about cross-implementation compatibility. # CTA If you have thoughts or opinions on the repo or the line of inquiry I'd love to hear your feedback. Keags -- You received this message because you are subscribed to the Google Groups "Bitcoin Development Mailing List" group. To unsubscribe from this group and stop receiving emails from it, send an email to bitcoindev+unsubscribe@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/CALeFGL2G3O7Mb2gk6vLT_cb3MBwU%3Dupt0RLRisyPGCXDN4foYg%40mail.gmail.com. --0000000000008ce69b06559313f0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Esteemed colleagues,

Today I'd = like to share something I've been working on for the last month or so. = I have been attempting to define the Bitcoin protocol in Lean4 and have got= ten to a point where I can point to an interesting result in an attempt to = demonstrate the type of value that something like this can provide. If you = wish to jump immediately to the repository, you can find it here:

https://github.com/P= roofOfKeags/btc-verified

# Background

For the uninitiated, Formal Verification is a practice in = software development that gives greater assurances than typical testing pro= cedures or forum arguments on how various schemes, protocols, and implement= ations behave. When we argue about how Bitcoin is designed or how it ought = to be designed, engineers will make statements of fact about how the system= works, but depending on how much effort is put into the presentation of th= at argument, it can be difficult to tell if a statement is true, or if it i= s, why it is true. By formally specifying these statements of fact on how t= he Bitcoin protocol works we can be precise about what we are saying, what = properties we have, what properties we want, and whether the system actuall= y delivers those properties or not.

Normal program= ming languages do this to an extent, and indeed one of the best ways to set= tle a dispute is to look at how the code is implemented. However, the natur= e of C++ can make it difficult to get certainty over certain claims about t= he behavior of the protocol due to its type system being comparatively weak= when judged against the tools typically tasked with this responsibility.

If you want to be able to make specific arbitrary l= ogical statements about Bitcoin or any other software you typically need to= specify it in a language with a Dependent Type Theory. The class of tools = used for this is called an Interactive Theorem Prover (ITP). There are many= , but the one I chose for this project is Lean4 due to its recent momentum = and its corpus of mathematical facts defined in the open source "mathl= ib" which ends up being a useful piece of infrastructure to rely on wh= en you start wanting to ask deeper questions about the protocol and don'= ;t want to have to rederive all mathematical knowledge from scratch.
<= div>
# Goals

Like most open source w= ork this is to scratch a personal itch of mine, but I do think that it has = the ability to help settle disputes of fact (as opposed to disputes of valu= e) when we have design discussions suggesting changes to how the system wor= ks.

Consider bip340 (schnorr). In that BIP it makes the claims that Schno= rr signatures are "pro= vably secure", "non-malleable", and "linear". In that BIP it has good citations about the ev= idence for the claim of "provably secure" and prose definitions o= f what those claims are trying to say, but what's cool is that these ar= e all statements that have precise mathematical formulations that can be wr= itten down, verified, and later reused in other arguments that rest on thos= e assumptions. At it's best, this project would be able to help documen= t the set of interlocking behaviors in the protocol that allow us to sleep = easy about how it works, know where the holes are (yes there are some), and= waste less energy arguing about what *is*, and save all of our arguments f= or what *ought*.

# Initial Result

Like software, this process of formal verification requires buildi= ng the protocol up from scratch, and so most of the value still lies in the= future, but an interesting first result I stumbled on is related to the Me= rkle Tree and Root construction inside of Bitcoin blocks.

One of the important properties we rely on in Bitcoin is that a Mer= kle Root *uniquely* identifies the Merkle Tree from which it is derived. Th= is property is usually stated as "non-malleability" and to some m= ay be more easily understood as "injectivity" of the inverse rela= tion. However you wish to name it, we rely on the idea that for an arbitrar= y Merkle Root, I should only be able to show you a single Merkle Tree that = has that root that would be accepted by the Bitcoin network.

=
Bitcoin Core does this check via the (poorly named) "mutati= on check" in Comput= eMerkleRoot. This computation that Bitcoin Core has a primary design go= al of being efficient to compute, as indeed these types of computations can= be expensive during IBD and being smart about how to compute them has a re= al impact on users running the software in normal operations. However, it i= s not obvious from the C++ code why this check is there or why it's imp= ortant. The prose descrip= tion at the top of the file does a decent job of trying to close that g= ap but still leaves a lot to be desired in terms of understanding how the c= heck fixes the flaw mentioned.

btc-verified instea= d specifies a notion of=C2=A0Canonicality, a check that determines whether a = tree is defined in its "most reduced form", and a simple algorithm fo= r computing the merkle root. Then it specifies the more memory efficien= t algorithm used by Core and proves the equivalence of those algori= thms for all possible merkle trees. With this equivalence in hand, we c= an then show that the structure of this computation combined with a canonicality assum= ption=C2=A0built from Core's "mutation check" imp= lies that a merkle root identifies a merkle tree or we have a sha256 collision.


Before any of you get out your pitchforks, let me discuss a bit= about what this project does not claim, because claiming certainty where i= t doesn't exist is what inevitably gets us in trouble. For obvious reas= ons this implementation, at any time, can diverge from how Bitcoin Core wor= ks and as such should not be used as a final arbiter of how the Bitcoin pro= tocol works. However, it does have the ability to tell us what properties a= re provably true under the model of implementation specified in btc-verifie= d. Additionally, like in the example above, we can specify Bitcoin Core'= ;s=C2=A0actual semantics (along with alternative implementations such as btcd) and prove equivalence = to a less computationally efficient but correct-by-construction representat= ion of the same ideas that is more suitable for this type of reasoning.

This repository is structurally incapable of givin= g guarantees about Bitcoin Core's=C2=A0behavior.
<= b>
There is a camp of people that says that the Bitcoin C= ore codebase IS the spec. I have always hated that this is true, but in 202= 6 it is an accurate statement and safe=C2=A0bet for anyone writing producti= on systems. That said, Bitcoin Core's=C2=A0code is generally not useful= as a specification as the requirements are very often obscured by optimiza= tion decisions. As such there is still utility in this type of a project wh= ere we can map out the architecture of the protocol's soundness more cl= eanly.

# Disclaimers

1. T= his is a brand new project and should be treated as a curious "science= project" with all of the positive and negative connotations associate= d with that term.
2. I am NOT a seasoned professional at formal v= erification. I have had a pet-interest in this level of rigor in reasoning = about the correctness of systems, but the tools and techniques are new to m= e. Those who have worked with me before know that I have been circling thes= e ideas for the better part of a decade, but I am still just a software eng= ineer with math envy and a reading habit.
3. 100% of the code in = this repository is authored by AI. However, I have personally laid eyes on = every line of code in this repository and have interactively guided decisio= ns at every step along the way.
4. The proof bodies themselves, w= hile they pass the lean kernel, leave a lot to be desired in terms of their= legibility. Whether I put work into making the proofs themselves easier to= digest will depend on whether there is appetite for being able to read the= m as opposed to just knowing that the statements are provable and have been= verified by the Lean4 kernel.
5. This project doesn't offer = much in terms of normative claims about how the Bitcoin protocol SHOULD wor= k and what tradeoffs are desirable, however, I think it has the potential t= o offer a lot in terms of settling disputes about descriptive claims on how= either the current protocol works, how a hypothetical change to the protoc= ol would affect invariants we've come to rely on, or which parts of var= ious implementations are load bearing or not.

# On= e More Thing

I think the most exciting aspect of t= his type of work is that since Lean4 is capable of generating working C cod= e, at a sufficient level of maturity, it can make things like libbitcoinkernel=C2=A0a = formally verified piece of common infrastructure that also discharge skepti= cism about cross-implementation compatibility.

# C= TA

If you have thoughts or opinions on the repo or= the line of inquiry I'd love to hear your feedback.

Keags


--
You received this message because you are subscribed to the Google Groups &= quot;Bitcoin Development Mailing List" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to bitcoind= ev+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/= msgid/bitcoindev/CALeFGL2G3O7Mb2gk6vLT_cb3MBwU%3Dupt0RLRisyPGCXDN4foYg%40ma= il.gmail.com.
--0000000000008ce69b06559313f0--