---
license: apache-2.0
task_categories:
- text-classification
- tabular-classification
tags:
- formal-methods
- theorem-proving
- post-quantum
- cryptography
- protocol-verification
pretty_name: "PQC Formal Corpus: named results from a post-quantum verification effort"
size_categories:
- n<1K
configs:
- config_name: default
data_files: src/pqc_formal_corpus/data/pqc_formal_corpus.jsonl
---
# pqc-formal-corpus
[](LICENSE)
[](src/pqc_formal_corpus/data/pqc_formal_corpus.jsonl)
[](DATASET_CARD.md)
[](https://github.com/nickharris808/pqc-formal-corpus/actions/workflows/ci.yml)
[](pyproject.toml)
**What does it actually take to formally verify a post-quantum handshake? Here are all 122 results, named.**
Theorems, lemmas, invariants and goals from one sustained multi-prover verification
effort — Lean, EasyCrypt, Tamarin, TLA+, CryptoVerif, Squirrel — in one queryable file.
**📖 Full documentation, tutorial and conceptual guide: **
---
## Verify this in ten minutes
**The claim.** 122 named formal results across 6 prover dialects (Lean, EasyCrypt, Tamarin, TLA+, CryptoVerif, Squirrel), each row carrying which prover carried it and what kind of obligation it was.
**The command that regenerates it.**
```sh
pip install -e . && pqc-corpus stats && pqc-corpus query --category resource-bound
```
**The negative control — run it first.** 4 rows are **controls** rather than safety properties, and `pqc-corpus query --polarity control` lists them. A corpus with no controls cannot tell you whether a prover run means anything.
**Pinned.** `0.1.0` (git tag `v0.1.0` = package version) · **License.** Apache-2.0 (`LICENSE`) · **Cite.** `CITATION.cff`
---
## Why this exists
Papers report *that* a protocol was verified. They rarely publish the shape of the work:
how many named results it took, which prover carried which burden, how many were controls
rather than properties.
That shape is useful. It tells you where verification effort actually goes, it gives a
third party a concrete re-derivation target list, and it is the sort of thing that is
tedious to reconstruct from a repository but trivial to publish once.
So: 122 rows, six dialects, one JSONL.
## Install
```bash
pip install git+https://github.com/nickharris808/pqc-formal-corpus
```
Not on PyPI yet. The dataset is also on the Hugging Face Hub, which needs no
install at all — see the usage snippet below.
Zero dependencies.
## 30-second quickstart
```python
from pqc_formal_corpus import load, by_prover, by_category
results = load()
len(results) # 122
by_prover(results) # where the effort went
```
## Worked example — actual output
```python
>>> from pqc_formal_corpus import load, by_prover
>>> results = load()
>>> len(results)
122
>>> by_prover(results)
{'cryptoverif': 1, 'easycrypt': 51, 'lean': 20, 'squirrel': 1, 'tamarin': 35, 'tla': 14}
>>> [r.name for r in results if r.category == "resource-bound"]
['bounded', 'bounded_at_canonical', 'naive_unbounded', 'separation',
'window_admits_and_bounded', 'window_nonempty']
>>> next(r for r in results if r.name == "bounded")
Result(prover='lean', name='bounded', kind='theorem', module='Bound',
category='resource-bound', polarity='bound')
```
**EasyCrypt carries 51 of 122** — that's where the computational reductions live. Tamarin
takes 35 symbolic results, Lean 20 machine-checked bounds. That distribution *is* the
finding.
## CLI
```bash
pqc-corpus stats # summary by prover and category
pqc-corpus query --prover lean --category resource-bound
pqc-corpus export --format csv -o corpus.csv # or jsonl, json, parquet
```
`--json` is global. Every unknown filter value lists the valid ones rather than
returning nothing.
## Schema
`prover` · `name` · `kind` · `module` · `category` · `polarity`
The first four are extracted verbatim. **`category` and `polarity` are heuristics derived
from the identifier string** — good for filtering, not ground truth. See
[`DATASET_CARD.md`](DATASET_CARD.md) for the full schema, provenance and limitations.
## What is not here
**No proof bodies, no tactic scripts, no model source.** A name plus its provenance is an
index; the mechanised argument stays closed, because several of these proofs encode repair
mechanisms directly. A test greps the shipped file for proof syntax and fails if any
appears.
**ProVerif contributes zero rows.** Its models are query-driven in a form this extractor
does not treat as named results — and its builtin `attacker` predicate was being extracted
as the sole "ProVerif result" until a denylist stopped it. That is disclosed as a real
limitation rather than papered over.
## Regenerate it
```bash
python -m pqc_formal_corpus.build \
src/pqc_formal_corpus/data/pqc_formal_corpus.jsonl
```
Output is sorted and byte-stable, so a regeneration that changes anything shows up as a
clean diff.
## Tests
```bash
pip install -e ".[dev]" && pytest # 66 passed
```
Tests cover shape, uniqueness, the builtin denylist, the moat boundary, heuristic
behaviour on known names, and that the data ships **inside** the wheel rather than beside
it.
## Scope
An index of what one effort named. **Not the proofs**, not a benchmark, not a completeness
claim — a property nobody named is simply absent, and absence here says nothing about the
protocol.
## Related
[`pqc-mfb`](https://github.com/nickharris808/pqc-mfb) (a scorable benchmark) ·
[`pqc-sizes`](https://github.com/nickharris808/pqc-sizes) · [`farkas-check`](https://github.com/nickharris808/farkas-check) (one of these bounds,
re-verifiable on-device)
This corpus names what was proven. The proofs, and the mechanisms they establish, are a
separate closed codebase.
Relevant subject matter is covered by a filed provisional patent application.
For commercial use, open a [GitHub Discussion](https://github.com/nickharris808) or an issue.
## Honest scope
**What this proves.** That one sustained verification effort named these 122
results, in these six prover dialects, in these modules. `prover`, `name`, `kind`
and `module` are extracted verbatim from the committed prover sources.
**What it does NOT prove.**
- **Not that the results are correct.** This is an index of *names*. The proofs
are not here, so nothing in this dataset can be checked against them. For a
development you can actually run, see
[`pqc-bounds-lean`](https://github.com/nickharris808/pqc-bounds-lean) — 20 of
these names live there, with 0 `sorry`.
- **Not ground truth for `category` and `polarity`.** Both are derived from the
identifier string alone by substring matching, never from the proof body. They
exist to make 122 rows browsable and are wrong often enough that you should not
build a claim on them. 15 rows land in `polarity: other` because their names
carry no signal the heuristic recognises.
- **Not complete.** Extraction is regex-based, so a result declared in an unusual
syntactic form is missed. ProVerif contributes **zero** rows for exactly this
reason — a real limitation, disclosed rather than papered over.
- **Not a benchmark.** No task, no split, no metric. For a scorable benchmark see
[`pqc-mfb`](https://github.com/nickharris808/pqc-mfb).
- **Not representative of the field.** One effort, one protocol family. That
EasyCrypt carries 51 of 122 reflects where this effort's computational proofs
live, not that EasyCrypt results matter more.
---
## The PQC migration toolkit
Eleven free tools for teams moving authenticated key exchange to post-quantum. They **find and measure**; they do not repair.
| Tool | What it does | Where |
|---|---|---|
| [pqc-sizes](https://github.com/nickharris808/pqc-sizes) | Sizes, fragment counts, and the two-sided reassembly window | source |
| [pqc-sizes-js](https://github.com/nickharris808/pqc-sizes-js) | The same arithmetic for Node and the browser | source |
| [pqc-guard-action](https://github.com/nickharris808/pqc-guard-action) | Fail the build when the window is empty | GitHub Action |
| [pqc-dos-embedded](https://github.com/nickharris808/pqc-dos-embedded) | 169 lines of C: the failure on a real 64 KB device | source |
| [farkas-check](https://github.com/nickharris808/farkas-check) | Re-verify the bound on-device, no SMT solver | source |
| [pqc-bounds-lean](https://github.com/nickharris808/pqc-bounds-lean) | The same bound in Lean 4 — 0 `sorry`, 0 imports | source |
| [pqc-dos-gate-rtl](https://github.com/nickharris808/pqc-dos-gate-rtl) | The gate in synthesizable RTL, 5 Yosys proofs | source |
| [pqc-migration-mcp](https://github.com/nickharris808/pqc-migration-mcp) | Six MCP tools for AI agents | source |
| [pqc-mfb](https://github.com/nickharris808/pqc-mfb) | 322 cases · 39 failure families · scorer | source |
| [pqc-mfb (data)](https://huggingface.co/datasets/nickh007/pqc-mfb) | The benchmark as a dataset | HF |
| **pqc-formal-corpus** ← you are here | 122 named formal results, 6 provers | HF |
| [pqc-explorer](https://huggingface.co/spaces/nickh007/pqc-explorer) | Try it in your browser, no install | HF Space |
**New here?** The [end-to-end tutorial](https://github.com/nickharris808/pqc-sizes/blob/main/TUTORIAL.md) walks one realistic migration through all of them in about ten minutes: sizes -> window -> CI gate -> benchmark.
**In a hurry?** [`pqc-sizes`](https://github.com/nickharris808/pqc-sizes) tells you in five seconds whether your credential fragments and whether a safe cap exists. [`pqc-explorer`](https://huggingface.co/spaces/nickh007/pqc-explorer) does the same in a browser, with no install.
### The closed core
Closing the 39 failure families — downgrade binding, retransmission-safe installation, fragmentation transcripts, roaming forward secrecy, multi-link key separation, admission control, group-key binding — is a separate proprietary codebase. 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.
For commercial licensing, open a [GitHub Discussion](https://github.com/nickharris808/pqc-sizes/discussions) or an issue on any of these repos.
## License
Apache-2.0. See [LICENSE](LICENSE), [CONTRIBUTING.md](CONTRIBUTING.md) and
[SECURITY.md](SECURITY.md).