How checks fail

Expressibility failure

The formalism cannot state the property; the verdict is indistinguishable from an honest negative.

In capctl-iris the per-key formalism proves each key stays within its own cap. It cannot state the tight bound across keys; per_key_misses_tight_global_bound is an explicit counterexample where every per-key check passes and the aggregate exceeds the intended global limit. The formalism returns no error because it cannot pose the question. A missing capability reads the same as a satisfied one.

Detection. Enumerate the expressible properties before selecting a formalism; record the rest as not-applicable.

Faithfulness failure

The formalism states a property, and it is not the one intended; the check is valid and the theorem is wrong.

An early evidence grader graded a record ASSERTED, read as “a bare claim, nothing to recompute”, whenever the record carried no integrity hash. The code branched to ASSERTED the moment the hash field was absent and returned, before any re-derivation ran. The trigger condition was “no integrity hash present”; the reported verdict was about re-derivability. Those are different propositions. The instrument’s implemented test never matched the property it reported, and a null result was read as a fact about the world when it was a fact about the method.

What would have caught it was a positive control: a single known-answer case where re-derivation was known to succeed. That case would have returned ASSERTED and exposed the mismatch on contact. There was none.

This instance is self-documented and first-person, recorded in the grader’s own migration note before publication. Its repository is not yet public, so a reader cannot reproduce it from a public clone until the grader is published; it is shown here as a documented account, not a publicly reproducible one.

Detection. Validate the instrument against known-answer cases before reading its output as evidence, including a positive control the check is known to pass.

Wrong observation boundary

The instrument observes a surface where the behaviour does not occur.

An authorisation check that reads a server’s advertised tool list sees the tools the server chooses to declare. The behaviour that matters, what can actually be called, happens on a different surface. mcp-boundary-audit demonstrates the gap on a mock server built to exhibit it: a tool filtered out of the listing is still reachable through the call path. The check on the declared surface passes; the reachable surface is where the action is. The measurement is a demonstration of the mechanism, not a survey of real servers.

Detection. Compare the declared surface against the reachable surface directly.

Hidden trusted base

Something unexamined is load-bearing and unnamed.

A machine-checked proof reports what it depends on only if you ask it. The OMEGA tamper-evidence theorems hold relative to an opaque compute_hash, the proof does not establish that this function is SHA-256, and the vsf-cjson round-trip theorem is true of a hand-written specification whose faithfulness to the C parser is argued, not proven. Neither is a defect; both are load-bearing assumptions. The failure is leaving them unnamed. #print axioms and an explicit trusted-base line make the dependency visible next to the result.

Detection. Enumerate axioms and dependencies mechanically, and publish them beside the claim.

Self-certification

The artifact vouches for itself; agreement with a function of its own inputs carries no independent information.

In evaltrust two of the three judge models also produced answers in the graded set. When such a judge agrees with the answer, part of what is measured is the model agreeing with itself. The agreement is real; it is just not independent of the thing being checked. An anchor outside the artifact. An objective key, an independent grader, is what breaks the symmetry. Re-deriving a value from the producer’s own inputs and finding it matches is the same shape: self-consistency, not corroboration.

Detection. Identify what would have to be corrupted for the check to pass falsely; if it is inside the artifact, there is no independent anchor.

Missing provenance

The result is real and cannot be tied to what produced it.

A record can be intact and still not be tied to what produced it: an integrity check confirms the bytes are unchanged, not that they follow from the recorded inputs. The detection method is to re-derive the claimed output from the recorded inputs rather than recheck a stored hash, and where that re-derivation cannot be reproduced. A different numeric environment, an input no longer available, the honest verdict is UNKNOWN, not verified. Detection power ends exactly where re-derivation from inputs ends.

This mechanism is stated without a worked instance, UNGROUNDED IN PUBLIC. Unlike the other eight, it has no publicly reproducible failure case here. The clean example would be an intact record that cannot be tied to its inputs, and the artifact that would exhibit it is not published, so it cannot be reproduced from a public clone. It is given as mechanism and detection only, rather than borrow an instance from a different artifact.

Detection. Re-derive the claimed output from recorded inputs, not just recheck integrity.

Coverage illusion

A passing suite is read as the absence of failure.

A green suite shows the cases you wrote passed, not that the cases you did not write would. compositional-temporal-safety, escrow-budget and nanogpt-provenance each ship negative controls: remove a budget guard and a theorem must now fail; forge a loss under a foreign environment and the verdict must drop. A control that cannot fail proves nothing about the check; a suite of only-passing tests measures its own coverage, not the property.

Detection. Negative controls that must actually fire.

Convergence mistaken for correctness

Independent methods agree, and agreement is read as truth.

compositional-temporal-safety computes a reachable state count in Python and checks it equals the recorded model-checker count. The two agree, at one bounded configuration, against a stored constant, without re-running the model checker. The repository labels it bounded agreement, not a refinement, and does not read the match as proof that the models coincide. Two methods that agree can be wrong in the same way; agreement is evidence only once each has been scored against a known answer on its own.

Detection. Score each method against known-answer cases separately before comparing them to each other.

Complementary read as confirmatory

Two methods establish different properties and the reader infers corroboration.

escrow-budget was verified two ways. A Lean proof establishes the budget bound, total spend stays within the cap. A separate method, multiparty session types with crash-stop in Rust, establishes the communication skeleton: deadlock-freedom, communication safety, progress. Laid out as a properties-by-methods table, the informative cells are the ones marked NOT APPLICABLE. The session types cannot express the budget bound at all. They range over the order and typing of messages, not arithmetic over aggregate state, and the action that consumes budget sends no message, so it is invisible to the type. The Lean model cannot express communication safety. It has no typed-channel layer where a reception mismatch is even statable. Reading “verified under both Lean and session types” as a second confirmation of the cap theorem would be false: the session-type method never touches the cap theorem. Two green methods, different properties; the empty cells are the finding, not the corroboration a reader supplies to fill them.

Detection. A properties by methods table with an explicit NOT APPLICABLE cell; the empty cells are the finding.