Agents reused proofs of OpenSSL routines across three callers

[ 2026-10-05 · updated 2026-10-23 ] // GPT-6.1 Sol · HOL Light · x86-64 // 12 MIN READ

I wanted to know whether a proof about a shipped library binary could become something other programs build on. GPT-6.1 Sol agents used machine-checked contracts for two unchanged OpenSSL routines, exactly as Debian ships them, to verify three experimental callers through their actual linkage. The library bytes stayed the same; what was added is a checked account of how other code can call them.

Question and setup

My recent projects used proofs to justify faster code; here I wanted to add assurance to code without changing it at all. Shared libraries are the natural place to try: one copy of OpenSSL's libcrypto serves many programs, so a proof about its shipped bytes is worth more if each caller can build on it instead of reasoning about the library's instructions again. The idea comes from Theorem's essay Bootstrapping the Verified Software Stack, which argues for verifying production machine code and reusing verified interfaces across the programs that depend on it. The essay doesn't give an implementation recipe, and this experiment is mine, not theirs.

The targets were two routines from a pinned Debian OpenSSL build, 3.0.22-1~deb12u1. CRYPTO_memcmp had a checked comparison contract and OPENSSL_cleanse a checked zeroing contract. Earlier work in the project had composed them into one caller. This experiment asked whether the same assurance could serve more callers with different behavior.

The proofs are in HOL Light, a proof assistant whose small logical kernel checks every inference. They use the x86-64 instruction semantics and decoder from AWS's s2n-bignum at a pinned revision: a formal description of what the modeled instructions do to registers and memory. The theorems are about the shipped machine code, not its C source.

A caller needs more from an interface than its result. A correct comparison alone does not tell it whether its saved pointer or return address is still usable, which is why the contracts also cover memory effects, preserved state and the routine's return.

Who did what, and what checked it

I chose the question and, once the first two callers were accepted, authorized one bounded trial on a third, held-out caller (recorded in the steering amendment). Working from a brief for the wider glibc and OpenSSL project and this study's preregistered experiment plan, GPT-6.1 Sol agents wrote the contracts and caller specifications, the caller proofs and checking drivers, the failed trial's postmortem, the successor proofs and the review packet. The checks are mostly mechanical: HOL Light's kernel rebuilds every theorem from source, the supplier proofs included, and each package's acceptance gate adds the exact frozen statements, an extraction cross-check tying the theorems to the final binary and its linkage, five integrity controls, and a binding probe showing the caller proof fails without the public contract. Agents inspected the proof sources to check that the caller proofs use only the public contracts. No person has yet reviewed the specifications.

The call itself is part of the proof

A dynamically linked program does not jump straight into the library. Its call goes to a small stub in the procedure linkage table (PLT), which jumps to an address stored in the global offset table (GOT). Each caller proof follows the actual CALL instruction through that stub and GOT slot to the supplier entry point, shows that the state there satisfies the supplier's precondition, and carries the supplier's result and preservation guarantees through the caller's remaining instructions to its actual RET.

The loaded image, the program and library as laid out in memory after the dynamic loader runs, is still an assumption: the experiment verifies the call paths within it, not the loader. Within that boundary, the call target and the conditions for applying its contract are checked rather than assumed.

Three callers, three different obligations

The callers are small experimental programs, not production applications, chosen to use the same supplier assurance in different ways.

The theorems range over arbitrary contents and lengths that satisfy explicit memory, address and entry conditions (the admissible domain in Table 01), not over a set of test inputs.

C2: not writing is stronger than restoring

For the conditional-cleanup caller, unequal inputs leave the destination unchanged, and the access policy forbids even intermediate writes to it. A write followed by a restore would pass a check of final memory but violate this guarantee.

On equality, every destination byte is zero at return, and memory outside the destination and a declared scratch area is preserved. The returned comparison refers to the inputs before cleanup. Identical and partially overlapping inputs are admitted, and bytes of the second input inside the cleared region are not promised to survive.

That separates a path that leaves data alone from one allowed to destroy it, which a surrounding proof needs. The no-write result does not widen the admitted permissions: the nonempty destination must still be writable at entry on both paths.

C3: the second comparison sees different memory

The third caller makes the memory snapshot explicit. It behaves roughly like this:

first_equal = compare(p, q, n) == 0
clear(p, n)
second_equal = compare(p, q, n) == 0

if not first_equal:
    return 2
return 1 if second_equal else 0

This is explanatory pseudocode; the verified artifact is an 89-byte, 32-instruction assembly-authored caller plus its two six-byte linkage prefixes.

Take two disjoint one-byte inputs that both hold 7. They compare equal, but after the first is cleared the second comparison sees 0 and 7, so the result is 0. With identical pointers, clearing the first input clears the second, so both comparisons agree and the result is 1. These examples illustrate the specification; they are not separate machine runs.

The proof handles that difference without banning overlap. It keeps the first comparison result across the cleanup, relates the second comparison to the actual cleared memory, restores the saved slots and return address, and closes every return path.

This is the strongest transfer of the three: the contracts supported a caller whose behavior depends on both the old and the new memory.

The held-out caller missed its cap; a successor completed it

C1 and C2 were development cases: the integration machinery (the general lemmas and proof automation that connect a caller's proof to the contracts) changed while they were built, and those changes are recorded as adaptation. Before the exact C3 case was exposed, the agents froze a common integration layer and rebuilt both development cases against it; C3 was then chosen and written in a separate agent context. The layer had been prepared for a declared family of callers that make several library calls and keep a result between them, but not for C3's exact code, domain or specification, so the trial tests whether it carries to a concrete case it was not tuned to.

The first C3 attempt had a three-hour construction cap. It didn't finish, and under the original rules that result stays a failure.

A postmortem found specific proof problems: a helper discarded a premise needed later, facts about the loaded image had to be selected at the right intermediate state, and saved slots, frames and memory snapshots still had to be connected across the two calls. A separately authorized successor completed those obligations, keeping the supplier contracts, the frozen integration algorithms, the binary and the original caller domain.

At one instruction site the convenience automation failed, and a local proof established that site's behavior from the existing primitives without changing the instruction semantics or the general dispatch algorithm. The foundation was usable where the automation was incomplete, which does not mean every new caller can be handled automatically.

The frozen layer was sufficient for this caller after additional caller-local work. The missed deadline says something different, about how much work that took. I'm reporting both.

Rebuilding the packages from the delivery

The final stage rebuilt all three accepted packages from the delivered checking sources in a new filesystem location, with no new caller and no proof repair. Each passed its complete acceptance gate, including the integrity controls and a fresh binding probe.

The complete session includes the positive reconstruction, the controls, the binding probe and the gate, so the columns must not be added. These are checking times, not proof-construction times; setup and image export are counted separately.

Inside each positive reconstruction, rebuilding the supplier proofs took 419 to 433 seconds and the caller's own proof 46 to 122 seconds: checking a package never skips the supplier proofs, and each caller proof then applies the freshly rebuilt contracts.

The controls reject changed package inputs and missing proofs, including a missing caller proof with stale success metadata. They test that the selected proofs are bound to the intended inputs, not that every binary mutation is semantically wrong, and they do not validate the instruction model.

What this stage adds is a checking-only delivery, so the proofs no longer exist only in a development session. The run used the same machine and Docker service as the development work, with an agent operator that had prior context, so it is not yet evidence from an independent person or organization.

What you can inspect

The public repository is a source and review edition. It contains the proof and caller sources, the checking scripts, a human-review packet with the literal contracts and trust assumptions, the release index and report, the original held-out failure record and postmortem, the successor's report, and compact receipts from the later rebuild. A reader can check what each theorem states and how the recorded evidence fits together.

It does not contain the sealed checking and review archives, the Docker runtime images, the compiled callers and library binaries, or the Intel manuals and their converted text. The publication scope explains why: redistribution permission for the Intel manual text and the source and notice obligations for the runtime image are still pending. No license has been granted yet for the project's own code. So the public release offers source and recorded checking results, not an executable reproduction: the recorded checking commands do not run from a clone.

Interpretation and limits

The positive result is composable assurance. Public contracts for two unchanged, shipped routines were enough to verify three different linked experimental callers, including one chosen after the integration layer was frozen and completed by a separately recorded successor. The work went into specifications, caller proofs and binding the proofs to the artifacts, not into replacing the library routines with friendlier implementations.

The most consequential limit is that the result has only been checked inside the setup that produced it, and no person has reviewed whether the contracts and the architectural interpretation say what they should. The other limits are narrower:

• The proofs hold in a pinned x86-64 model under explicit address, memory-permission, stack-separation and normal-entry conditions (RF = TF = 0, so the call is not resuming from a debug fault or single-stepping). They assume the declared initialized images and architectural environment.
• They do not cover all of OpenSSL, library upgrades, arbitrary ASLR or the dynamic loader. There is no constant-time theorem for the callers, and clearing the destination is not a claim that every copy of a secret is physically erased.
• The HOL Light kernel and runtime, the s2n-bignum instruction model and decoder with this project's frozen additions to them, the processor state added to the model for the calling convention (ABI), and the binary extraction and loading steps are trusted. Successful checking does not validate those tools in general.
• That the caller proofs use only the public interfaces is supported by agents' source and tactic inspection. Supplier theorems stayed accessible in the shared proof environment. There is no formal capability isolation and no certificate of every transitive proof dependency.
• There is no matched construction baseline without the supplied interfaces, and construction cost, tokens and coordination time were not fully recorded, so the experiment says nothing yet about whether reuse saves effort. I have not compared this work with related binary verification, such as s2n-bignum's own machine-code proofs, SAW or Macaw.

Next experiment

The next step is checking by someone outside this setup, not another caller.

• A minimal replay package that someone else can run on another machine to rebuild the three packages, once the redistribution questions are settled.
• Human review of the specifications and the architectural interpretation.
• Only then another caller, or a matched construction trial without the supplier interfaces to measure what reuse saves.

Reproducibility