Independent assurance audit · Revision 2
OpenAI's ten machine-checked advances are backed by unusually strong proof artifacts. This audit found one materially different validation boundary, one missing provenance layer, and one claim from our first release that needed to be corrected.
This is not a claim that any result is false. It is an audit of what the public release proves, what it asks us to trust, and what evidence would make that trust portable.
Formal verification closes the proof layer. It does not automatically settle the statement's intended meaning, the definition bodies a challenge allows a solver to fill, or which checker versions produced the acceptance claim.
The remaining trust surface may be small in volume, but it controls what the machine-checked artifact means and whether the verification event can be reproduced later.
bundles use theorem-hole comparator boundaries only.
includes four definition holes and therefore requires a different review path.
request the independent nanoda checker in their public configurations.
It compared proof-file bytes with statement-file bytes. Bytes are not units of confidence, effort, or consequence. The better insight is that a tiny human trust surface can determine the meaning of millions of machine-checked characters.
The proof is one layer in a larger assurance case. Overall confidence is bounded by the weakest consequential layer, not averaged across all of them.
The GapCVP comparator configuration lists four theorem targets and four definition holes. That makes its validation path structurally different from the other eleven bundles.
Comparator checks that each filled definition has the expected name, type, universe, safety level, permitted axioms, and kernel acceptance. Its own documentation also says definition-hole solutions must always receive an additional verifier because their bodies can satisfy the interface without satisfying the challenge's intended meaning.
No evidence here says the GapCVP result is wrong. The finding is narrower and more useful: the release should expose the extra definition-body review as a first-class part of its assurance case.
Interface match, allowed axioms, kernel acceptance, and external-checker execution.
That the filled definition bodies represent the intended computational problems.
“This checked” is a claim about a particular proof artifact, challenge, dependency graph, kernel, external checker, sandbox, and moment in time.
Every public “verified” claim should be accompanied by a portable, signed record of the exact artifacts and validation environment that produced it.
This audit does not claim the released proofs exploit the July bug. All twelve public configurations request nanoda. The point is that enable_nanoda: true is an instruction, not a durable attestation of which nanoda binary actually ran.
Our first release drew the line too sharply. A checker cannot infer private intent from a proof alone. But independent source statements and counterfactual probes can test many forms of semantic drift.
Does the statement parse and inhabit the formal language?
Can a valid proof be constructed for that formal statement?
Does the formalization behave correctly when meaning-bearing conditions change?
Does an accountable expert or organization accept it as the intended claim?
A 2026 preprint reports that bidirectional provability fingerprints plus counterfactual probes detected 89.6% of controlled statement drift at a 3.0% false-positive rate across 2,183 natural-language/Lean pairs. That is promising evidence, not a final replacement for expert acceptance.
The corrected claim: semantic faithfulness cannot be certified from the proof artifact alone. It can be instrumented when an independent source specification exists, while final reliance remains an accountable decision.
An agent can prove it followed a workflow and still pursue the wrong intent, rely on stale evidence, or stop before the real-world outcome occurred. Consequential actions need a portable assurance record.
Proposed operating artifact
Not a transcript. Not a compliance badge. A compact, inspectable record of what the system was authorized to do, what evidence it used, what changed, how the outcome was verified, which validator ran, and who owned the exception.
Did the real-world outcome occur, or did the workflow merely end?
Which policy, evidence, and validator version governed the action?
Who approved the exception, and what was changed?
What inspectable evidence arrives with every consequential action?
This proposed record is not a standard or a claim of NIST endorsement. It is a practical artifact designed to complement lifecycle governance, documentation, and testing/evaluation/verification/validation practices.
The public release is stronger than a folder of proofs: it publishes trusted challenge files, explicit permitted axioms, and independent-checker configuration. The matrix below shows the boundary for each bundle.
Terminology matters: the four GapCVP definition holes are in the trusted comparator challenge interface. They are not sorry holes in the released solution, whose manifest reports a sorry count of zero.
This revision separates what the public artifacts establish from what would require mathematical peer review, independent reproduction, or additional organizational acceptance.
That is the more defensible research claim, and the more useful operating principle for any company giving AI systems real authority.