DeepMind’s Signal Proofs Turn “Verified” Into a Scope Statement: One-to-One Sessions in a Command-Line Harness, 39 Hooked Routines on Trust, No Proof of Post-Quantum Healing, and a Bound That Goes Vacuous at About 25,000 Messages

On November 10, Google DeepMind published “Introducing AlphaProof Code: a breakthrough in verifying complex software at depth,” a blog post by Pushmeet Kohli and Swarat Chaudhuri, together with a technical paper, “AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level,” by nine authors at Google DeepMind and Google. WIRED ran the story under the headline “A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure,” and SecurityWeek reported that agents built on Gemini 4 Carbon helped formally verify core security guarantees in the code behind the Signal protocol.

I read the paper’s introduction, setup, limitations, trusted-base, bug-test, practice, related-work and discussion sections. I cloned the Lean repository (commit 808b4b7, its only commit, dated November 10), read its two headline theorem files, its paper map and its deviations catalog, and wrote a short standard-library script that recounts the repository. I did not work through the proofs’ derivations or the appendices, and I did not build the Lean development or kernel-check anything; the repository’s README puts a full check at several hours and 15 to 34 GiB of peak RAM.

Here is what I found:

• The headline is wider than the theorem. The proofs cover the one-to-one session code of libsignal-protocol v0.105.4 with spqr v1.6.0, meaning PQXDH session setup and Triple Ratchet messaging, driven through a small command-line harness built for AArch64 Linux. Key generation is not verified. WIRED’s own text says the agents proved “a number of the Signal protocol’s key cryptographic guarantees.”
• Thirty-nine routines are contracts, not proofs. The cryptographic primitives are idealized and the results are conditional on their security; the other contracts, covering a few libc routines, the two output functions and some Rust library routines, are in the paper’s words “not proved against the real routines.”
• Post-quantum healing is not proved. The paper’s discussion says the theorems do not prove the healing that SPQR is designed to provide, and the computational theorem is classical. Neither the blog nor WIRED mentions it.
• The computational bound runs out at modest scale. The paper says its statistical terms make the bound vacuous for single sessions of about 25,000 messages, or for 2²⁰ sessions of 2¹⁰ messages, if nearly every message starts a new epoch.
• The bug test is symbolic only, and an earlier formal analysis had already found both bugs. The blog says the system produced a machine-checked proof that the buggy version was insecure; the paper proves that the symbolic theorem fails for the two reintroduced bugs and says refuting the computational theorem is much harder.
• The public repository cites files it does not contain. At commit 808b4b7, Computational/docs/TRUSTED_BASE.md, which 128 files cite (the computational headline theorem file sends readers there for the trusted definitions), is missing, and so are eight scripts that the paper map and the lakefile name, including scripts/bug_injection.py, the CI axiom guards and the trusted-closure script. A GitHub issue opened that afternoon reports the same gap.
• The verified release is already three releases behind. Between v0.105.4 and v0.106.2, libsignal’s repository took 24 commits, 40 changed files under rust/protocol/ and 12,159 changed lines there.
• The counts mostly reproduce. Outside stubs, tests and the comparator folder, the proof tree has no sorry, axiom or native_decide, and four of five line counts land within 8 percent of the paper’s. The exception is the computational proof, which is 24 percent larger than the paper says.

None of this makes the work small. A proof that follows a compiled AArch64 binary through PQXDH and the Triple Ratchet, checked by Lean’s kernel, with agents writing every line of proof, is a real advance, and the paper’s own tables and limitation sections say most of what is listed above. What does not hold up is how far the headline and the blog sit from those sections, and how much of the artifact’s documentation points to files that were not published. As the paper puts it, “once proofs become cheap, the hard question is what to prove.” That question is a scope question, and the scope is where the security content lives.

What each account claims, and what the paper says

The blog is the most sweeping, WIRED’s headline claims more than its own text does, and SecurityWeek carries the caveats. The table sets six claims against the paper and the artifact.

The paper itself is more careful than the blog about “first.” It says “To our knowledge,” and it carries three qualifiers that do the work: unmodified code, protocol-level properties, and a widely deployed implementation. Lean checks proofs, not statements, a point our read of the two claimed refutations of the Exponential Time Hypothesis made, and the same question of what a contract actually says ran through our look at Microsoft’s PDD Kit and its Verus contract. The same lab’s RSA-1024 results, which we looked at on November 9, also came with qualifiers that the headline numbers left out.

What was verified: one operation per run, in a harness

A command-line build

The paper wraps the unmodified libsignal crates in a small program, libsignal-cli. Each run performs one operation for one party: keygen, init (start a session from a prekey bundle), send or recv. A party’s state is a directory of files, and the theorems speak about whole runs of the compiled executable. They cover init, send and recv; the paper says “keygen is not verified,” and the theorems take the parties’ keys as part of their setup. The code is built with stock rustc 1.98.1 and linked statically with musl into one AArch64 Linux executable, and the paper says “The proofs follow each init, send and recv run from the executable’s entry point to its final exit_group system call.”

The environment plays Signal’s server by copying each party’s public files into a bundle directory, supplies every run’s random coins, and hosts the attacker, which controls the network and receives a party’s directory when it asks to compromise that party. That is a clean model, and it is also why the results are about this harness rather than about the server or the apps.

The scenario each theorem assumes

The two proofs state their scenarios differently, and the paper lists the restrictions in its limitation sections.

• Symbolic theorem, assembly level. Two honest parties with fixed roles and one session per session file. Both start with each other’s identity key pinned, so libsignal’s trust-on-first-use path is not exercised. Bob has one signed prekey, one reusable last-resort Kyber prekey and at most one one-time prekey; one-time Kyber prekeys are not covered. Input sizes and the number of sends are bounded, the coins files must be exactly 192, 64 and 32 bytes for init, send and recv, and a run that aborts, for instance on a failed allocation, ends the trace. Leaks reveal only long-term and prekey secrets and the keys of a party’s current session; “side channels and other secrets in memory are out of scope.”
• Computational theorem. Each promotion starts one session, messages have a fixed length, and there is no multi-device state. Identity keys are trusted on first use. “The most significant restriction is that the adversary cannot inject its own PQXDH initial message to the responder of a session that is later promoted.” The game also refuses corruption until the initiator reaches epoch 10.

What the harness leaves out

The paper’s own list of future work includes “Signal’s group messaging, sealed sender and server-side protocols.” The introduction says “variants of the protocol are deployed in WhatsApp, Meta’s Messenger app, and Google Messages,” and the paper does not say those apps run this code. WIRED’s sentence that the work validates the cryptography on those platforms is therefore a statement about the protocol’s design, not about their implementations. The paper also says some of the environment assumptions “are argued informally.”

What the proofs take on trust

The paper’s selling point is what it removes from the trusted base: “the Rust compiler is not trusted,” because the theorems are about machine code. What remains is the list below, which comes from the paper’s setup and trusted-base sections.

The specifications are repaired restatements

The paper records every place where its Lean statements depart from the reference papers or from libsignal: over 200 entries for the computational side and about 35 for the symbolic side. Most are routine. Some are not: “Some, however, are errors in the published analyses that we had to repair before the proofs could go through.” Fifteen are gaps or bugs in the computational analysis of the Double Ratchet, such as missing hypotheses and game conditions that allow trivial wins. The printed ProVerif queries of Cheval, Jacomme and Richards look up skipped message keys at the wrong ratchet index, “which makes receiver-side forward secrecy false as printed.” In the PQXDH analysis of Bhargavan and colleagues, reading one compromise condition literally makes a corollary unprovable, so the authors bind it to the session’s own signed prekey.

That is a real finding of the project, and it cuts both ways. It shows what formalizing against real code can catch. It also means the theorems are about DeepMind’s repaired versions of the published statements, which a reader must review to trust them. The deviations file in the repository records them; I count 239 distinct DEV- identifiers in it. WIRED calls the work “further independent validation of the cryptography.” Three Signal engineers gave feedback on the specifications, according to the paper’s acknowledgments, and the authors are at Google, which ships the protocol in Google Messages. “Independent” is WIRED’s word.

What the proofs do not cover

These limits are in the paper’s sections 5.1.6 and 5.2.5, its discussion and its Table 1. The only caveat I found in the blog is “Scaling these techniques requires continued research.”

• Post-quantum healing. The paper says its “ratchet theorems let the attacker choose the SPQR keys, so they show that the Triple Ratchet is no weaker than the Double Ratchet, not the post-quantum healing that SPQR adds.” The discussion repeats it: the computational theorem is classical, “so neither proves the post-quantum healing that SPQR is designed to provide.” What the symbolic proof does give is handshake secrecy against a future quantum attacker.
• Quantum attackers in the computational model. “Our bounds give no guarantee against a quantum adversary.” The computational deviations catalog is blunter: “If X25519 is broken, the theorems give nothing,” and “No post-quantum or harvest-now-decrypt-later (HNDL) security is claimed.”
• Healing after DH is broken. In the symbolic model, once DH is broken the ratchet’s DH secrets count as compromised, so post-compromise security claims no healing against an attacker who can break DH, even one who cannot break the KEM.
• Scale. “The statistical terms limit the bound to moderate scale.” If nearly every message starts a new epoch, the bound is vacuous for single sessions of about 25,000 messages, or for 2²⁰ sessions of 2¹⁰ messages, which is about 1.07 billion messages in all (my arithmetic).
• Replay. The forward secrecy and post-compromise security theorems do not rule out the replay-based loss of forward secrecy that Cheval and colleagues described: “the binary runs libsignal’s deduplication of base keys, but the model does not require it.”
• Everything outside the harness. Key generation, groups, sealed sender, server-side protocols, multi-device state, and side channels.

The bug test shows less than the blog says

The paper reintroduced two libsignal bugs that Cheval, Jacomme and Richards found with an automated analysis of the Double Ratchet composed with PQXDH: a weak-state bug (fix cd36118), where a prekey message that fails to decrypt on its new session is trial-decrypted with older sessions, and if that succeeds the new session’s unconfirmed state, which holds a copy of the signed prekey secret, is stored; and a small-subgroup bug (fix 5293caa), where the PQXDH responder does not check that the initiator’s X25519 base key is torsion-free and in range. It injected each by reverse-applying the upstream fix to v0.105.4 and recompiling.

For both, the paper has complete Lean proofs that the symbolic theorem does not hold of the bug-injected binary. That demonstrates that the symbolic specification is sensitive to these two bug classes, both of which an earlier formal analysis had already found. It is not the computational result the blog’s “insecure” suggests, and WIRED reports that the analysis found no new vulnerabilities in the portions it examined.

The artifact adds three details.

• The four disproof files (two bugs, four witness variants) each state the negation of the final headline predicate, ¬ SignalSessionSecurePlaced mutantCliElfBytes. Their header says “Nothing imports this file; it is in no default target or audit,” and building them needs scripts/bug_injection.py, which is not in the clone.
• The paper map says the retargeting of those disproofs to the final headline is still pending and that “until T-12(d) lands, the mutant disproofs do not yet negate the placed F3 headlines.” The files say it is done. I could not build either, so the claim that the bug test reaches the final theorem rests on the authors’ files and the paper’s text, not on anything I ran.
• Ten further synthetic bug obligations, one per file under Symbolic/BugInjection/Synthetic/Disproofs/, “remain sorry-exempt stubs on main,” in a library outside the default build. Neither the paper nor the blog mentions them.

The artifact: the counts, the clean tree and the missing files

Do the paper’s numbers reproduce?

Mostly. The table compares the paper’s figures with my count of the clone, using the nearest folder; the paper may scope its figures differently.

Four of the five proof figures land within 8 percent. The computational one is 24 percent larger. The paper says standalone proofs for two models “remain in the artifact outside the trusted base,” which may explain it; I did not test that. The 26,000-line trusted total the paper gives sits inside the range my two whole-file counts bracket, 20,053 to 32,359 code lines (my arithmetic), so I can neither confirm nor reject it without the closure script that computes it.

The proof tree is clean of the usual weakeners

I removed comments and string literals and counted three words that would weaken a Lean proof.

The first row is what the paper’s claim needs. The stubs are the ten obligations above. The comparator folder holds the challenge statements for the headline theorems, so I take the sorry there to be expected. The fixtures include the audit tooling’s own deliberate cases. This is a static text scan; it does not replace Lean’s #print axioms on the headline theorems, which is what the missing CI scripts do.

What the repository cites but does not contain

The missing document matters most. The computational headline theorem file says to see it for “the trusted definitions and kernel axioms of each theorem,” and the symbolic theorem’s docstring cites it for the symbol-name assumption. A reviewer therefore cannot read, in the public tree, the list the authors designate as the place to check what each theorem trusts. Issue 1, opened at 14:11 UTC on November 10 by another GitHub user, reports the same gap and also names scripts/TrustedClosure.lean, which is absent from scripts/ too (library files of that name exist under arm64-semantics, so my basename check does not flag it). The issue had no replies when I checked at about 20:05 UTC.

The documentation that is present lags the paper in places. The paper map says it covers a “draft of 2026-10-26” under another title, lists “37 external hooks” where the paper says 39 hooked routines (I did not reconcile the two), and, as noted, calls the bug-disproof retargeting pending. The deviations file still describes SPQR as “off in the verified image” and says a temporary hypothesis “will be removed once the SPQR-on (V1) headline is on main.” The paper and the headline theorems’ docstrings say SPQR V1 is composed in, so I read that as stale prose, but I did not resolve it by building. The lesson is the one the paper draws about specifications: read the Lean statements, and treat the surrounding prose as a hint. The repository may well be fixed after this was written; my check is of the single commit above.

The verified release is already behind

The proofs are tied to one pinned binary, built from libsignal v0.105.4. The paper says “early in the project, small source changes or a recompiled binary required large proof repairs,” and “We are keen to use this workflow to verify new releases of libsignal before they ship.” Meanwhile the project kept shipping.

GitHub’s comparison of v0.105.4 with v0.106.2 shows 24 commits, 183 changed files, and 40 of those files under rust/protocol/, the crate that holds the verified session code, with 12,159 changed lines there. The largest changes are in session_management.rs (390 added, 2,690 removed), session_cipher_legacy.rs (827 removed) and a new tahini.rs (486 added). Whether those changes alter the compiled behavior of init, send and recv is not something I checked, and a refactor can leave behavior unchanged. But the proofs are about bytes, and the paper says a rebuilt binary needs proof repair.

Effort, cost and credit

• Effort. The paper says the proof work “was done by a team of five over four weeks,” working in parallel on the symbolic and computational proofs. A proof campaign “typically had 40 to 80 agents and ran on a single machine for 24 to 72 hours.” The paper does not say how many campaigns there were.
• Who wrote what. The proofs came from agent teams on Gemini 4 Carbon, and “none of the authors wrote any proof code.” The paper adds that “The majority of our effort went not into proofs but into specifications.” The specifications came from humans working with agents on both Gemini 4 Carbon and Claude Opus 5.5, with a reviewer from a different model family; SecurityWeek names “agents running on Carbon and Claude Opus 5.5,” while the blog says only “a mix of models.”
• Human review. The blog says human experts reviewed every specification. The paper adds that specifications were amended during the campaigns, with a critic agent vetting proposals, and that amendments that change trusted assumptions were “approved during the campaign, by one of us or under a policy we set,” with all amendments reviewed at the end of each campaign. One example it gives is a trusted contract for library functions that was strengthened to match their real behavior.
• Cost. The abstract says the results suggest AI can make formal verification “practical for real-world systems,” which is a claim about cost. WIRED reports that “Google declined to share the cost of the analysis,” and the paper gives no token or dollar figure.
• Signal’s role. The paper thanks three Signal engineers “for their feedback on our specifications”; the blog’s acknowledgments say “methodology.”

If you ship Signal-protocol code

The proofs do not make a messaging product verified, but they give you five questions that apply to any verification claim.

1. Which build? One AArch64 Linux executable, built with rustc 1.98.1 and musl. If your app compiles libsignal differently, the paper’s guarantee transfers only as far as you trust the compilation to preserve the behavior the harness exercises.
2. Which version? v0.105.4 with spqr v1.6.0, three tagged releases ago.
3. Which properties against which attacker? Forward secrecy, authentication, post-compromise security and handshake secrecy, against a classical attacker in the computational model, with no proof of post-quantum healing.
4. What is assumed? The 39 contracts, the semantics and the primitives. The paper notes the idealized primitive contracts could be connected to verified implementations such as HACL★ and libcrux; today they are assumptions.
5. What can you re-run? The Lean sources are public (the README says Apache 2.0), and a full check takes hours. The trusted-base document and the CI scripts the headline files cite are not in the tree.

Nothing in the paper or the coverage suggests Signal users should change anything. The analysis found no new vulnerabilities, and the protocol’s design has been checked by several earlier formal analyses. The change is in what a reader should take “verified” to mean.

Reproduce the recount

Both scripts need Python 3.13 and nothing else, plus Git for the clone. The first reads about 450 MB of Lean and took about 20 seconds here; the second makes about a dozen unauthenticated GitHub API calls and can hit the 60-per-hour limit if you rerun it. The output below is from November 10, 2026, at commit 808b4b7.

git clone https://github.com/google-deepmind/code-verification
cd code-verification
git checkout 808b4b7ffef198e6a91f71ed776d641a1c236882
cd ..
python audit_cv.py code-verification
python libsignal_compare.py

# audit_cv.py
"""Audit the public Lean artifact of DeepMind's Signal verification.
Usage: python audit_cv.py PATH_TO_CLONE   (standard library only; reads about 450 MB of Lean)"""
import os
import re
import subprocess
import sys

ROOT = sys.argv[1]
BLOCK = re.compile(r"/-.*?-/", re.S)
STRING = re.compile(r'"(?:[^"\\]|\\.)*"', re.S)
LINE = re.compile(r"--[^\n]*")
AXIOM = re.compile(r"^\s*(?:@\[[^\]]*\]\s*)*(?:private\s+)?axiom\s", re.M)
SORRY = re.compile(r"\bsorry\b")
NATIVE = re.compile(r"\bnative_decide\b")
FOLDERS = [
    ("binary proofs", "LibsignalBinary/Proofs"),
    ("computational proofs", "Computational/Proofs"),
    ("symbolic proofs", "Symbolic/Proofs"),
    ("bug-injection folder", "Symbolic/BugInjection"),
    ("allocator proofs", "LibsignalBinary/Heap"),
    ("AArch64 semantics", "arm64-semantics"),
]
CITED = ["TRUSTED_BASE.md", "bug_injection.py", "check_no_sorry.py", "HeadlineAxioms.lean",
         "CheckMainOfLemmasClosure.lean", "CliAxiomGuard.lean", "CliElfAxiomGuard.lean",
         "trusted-closure.sh", "closure_diff.py", "DEVIATIONS.md"]
SPEC_DIRS = ["Computational/Specifications", "Symbolic/Specifications", "LibsignalBinary/Specifications",
             "Computational/Theorems", "Symbolic/Theorems"]


def walk(sub, exts):
    for dirpath, dirs, files in os.walk(os.path.join(ROOT, sub)):
        dirs[:] = sorted(d for d in dirs if d not in (".git", ".lake"))
        for name in sorted(files):
            if name.endswith(exts):
                yield os.path.join(dirpath, name)


def read(path):
    return open(path, encoding="utf-8", errors="replace").read()


def count_lines(raw):
    return raw.count("\n") + (0 if raw.endswith("\n") else 1)


def code_lines(raw):
    text = LINE.sub("", BLOCK.sub("", raw))
    return sum(1 for line in text.split("\n") if line.strip())


print("=== commit")
print(subprocess.run(["git", "-C", ROOT, "rev-parse", "HEAD"], capture_output=True, text=True).stdout.strip()[:7])

folder_lines = {sub: [0, 0] for _, sub in FOLDERS}
words = {}
cites = {name: 0 for name in CITED}
total = [0, 0]
for path in walk("", ".lean"):
    rel = os.path.relpath(path, ROOT).replace("\\", "/")
    raw = read(path)
    n = count_lines(raw)
    total[0] += 1
    total[1] += n
    for sub in folder_lines:
        if rel.startswith(sub + "/"):
            folder_lines[sub][0] += 1
            folder_lines[sub][1] += n
    for name in CITED:
        if name in raw:
            cites[name] += 1
    text = LINE.sub("", STRING.sub('""', BLOCK.sub("", raw.replace("'\"'", "''"))))
    if "/Synthetic/" in "/" + rel:
        kind = "synthetic stubs"
    elif rel.startswith("comparator/"):
        kind = "comparator challenge"
    elif "/Testing/" in rel or "/Tests/" in rel:
        kind = "tests and fixtures"
    else:
        kind = "everything else"
    for word, rx in (("sorry", SORRY), ("axiom", AXIOM), ("native_decide", NATIVE)):
        words[(kind, word)] = words.get((kind, word), 0) + len(rx.findall(text))

print("=== Lean lines by folder (comments and blank lines included)")
for label, sub in FOLDERS:
    files, lines = folder_lines[sub]
    print(f"{label:<22}{sub:<28}{files:>6} files{lines:>11,} lines")
print(f"{'all folders':<22}{'':<28}{total[0]:>6} files{total[1]:>11,} lines")

print("=== proof-weakening words (comments and strings removed)")
print(f"{'where':<22}{'sorry':>7}{'axiom':>7}{'native_decide':>15}")
for kind in ("everything else", "synthetic stubs", "comparator challenge", "tests and fixtures"):
    print(f"{kind:<22}{words[(kind, 'sorry')]:>7}{words[(kind, 'axiom')]:>7}{words[(kind, 'native_decide')]:>15}")

print("=== specification files by trust marker in their first 70 lines")
table = {}
for sub in SPEC_DIRS:
    for path in walk(sub, ".lean"):
        raw = read(path)
        head = "\n".join(raw.split("\n")[:70])
        if "**Trusted:" in head:
            kind = "Trusted"
        elif re.search(r"trusted in part", head, re.I):
            kind = "Trusted in part"
        elif re.search(r"checked by lean", head, re.I):
            kind = "Checked by Lean"
        else:
            kind = "no marker"
        row = table.setdefault(kind, [0, 0, 0])
        row[0] += 1
        row[1] += count_lines(raw)
        row[2] += code_lines(raw)
print(f"{'marker':<18}{'files':>6}{'lines':>9}{'code lines':>12}")
for kind in ("Trusted", "Trusted in part", "Checked by Lean", "no marker"):
    files, lines, code = table.get(kind, [0, 0, 0])
    print(f"{kind:<18}{files:>6}{lines:>9,}{code:>12,}")
sem = [0, 0, 0]
for path in walk("arm64-semantics/Arm64/Trusted", ".lean"):
    raw = read(path)
    sem[0] += 1
    sem[1] += count_lines(raw)
    sem[2] += code_lines(raw)
print(f"{'arm64 Trusted/':<18}{sem[0]:>6}{sem[1]:>9,}{sem[2]:>12,}")

print("=== names the repository cites, and whether a file of that name exists")
present = {os.path.basename(p) for p in walk("", ("",))}
for path in walk("", (".md", ".toml", ".py")):
    raw = read(path)
    for name in CITED:
        if name in raw:
            cites[name] += 1
print(f"{'name':<32}{'files citing it':>16}{'file present':>14}")
for name in CITED:
    print(f"{name:<32}{cites[name]:>16}{'yes' if name in present else 'NO':>14}")

# libsignal_compare.py
"""How far the verified libsignal release is from newer ones (GitHub API, no token needed)."""
import json
import urllib.request

API = "https://api.github.com/repos/signalapp/libsignal"
OLD, NEW = "v0.105.4", "v0.106.2"


def get(path):
    request = urllib.request.Request(API + path, headers={"User-Agent": "sxz-audit", "Accept": "application/vnd.github+json"})
    with urllib.request.urlopen(request, timeout=30) as response:
        return json.load(response)


print("=== releases (date of the tagged commit)")
for tag in (OLD, "v0.106.0", "v0.106.1", NEW):
    ref = get(f"/git/ref/tags/{tag}")["object"]
    sha = ref["sha"]
    if ref["type"] == "tag":
        sha = get(f"/git/tags/{sha}")["object"]["sha"]
    commit = get(f"/commits/{sha}")["commit"]
    print(f"{tag:<10}{commit['committer']['date']}  {commit['message'].splitlines()[0][:58]}")

print(f"=== compare {OLD} to {NEW}")
cmp = get(f"/compare/{OLD}...{NEW}")
files = cmp["files"]
protocol = [f for f in files if f["filename"].startswith("rust/protocol/")]
changed = sum(f["additions"] + f["deletions"] for f in protocol)
print(f"commits {cmp['total_commits']}, files changed {len(files)}, under rust/protocol/ {len(protocol)} ({changed:,} changed lines)")
src = [f for f in protocol if f["filename"].startswith("rust/protocol/src/")]
for f in sorted(src, key=lambda f: -(f["additions"] + f["deletions"]))[:6]:
    print(f"  {f['filename']:<46} +{f['additions']:<4} -{f['deletions']}")

The output of the first script, then the second:

=== commit
808b4b7
=== Lean lines by folder (comments and blank lines included)
binary proofs         LibsignalBinary/Proofs        7761 files  5,403,450 lines
computational proofs  Computational/Proofs          1115 files  1,068,713 lines
symbolic proofs       Symbolic/Proofs                785 files    351,050 lines
bug-injection folder  Symbolic/BugInjection          552 files    140,879 lines
allocator proofs      LibsignalBinary/Heap            96 files     75,538 lines
AArch64 semantics     arm64-semantics                726 files    407,549 lines
all folders                                        11323 files  7,528,295 lines
=== proof-weakening words (comments and strings removed)
where                   sorry  axiom  native_decide
everything else             0      0              0
synthetic stubs            10      0              0
comparator challenge       24      0              0
tests and fixtures          4      1              1
=== specification files by trust marker in their first 70 lines
marker             files    lines  code lines
Trusted               70   16,286       9,532
Trusted in part       50   19,129      12,306
Checked by Lean       31    6,262       3,828
no marker             24    5,217       3,527
arm64 Trusted/        61   16,767      10,521
=== names the repository cites, and whether a file of that name exists
name                             files citing it  file present
TRUSTED_BASE.md                              128            NO
bug_injection.py                              53            NO
check_no_sorry.py                              1            NO
HeadlineAxioms.lean                            1            NO
CheckMainOfLemmasClosure.lean                  1            NO
CliAxiomGuard.lean                             1            NO
CliElfAxiomGuard.lean                          1            NO
trusted-closure.sh                             1            NO
closure_diff.py                                1            NO
DEVIATIONS.md                                 21           yes

=== releases (date of the tagged commit)
v0.105.4  2026-10-22T02:15:34Z  Distrust compromised weak intermediate certs
v0.106.0  2026-10-23T19:07:35Z  Address cargo audit findings
v0.106.1  2026-10-27T23:50:19Z  Fix envvar forwarding in swift/run_ios_tests.sh
v0.106.2  2026-11-05T18:10:02Z  swift: Simplify process to use a local libsignal with Sign
=== compare v0.105.4 to v0.106.2
commits 24, files changed 183, under rust/protocol/ 40 (12,159 changed lines)
  rust/protocol/src/session_management.rs        +390  -2690
  rust/protocol/src/session_cipher_legacy.rs     +0    -827
  rust/protocol/src/tahini.rs                    +486  -0
  rust/protocol/src/state/session.rs             +251  -201
  rust/protocol/src/session_management/tests.rs  +316  -0
  rust/protocol/src/session.rs                   +64   -41

The first script’s sections are the line counts by folder, the three weakening words by location, the files marked by trust level, and the names the repository cites. The shares, brackets, percentages and the 1.07 billion figure above are my arithmetic on these outputs and the paper’s printed numbers.

What I could not check

• I did not build the Lean development or run the kernel check, so every statement about what the theorems say rests on the paper and the theorem files, not on my run. I also did not run #print axioms.
• I did not read the paper’s proof sections or appendices, so the 200-plus departures and the three assumption lists are as the paper states them.
• I did not reconcile 37 external hooks (the paper map) with 39 hooked routines (the paper), or the “SPQR off” prose with the paper’s SPQR V1 statement.
• I did not test whether the libsignal changes since v0.105.4 alter the verified code paths.
• I did not see Google’s cost, the number of proof campaigns, or any interview material beyond WIRED’s and SecurityWeek’s text.
• The repository was a single commit on November 10; later commits may add the missing files or correct the map.

Sources

• Pushmeet Kohli and Swarat Chaudhuri, Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Google DeepMind, November 10, 2026.
• Swarat Chaudhuri and eight co-authors, AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level, November 10, 2026, and its reviewers’ site.
• Google DeepMind, code-verification at commit 808b4b7: the paper map, the deviations catalog, the symbolic headline theorem, the computational headline theorem and a bug disproof file.
• Lily Hay Newman, A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure, WIRED, November 10, 2026.
• Eduard Kovacs, Google Widens Gemini 4 Carbon Access After AI Agents Verify Signal Code, SecurityWeek, November 10, 2026.
• GitHub, Trusted-base documentation and closure script references are missing, issue 1 in google-deepmind/code-verification, opened November 10, 2026.
• Signal Foundation, libsignal v0.105.4 to v0.106.2 comparison and releases.