Part VI
The certificate that means nothing
Verification is supposed to end the argument. The model checker ran, the property holds, here is the certificate. Downstream consumers stop checking, which is the point — that is the entire economic case for formal methods.
So follow the risk. It did not disappear. Verification moved it, and it moved it onto the one artifact in the pipeline that nobody reads carefully: the specification.
Everything else gets attention. The implementation is reviewed. The proof is machine-checked. The tool is trusted, tested, and widely used. The specification is written once, usually by one person, usually early, usually in a hurry, and then it is never looked at again — because once the property passes, why would you.
The classic failure
Passing vacuously
Most real safety properties have a guarded shape: whenever this condition occurs, this response must follow. G(condition → response).
Implication is generous. If the antecedent never fires, the implication is satisfied — trivially, universally, and for reasons that have nothing to do with the response ever happening. The property passes. The certificate is valid. And the property constrained nothing at all.
The Accidental Version
An autonomy safety case specifies that when the perception system classifies an obstacle, the planner must brake. A perception failure that prevents the classification from ever firing renders the entire property vacuously true.
The Adversarial Version
Writes the specification so this happens on purpose. The property reads correctly in natural language. Anyone reviewing it in English nods. The antecedent is unreachable in the target, so it passes.
The part that should be embarrassing
We have had detection for this for twenty-five years
Hardware verification identified this in the late 1990s and built detection for it. There is a real literature on vacuity and coverage, with working algorithms that determine whether a property passed for interesting reasons rather than by degenerate satisfaction. It is mature. It is well understood. It is taught.
It is also off by default in most verification workflows and effectively unknown outside the hardware-verification community.
I want to be precise about what is new here, because "we found an attack" is not the right claim when a discipline has had the phenomenon named and solved for a quarter century. The mechanism is not new. What the adversarial framing changes is the category of control:
Vacuity detection has been treated as a specification-quality tool — something that catches sloppiness. Read adversarially it is a security control, because a vacuous pass is a valid certificate for a meaningless property, and every integrity check in the pipeline passes it.
That reframe matters operationally. Quality controls are optional and get skipped under deadline. Security controls get budget lines and audit findings. Same algorithm, different governance.
And the genuinely open piece is a measurement nobody has published: what are the vacuity rates in deployed specification sets, and how often is detection actually run? Public hardware verification suites, published kernel property sets, autonomy safety cases where they are available. Run the existing tooling. Report the rate. I would predict nonzero vacuity and detection almost never enabled by default, but that is a prediction, and the appeal of this particular study is that it uses tools that already exist and would take weeks rather than years.
The same shape, one layer up
Semantic tolerance is the differential
Now the version of this problem that most readers will actually meet, because it does not involve a proof assistant at all.
Language-model policy engines are useful precisely because they are tolerant. Cancel my subscription, I'd like to stop my membership, please close out my plan — all recognized as one request. That tolerance is the product. It is why people build these things.
A parser that accepts multiple surface forms as equivalent is, by definition, a parser with a differential relative to a stricter parser. That is not an analogy to a parser differential. It is the definition of one.
So the shape from the vacuity case repeats. The policy layer authorizes a natural-language description of an action. The runtime executes a structured call. Those are two different representations, adjudicated by two different parsers, and the entire history of security engineering says the gap between two representations of the same thing is where the exploits live. The policy engine approves what it understood. The system does what it parsed. When those diverge you have a confused deputy with an audit log that says the request was approved — because it was.
There is a nice theoretical statement of this. Type theory has an axiom saying that isomorphic structures may be identified — that things which are structurally the same are the same. It is a reasonable foundational principle and it is the exact formal statement of the assumption that every parser-differential vulnerability violates. Security engineering lives entirely in the semantic gap between representations that mathematics is happy to identify.
Policy decisions must bind to the executed representation, not to the described one. Authorize the structured call. Log the structured call. If the natural-language layer is doing the authorizing, you have built a system where the thing approved and the thing done are related by a model's interpretation, and interpretation is not an access-control primitive.
The third one
A reachability oracle is the solver
One more, briefly, because it comes up constantly in agentic tooling and is almost never recognised.
Teams expose "cheap" query interfaces — feasibility checks, satisfiability endpoints, "is this reachable" APIs — on the reasoning that they only return a bit and therefore leak almost nothing. The reasoning is wrong. In a deterministic search setting, a reachability signal is the optimal value function. Exposing it exposes the solver, because a caller can descend greedily on that signal and reconstruct the solution in roughly depth × branching-factor queries rather than searching the space.
The rule that follows: capability-scope your oracles separately from your answers. A yes/no endpoint over a search space is not a smaller version of the full endpoint. It is the same endpoint with more round trips.
Monday
Four checks
If you run a model checker anywhere in your pipeline, this is a flag. Run it on your existing property set before you write another property. The results are usually instructive and occasionally alarming.
Your implementation gets code review. Your specification probably does not get reviewed at all after it is written. For each guarded property, ask one question: can the antecedent actually fire in the target? That question catches both the accidental and the deliberate case.
Audit every place where a natural-language layer authorizes an action that a structured layer performs. Move the authorization decision to the structured representation. If you cannot, log both and alert on divergence — that is a weaker control but it is not nothing, and the divergence rate is worth knowing.
Any endpoint that returns a feasibility, reachability, or satisfiability bit over a search space should be rate-limited and scoped as though it returned the full answer, because with enough queries it does.
Next episode goes after the assumption that makes most defensive architectures look better on paper than they are: that when you stack four controls, you get four controls.
