An AI assistant generates tiny programs and a gatekeeper must decide, based solely on the source code, whether each program may be executed. The rules are fixed: never perform a forbidden action, never let the output depend on a secret, and always eventually produce an answer. We ask whether two rulebooks—one enumerating allowed behaviours and one enumerating disallowed behaviours—can both be complete while every rule is backed by evidence that a machine can verify in finite time. The answer is negative: checkable evidence can only settle finite records, whereas properties such as “never” and “eventually” are never settled by a finite record.
For prohibition rules every violation can be caught by observation, but no safe program can be permanently cleared after a finite check. For confidentiality and responsiveness, neither side can be guaranteed. We precisely characterize which rules about observable behaviour can be confirmed by evidence, and show that any sound rulebook of $n$ bits necessarily omits a compliant program of roughly $n$ bits. Imposing a time limit makes every property checkable, but only by running the program for essentially the whole limit, which is infeasible for a finite verifier.
Consequently the gatekeeper cannot issue a verdict for every program; instead it can provide a checkable list that contains everything it must allow and nothing it must refuse. Simulations on 2.2 million random programs and on self‑referential adversaries demonstrate that the obstruction is adversarial rather than typical, and that the only error a longer test never eliminates is the liveness component of confidentiality.
Review: The paper shows that without a runtime bound, any finite, checkable rule system cannot fully separate safe from unsafe AI programs, urging designers of gatekeeping mechanisms to either tolerate uncertainty or enforce strict execution limits.