The verifier that cannot know everything
Verification sounds like the sensible adult in the AI safety room. The model may hallucinate, the benchmark may flatter, the demo may sparkle under conference lighting, but the verifier is supposed to be the hard stop: a formal mechanism that checks whether an AI system’s behavior satisfies a specified policy.
That is the comforting version.
Munawar Hasan’s paper, Incompleteness of AI Safety Verification via Kolmogorov Complexity, makes the comfort rather expensive.1 It does not argue that today’s verifiers are poorly engineered, too slow, or underfunded. Those are ordinary problems, and the industry has a well-rehearsed ritual for them: add compute, hire specialists, rename the product line, repeat. The paper argues something colder. For sufficiently rich AI behavior spaces, no fixed sound computably enumerable verifier can certify every true policy-compliant instance once those instances become descriptively complex enough.
The important word is not “difficult.” It is “certify.”
A behavior may be valid. The output may satisfy the policy. The system may have done the right thing. And still, within a fixed formal verification system, that truth may not be provable. That gap between truth and certifiability is the entire article. Miss it, and the paper becomes another vague sermon about “limits of AI safety.” Understand it, and the practical design recommendation changes: stop pretending that one global verifier can characterize all safe behavior; build systems where each important output carries structured evidence of its own correctness.
That is less glamorous than universal safety. It is also much closer to something one can actually deploy.
The paper changes the object being verified
The first move in the paper is not the theorem. It is the encoding.
Instead of treating AI safety as a fuzzy property of a model, the paper treats a single AI interaction as a finite binary object:
Here, $z$ is the input, $y$ is the system output, and $\Pi$ is the formal policy specification. For an autonomous vehicle, $z$ might encode the observed environment, $y$ might be a trajectory or control action, and $\Pi$ might encode constraints such as collision avoidance or minimum stopping distance. For a business process automation system, $z$ could be a customer request, $y$ the proposed action, and $\Pi$ the applicable approval, privacy, or compliance policy.
The paper then defines a policy-compliance predicate:
This is a deliberately austere model. It strips away architecture, training data, brand names, and the usual decorative fog around “responsible AI.” Good. A verifier cannot verify vibes. It verifies claims.
The formal verifier is modeled as a sound computably enumerable theory $T$ with a proof checker:
The checker returns 1 if $\pi$ is a valid proof of statement $\varphi$ in $T$. In this setting, the statement of interest is $P(x)$: this particular encoded interaction complies with the policy.
This framing matters because it moves the discussion from “Can we make the AI safer?” to a sharper question: can a fixed formal system prove that every actually compliant instance is compliant?
The answer is no. Not because neural networks are messy. Not because regulators are slow. Not because someone forgot to update the YAML file. The answer comes from the information content of individual instances.
Kolmogorov complexity turns “large behavior space” into a formal problem
Kolmogorov complexity measures the shortest program that can generate an object. For a string $x$, the paper uses prefix Kolmogorov complexity:
where $U$ is a fixed universal prefix-free Turing machine. If $x$ can be generated by a short program, it has low complexity. If there is no short description, $x$ has high complexity.
This is not “complexity” in the consulting-slide sense, where every mildly inconvenient workflow becomes a transformation journey. It is description length. How much information is required to specify this exact instance?
The paper’s next step is a richness assumption. In plain terms: policy-compliant behavior is not limited to a tiny, highly structured set. There are many valid instances. Formally, for infinitely many lengths $m$, the number of compliant strings is at least:
for some constant $d$.
This is the assumption that makes the result relevant to AI systems rather than merely cute as logic. Many safety policies allow a wide variety of acceptable behaviors. A vehicle may have many safe trajectories. A multi-agent perception system may have many consistent output combinations. A document-processing agent may have many compliant ways to route, redact, or escalate a case.
The policy itself does not need to be complicated. The variation can come from the input and output space. Even simple safety rules can admit a huge number of valid instances because reality is inconveniently large. Reality has always been poor at respecting dashboard schemas.
From this richness assumption, the paper derives the existence of high-complexity compliant instances. The counting logic is simple but powerful: there are fewer short descriptions than there are long strings. If there are enough compliant strings of length $m$, at least some of those compliant strings cannot be compressed below roughly $m-d$ bits.
So the first mechanism is:
| Step | Technical claim | Intuition | Business translation |
|---|---|---|---|
| 1 | Many strings satisfy $P(x)=1$ | Safe behavior is diverse, not a short list | Compliance cannot be reduced to a few canonical cases |
| 2 | Fewer than $2^{m-d}$ strings have complexity below $m-d$ | There are not enough short descriptions for all valid cases | Some safe cases are inherently information-heavy |
| 3 | Therefore some compliant $x$ has $K(x) \ge m-d$ | A true safe instance can be hard to describe compactly | A valid output may not be easy to certify through a fixed global rulebook |
The last column is where the business relevance begins. The paper is not saying “complex systems are hard.” That sentence should be retired along with several enterprise AI roadmaps. The paper is saying that once the space of valid instances is rich enough, some valid instances carry too much information to be captured by the proving capacity of a fixed verifier.
The theorem: if a verifier proved every complex truth, it would compress the uncompressible
The core theorem states that for any sound computably enumerable formal theory $T$ expressive enough to represent statements involving $P(x)$ and $K(x)>n$, there exists a constant $c_T$ such that, for sufficiently large $n$, no statement of the form
is provable in $T$.
This statement is easy to misread. It does not say high-complexity compliant instances do not exist. The earlier richness argument says they do. It does not say the system’s behavior is unsafe. It says a fixed verifier cannot prove all such true statements once the complexity threshold is high enough.
The proof mechanism is a compression contradiction.
Suppose, for arbitrarily large $n$, the formal system $T$ could prove a statement saying: this instance $x$ is policy-compliant and has complexity greater than $n$. Because $T$ is computably enumerable, one could write a program that enumerates proofs in $T$, searches for a proof of that form, extracts the corresponding $x$, and outputs it.
That program needs only a fixed proof-enumeration procedure, a fixed description of $T$, and an encoding of $n$. Its length is bounded by something like:
But the proof was supposed to establish:
For sufficiently large $n$, these two claims cannot both hold:
Eventually, $c_T + O(\log n)$ is smaller than $n$. The alleged proof would let us generate, through a short description, an object that the proof claims has no short description. That is the contradiction.
This is the mechanism the article must not skip. The limitation is not that the verifier runs out of time. It is that complete certification would create too much information from too little information. A fixed formal system cannot both be sound and certify every true high-complexity compliance claim.
A crude but useful analogy: a verifier cannot be a universal receipt printer for every possible safe behavior if some safe behaviors are too information-rich to be captured by the receipt-printing machinery. You can widen the printer. You can upgrade the ink. You can commission a glossy procurement memo. The theorem is not impressed.
Truth, provability, and the unhelpful instinct to scale everything
The industry’s default answer to verification failure is usually expansion. Add more policies. Add more static checks. Add more test scenarios. Add more synthetic data. Add more red-team prompts. Add more monitoring. Each tool can be useful. None of them overturns the theorem.
The paper separates three things that are often mixed together in AI governance discussions:
| Question | What it asks | What the paper implies |
|---|---|---|
| Is the behavior compliant? | Whether $P(x)=1$ is true | Some high-complexity instances may indeed be compliant |
| Can this fixed verifier certify it? | Whether $T$ proves $P(x)$, or a stronger claim involving complexity | Not all true compliant instances are certifiable by one fixed system |
| Can the system provide instance-specific evidence? | Whether an attached proof or certificate can be checked | This is the practical escape route the paper motivates |
The misconception is obvious because it is emotionally convenient: if the verifier is strong enough, it should eventually certify every genuinely safe behavior. This is the same organizational fantasy that says a sufficiently elaborate approval workflow will remove judgment from management. Charming. Also false.
A stronger verifier may certify more cases. A better policy language may reduce ambiguity. Better tooling may make formal methods more usable. The theorem does not deny any of that. It denies the leap from “more capable” to “complete.”
This is a useful distinction for business readers. A verification program can improve coverage without becoming complete. A compliance pipeline can reduce risk without becoming an oracle. A safety case can be rigorous without pretending that every valid future behavior is already capturable inside one finite formal system.
The paper’s evidence is a proof, not an experiment pretending to be one
There are no benchmark tables in this paper. No ablation study. No “our verifier improves safety by 7.3% on a suspiciously named dataset.” That is not a defect. The paper’s contribution is theoretical.
The supporting components have different roles:
| Component in the paper | Likely purpose | What it supports | What it does not prove |
|---|---|---|---|
| Encoding $x=\langle z,y,\Pi\rangle$ | Problem formulation | Turns AI policy compliance into a statement about finite strings | Does not capture every messy institutional meaning of safety |
| Richness assumption | Structural condition | Ensures compliant instances can include high-complexity cases | Does not show every policy domain satisfies the assumption |
| Counting lemma | Main proof support | Shows enough compliant strings imply some are incompressible | Does not identify which real-world instances are high complexity |
| Incompleteness theorem | Main result | Separates truth from provability for fixed verifiers | Does not rank existing verification tools |
| Appendix proof | Formal support, not a second thesis | Supplies the contradiction argument in full | Does not add an empirical validation layer |
| Figure 1 | Conceptual architecture diagram | Shows the shift from fixed checking to proof-carrying acceptance | Does not demonstrate deployed system performance |
This matters because theoretical papers are often misused in two opposite ways. One camp treats them as irrelevant because they do not contain empirical charts. The other camp turns them into metaphysical doom posters. Both readings are lazy, though in different fonts.
The right reading is narrower and stronger: under the paper’s formal assumptions, complete policy verification by any fixed sound computably enumerable verifier is impossible for arbitrarily high-complexity compliant instances. That is a clean theoretical result. Its business value lies in how it changes system architecture expectations.
The design shift is from global detection to proof-carrying outputs
The paper’s practical recommendation is not “give up on verification.” It is almost the opposite. It says verification should become more local, more structured, and more explicit.
Instead of asking a fixed verifier to characterize all valid behaviors globally, the paper points toward proof-carrying approaches. The instance is augmented:
where $\pi$ is a proof that the instance satisfies the policy. Verification then becomes checking the proof, not rediscovering the entire space of valid behavior.
This is the architectural hinge of the paper.
In a detection-based model, the system tries to decide whether an output belongs to the global set of valid behaviors. In a proof-carrying model, the output arrives with evidence that can be checked against a specified policy. That evidence may be a formal proof, a certificate, a constraint satisfaction witness, or a cryptographic proof artifact depending on the domain.
The operational shift looks like this:
| System layer | Global-verifier mindset | Instance-certificate mindset |
|---|---|---|
| Model output | Produce an answer or action | Produce an answer or action plus structured evidence |
| Policy layer | Try to define all acceptable behaviors in advance | Define what evidence must establish for each case |
| Verification layer | Search or infer compliance | Check the supplied certificate |
| Failure mode | “Unsafe” and “uncertified” blur together | “Rejected,” “unknown,” and “invalid proof” can be separated |
| Audit trail | Often reconstructed after the fact | Built into the output protocol |
The distinction between reject and unknown is not cosmetic. In regulated environments, an uncertified action is not necessarily wrong; it is operationally unusable until supported. That changes escalation design. A healthcare decision-support system may route uncertified recommendations to human review. A financial compliance agent may require additional evidence before execution. An autonomous system may fall back to conservative control when proof generation fails.
The paper’s Figure 1 captures this split. A fixed verifier checking $P(x)$ may route an instance to “Not Certified,” while a proof generator can attach $\pi$ and allow a proof-checking path toward acceptance. The figure is not empirical evidence. It is a design diagram: validity alone is not enough; certifiable evidence must become part of the system interface.
What this means for safety-critical AI procurement
For companies buying or building AI systems, the paper pushes against a dangerous procurement habit: asking vendors whether their system is “verified” as though verification were a blanket property.
A better procurement question is more annoying, therefore more useful:
For which classes of outputs, under which policy encoding, with which certificate format, can the system provide checkable instance-level evidence?
That question forces the architecture into the open. It asks what is being verified, what counts as proof, how failures are represented, and whether the system can distinguish between a false output, an unsupported output, and a policy boundary case.
The ROI is not magic safety. The ROI is better allocation of trust.
A proof-carrying architecture can reduce the cost of auditing high-stakes outputs because evidence is generated at the point of action. It can reduce ambiguity in incident review because the system records which policy, proof, and verifier were involved. It can also support selective automation: actions with valid certificates may proceed automatically, while uncertified cases are escalated.
That is the grown-up version of AI assurance. Less slogan, more plumbing.
| Business need | Design implication from the paper | Practical question |
|---|---|---|
| Automating regulated workflows | Do not rely only on global policy filters | What proof or certificate accompanies each automated decision? |
| Deploying autonomous agents | Treat “not certified” as a first-class state | What does the agent do when proof generation fails? |
| Auditing safety-critical outputs | Preserve instance-level evidence | Can an auditor replay the policy, proof, and verifier result? |
| Scaling compliance | Separate proof generation from proof checking | Which checks are lightweight enough to run continuously? |
| Vendor evaluation | Avoid claims of universal verification | What exact behavior class is covered, and what remains unknown? |
The commercial lesson is not that every AI workflow needs zk-SNARKs stapled to it. That would be one way to convert theoretical insight into procurement theater. The lesson is that assurance architecture should be explicit about where correctness is proven, where it is merely tested, and where the system must return “unknown” instead of improvising confidence.
Governance becomes procedural, not absolute
The paper also has a regulatory implication, although it should be stated carefully. It does not prove that regulation is futile. It does not prove that safety standards are impossible. It does not give anyone permission to shrug and deploy chaos under the banner of incompleteness. That move is popular among people who enjoy conclusions that remove their responsibilities.
What the paper does suggest is that a standard requiring complete verification of all safe behaviors is the wrong target. Governance should focus on procedures that manage certifiability:
- define policy encodings for specific operational domains;
- specify acceptable certificate formats;
- require systems to expose proof-checking outcomes;
- distinguish certified, rejected, and unknown cases;
- log the instance, policy, proof artifact, verifier version, and fallback action.
This is less elegant than saying “the AI is safe.” It is also more auditable.
In practice, this means AI governance will likely resemble safety-case management and protocol assurance more than one-time model certification. A model may be approved for a domain, but individual outputs in high-stakes contexts still require local evidence. The system is not trusted because it belongs to a certified model family. It is trusted, within a defined boundary, because this output in this context carries checkable support.
The phrase “within a defined boundary” is doing real work. Without it, verification language becomes marketing mist.
The boundary: this theorem is powerful, but not a product review
The paper’s result is formal, and formal results bring formal boundaries.
First, the theorem depends on the modeling choice that AI interactions can be encoded as finite strings and policy compliance can be expressed as a predicate. That is a useful abstraction for formal verification, but it does not automatically resolve vague human concepts such as fairness, appropriateness, dignity, or business reasonableness. Some policies are not naturally clean predicates until an organization does the hard work of specification.
Second, the result assumes richness: the compliant instance space is large enough to contain high-complexity strings. This is plausible for many perception-driven, environment-dependent, or agentic systems. It may be less central for narrow workflows where the valid action space is tiny, heavily templated, or intentionally constrained.
Third, the theorem applies to fixed sound computably enumerable verifiers. Changing the verifier can change what is certifiable. Expanding the proof system can improve coverage. The point is not that all verifiers are equally weak. The point is that no fixed verifier becomes universally complete over arbitrarily high-complexity compliant instances.
Fourth, the paper does not empirically compare formal verification tools, proof systems, safety filters, or governance frameworks. It provides a theoretical foundation for why proof-carrying and certificate-based designs are attractive. It does not tell a CTO which vendor to buy. A rare mercy, perhaps.
Finally, the theorem does not make testing useless. Statistical validation, simulation, red teaming, formal checking, runtime monitoring, and human review still matter. They answer different questions. Testing estimates behavior across sampled cases. Formal verification proves specified properties where possible. Instance certificates provide checkable local evidence. A mature assurance stack uses all three without pretending they are the same instrument.
The practical framework: certify what can be carried, escalate what cannot
A business-facing architecture inspired by the paper would not ask for impossible completeness. It would divide outputs into operational states:
| Output state | Meaning | Action |
|---|---|---|
| Certified | The output has a valid certificate under the relevant policy and verifier | Allow automated execution within the approved scope |
| Rejected | The certificate is invalid or the policy is violated | Block, repair, or regenerate |
| Unknown | The system cannot produce acceptable evidence | Escalate, defer, or fall back to a conservative pathway |
| Out of scope | No policy encoding or certificate protocol applies | Human handling or separate governance process |
This framework is intentionally procedural. It does not promise that every safe action will be certified. In fact, the paper tells us not to expect that. Instead, it creates a disciplined path for deciding what to do when certifiability fails.
That is the difference between safety engineering and safety branding.
The branding version says, “Our AI is verified.” The engineering version says, “For this class of outputs, under this policy encoding, this certificate was checked by this verifier, and uncertified cases follow this fallback path.” One fits on a slide. The other survives an audit.
The proof is in the instance
The paper’s main contribution is not another verification algorithm. It is a change in what verification should be expected to accomplish.
A fixed verifier can be useful. It can be rigorous. It can be necessary. But it cannot be a complete oracle over all true high-complexity policy-compliant behavior. Once the space of valid instances becomes rich enough, truth and provability diverge. Some safe behaviors will not be certifiable within the chosen formal system.
That sounds like bad news only if the goal was omniscience. For anyone building real systems, it is more useful than that. It tells us where to stop wasting energy.
The design target should not be a single verifier that knows every safe behavior in advance. The target should be an assurance protocol in which important outputs carry instance-specific evidence, proof checking is explicit, uncertified cases are handled honestly, and governance records what was certified rather than what everyone hoped was true.
Universal verification is a beautiful idea. It is also, under the paper’s assumptions, not available.
So the proof has to travel with the instance.
Cognaptus: Automate the Present, Incubate the Future.
-
Munawar Hasan, “Incompleteness of AI Safety Verification via Kolmogorov Complexity,” arXiv:2604.04876v1, 2026, https://arxiv.org/abs/2604.04876. ↩︎