pq-verify v2.12.0 — PQC Implementation Verification

Independent verification for ML-KEM (Kyber), ML-DSA (Dilithium), SLH-DSA (SPHINCS+), LMS/HSS and XMSS/XMSS^MT implementations.

You deploy post-quantum cryptography. pq-verify checks that your implementation computes the standard correctly, three ways:

• A library you can load (--audit-kem, --audit-dsa, --audit-hbs, --audit-so): pq-verify drives the vendor's own entry points with every NIST ACVP vector, Wycheproof's edge cases and malformed inputs, in a child process with a timeout, and binds the verdict to the sha256 of every shared object that ran.
• An implementation you cannot load — an HSM, a sealed binary, a remote service (--emit-prompt SET --fresh-key K): fresh ACVP questions derived from a seed only the auditor holds, in NIST's own format. Their answers exist nowhere until pq-verify computes them, so a correct response had to be computed, not copied.
• pq-verify itself: its reference chain passes all 1566 pinned NIST ACVP vectors (ML-KEM, ML-DSA, SLH-DSA, LMS), and the NTT layers carry Coq proofs for every input. This is what makes its verdicts on your code worth trusting; it is not a verdict on your code.

Results are evidence toward FIPS 140-3 / CMVP readiness and CNSA 2.0, not a certificate: a CMVP certificate is issued by NIST and the Canadian Centre for Cyber Security, after an accredited laboratory has tested the module.

It does not compute PQC. It verifies the implementations that do: liboqs, BoringSSL, OpenSSL+OQS, HSM firmware, or your own code.

Enterprise audits and pre-CMVP readiness

pq-verify is open source and free to run yourself. Its maintainer also runs audits with it for teams that want the evidence before a certification lab, a customer or a deployment sees their code:

• Library audit: ML-KEM and ML-DSA libraries through their own entry points, LMS/HSS and XMSS through a small adapter, and SLH-DSA, HSMs and sealed binaries through fresh ACVP questions. Each audit runs the checks that apply: NIST's ACVP vectors, Wycheproof and CCTV edge cases, malformed inputs, key-state handling for LMS and XMSS, and constant time for ML-KEM.
• Pre-CMVP gap assessment: the ACVP algorithm tests a CMVP submission depends on, run beforehand, with each failure traced to its cause.
• Hybrid TLS review: RFC 10024 groups such as X25519MLKEM768, checked from the wire bytes, where ACVP never looks.
• Remediation verification: the same audit re-run on the fixed build, bound to its sha256.
• CI integration: the GitHub Action gates merges on the result, and SARIF 2.1.0 carries the findings to GitHub Code Scanning or DefectDojo.
• CNSA 2.0: its post-quantum algorithms, ML-KEM-1024, ML-DSA-87 and LMS/XMSS for firmware signing, are all covered.

The deliverable is evidence, not certification: a CMVP certificate is issued by NIST and the Canadian Centre for Cyber Security, after an accredited laboratory has tested the module. What pq-verify has found in public libraries is in AUDITS.md; what it cannot check is in LIMITS.md; how each requirement maps to a check is in ARCHITECTURE.md. To discuss an audit, see Contact.

What you get

Layers of an audit:

Plus per-layer algebraic protection allocation: which NTT layers are worth masking, computed from the transform's structure. That is a design input, not a measurement — see Scope.

Every result is reproducible — deterministic output, SHA-256 fingerprint, re-runnable by your own auditors.

Proven

• 160/160 self-test across 6 field-native engines, of which 54 verify PQC directly; the others check the harness itself or are classical and research engines, never counted as PQC evidence (how the checks are tracked). A check whose optional dependency is missing reports ⊘ SKIPPED, never a pass and never a failure
• NIST ACVP, every vector passing: ML-KEM 240/240, ML-DSA 615/615, SLH-DSA 1248/1248 across all 12 parameter sets (sigGen opt-in, --slhdsa-siggen), LMS 87/87
• LMS/HSS and XMSS/XMSS^MT (SP 800-208, CNSA 2.0's firmware-signing schemes) against every other pinned source, --lms-xmss
• Proofs for every input (pq-verify --proofs, Coq) of the FIPS 203 and FIPS 204 NTTs and their modular reductions

All of it on commodity hardware (Google Colab CPU); each item in full, with the native full-KEM, non-circular KAT and lattice-estimator results, is in ARCHITECTURE.md.

Quick start

pip install "pq-verify[full]"
pq-verify --acvp-all            # 1566/1566, offline, no configuration, ~1 min
pq-verify --slhdsa-siggen      # + SLH-DSA sigGen, 624 signatures, ~30 min
pq-verify --fndsa              # FN-DSA verification, FIPS 206 DRAFT track, ~1 s
pq-verify --mceliece           # Classic McEliece reference vs the KATs, NOT a FIPS standard
pq-verify --hqc                # HQC's error-correcting code vs the submitters' decoders, ~2 s

That is the whole installation. It is a command-line tool: Python 3.9+, gcc, and nothing else. No notebook, no network, no service. The NIST vectors ship inside the package, so air-gapped environments work out of the box.

Edge cases, offline: C2SP's Wycheproof and CCTV vectors (strcmp traps, unlucky sampling, every out-of-range ek coefficient, malformed ML-DSA hints) are pinned to exact commits and run by --audit-kem and --audit-dsa against a vendor library, and by pq-verify --edge-cases against pq-verify's own references. The latter currently reports one finding, a known defect in the pinned dilithium-py 1.4.0 (a repeated hint index is accepted; fixed upstream, not yet released).

To audit a compiled library:

pq-verify --audit-so build/libmlkem768.so PQCLEAN_MLKEM768_CLEAN_ntt
pq-verify --audit-kem build/libmlkem768.so ML-KEM-768     # the whole KEM
pq-verify --audit-dsa build/libmldsa65.so ML-DSA-65       # the whole signature scheme
pq-verify --audit-hbs build/libhashsigs.so                # LMS/XMSS, via a pqv_hbs adapter

The minimal audit. If you run one command against an ML-KEM library, run this one: NIST, Wycheproof and CCTV vectors, the FIPS 203 input checks, 10 000 accumulated cases and the constant-time check, with a JSON report bound to the library's SHA-256, and (the default) a nonzero exit on any finding:

pq-verify --audit-kem build/libmlkem768.so ML-KEM-768 --constant-time --json report.json

For ML-DSA, the same with --audit-dsa (no --constant-time yet).

liboqs. A library can hold more than one implementation: liboqs exports its public OQS_* API and, beside it, every backend it dispatches to (mlkem-native's and mldsa-native's portable C and x86-64 code). pq-verify refuses to guess between them, lists them, and audits the one you name:

pq-verify --audit-kem   liboqs.so ML-KEM-768 --symbol-prefix OQS_KEM_ml_kem_768_ --constant-time
pq-verify --audit-dsa   liboqs.so ML-DSA-65  --symbol-prefix OQS_SIG_ml_dsa_65_
pq-verify --audit-fndsa liboqs.so FN-DSA-512 --symbol-prefix OQS_SIG_falcon_512_   # draft track

The public API is what your application calls; a backend's prefix (PQCP_MLKEM_NATIVE_MLKEM768_C_, for one) audits the code a CPU without AVX2 runs. liboqs 0.16.0 passes all of it, per implementation, rebuilt and re-audited in CI (AUDITS.md).

For an implementation that cannot be loaded — an HSM, a sealed vendor binary, a build with the transform inlined — ask it the questions instead:

pq-verify --emit-prompt ML-DSA-65 --prompt-out prompt.json   # 205 questions, no answers
#   ... the implementer runs them, wherever it lives, and returns a response ...
pq-verify --verify-response response.json                    # byte-exact, per test case

This route is weaker than --audit-so, and the report says so: a passing response shows the standard was computed correctly, not which binary computed it, so the result carries artifact: none (below). Use it when the alternative is no verification at all, not when you can point at a file.

Nothing in production negotiates bare ML-KEM. To check the part ACVP cannot see — how the two halves of a hybrid key agreement are put together:

pq-verify --emit-hybrid-prompt X25519MLKEM768 --prompt-out hybrid.json
#   ... fill in the wire bytes from one handshake ...
pq-verify --verify-hybrid hybrid.json                        # RFC 10024 composition

DEMO.ipynb runs the same thing in Colab if you prefer a notebook.

The Python API, and the other install routes, are in ARCHITECTURE.md.

What a result is bound to

Every report states its binding as a field, not as prose:

The binding is recorded independently of the verdict, because they are different facts. A library that exposes no derandomised entry points is artifact: sha256 <hash> (the file was read) with status CANNOT VERIFY (no vector was ever driven through it). In SARIF the hash is emitted as the run's artifacts[].hashes.sha-256, which is where a security platform already looks for "this exact file was analysed".

Isolation and what actually ran. Each --audit-* runs in a child process (--audit-timeout, default one hour). A library that crashes on a test vector or hangs is reported — CANNOT VERIFY, with the signal or the limit — instead of taking pq-verify and its report down with it, and the code under audit does not share memory with the code that decides its verdict. The child records every shared object the audit mapped (artifact.loaded_objects: path, inode, sha256), so the binding covers the vendor library and what it pulled in — a libcrypto, a dependency found through LD_LIBRARY_PATH — plus any LD_PRELOAD/LD_LIBRARY_PATH in effect (artifact.loader_environment). If the audited file changes during the run, the verdict is CANNOT VERIFY.

Never ship a test build. The randomness harness and the pqv_hbs adapters make a library deterministic and stateless on purpose. pq-verify --check-no-harness lib.so exits 1 if either is present; put it in the release job of anything audited this way.

Ask fresh questions. NIST's published questions have published answers: NIST ships expectedResults.json beside every prompt, and so does this package. A response to them that matches shows only that the answers were obtained. For an audit through --emit-prompt, pose questions derived from a seed only you hold:

pq-verify --emit-prompt ML-DSA-65 --fresh-key audit.key      # send the prompt, keep the key
pq-verify --verify-response response.json --fresh-key audit.key

How fresh questions are derived and checked, LMS key-reuse detection, the scope field, and how incomplete or unanswerable runs are reported: ARCHITECTURE.md.

Use it in CI

A few lines in any repository that builds a post-quantum library. Findings appear as annotations on the pull request, and the build fails on any result that did not verify — including one that could not run.

- uses: bigDSanalyst/pq-verify@v2.12.0
  with:
    audit: dsa                       # kem | dsa | hbs | ntt
    library: build/libmldsa65.so
    param-set: ML-DSA-65

With no library at all, it runs the NIST ACVP suites against pq-verify's own reference chain:

- uses: bigDSanalyst/pq-verify@v2.12.0

Outputs: verified (true only if every task that ran verified), findings, sarif-file. Every input reaches the shell through the environment, never by template substitution, and every action the Action uses is pinned to a commit. Pin the Action itself to a release tag: @v1 is the first upload and is not maintained.

Exit status of the CLI, since 2.10.0: 0 verified, 1 a task found problems or could not verify, 2 bad input. Gating is the default; --no-fail reports without gating. Before 2.10.0 every task exited 0 unless --fail-on-finding was passed, which the Action did not pass for its ACVP step. A complete workflow is in example-workflow.yml.

Machine-readable output

pq-verify --audit-so build/libmlkem768.so PQCLEAN_MLKEM768_CLEAN_ntt \
          --sarif results.sarif --json results.json --fail-on-finding

SARIF 2.1.0 is imported directly by GitHub Code Scanning (the Action uploads it) and DefectDojo, so findings land in the security tooling a team already runs rather than in a terminal someone has to read. AWS Security Hub takes its own format (ASFF), so it needs a SARIF-to-ASFF conversion step.

--fail-on-finding exits non-zero, so it can gate a merge.

Independent audits

pq-verify has been run against eight upstream projects — all verify clean, with negative controls that correctly fail. Exact commits, build commands and per-check output are in AUDITS.md.

The full scheme rows drive the library's own code with every NIST ACVP vector for the scheme and Wycheproof's edge cases: --audit-kem for ML-KEM, --audit-dsa for ML-DSA. The NTT-level rows check the transform against an independently computed FIPS reference.

Every pinned library also carries mutants, one planted bug each, which CI requires the audit to fail; how --audit-dsa reaches each FIPS 204 interface, and randomised APIs, is in ARCHITECTURE.md.

More audit modes

Accumulated vectors: 10 000 random cases, one digest

Every --audit-kem, --audit-dsa and --audit-harness run also drives 10 000 seeded random cases through the library and compares a SHAKE-128 digest of every output with a pinned value -- the way Go and BoringSSL test themselves. Fixed vectors cover the edge cases someone thought of; these reach the ones nobody did (a planted bug that fires on 1 ciphertext in 8 192 passes every NIST, Wycheproof and CCTV vector and is caught here). Coverage is probabilistic: bugs rarer than about 1 in 10 000 operations may not be hit. ML-DSA digests are C2SP CCTV's; ML-KEM's are Go's, because CCTV's published ML-KEM digests turn out to be the FIPS 203 draft (details). --accumulated 0 skips them.

Any language: Crucible-protocol harnesses

A harness result is not bound to a library. pq-verify hashes the harness executable, not the library behind it, so a harness audit says what something answering through that harness computes. It is not artifact-bound evidence about a specific binary, of the kind a CMVP-style review needs; for that, load the library (--audit-kem, --audit-dsa).

pq-verify --audit-harness './harness-go-stdlib' ML-KEM-768 audits an implementation in any language through a harness speaking Crucible's JSON-line protocol, with pq-verify's own vectors and verdicts — only the wire format is Crucible's. Go's crypto/mlkem and Cloudflare CIRCL (ML-KEM and ML-DSA) are VERIFIED through Crucible's unmodified harnesses, rebuilt and re-audited in CI. A harness is untrusted: its message convention is settled against NIST, its determinism is tested, and a crash is CANNOT VERIFY, never a refusal. The library behind a harness is not hashed, and the report says so (AUDITS.md).

Draft track: FN-DSA (FIPS 206)

pq-verify --fndsa checks FN-DSA (Falcon) verification ahead of the final FIPS 206. It is a separate task with its own report (track: "draft", standard: "FIPS 206 (draft)"): it is not one of the 160 self-suite checks, not one of the 1566 ACVP vectors, and never part of a FIPS 203/204/205 verdict.

pq-verify --audit-fndsa lib.so FN-DSA-512 audits a vendor's FN-DSA library the same way, through its own entry points (the NIST API as PQClean exports it, or liboqs's OQS_SIG_falcon_*): the pinned signatures verify, every malformed input is refused, its keys are canonical and match their secret keys, every secret key solves the NTRU equation f·G − g·F = q and meets both Gram–Schmidt bounds (checked in exact integer and rational arithmetic), and its signatures verify under pq-verify's verifier with no nonce reused. PQClean's Falcon passes; eight planted bugs in its source each fail the audit in CI (AUDITS.md).

What is checked is Falcon round 3, the scheme FIPS 206 standardises. Verification is integer arithmetic that the final standard is not expected to change; framing (headers, padding, how a context string is bound) may change, and lives in one section of pq_verify/fndsa.py. Signing — floating-point FFT and a Gaussian sampler, where Falcon implementations actually go wrong — is not checked until the final standard's vectors exist.

Not a FIPS standard: Classic McEliece

Classic McEliece was a NIST round-4 candidate that NIST did not select (it chose HQC); it is on an ISO track (ISO/IEC 18033-2). pq-verify checks it on a track of its own (track: "classic-mceliece"), never part of a FIPS verdict.

pq-verify --mceliece holds pq-verify's own implementation to the official KATs for all ten parameter sets. The public keys (0.26–1.36 MB) are not pinned: each is regenerated from the private key's seed, and the rebuilt KAT must hash to the nistkat-sha256 PQClean publishes for it.

pq-verify --audit-mceliece lib.so mceliece348864 audits a library through its own entry points (the NIST API, or liboqs's OQS_KEM_classic_mceliece_*):

PQClean's reference passes all ten sets; eight planted bugs each fail the audit in CI (AUDITS.md). Encapsulation's error-vector sampling is checked for validity and repetition, not distribution.

A pass means the library computes Classic McEliece exactly. It says nothing about the scheme's security: its cryptanalysis is active (key-recovery cost estimates were published in 2025–2026 and disputed by the submitters), so whether to deploy it, and with which parameter set, follows current agency guidance such as BSI's TR-02102-1.

Standard not final: HQC's error-correcting code

HQC was selected by NIST in March 2025; its standard is not final. pq-verify checks its code layer on a track of its own (track: "hqc"), never part of a FIPS verdict: the Reed–Solomon code over GF(2⁸) concatenated with a duplicated Reed–Muller RM(1,7) that decryption decodes. Not the KEM around it.

The decoder is audited on its own because nothing else reaches it. Honest decryptions rarely put more than two errors in front of the outer decoder, and decapsulation re-encrypts, so no ciphertext, honest or built, can drive the decoder into a corner and show its answer. A decoder bug that only bites on rare error patterns passes every KAT and every round trip.

pq-verify --hqc holds pq-verify's reference to the submitters' published generator polynomials and to their own decoders' answers on its built vectors, for HQC v5.0.0 (whose code layer is the 2023 submission's) and the unreleased next-release branch (a different field polynomial and bit order).

pq-verify --audit-hqc lib.so HQC-1 calls a library's encoder and decoder functions directly (reed_solomon_*, reed_muller_*, code_*; --hqc-profile next for the next-release code):

Built vectors, not random ones: four planted Berlekamp–Massey bugs fail on 5–9% of random full-weight error patterns and essentially never on honest decryptions; the Hankel-built patterns trigger three of them every time. The blocks between two codewords found a defect in the submitters' AVX2 decoder that 40 800 random and noisy blocks did not trigger once (AUDITS.md). liboqs builds these functions with hidden visibility, so its shared library cannot be audited this way: build its HQC sources with default visibility. Not a side-channel review.

Hybrid key agreement (RFC 10024)

Nothing in production negotiates bare ML-KEM: post-quantum TLS runs a hybrid group, and ACVP never sees how its two halves are concatenated. RFC 10024 does not use one order:

The first row is reversed relative to its own name. The RFC says so itself, and calls it historical. So an implementation can pass every ACVP vector byte-for-byte and still be wrong, because ACVP never sees the concatenation.

--verify-hybrid checks one handshake's wire bytes: every length, the FIPS 203 §7.2 encapsulation-key check, the ECDHE point, the X25519 all-zero check and, given ephemeral test keys, both halves of the shared secret recomputed. When a check fails it tests the other order and names the root cause. Commands are in the Quick start; what is checked, and how, is in HYBRID.md.

Scope

pq-verify verifies the algebraic substance of ML-KEM/ML-DSA (NTT, module-LWE relations, parameter security) natively in Z₃₃₂₉ / Z₈₃₈₀₄₁₇. The non-algebraic layers (SHAKE/SHA3 hashing, sampling, compression, the FO transform) are bit/byte operations verified by NIST ACVP end-to-end testing, not native field solving.

The algebraic core is proven natively where the proof is exact; the full implementation is proven byte-exact against NIST's own bytes. We make the claims we can prove.

Everything pq-verify does not check — schemes, side channels, parameter security, which paths are proved and which are only tested — is collected in LIMITS.md.

Side channels are not measured

pq-verify compares values. It never executes an implementation under measurement, collects no traces, and observes no timing, power or electromagnetic behaviour. It cannot detect an implementation that computes the correct answer and leaks the key while doing it.

This is not hypothetical. KyberSlash and Clangover were byte-exact correct against every vector and still recovered secret material through timing. A tool that checked only values would have passed both.

--audit-kem ... --constant-time closes part of that gap, and says exactly which part. It runs the vendor's own Encaps (m secret) and Decaps (the secret key and z secret, on a valid and on a random ciphertext) under Valgrind memcheck with the secret bytes marked, and fails on every branch and every memory address that depends on them, naming the function -- the technique mlkem-native and BoringSSL use on themselves. It catches the Clangover class (a compiler-introduced branch on a secret bit) and cache-timing table lookups; three such leaks planted in PQClean, each leaving every output correct, are caught in CI. It does not see instruction timing -- KyberSlash's secret division -- so the report lists the library's division instructions for a reviewer instead; it cannot check key generation (the public matrix seed is derived from the secret seed); and it measures nothing physical. The report records exactly that scope, and without the flag claims nothing (the report fields). --leakage is not an exception: it is a design input computed from the NTT's structure, not an observation of execution.

Verifying a release

Releases are built by .github/workflows/release.yml on GitHub's runners, from a reviewed commit, after the full suite and all 1566 NIST ACVP vectors pass on Python 3.9 through 3.13. Each artifact carries SLSA build provenance and an attested SPDX SBOM. Check them yourself, trusting nothing this repository says:

gh attestation verify pq_verify-2.12.0-py3-none-any.whl --repo bigDSanalyst/pq-verify

That tells you which workflow built the file, from which commit, on whose runners — not that we assert it, but that GitHub signed it. Provenance cannot be added to an artifact after the fact, which is why a release built anywhere else can never have it.

The SBOM is short: pq-verify has no unconditional runtime dependencies. kyber-py, dilithium-py, sympy and slh-dsa are optional extras used to cross-check against independent implementations; the package itself installs with none of them.

How it works

ARCHITECTURE.md holds what is not needed to run an audit:

• Engines and where they are heading: the PQC, harness, classical and research tracks, and why only the first is PQC evidence
• The six field-native engines and the specification front-end
• Deterministic by default: the pinned NIST vectors and how they are re-pinned
• The Python API
• What a result is bound to, in depth and the side-channel report fields
• What's in this package

Third-party audit results, build commands and every planted bug are in AUDITS.md; hybrid composition in HYBRID.md.

Requirements

Minimum (core engines + ~149 self-tests):

• Python 3.9+ — every version of the declared range (3.9, 3.10, 3.11, 3.12, 3.13) runs the full test suite and all 1566 ACVP vectors in CI. The floor is 3.9 rather than 3.8 because pq-verify[full] cannot resolve below it: kyber-py and dilithium-py both require >=3.9. requires-python and the code are held together mechanically — a module that stops parsing at the declared floor fails the suite, and widening the floor fails it too.
• gcc and g++ (the C/C++ engines compile at runtime); on macOS, Xcode's command-line tools (Apple clang) — every engine still builds with -march=native, falling back to -mcpu=native
• Linux (x86-64) or macOS (Apple silicon); both run the full suite in CI

For the full 160/160 self-suite and the 1566/1566 ACVP claim:

• kyber-py — required for pqverify_acvp() (the byte-exact NIST reference) and the FIPS 203 roundtrip tests
• dilithium-py — required for pqverify_mldsa_acvp() (the 615 ML-DSA vectors)
• coq — required for the Coq certificate verification tests
• sympy — required for the Engine-6 Conjecture 7 exact-rational test (without it that check reports as skipped, not failed)

apt-get install -y coq gcc g++
pip install "pq-verify[full]"   # kyber-py, dilithium-py, sympy, slh-dsa

Optional (1 test each, everything works without them):

• cryptominisat — the CMS5 speed-comparison benchmark
• slh-dsa — the SLH-DSA ACVP reference and live roundtrip (parameters still validate without it)
• network access — pqverify_acvp() fetches NIST vectors from GitHub live; for air-gapped use the pinned vectors are used by default, or pass vector_dir= pointing at your own local vector set

Deliberately NOT required (a deployment advantage):

• No numpy, scipy, or PyTorch — pure Python + ctypes + inline C
• No SageMath — the pqverify_params lattice estimator is self-contained (ML-KEM's lattice-estimator values are pinned; custom parameters use a calibrated formula, close but not exact)

License

MIT. Audits and commercial support: see Enterprise audits and pre-CMVP readiness.

Citing this software

Archived on Zenodo with a citable DOI:

Maino, N. C. (2026). pq-verify: Independent verification for ML-KEM / ML-DSA implementations (v2.9.0). Zenodo. https://doi.org/10.5281/zenodo.23092768

@software{maino_pqverify_2026,
  author    = {Maino, Nicholas Clifford},
  title     = {pq-verify: Independent verification for ML-KEM / ML-DSA implementations},
  version   = {2.9.0},
  year      = {2026},
  publisher = {Zenodo},
  doi       = {10.5281/zenodo.23092768},
  url       = {https://doi.org/10.5281/zenodo.23092768}
}

The DOI above resolves to this specific release. The companion paper is 10.5281/zenodo.19302050.

CITATION.cff names the version deposited on Zenodo. When a release is newer than the last deposit, the citation lags on purpose until a new one exists — a DOI that does not resolve to the version printed beside it would be worse than one a release behind. For the current version see Releases or the PyPI badge at the top.

Contact

Nicholas Maino (iamweare) · maiknown@gmail.com · https://github.com/bigDSanalyst Zenodo: https://doi.org/10.5281/zenodo.19302050