Turn "we found no escapes" into an exact integer — or an honest refusal.
EXACT an exact integer count carries `count`
BOUNDED a sound interval + confidence carries `ci_low`/`ci_high` — and NO point estimate
REFUSED nothing was computed carries `reason`, and no numbers at all
A caller must never be able to consume an approximation as if it were an exact count.
Reading .count off a non-EXACT result raises. bool(), int() and float() on a
result all raise. There is no estimate key anywhere, in any verdict.
That is not a style preference. The bug it prevents was measured: an over-capacity query
once returned an estimate with no count key, so the natural
r.get("count", r.get("estimate")) # ← silently produced 1000000300000029966336handed back a Monte-Carlo point estimate where an exact count had been requested.
from exploit_counter import exact, refused, NotAnExactCount
r = refused("enumeration too large: 10^21 points")
r.verdict # 'REFUSED'
r.count # raises NotAnExactCount — there is no count to read
r.to_dict() # {'schema': 'crs/count/v1', 'verdict': 'REFUSED', 'reason': ..., 'scope': {}}
exact(65536).count # 65536
exact(65536).interval # (65536, 65536) — an exact count IS a degenerate intervalFull normative contract: CONTRACT.md. A 14-case conformance corpus ships
in conformance/ so you can prove your integration reads refusals correctly before you
trust it — python -m exploit_counter.conformance.
Check the contract before you trust it. The 14-case corpus is not a formality — it is a conformance suite you run against your integration to prove it reads a refusal as a refusal. Most numeric APIs give you no way to test that. This one fails loudly if you get it wrong.
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.
Counting the whole violating region to answer "is this guard sound?" is waste that grows with the
box. Deciding stops at the first escaping state, so it stays flat while counting does not
(python benchmarks/decide_vs_count.py, unsound guard 1 + payload <= record_len):
| box | volume | count | decide | factor |
|---|---|---|---|---|
0:255 |
65,536 | 0.15 ms | 0.0131 ms | 11x |
0:4095 |
16,777,216 | 2.29 ms | 0.0134 ms | 171x |
0:65535 |
4,294,967,296 | 36.72 ms | 0.0129 ms | 2,843x |
On a sound guard there is no difference at all, because the full enumeration is required either way. Timings are from one machine and will differ on yours; the shape is what the script exists to show. (An earlier version of this section quoted "286 ms versus 0.03 ms" without naming the box. After the integer fast path landed, no box reproduced it — which is why the numbers now come from a script you can run.)
from exploit_counter import decide_soundness
d = decide_soundness(domain, guard, safety, box)
d.is_sound # True, False, or None
d.witness # the escaping state, when there is oneis_sound is None — never True — when the box is above the cap, because a search that did not
run has established nothing. Decision refuses bool() outright, so if d: cannot silently come
to mean "sound".
Use over_acceptance when you want the magnitude; use this when you want the verdict.
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 |
decide_soundness(domain, guard, safety, box) |
is it sound — without counting how unsound |
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]"
pytest133 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.
CONTRACT.md and the shipped conformance corpus exist because of a specific failure, and the
history is here rather than at the top of the page: it is the reason for a design decision, not a
headline.
A downstream consumer needed exactly this capability and used the engine — but had to vendor a
copy, because our packaging shipped a distribution with no counter in it, and because importing
the standard-library-only counter dragged in numpy, scipy, matplotlib and Pillow. Both causes are
fixed. The contract had a second problem: it lived only in a private repository, so nobody outside
could read the rules their integration was supposed to follow. CONTRACT.md, the conformance
corpus, and the verdict section at the top of this README are that fix.
(An earlier version of this note claimed an adoption criterion had fired and that nobody had
adopted the engine. That was wrong and is withdrawn — the adoption predated the claim by three
weeks, with attribution in the consumer's own file header. Evidence: _ORCH/SPRINT_FINDINGS.md §1
in the origin repository.)
Apache-2.0 (LICENSE). If you use this in work you publish, there is machine-readable
citation metadata in CITATION.cff — GitHub's "Cite this repository" button reads it.
CONTRIBUTING.md— the house rules, and the one invariant a change must not break.ARCHITECTURE.md— the module map and where the trust boundary sits.TROUBLESHOOTING.md— keyed to the error messages this actually prints.SECURITY.md— a checker that accepts something false is the highest severity class here.
Part of certified discovery — ten artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted.