The PQC Migration Toolkit¶
One fact reopens a decade of solved protocol bugs: post-quantum key material no longer fits in a single frame.
An X25519 share is 32 bytes. A category-3 post-quantum credential — ML-KEM public key, ciphertext, ML-DSA public key, signature — is 7,533 bytes, and becomes 20 fragments on an 802.11 management path.
That is not a quantitative change. It is a structural one. A receiver now holds attacker-influenced partial state before it can authenticate any of it. Every state-machine failure the industry closed over the last decade — downgrade binding, key reinstallation, fragment splicing — becomes reachable again on the ordinary path rather than in exotic configurations.
These eleven tools help you find out whether it has happened to you.
They find and measure. They do not repair.
Every tool here is a detector. Closing the 39 failure families is a separate proprietary codebase, and relevant subject matter is covered by a filed provisional patent application.
That split is measured, not asserted: under a replicate noise control only 4 of 32 repair mechanisms are externally distinguishable, so publishing these detectors does not disclose the repairs.
Start here¶
=== "I have five minutes"
```bash
pip install git+https://github.com/nickharris808/pqc-sizes
pqc-sizes credential --kem ML-KEM-768 --sig ML-DSA-65
pqc-sizes window --largest-object 7533 --budget 65536 --concurrency 4
```
Or [try it in a browser](https://huggingface.co/spaces/nickh007/pqc-explorer)
with no install at all.
=== "I have ten minutes"
The [**tutorial**](tutorial.md) walks one realistic migration end to end:
credential size → fragmentation → the reassembly window → a CI gate → the
39-family benchmark.
=== "I want the argument"
[**What this proves**](concepts.md) is the conceptual guide: why the cap has
*two* boundaries, why the interval can be empty, and — carefully — what none
of this establishes.
The one idea worth taking away¶
A reassembly cap has two boundaries, not one:
floor = the largest legitimate object you must accept
ceiling = memory budget ÷ worst-case concurrent contexts
Below the floor you reject honest peers. Above the ceiling, concurrent sessions exhaust your budget. If floor > ceiling, no cap works at all — and that is a design answer available before anyone writes code.
Most teams reach for a per-object bound. That is the wrong shape: exposure is retention × concurrency, not retention alone.
The eleven tools¶
Measure your configuration¶
| Tool | What it answers |
|---|---|
| pqc-sizes | How big is my credential, how many fragments, does a safe cap exist? |
| pqc-sizes-js | The same arithmetic for Node and the browser |
| pqc-explorer | The same, in a browser, with no install |
Put it in your pipeline¶
| Tool | What it does |
|---|---|
| pqc-guard-action | Fails the build when the window is empty |
| pqc-migration-mcp | Six MCP tools, so an agent computes instead of guessing |
Score your implementation¶
| Tool | What it does |
|---|---|
| pqc-mfb | 322 cases, 39 failure families, a scorer with three verdicts |
| pqc-mfb (data) | The benchmark as a Hugging Face dataset |
Check the claim yourself¶
The same memory bound, verified three independent ways — pick whichever you trust:
| Tool | Trusted base |
|---|---|
| pqc-bounds-lean | The Lean 4 kernel alone — 0 sorry, 0 imports, mathlib-free |
| pqc-dos-gate-rtl | Yosys k-induction over synthesizable RTL |
| farkas-check | 123 lines of integer C, on-device, no SMT solver |
| pqc-dos-embedded | 169 lines of C on emulated ARMv7-M |
Read the evidence¶
| Tool | What it is |
|---|---|
| pqc-formal-corpus | 122 named formal results across 6 prover dialects |
Why the redundancy is the point¶
The residency bound is checked in three independent systems — Lean, Yosys, and integer C — plus demonstrated on emulated silicon. Not because one of them is doubtful, but because a bound that only one toolchain believes is a bound you are trusting that toolchain for.
You do not have to accept any of it on authority. Every claim on this site is reproduced by running published code, and the numbers are asserted in CI.
Honesty commitments¶
These hold across every repository here:
- Every number is reproducible. A checker runs each documented command and diffs the output against the transcript. A stale number fails CI.
- When in doubt, refuse. Tools abstain rather than emit a confident answer
they cannot support.
farkas-checkreturnsREFUSEon arithmetic overflow;pqc-mfbreturnsINCOMPLETErather than passing a submission that answered nothing;pqc-sizes-jsthrows above 2^53 rather than losing precision silently. - What we do not prove is written down. Every repository has an Honest scope section naming its limits.
- Prior-art analogues are shapes, not disclosures. Where a case resembles a published failure, that is a pointer for the reader — never a claim about any vendor's product.