pq-verify v2.6.7 — PQC Implementation Verification

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

You deploy post-quantum cryptography. pq-verify proves your implementation computes the FIPS 203/204 standard correctly — in the native finite field, against NIST's own test vectors, with machine-checkable certificates. 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
• 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.8+, 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

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.

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.

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 (11 functions)
  core.py                  The stack (~6,100 lines, 6 field-native engines)
  cli.py                   Command-line interface
tests/test_pqverify.py     18-test pytest suite
pyproject.toml             Build config + console-script entry point
dist/
  pq_verify-2.6.7-py3-none-any.whl    Installable wheel
  pq_verify-2.6.7.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 dist/pq_verify-2.6.7-py3-none-any.whl

Requirements

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

• Python 3.8+
• 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: 159/160)

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, pass prompt_dir= pointing at local vector files

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.6.7). 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.6.7},
  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