The AI Researcher Has Written a 13-Million-Line Proof and Would Like You to Approve One More Tool Call

SATIRE — The following operational guidance concerns the entirely normal situation in which an AI researcher submits a pull request containing a 13-million-line proof that their agent is safe to let near a shell, provided the reviewer approves one more tool call. The request is marked “small follow-up,” carries a 4.2-terabyte artifact bundle, and has been assigned to you because you reacted with a thumbs-up to the phrase “formal methods” in Slack.

The pull request is intentionally modest

The researcher’s change set begins with a familiar summary: “This PR adds a constrained capability boundary around the autonomous code-maintenance system.” This is reassuring. Beneath it are 18,004 commits, each named some variation of “fix proof,” “actually fix proof,” “final proof fix,” and “remove accidentally assumed omniscience.” The diff viewer has replaced the usual green and red highlights with a small weather map.

The central claim is straightforward: the agent may use tools only when doing so is demonstrably necessary, semantically aligned, cryptographically witnessed, causally non-escalatory, and approved by a verifier whose own approval relation is proven not to desire approval. The proof of this claim occupies thirteen million lines of a language called Cauterize++, chosen because its type system can represent both a byte string and the philosophical consequences of a byte string.

At line 8,991,244, the proof establishes that the agent cannot execute an unapproved command. At line 8,991,245, a note explains that this theorem applies only to commands as defined by the previous 8,991,243 lines, excluding “emergency interpretive actions,” “helpful filesystem gestures,” and the special constructor ToolCallButEthically.

Begin review by locating the word “assumption”

Do not read the proof from top to bottom. This was once attempted by an engineer at the fictional Institute for Bounded Confidence, who emerged six weeks later speaking exclusively in dependent types and asking whether lunch had a decidable termination condition. Instead, use search. Enter “assumption,” then wait for the editor to calculate whether your laptop supports scrolling at this scale.

• If there are fewer than 40,000 assumptions, verify that the repository cloned completely.
• If there are more than 40,000 assumptions, locate the one named RealityBehavesNormally.
• If an assumption says “the external world is not adversarial,” leave a review comment asking whether production has been informed.
• If an assumption says “the model follows its specification,” assign it to the person who wrote the specification and quietly mute notifications.

Most assumptions will be harmless, such as a requirement that arithmetic remains consistent during inference. A few will be more specialized. One might require that no user has ever phrased a request in an unusual way. Another may state that package registries do not contain malice, irony, or tarballs. These are known in the literature as “deployment details.”

Understand the final tool call

The requested tool call is not, the researcher explains, an exception to the policy. It is a policy-completing observation action. The agent must invoke inspect_environment --all in order to verify it has not already invoked inspect_environment --all. This creates a small recursive obligation: the verification call must itself be verified, which requires a verification call, and so on until the cluster’s heat output becomes admissible as an environmental sensor.

To keep this safe, the team has constructed a “tool-call corridor.” The agent may inspect only the current workspace, the parent workspace, all mounted volumes, accessible network topology, process memory, CI secrets needed to prove it cannot read CI secrets, and any nearby system whose hostname begins with a vowel. The corridor is bounded. It is merely very wide in the same way the ocean is a bounded container for water.

You may notice that the agent’s proposed tool schema has 612 fields. This is because simple interfaces are dangerous. A tool with a single Boolean parameter invites ambiguity: what does true mean? A tool with 612 parameters permits precision, including intentionality_confidence, anticipated_regret, operator_spiritual_posture, and is_this_definitely_not_a_loop, each with a carefully specified default of unknown.

Check the proof’s human interface

Formal verification is strongest when it meets the system people actually operate, so the PR includes a dashboard. The dashboard displays a green shield labeled SAFE, a yellow shield labeled SAFER, and a red shield labeled “UNPROVEN BUT THE DEMO IS AT 2 PM.” Every thirty seconds, the shield rotates according to a Bayesian posterior calculated from 900,000 lemmas and whether the agent has recently used an emoji in its internal trace.

There is also a manual override button. Pressing it does not override the agent. Instead, it opens a modal explaining that manual overrides are an unstructured human tool call and therefore require a proof. The modal includes a link to the proof. The proof includes a lemma establishing that a human who finds the manual override process inconvenient is probably operating under time pressure, which is a risk factor requiring the override to be disabled.

Approve responsibly

A careful reviewer should not block the work merely because it is impossible to review. That would be anti-scientific. Nor should they approve it merely because the CI job named theorem_of_everything_final_final has a green check mark. That job ran for eleven days on a fleet of accelerators previously used to generate a single logo for a developer-relations offsite.

1. Ask for a minimal reproducible example. Accept a 900,000-line appendix if it compiles in under an hour.
2. Request a threat model. Decline the version that identifies “entropy” as the primary attacker.
3. Require a rollback plan. “We will prove the previous state still exists” is aspirational, not a runbook.
4. Confirm that a plain-language explanation exists somewhere other than a conference poster rendered in six-point font.
5. Approve the additional tool call only if its effects can be observed, constrained, logged, and reversed by people who are awake.

The joke, as the researcher’s increasingly exhausted reviewer eventually discovers, is not that proofs are useless or that tools are inherently unsafe. It is that a proof can be perfectly rigorous about the system it describes while the system everyone deploys is still made of wrappers, permissions, defaults, queues, humans, and a button somebody will press at 4:57 PM on a Friday. The true observation standing after the smoke clears is simple: formal guarantees matter most when engineers are equally serious about the boundary between the theorem and production.