How checks fail
A check can fail to establish its intended property because of what it observes, what it can express, where it sits in the execution path, what it assumes, and what its oracle actually distinguishes. 9 recurring mechanisms, across proof, testing, evaluation and audit. None of them is new. What is useful is having them named, so a check can be held against the list.
Seven are grounded in public repositories, one is self-documented, and one is stated without an instance and labelled as such rather than illustrated with a borrowed example. Where a finding on this site is an instance of a mechanism, it is linked from the mechanism.
Three of the mechanisms, drawn
Position: a monitor beside the action records intentions that read as outcomes.
Observation boundary: mediation held on the authorised operation; the executed one was a different object.
Faithfulness and expressibility: the properties written from the specification pass; the requirement they were meant to stand for was never stated.
What the instrument observes, expresses and assumes
Expressibility failure
The formalism cannot state the property; the verdict is indistinguishable from an honest negative.
Detected by. Enumerate the expressible properties before selecting a formalism; record the rest as not-applicable.
In full
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.
Instance. capctl-iris, SCOPE.md, Floor E (per_key_misses_tight_global_bound)
- MEASURED Blind to the pool, the budget was breached in 60 of 60 episodes on each of three models with no agent over its own allowance. With the pool state shown the budget was still breached on every model, at rates that differ by model; the per-cell counts, including episodes where an agent exceeded its own allowance, are in the table on the collective-bound page.
- PROVEN Six agents each inside a cap of 10 breach a pool of 40; a single rule on the sum removes every such breach, while a harm equal to one agent's draw (threshold 15, below the pool) escapes it and a per-recipient cap closes it.
Faithfulness failure
The formalism states a property, and it is not the one intended; the check is valid and the theorem is wrong.
Detected by. Validate the instrument against known-answer cases before reading its output as evidence, including a positive control the check is known to pass.
In full
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.
Instance. evidence_witness.py:262 (v0.3), self-documented first-person in the grader's migration note ('Defect 1'). SELF-DOCUMENTED, its repository is not yet public, so it is not reproducible from a public clone until the grader is published.
- OBSERVED An agent was limited to 4 KB. It wrote 100 KB. Every test passed, an independent replay verifier said VERIFIED, and a checked invariant held.
- OBSERVED Two injected hardware defects passed every property written from the original specification, because the specification never stated the requirement they break.
- OBSERVED A battery model ran to completion on every revision tested and lost 2.4% of its lithium. Independent inventory accounting localised the loss to one equation, and a project contributor confirmed the missing term.
Wrong observation boundary
The instrument observes a surface where the behaviour does not occur.
Detected by. Compare the declared surface against the reachable surface directly.
In full
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.
Instance. mcp-boundary-audit (demonstrated against an authored mock server, not a field measurement)
- MEASURED A dashboard reported 1,026 actions prevented. All 1,026 had already executed.
- OBSERVED Tools removed from the list an agent is shown were still there to call by name.
- OBSERVED A convincing-looking Unreal validator was rejected because it reconstructed transforms from the source CSV instead of observing instantiated geometry. Three planted geometry corruptions left its result byte-identical.
Self-certification
The artifact vouches for itself; agreement with a function of its own inputs carries no independent information.
Detected by. Identify what would have to be corrupted for the check to pass falsely; if it is inside the artifact, there is no independent anchor.
In full
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.
Instance. evaltrust, README.md:107-108
Missing provenance
The result is real and cannot be tied to what produced it.
Detected by. Re-derive the claimed output from recorded inputs, not just recheck integrity.
In full
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.
Instance. UNGROUNDED IN PUBLIC, no publicly reproducible failure instance; stated as mechanism and detection only, no instance borrowed
What is concluded from a result
Coverage illusion
A passing suite is read as the absence of failure.
Detected by. Negative controls that must actually fire.
In full
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.
Instance. compositional-temporal-safety, Negative.lean (4 controls); escrow-budget (4 controls); nanogpt-provenance (12 controls)
- OBSERVED A program passed all 24 of its recorded tests and still accepted a permission record that had never been issued.
- OBSERVED Three green verification runs could not have failed: an unreached assertion, a model checker that instrumented nothing, and an axiom audit identical for correct and wrong models.
- OBSERVED A local language-model worker emptied a 415-line module to two lines. The repository’s 24 tests still passed. An independent syntax-tree gate, in series before any merge, rejected the patch.
- OBSERVED An error-correcting decoder in an open hardware library declared a syndrome output that nothing drove. A cover requirement added while proving the encoder and decoder pair found it; the one-line fix and the proof were reviewed and merged by the maintainer.
- OBSERVED A three-phase power-flow solver reported convergence for four transformer types it does not support, returning bus voltages near a million per unit with no warning. Ten other unsupported types were correctly rejected.
Worked example
A system passed all 24 of its recorded tests and still had a serious flaw. Passing everything you checked is not the same as checking everything that matters.
Convergence mistaken for correctness
Independent methods agree, and agreement is read as truth.
Detected by. Score each method against known-answer cases separately before comparing them to each other.
In full
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.
Instance. compositional-temporal-safety, impl/test_model.py:6
Complementary read as confirmatory
Two methods establish different properties and the reader infers corroboration.
Detected by. A properties by methods table with an explicit NOT APPLICABLE cell; the empty cells are the finding.
In full
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.
Instance. escrow-budget-mpst @ 59bbc08, COMPARISON.md (the NOT APPLICABLE cells); escrow-budget, CLAIMS-AUDIT.md:21
The same list, held against this site
The generator that builds these pages derives every count and halts on a bad denominator; a publication audit runs in series and is exercised by 25 injected leak classes; the build gates are exercised by mutations that must make the build fail. That is coverage illusion (§10.7) and self-certification (§10.5) applied to the site's own claims, and it is described on the method page.