Turn "we found no escapes" into an exact integer.
Try it now, no install: open the browser demo and press Load a forgery — the checker refuses it, client-side.
"We fuzzed it and found nothing" is unfalsifiable, and everyone in the room knows it. It is equally consistent with the guard is correct and we did not look hard enough. This package replaces that sentence with a number:
Weakening this guard admits exactly 509 states the safety property forbids — a per-draw hit probability of 0.0078, so a uniform fuzzer needs ~129 draws to find one.
pip install "exploit-counter@git+https://github.com/nickharris808/exploit-counter@main"Pre-release. The PyPI name is reserved and publication is imminent; until then the line above is the working install. It is tested in CI on Linux, macOS, and Windows.
The examples ship inside the package, so this works immediately after pip install — no repository
checkout needed:
exploit-counter demoexploit-counter demo -- CVE-2014-0160 (Heartbleed) shape
safety: 3 + payload <= record_len, payload in [0, 255]
sound (19 + p <= r)
over-acceptance: 0 of 65536 states
no state escapes; the guard is sound over this box
weakened (1 + p <= r)
over-acceptance: 509 of 65536 states
expected uniform draws to hit: 129
The weakened guard's gap is exactly counted, not estimated.
To count against your own spec:
exploit-counter count --spec my.spec.json --box payload=0:255,record_len=0:255heartbleed-weakened: over-acceptance = 509 state(s) [exact, exact]
domain volume: 65536
per-draw hit probability: 0.00776672
expected uniform draws to hit: 129
Exit code is 0 when over-acceptance is exactly zero and 1 otherwise, so this drops into CI as a
gate.
from certkit import atom
from exploit_counter import over_acceptance
domain = [atom({"p": -1}), atom({"p": 1}, -65535)] # 0 <= p <= 65535
guard = [atom({"p": 1, "r": -1}, 19)] # 19 + p <= r
safety = [atom({"p": 1, "r": -1}, 3)] # 3 + p <= r
box = {"p": (0, 65535), "r": (0, 65535)}
result = over_acceptance(domain, guard, safety, box)
print(result.exact) # 0
print(result.is_sound_guard) # True
print(result.expected_draws_to_hit()) # None -- unreachableEnumerate every variable except one, and close-form the last.
Once you fix integer values for all but one variable, each atom becomes a half-line on the remaining
target: c*target + rest {<,<=} 0 where rest is now constant. The intersection of half-lines is an
interval, and counting integer points in an interval is arithmetic, not search.
So the cost is the product of the enumerated ranges — and the counter closes the form over the widest variable, removing the largest factor. For a payload/record-length pair over 2^16 × 2^16, that is 65,536 interval computations instead of 2^32 point tests. The bundled test suite verifies this against brute-force enumeration on every shape small enough to enumerate.
The exact leg returns a refusal — not a zero — when the enumeration would exceed its cap. You then get a sound bracket instead of a point guess:
from exploit_counter import monte_carlo_count
approx = monte_carlo_count(atoms, box, n_samples=200_000, alpha=0.05)
print(approx.ci_low, approx.ci_high) # the true count lies inside, w.p. >= 95%The interval is Clopper-Pearson, deliberately, over the faster normal-approximation intervals. It is conservative in coverage: it over-covers, so the true count falls inside at least as often as the stated confidence. For a risk figure a decision depends on, over-covering is the correct direction to fail. A Wald interval is tighter and wrong near zero — exactly the regime a security count lives in.
The zero-hit case is handled exactly rather than reported as zero: 0 hits in n draws gives an
upper bound of 1 - (alpha/2)^(1/n). "We sampled and saw nothing" produces a real bound, not a claim
of absence.
Sampling is seeded and deterministic, so a published figure reproduces.
- Sampling cannot establish a zero.
is_sound_guardreturnsNone, notFalse, when only a bracket is available. Do not coerce it. - Multi-conjunct safety properties are upper-bounded, not exact. Regions may overlap; the counter sums them, which over-counts. Over-counting never reports a smaller attack surface than exists. The single-conjunct case — which is most real guards — is exact.
- This is a triggerability count under a uniform sampling model. It is not CVSS, not impact, and not a claim that any counted state is exploitable in the weaponised sense. It bounds reachability of a forbidden state, which is a floor on badness, not a severity score.
- The count is only as meaningful as the domain you declare. An unbounded variable has no finite
model count;
box_from_atomswill not invent bounds for you — it raisesUnboundedVariableErrorrather than quietly substituting a range you did not choose.
A zero can be earned by checking every point, or it can fall out of a box that had nowhere for a counterexample to be. Those are indistinguishable once printed, so the second kind is refused:
| Box | Refusal |
|---|---|
Every variable pinned, e.g. {"x": (0,0), "y": (0,0)} |
DegenerateBoxError — "no escapes" holds however unsound the guard is |
An inverted range, e.g. {"x": (10, 2)} |
InvertedBoxError — the box is empty |
| An atom naming an undeclared variable | UnknownVariableError, naming the variable |
| A variable no domain atom bounds | UnboundedVariableError, naming the side that is open |
All four subclass BoxError, which subclasses ValueError. Pass allow_degenerate=True to
over_acceptance if you genuinely mean to ask about a single point.
This is the fix for a real defect: box_from_atoms(["x","y"], []) used to return {"x": (0,0), "y": (0,0)}, and over_acceptance over that box then returned exact=0, is_sound_guard=True — a
confident soundness verdict for a guard nothing had examined.
| Function | Purpose |
|---|---|
over_acceptance(domain, guard, safety, box) |
how many states the guard wrongly admits |
count_conjunction(atoms, box) |
exact model count, or None if over the cap |
count_models(atoms, box) |
(exact, None) or (None, bracket) — never both |
monte_carlo_count(atoms, box) |
sampled count with a Clopper-Pearson bracket |
clopper_pearson(k, n, alpha) |
the exact binomial interval on its own |
box_from_atoms(vars, domain) |
derive integer bounds from single-variable atoms; raises if any is unbounded |
validate_box(box, atoms) |
refuse a box that cannot carry a verdict |
enumeration_cost(box) |
points actually enumerated, and the variable solved in closed form |
Atoms come from certkit, which also defines the certificate format and the
independent checker. The division is deliberate: certkit answers is this guard sound? and
exploit-counter answers if not, by exactly how much? They share one atom type so a spec written
for one works with the other unmodified.
pip install -e ".[dev]"
pytest71 tests. The exact leg is checked against brute-force enumeration on every shape small enough to enumerate — if the closed form and the enumeration disagree, the closed form is wrong. The Clopper-Pearson coverage property is verified by simulation rather than asserted.
tests/test_adversarial.py adds the differential and metamorphic layers: 400 random conjunctions
counted both by the closed form and by brute force, plus properties no correct counter may violate —
strengthening a guard must never increase over-acceptance, widening a box must never decrease it, and
renaming variables or permuting atoms must not move the number at all.
SCOPE.md |
what the number establishes, and what it does not |
| certkit's TUTORIAL | end-to-end worked example using both tools |
| certkit's TROUBLESHOOTING | every error string in the toolkit |
| certkit | the certificate format and the independent checker |
| exploit-counter | if a guard is unsound, exactly how many states escape |
| crs-mcp | the verdict surface AI coding agents call, over MCP |
| soundnessbench | the benchmark that grades all of the above |
| certkit-action | run the check in your CI |
| pytest-mutation-verified | prove your regression test can actually fail |
| cve-proof-corpus | six real CVEs with machine-checkable proofs |
| Try it in your browser | no install; watch a forgery get refused |
These packages are the checking half. They deliberately contain no proof search, which is what keeps them small enough to audit — and it means something upstream has to produce certificates.
For obligations over full machine-word domains, enumeration does not scale and a decision procedure that does not enumerate is required: solver-free elimination emitting replayable certificates. That engine, the repair synthesiser that derives a minimal guard from a refutation, and the evolutionary search that drives them are not in this repository and are available commercially.
The split is deliberate and permanent. The checker is free and always will be — a certificate you cannot independently verify is worth nothing, so charging for verification would defeat the format. What costs money is producing certificates at scale.
Apache-2.0.