Verified once, reused three times: agents carried proofs of shipped OpenSSL code into new callers

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

I wanted to know whether a proof about a library binary could become something another program uses. GPT-6.1 Sol agents took machine-checked contracts for two unchanged, distribution-shipped OpenSSL routines and used them to verify three different 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.

Setup

My recent projects used proofs to justify changes that made code faster. Here I wanted to add assurance without changing the library at all. 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. Both also had guarantees about permitted memory accesses, finite return and the state they preserve. 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, using the x86-64 instruction semantics and decoder from AWS's s2n-bignum at a pinned revision. The agents were GPT-6.1 Sol. They wrote the contracts, the caller proofs, the checking drivers and the release.

A caller needs more from an interface than its result. It needs to know which memory can change, which registers survive, what permissions are required and whether the callee returns. Without those, a correct comparison result does not tell the caller whether its saved pointer or return address is still usable.

Here those facts are part of the public contracts. A caller proof establishes the contract's entry conditions, applies its guarantees and continues from the resulting state. In the inspected proofs, callers do not step through the supplier's instructions again. Fresh checking still rebuilds the supplier proofs from source, so reuse here does not mean trusting an old success log.

The call itself is part of the proof

These proofs are about concrete final binaries and their declared loaded images. They don't stop at a source-level statement that says "call the verified function".

For each client, the chain runs through the actual CALL instruction, the PLT stub and GOT slot the linkage uses, the established supplier entry point, and the continuation after the callee returns. The caller proof must show that the state it reaches satisfies the supplier's precondition. It must then carry the supplier's result and preservation guarantees through the caller's remaining instructions to its actual RET.

The loaded image is still an assumption. The experiment verifies the call paths within it, not the dynamic loader that produced it. Within that boundary, the call target and the conditions under which its contract applies are checked rather than assumed.

Three callers, three different obligations

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

Each package also proves its access policy, finite execution to the actual return, and the required stack, register and memory preservation. The theorems range over arbitrary contents and lengths that satisfy explicit memory, address and entry conditions, 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. The access policy goes further and forbids even intermediate writes to it. A write followed by a restore would pass a check on final memory only, but it does not satisfy 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 that lie inside the cleared region are not promised to survive.

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

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, not a C translation of the sketch.

Take two disjoint one-byte inputs that both hold 7. They compare equal. 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 too, because they are the same memory. 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, and it relates the second comparison to the actual cleared memory. It also restores the saved slots and the incoming return address, carries the required code and GOT facts forward, 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, then completed

C1 and C2 were development cases. The integration machinery 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 in a separate agent context.

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 that was needed later. Facts about the loaded image had to be selected at the right intermediate state. Saved slots, frames and memory snapshots still had to be connected across the two calls. A separately authorized successor completed those obligations. It kept the supplier contracts, the frozen integration algorithms, the binary and the original caller domain.

At one instruction site, the convenience automation failed. A local proof established that site's behavior from the existing primitives instead, with no change to the instruction semantics or the general dispatch algorithm. That shows the foundation was usable where the automation was incomplete. It does not show that 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. Each passed its complete acceptance gate, including the inherited integrity controls and a fresh probe that the proofs fail when a required public interface is unavailable. No new caller and no proof repair was part of that stage.

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 accounted for separately.

The controls reject changed package inputs and missing proofs, including a missing caller proof accompanied by stale success metadata. They test that the selected proofs are bound to the intended inputs. They do not prove 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. This consumption run used the same machine and Docker service as the development work, and its operator was an agent with prior context. It shows the package can be rebuilt from its delivery. It is not yet evidence from an independent person or organization.

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. I didn't replace the two library routines with friendlier implementations. The work went into specifications, caller proofs and binding the proofs to the artifacts.

• The proofs hold in a pinned x86-64 model under explicit address, memory-permission, stack-separation and normal-entry conditions (RF = TF = 0). 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, the added ABI state and the binary extraction and loading steps are trusted. Successful checking does not validate those tools in general.
• That callers use only the public interfaces is supported by 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.
• The held-out C3 trial failed within its cap. Its successor's completion does not turn it into an unchanged transfer within the original budget.
• There is no matched construction baseline without the supplied interfaces, and construction cost, tokens and coordination time were not fully recorded. I am not claiming construction savings, and I haven't compared this with related work, so I make no novelty claim.

Next experiment

• Publish the replay assets, then have someone else rebuild the packages on another machine.
• 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