CLI and API reference

Every command is verified by the doc checker; every exit code is asserted by a test.

Exit codes, portfolio-wide

The same three meanings everywhere. A CI gate must be able to tell "your design is unsafe" from "you typed the flag wrong", and neither from success.

Code	Meaning
0	the check ran and the answer is good
1	the check ran and the answer is bad — a real finding
2	the invocation was wrong (bad flag, missing file, unknown name)
3	the tool refused or abstained — it could not earn an answer

---

pqc-sizes

Command	What it does	Exit
sizes [--kind KEM\|signature]	The algorithm table	0
credential --kem K --sig S	Credential bytes, component by component	0
fragments TRANSPORT --kem K --sig S	Fragment count on a transport	0
fragments TRANSPORT --bytes N	Same, for a raw object size	0
window --largest-object N --budget N --concurrency N	Does a safe cap exist?	0 / 1
sweep --largest-object N --budget N --max-concurrency N	Where the window collapses	0
budget (--kem K --sig S \| --largest-object N) --concurrency N	How much memory do N contexts need?	0
check CONFIG [--format sarif]	Gate on a committed JSON/YAML config	0 / 1

--json is global and precedes the subcommand: pqc-sizes --json window ….

Library

from pqc_sizes import (
    ALGORITHMS, TRANSPORTS, Credential, Window,
    credential_bytes, fragments_for, max_concurrent_contexts, reassembly_window,
)

credential_bytes("ML-KEM-768", "ML-DSA-65")   # 7533
fragments_for(7533, 384)                      # 20
win = reassembly_window(12000, 32768, 3)
win.is_empty                                  # True
win.explain()                                 # one unbroken sentence
win.admits(10000)                             # False
max_concurrent_contexts(12000, 32768)         # 2

Window.explain() deliberately returns a single unbroken string — the MCP server embeds it in JSON and the Action in an annotation, neither of which wants hard line breaks. Wrapping is the CLI's job.

---

pqc-mfb

Command	What it does	Exit
info	Case, failure, family and design counts	0
cases [--family F] [--design D] [--failures-only]	List cases	0
explain FAMILY	What breaks in one family	0 / 2
submit [-o FILE] [--fill baseline\|true\|false]	Write a complete submission template	0
score FILE [--format sarif\|junit] [-o FILE]	Score a submission	0 / 1 / 3
score --baseline naive\|perfect	Score a built-in reference	0
diff BEFORE AFTER	What a release closed and what it broke	0 / 1

Verdicts

Verdict	Meaning	Exit
PASS	every failure case answered, nothing regressed	0
FAIL	at least one regression — whatever the coverage	1
INCOMPLETE	at least one case unanswered, so no pass is claimed	3

Library

from pqc_mfb import (
    Case, Family, Score, families, load_cases,
    score_submission, sarif_report, junit_report, to_dataframe,
)

cases  = load_cases()                 # list[Case], cached per file
tax    = families(cases)              # list[Family], cached per corpus
score  = score_submission(sub, cases) # Score, with .verdict
df     = to_dataframe(cases)          # pandas, if installed

---

pqc-corpus

Command	What it does	Exit
stats	Summary by prover and category	0
query [--prover P] [--kind K] [--category C] [--polarity P] [--name SUB]	Filter	0 / 2
export --format jsonl\|json\|csv\|parquet [-o FILE]	Export	0 / 2

from pqc_formal_corpus import load, by_prover, by_category, to_dataframe
by_prover()          # {'cryptoverif': 1, 'easycrypt': 51, ...}
by_prover([])        # {} -- an empty corpus reports empty

---

pqc-migration-mcp

Six tools over line-delimited JSON-RPC on stdio: credential_size, fragments, reassembly_window, list_failure_families, describe_family, score_submission.

Keep each request on one line — the transport is line-delimited, and a request wrapped across two lines arrives as two incomplete ones.

Domain errors come back as tool results with isError: true and a message naming the valid options, so an agent can self-correct. Only protocol faults become JSON-RPC errors (-32601, -32602, -32700).

---

Verifiers

Tool	Command	Exit codes
farkas-check	make check · ./farkas_check < cert.txt	0 valid · 1 rejected · 2 malformed · 3 refused
pqc-bounds-lean	./verify.sh	0 all typecheck with no sorry · 1 otherwise
pqc-dos-gate-rtl	./verify.sh	0 all five proofs gave their expected verdict · 1 otherwise
pqc-dos-embedded	./run.sh	prints the QEMU transcript