FAQ

Written from real objections, including the ones that are uncomfortable.

Is this just a marketing funnel for a proprietary product?

Partly, and it says so on every page. The tools detect; the repairs are a closed codebase covered by a filed provisional patent application.

What makes that honest rather than a bait-and-switch is that the split is measured: under a replicate noise control only 4 of 32 repair mechanisms are externally distinguishable, so publishing these detectors does not disclose the repairs. The free tools are complete and useful on their own — nothing is crippled to force an upgrade, and no tool reports a problem it cannot substantiate.

If you never contact anyone, pqc-sizes still tells you whether your window is empty, and pqc-bounds-lean still typechecks.

Why should I trust numbers from a vendor with something to sell?

You should not, which is why nothing asks you to. Every documented number is regenerated by running published code, a checker diffs each documented command against its real output, and CI fails on drift. The memory bound is verified in three independent systems so you can pick whichever you already trust.

The strongest signal is what the tools refuse to say. A vendor optimising for impressive output would not have shipped INCOMPLETE, ABSTAIN and REFUSE.

Is this a vulnerability disclosure? Are you saying product X is broken?

No, and deliberately not. Cases run against a modelled state machine, never captured from shipping products, and the ten unrepaired designs are constructed baselines. Where a case names a published failure of similar shape — KRACK, Dragonblood, FragAttacks — that is a pointer for the reader, not a claim of equivalence and not an assertion about anyone's implementation.

39 families sounds arbitrary. Where does it come from?

One sustained modelling effort, and the number is what that effort produced — not a claim about the field. A failure mode the model cannot express is simply absent, and absence says nothing about your protocol. That limit is stated in every scope section.

Why does the naive baseline PASS at 0% coverage?

Because PASS is the regression gate, not the score. The baseline answers every case honestly and breaks nothing, so it is complete and non-regressing — and useless, which its 0% coverage says plainly. Coverage is the number you report.

This confused people enough that the reference table now shows all three reference points side by side.

Why three verdicts instead of pass/fail?

Because two was wrong. passed was defined as "no regressions", so a submission of {} — answering nothing — scored PASS at 0% coverage with 312 unanswered cases. A vendor could have submitted an empty file and truthfully reported a passing run. Silence is not credit, so silence is now INCOMPLETE.

Why is a Lean proof useful if it does not describe my code?

It is not a proof about your code, and the repository says so. It proves the bound holds for the stated recurrence — which is worth having, because the alternative to a checked theorem is an unchecked belief. Whether your reassembly path refines that recurrence is a separate obligation nobody here discharges.

Why not just use an SMT solver?

For the offline proof, we do. The point of farkas-check is that you cannot ship a solver to a microcontroller — and if you could, you would have put a large, fast-moving dependency inside the thing you are trying to trust. Farkas' lemma removes the search: the expensive party finds the multipliers once, and 123 lines of integer C re-derive the conclusion on-device.

Why is nothing on PyPI?

Publication needs a browser step only the account owner can take. Trusted Publishing is configured and needs no stored token; the exact steps are in PUBLISHING.md. Meanwhile every install path in every README works today via git+https://, and no README claims otherwise.

Are these numbers stable? Will they change?

Data-derived numbers (322 cases, 39 families, 122 results, 7,533 bytes) are regenerated in CI and will only change if the data does. Toolchain-derived numbers are not claimed as fixed — the RTL cell count differs between Yosys releases, so only the flip-flop count is stated. Timing figures are not published at all, because they would be unreproducible on your hardware.

Can I use this commercially?

The tools are Apache-2.0 (the PQC-MFB dataset is CC-BY-4.0) — use them freely. The repairs are separate. For commercial use of the full envelope, open a GitHub Discussion or an issue.

How do I contribute?

See Contributing. Benchmark submissions are especially welcome, including ones that score badly — a leaderboard of perfect scores would tell nobody anything.