pq-verify v2.7.0 — PQC Implementation Verification

Independent verification for ML-KEM (Kyber) and ML-DSA (Dilithium) implementations.

You deploy post-quantum cryptography. pq-verify checks that an implementation computes the FIPS 203/204 standard correctly — the transform verified in the native finite field, the full ML-KEM scheme byte-exact against NIST's own test vectors, with machine-checkable certificates for the algebraic identities. Plus FIPS 205 SLH-DSA parameter validation across all 12 parameter sets.

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

What you get

A three-layer audit of any ML-KEM/ML-DSA implementation:

Plus per-layer side-channel leakage analysis with protection-allocation recommendations.

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

Proven (all tested on commodity hardware, Google Colab CPU)

• 160/160 self-test across 6 field-native engines, 6 phases — in an environment with every optional dependency present. Where one is missing the dependent check reports as ⊘ SKIPPED, is excluded from the ratio, and names what it needed. It is never counted as a pass, and never as a failure either
• 240/240 NIST ACVP ML-KEM vectors — keyGen + encaps + decaps byte-exact, KeyCheck bool-exact
• Native full-KEM verified at ML-KEM-1024 (Level 5): recovery 20/20, negative control caught
• Non-circular KAT 100/100 against the independent FIPS reference
• Calibrated lattice estimator: reproduces lattice-estimator exactly (Kyber-512 β=406/118.6 bits)
• Coq certificates verified by coqc with real exit codes

Quick start

pip install "pq-verify[full]"
pq-verify --acvp-all            # 855/855, offline, no configuration

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.

To audit a compiled library:

pq-verify --audit-so build/libmlkem768.so PQCLEAN_MLKEM768_CLEAN_ntt

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

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

exec(open('pq_verify/core.py').read())   # 160-test self-suite + loads the API

pqverify_acvp()                    # full NIST ACVP, all parameter sets
pqverify_params('ML-KEM-1024')     # parameter security check
pqverify_kem(k=4)                  # native full-KEM at Level 5

ntt = pqverify_load_so('/path/to/your_library.so', 'ntt_symbol')
pqverify_scan(ntt)                 # full audit + KAT + leakage

Use it in CI

Three lines in any repository that builds an ML-KEM or ML-DSA implementation. Findings appear as annotations on the pull request, and the build fails if the transform diverges from the FIPS 203/204 reference.

- uses: bigDSanalyst/pq-verify@v1
  with:
    library: build/libmlkem768.so
    symbol: PQCLEAN_MLKEM768_CLEAN_ntt

With no library at all, it runs the NIST ACVP suites:

- uses: bigDSanalyst/pq-verify@v1

Outputs: verified, findings, sarif-file. 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 ingested natively by GitHub Code Scanning, DefectDojo, Snyk and AWS Security Hub, so findings land in the security tooling a team already runs rather than in a terminal someone has to read.

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

Independent audits

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

Most rows are NTT-level: the transform is checked against an independently computed FIPS reference. Full-scheme auditing of a third party's keygen/encaps/decaps is available for ML-KEM (--audit-kem); the equivalent for ML-DSA signing is not, because most libraries do not export the derandomised entry points NIST's seeded vectors require.

Where no entry point can be loaded at all — ML-DSA signing, an HSM, a sealed binary — --emit-prompt / --verify-response asks the questions instead and checks the answers byte-exact. That result is not artifact-bound, and the report says so rather than implying otherwise; see What a result is bound to.

Architecture — six field-native engines

pq-verify does not encode cryptographic arithmetic as generic boolean SAT and hand it to a solver. It verifies each operation in the field the algorithm actually works in. Kyber's NTT is checked in Z₃₃₂₉ directly; Dilithium's in Z₈₃₈₀₄₁₇. That is what "field-native" means, and it is why the checks are exact rather than an encoding of an encoding.

Six C/C++ engines are compiled at runtime from sources embedded in core.py — no build step, no external .c files, no toolchain beyond gcc/g++.

The two schemes differ structurally and the tool distinguishes them: ML-KEM's ζ has order n, so 2n does not divide q−1 and the transform is incomplete — seven layers, last one deleted. ML-DSA's ζ has order 2n, so the transform is complete — eight layers. A verifier that assumes one shape silently mis-verifies the other.

Specification front-end

Alongside the engines, a pipeline turns a formal specification into field constraints:

CFL spec → lexer → parser → FOL → QBF → field router → engine dispatch
XML module → DQBF (Henkin dependency sets) → Tseitin linearization → GF(2)

The router picks the correct engine from the constraint structure — XOR-dense systems route to GF(2), ring arithmetic to the Z_q engines. Both paths are exercised in the self-suite (CFL 6/6, DQBF 7/7).

Public API

Deterministic by default

pq-verify ships with a frozen, versioned snapshot of NIST's ACVP vectors bundled inside the package (gzipped, ~7 MB). By default it verifies against those — so:

• the same input gives the same result, every run, forever
• it works with no network — air-gapped, offline, no GitHub reachability needed
• NIST editing their published files cannot change or break your result

That last point is not hypothetical: NIST periodically regenerates these vectors and has changed the ML-KEM encapDecap schema (the keyFormat seed/expanded split) more than once. A tool that fetches live gives different answers on different days. This one does not.

pqverify_acvp_all()              # pinned bundle, offline, deterministic  → 855/855
pqverify_acvp_all(live=True)     # opt in: fetch NIST's current vectors instead
pqverify_acvp_all(vector_dir=d)  # or point at your own local vector set

Vector provenance and per-file sha256 are recorded in pq_verify/vectors/MANIFEST.json. A scheduled GitHub Action watches upstream and opens an issue when NIST changes something, so re-pinning is a deliberate, reviewed act rather than a live dependency.

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 855 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.7.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.

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".

A passing response proves that whoever produced it computes FIPS 203/204/205 correctly for those inputs. It does not prove which binary did it: there is no signature over the computation and no binding to code. So the report says artifact: none rather than implying otherwise, and a reader can tell the two kinds of result apart without reading a footnote.

The same discipline applies to coverage. A response answering 3 of 205 questions reports 3 of 205 asked, groups nobody answered print NOT RUN rather than FAIL, and the verdict is INCOMPLETE — never 3/3 PASS.

And to pq-verify's own suite, which is where it was missing longest. A check that could not run — coqc absent, sympy absent — prints ⊘, stays out of the ratio, and registers the dependency it needed, so integrity_report() can never announce full coverage over a check that did not happen. Answering a different question set (promptId mismatch) is CANNOT VERIFY, which is reported separately from verified-and-failed: PQV000 for an absent check, PQV006 for an answer that is genuinely wrong.

--fail-on-finding exits non-zero for all of it — findings, INCOMPLETE, CANNOT VERIFY, a KEM audit that could not run, and an ACVP suite short of its full count. A run that did not verify does not pass a CI gate.

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.

What's in this package

pq_verify/
  __init__.py              Public API (15 functions)
  core.py                  The stack (~6,100 lines, 6 field-native engines)
  cli.py                   Command-line interface
  response.py              Prompt/response verification for un-loadable builds
  report.py                Native JSON + SARIF 2.1.0 output
tests/test_pqverify.py     53-test pytest suite
pyproject.toml             Build config + console-script entry point
dist/
  pq_verify-2.7.0-py3-none-any.whl    Installable wheel
  pq_verify-2.7.0.tar.gz              Source distribution
DEMO.ipynb                 One-click Colab demo → 855/855
vendor_audit_template.py   Drop-in .so audit → JSON report
sample_report.json         Example output (what your auditors receive)
README.md / QUICKSTART.md / LICENSE / CITATION.cff

Install: pip install "pq-verify[full]" — or download the wheel from Releases.

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 855 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)

For the full 160/160 self-suite and the 855/855 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 kyber-py dilithium-py sympy --break-system-packages

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

• cryptominisat — the CMS5 speed-comparison benchmark
• slh-dsa — SLH-DSA 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 (it reproduces the lattice-estimator's results without it)

License

MIT. The verifier is open-source — builds trust, enables adoption. Commercial support, custom engine development, and PQC audit engagements available separately.

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.7.0). Zenodo. https://doi.org/10.5281/zenodo.21739511

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

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

Contact

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