Why an AI code gatekeeper cannot certify every safe program

A limit on universal guarantees

The paper studies a deliberately idealised gatekeeper. Submitted programs are deterministic, written in a language capable of universal computation, and have potentially unlimited time and memory. The gatekeeper can inspect their code and simulate their execution.

Its decisions must have finite certificates: evidence checked by a procedure that always terminates. Finding that evidence, however, need not terminate. A system might keep searching forever without approving or rejecting a particular program.

The distinction matters. A short rule can describe a requirement precisely without providing an algorithm that checks every program against it. Nor does the result mean that individual safe programs cannot be proved safe. The obstacle is a sound certification system that covers all compliant programs in the unrestricted domain.

Three requirements, different obstacles

The author treats three requirements separately. Safety means never performing a designated forbidden operation. Confidentiality means producing identical complete public output sequences for either value of a secret bit. Responsiveness means eventually returning a valid answer on every natural-number input.

The central method is reduction from the halting problem. Consider a program that first simulates another computation, then performs the forbidden operation only if that computation stops. Certifying every such program as safe when appropriate would require recognising every computation that never stops—something no algorithm can do.

Safety nevertheless has an asymmetry: every violation eventually supplies evidence when the forbidden operation occurs. There is no corresponding procedure that eventually certifies every safe program without ever certifying an unsafe one.

For the paper’s confidentiality and responsiveness definitions, neither compliance nor violation has such a complete confirmation procedure.

Confidentiality illustrates why the observation model matters. Different published values can expose a leak immediately. But if one execution has published something and the other has not, the apparent difference might disappear later. Establishing that the second execution will never catch up is not generally possible. This model compares output values, order and sequence length, but ignores timing and does not directly observe termination.

Responsiveness has a different universal demand: answering every tested input does not establish that every possible input will receive an answer. Waiting without an answer also does not establish that one will never arrive.

What finite evidence can establish

The paper organises these results around a characterisation related to the classical Rice–Shapiro theorem. For requirements judged only by observable behaviour, a category is fully confirmable precisely when membership can be established by a finite observation pattern from an effectively enumerable collection, and further behaviour cannot undo that membership.

Seeing a forbidden action fits this pattern. Never seeing one does not.

A separate worst-case result examines execution budgets. Limiting the number of steps makes the bounded questions decidable by simulation; bounded responsiveness also requires a finite input set. These bounded requirements differ from their unbounded counterparts.

The computational lower bound depends on additional efficient-simulation and self-reference assumptions. With linear simulation overhead, an always-correct checker faces specially constructed programs requiring work proportional to the execution budget, up to model-dependent constants. Under the paper’s more general polynomial-overhead assumption, the lower bound is weaker: it rules out a checker whose running time is polynomial in the combined length of the program and the binary-encoded budget, but does not establish work proportional to the budget. Neither result says that static analysis cannot accelerate ordinary cases.

Simulations show examples, not deployment risk

Alongside the proofs, the author reports experiments on 2.2 million randomly generated register-machine programs, exhaustive short-program populations and adversaries constructed against particular checkers.

Among the resolved random-program cases, bounded safety tests missed no violations at horizons of at least 128 steps. That observation is specific to the sampled programs, not a universal safe timeout. Programs whose behaviour could not be settled by the reference methods were excluded from error counts.

Confidentiality produced another effect: some programs emitted the same infinite sequence at different speeds. Comparing their outputs at a fixed deadline could therefore reject programs that satisfied the unbounded, timing-insensitive requirement.

These experiments illustrate the constructions and one artificial program distribution. They do not measure how often deployed AI agents produce dangerous code.

Useful gatekeepers remain possible

The paper gives a conditional alternative to complete classification. Let obligatory programs be those the system must admit, and permitted programs those it may admit. A suitable admission set must contain every obligatory program and no forbidden program. The author calls such a set a separator.

The existence condition matters. A computable gatekeeper that always reaches an admission or rejection decision exists exactly when there is a decidable separator. A gatekeeper allowed to keep some programs waiting exists exactly when there is a computably enumerable separator: an algorithm can eventually recognise every admitted program without necessarily terminating on others.

Such a separator need not exist for the chosen obligations. If every permitted program must be admitted, the admission set must equal the entire permitted category, recovering the computability barriers above. Narrower obligations can make a separator possible—for example, admitting only a decidable syntax of simple constant-return programs. Even then, otherwise permitted programs outside that admission set may be rejected or left waiting.

Restricted languages, proof-carrying code, execution budgets and runtime interception offer different routes to narrower guarantees. They restrict the domain or admission set, change the requirement, or control execution rather than perfectly classify every original program in advance.

The source is an arXiv preprint. Its foundations are classical computability results; the author’s claimed contribution is their organisation into this gatekeeping framework. Its conclusions depend on explicit program and observation models, not a comprehensive definition of real-world harm. The takeaway is a boundary on perfect advance classification—not a verdict that AI safety checks are futile.