Every tool here answers one narrow question exactly, and refuses the rest. This page is about where that line falls — because the most expensive mistake with a verifier is not disbelieving a correct result, it is believing a result that means less than you think.
Finding a proof is hard. Checking one is easy. That asymmetry is the whole design: the thing that produces a proof can be a solver, a model, a stranger, or a program you would never run in production, because the checker re-derives the claim from scratch and needs to trust nothing the producer says.
A Farkas certificate is what makes the checking part small. To show that a guard implies a safety property, you show the opposite is impossible: assume the guard holds and safety fails, and exhibit nonnegative weights that combine those assumptions into an arithmetic contradiction — every variable cancels, and an impossible constant is left over. Verifying that is multiplication and addition. There is no search in it, no solver, and no floating point.
domain: 0 <= payload <= 65535
guard: 19 + payload <= record_len
safety: 3 + payload <= record_len
obligation: domain AND guard AND NOT(safety) <- must be impossible
weights: 1 x guard, 1 x NOT(safety) <- payload and record_len cancel; 16 > 0 remains
A checker that read the atoms out of the certificate and verified the weights against those would be close to worthless: a certificate carrying an easy, unrelated system together with a perfectly valid refutation of it would pass, having proved nothing about your program. So the checker ignores every atom the certificate carries and rebuilds the obligation from the specification. The certificate may supply the weights and nothing else.
The certificate is separately bound to the spec by a fingerprint over its canonical bytes. That detects drift, stale files, and copy-paste. It is not a defence against a determined forger, who would simply recompute it over an edited spec. What stands between you and a bad guard is that the relations are short enough for a person to read — which is why the format keeps them short.
Every tool in this portfolio has a verdict that is neither pass nor fail.
| Tool | Third verdict | Meaning |
|---|---|---|
| certkit | UNVERIFIED | The arithmetic checked out but a required precondition was never established. No claim is being made. |
| crs-mcp | OUT_OF_SCOPE | The region is too large to decide by enumeration. No verdict was reached. |
| exploit-counter | is_sound = None | Undecided. __bool__ raises, so if decision: cannot quietly mean "sound". |
| soundnessbench | ABSTAIN | A correct answer. It costs decisiveness and never fails the soundness gate. |
These exist so that "I did not establish this" never has to be rounded to "fine". It is the single most load-bearing decision in the toolkit, and it is why a refusal here is never a disproof: failing to find a proof is not a proof of the negation. A tool that reported "REFUSED" as "your guard is broken" would be inventing a result in the other direction.
It means the relations you wrote imply each other. Nothing here reads your source. If the spec models the wrong check, or the right check in the wrong place, the certificate is a correct proof about a model that does not describe your code. This is the most common way to be wrong while holding a valid certificate, and no amount of arithmetic rigour touches it.
Atoms are relations over the mathematical integers and rationals. x + 1 > x is a
theorem here and false for a 32-bit int at INT_MAX. If the arithmetic
in your program wraps, saturates, or truncates, a proof here says nothing about that path. The
SMT-LIB scripts certkit export writes carry this warning in a comment, because a
solver will not tell you either.
CERTIFIED from crs-mcp is a statement about the integer box you
declared. Outside it, nothing was examined. The tools say this in the verdict text rather than in
a footnote, because a verdict is what gets pasted into a pull request.
exploit-counter reports how many states a guard admits that safety forbids. That is
a triggerability figure under uniform sampling over a declared region. It is not CVSS, not a
severity score, and not a claim that any counted state is reachable from an attacker's position,
let alone weaponisable.