# ML-DSA Verification

> Verify post-quantum ML-DSA (Dilithium) signatures in zero knowledge at all FIPS 204 levels, many per proof, without revealing the key or the signature.

- URL: https://oumuamua.dev/primitives/signatures/mldsa
- Published: 2026-10-03T10:49:16+07:00
- Updated: 2026-10-11T12:51:24+07:00

The ML-DSA chiplet proves that signatures pass FIPS 204 verification at ML-DSA-44, ML-DSA-65 and ML-DSA-87, with the
public key and the signature kept in the witness. One pipeline verifies many signatures in a single proof. It
shares `hekate-pqc` with the [ML-KEM chiplet](https://oumuamua.dev/primitives/encryption/mlkem).

## What the proof states

Each call runs `ML-DSA.Verify_internal`, FIPS 204 Algorithm 8, on the encoded public key pk, the message
representative M′ and the encoded signature σ. The caller forms M′ from the message M and the context string the way
FIPS 204 Algorithm 3 does, and passes it to the call.

A verified call returns the two digests Algorithm 8 computes on the way: tr = H(pk, 64) and μ = H(tr ‖ M′, 64). The
host program decides what becomes public. The [example program][example] publishes M′ and tr and keeps pk and σ in the
witness: the proof says that the key whose hash is tr signed M′, and reveals neither the key nor the signature.

An invalid signature has no witness. Trace generation stops when the recomputed challenge c̃′ differs from the c̃ in
the signature, and the constraints check the same equality inside the proof.

- **Parameter sets:** ML-DSA-44, ML-DSA-65 and ML-DSA-87.
- **Signatures per proof:** 1 to 256, or 1 to 227 at ML-DSA-87.
- **M′ length:** fixed per call when the tables are compiled.

## How the tables split the work

Six tables carry a verification. The host program trades 32-bit words with the ctrl table over one service bus. Behind
it, the Sampler, Keccak, Codec, NTT and HighBits tables pass coefficients, words and Keccak lanes to each other over
internal buses, where every value is emitted once by its producer and once by its consumer. Each table is an AIR over
the binary tower fields, proven in GF(2^128), and the lattice arithmetic mod q runs on bit-decomposed carry chains.

## Outside the proof

- **Key generation and signing.** The chiplet verifies only.
- **Forming M′.** The proof starts at M′. A statement about M itself needs the host program to constrain how M′ was
  built from M and the context.
- **HashML-DSA pre-hashing.** A caller can pass the M′ that HashML-DSA forms (FIPS 204 Algorithm 5); the proof then
  covers `Verify_internal` on it, and the hash that produced PH(M) stays outside.

## How it is tested

The tests sign with RustCrypto's `ml-dsa` crate and verify through the pipeline at all three parameter sets, with
empty and 100-byte messages and with two calls in one proof. Forgery tests change one value at a time, such as a hint
bit, a matrix entry or a host word, and check that each change breaks the constraint or bus that guards it. A message
the key never signed breaks the c̃ comparison.

## Examples

[`hekate/examples/mldsa.rs`][example] verifies one signature at the level `HEKATE_LEVEL` selects and publishes M′ and
tr. From a hekate checkout:

```bash
HEKATE_LEVEL=65 just example mldsa public   # 44 | 65 | 87
```

`public` builds the variable-time `table-math` prover that the README's measurements use. Without it the recipe builds
the constant-time prover, the one to use when the witness is private.

The program below is the example at ML-DSA-65, in four files:

- `src/program.rs` declares the host table that feeds words to the ML-DSA tables, attaches those tables under one
  namespace and publishes M′ and tr.
- `src/trace.rs` fills the host table.
- `src/signer.rs` generates a key and signs M′ with `sign_internal` (FIPS 204 Algorithm 7) from the RustCrypto `ml-dsa`
  crate, standing in for the signer.
- `src/main.rs` builds M′ from the message and an empty context, traces the verification, proves and verifies.

Start from the crates in [Installation](https://oumuamua.dev/hekate/docs/getting-started/installation) and add `hekate-pqc`, `ml-dsa` and
`rand`.

```rust src/program.rs:1
use hekate_core::errors;
use hekate_math::{Block128, TowerField};
use hekate_pqc::mldsa::{self, MLDSA_DATA_BUS_ID, MlDsaChiplet, MlDsaParams};
use hekate_program::circuit::{Circuit, CircuitProgram, Col};
use hekate_program::{FixedShape, define_columns};
use std::error::Error;

pub const PARAMS: MlDsaParams = MlDsaParams::ML_DSA_65;

const DIGEST_WORDS: usize = 16;

pub type F = Block128;

define_columns! {
    pub VerifyColumns {
        WORD: B32,
        SEL: Bit,
    }
}

pub fn published_rows(m_prime: &[u8], words: usize) -> Result<Vec<usize>, Box<dyn Error>> {
    let pk_words = PARAMS.pk_bytes() / 4;
    let tr_row = words
        .checked_sub(2 * DIGEST_WORDS)
        .ok_or("the host words end before tr and μ")?;

    let rows = (pk_words..pk_words + m_prime.len().div_ceil(4))
        .chain(tr_row..tr_row + DIGEST_WORDS)
        .collect();

    Ok(rows)
}

pub fn build_program(
    pipeline: &MlDsaChiplet<F>,
    rows: usize,
    words: usize,
    published: &[usize],
) -> errors::Result<CircuitProgram<F>> {
    let mut cx = Circuit::<F>::new("MlDsaVerify", rows)?;

    let cols = cx.schema(&VerifyColumns::build_layout());

    let word = cols.at(VerifyColumns::WORD);
    let sel = cols.at(VerifyColumns::SEL);

    cx.fix(
        sel,
        FixedShape::Cadence {
            stride: 1,
            count: words,
            origin: 0,
            values: vec![F::ONE],
        },
    );

    let cs = cx.cs();
    let col = |c: Col| cs.col(c.index());
    let padding = cs.one() + col(sel);

    cs.constrain(padding * col(word));

    cx.call(&mldsa::service(), &[word], sel)?;

    for &row in published {
        cx.publish(word, row);
    }

    cx.attach_namespaced("mldsa", pipeline.defs()?, &[MLDSA_DATA_BUS_ID])?;

    cx.compile()
}
```

```rust src/trace.rs:1
use crate::program::VerifyColumns;
use hekate_core::errors;
use hekate_core::trace::{ColumnTrace, TraceBuilder};
use hekate_math::{Bit, Block32, TowerField};

pub fn host_trace(words: &[u32], rows: usize) -> errors::Result<ColumnTrace> {
    let num_vars = rows.trailing_zeros() as usize;
    let mut tb = TraceBuilder::new_secret(&VerifyColumns::build_layout(), num_vars)?;

    for (row, &word) in words.iter().enumerate() {
        tb.set_b32(VerifyColumns::WORD, row, Block32::from(word))?;
        tb.set_bit(VerifyColumns::SEL, row, Bit::ONE)?;
    }

    Ok(tb.build())
}
```

```rust src/signer.rs:1
use ml_dsa::{B32, MlDsa65, SigningKey};
use rand::{TryRng, rngs::SysRng};
use std::error::Error;

pub struct Signed {
    pub pk: Vec<u8>,
    pub signature: Vec<u8>,
}

pub fn sign(m_prime: &[u8]) -> Result<Signed, Box<dyn Error>> {
    let mut seed = [0; 32];
    let mut rnd = [0; 32];

    SysRng.try_fill_bytes(&mut seed)?;
    SysRng.try_fill_bytes(&mut rnd)?;

    let key = SigningKey::<MlDsa65>::from_seed(&B32::from(seed));
    let expanded = key.expanded_key();
    let signature = expanded.sign_internal(&[m_prime], &B32::from(rnd));

    Ok(Signed {
        pk: expanded.verifying_key().encode().to_vec(),
        signature: signature.encode().to_vec(),
    })
}
```

```rust src/main.rs:1
mod program;
mod signer;
mod trace;

use hekate_core::config::Config;
use hekate_crypto::DefaultHasher;
use hekate_crypto::transcript::Transcript;
use hekate_pqc::mldsa::{MlDsaChiplet, MlDsaInput};
use hekate_program::digest::program_id;
use hekate_program::{ProgramInstance, ProgramWitness};
use hekate_prover_sys::prove;
use hekate_sdk::preflight;
use hekate_verifier::HekateVerifier;
use program::{F, PARAMS, build_program, published_rows};
use rand::{TryRng, rngs::SysRng};
use signer::sign;
use std::error::Error;
use trace::host_trace;

const LABEL: &[u8] = b"mldsa65";
const MESSAGE: &[u8] = b"Hekate ML-DSA-65 verification example";
const CONTEXT: &[u8] = b"";

fn main() -> Result<(), Box<dyn Error>> {
    let m_prime = [&[0, u8::try_from(CONTEXT.len())?][..], CONTEXT, MESSAGE].concat();
    let signed = sign(&m_prime)?;

    let pipeline = MlDsaChiplet::<F>::new(PARAMS, &[m_prime.len()])?;
    let traced = pipeline.trace(&[MlDsaInput {
        pk: &signed.pk,
        message: &m_prime,
        signature: &signed.signature,
    }])?;

    let words = &traced.words;
    let published = published_rows(&m_prime, words.len())?;

    let config = Config::default();
    let rows = words.len().next_power_of_two();
    let program = build_program(&pipeline, rows, words.len(), &published)?;

    let public_inputs = published
        .iter()
        .map(|&row| words.get(row).map(|&word| F::from(u128::from(word))))
        .collect::<Option<Vec<F>>>()
        .ok_or("a published row lies past the host words")?;
    let instance = ProgramInstance::new(rows, public_inputs);

    let witness = ProgramWitness::new(host_trace(words, rows)?).with_chiplets(traced.traces);

    let report = preflight(&program, &instance, &witness)?;

    if !report.is_clean() {
        eprintln!("{report}");

        return Err("the trace fails preflight".into());
    }

    let mut seed = [0; 32];
    SysRng.try_fill_bytes(&mut seed)?;

    let proof = prove(LABEL, &program, &instance, &witness, &config, seed, None)?;

    let id = program_id::<F, _>(&program)?;
    let mut transcript = Transcript::<DefaultHasher>::new(LABEL);

    let valid = HekateVerifier::<F, DefaultHasher>::verify(
        &id,
        &program,
        &instance,
        &proof,
        &mut transcript,
        &config,
    )?;

    if !valid {
        return Err("the verifier rejects the signature".into());
    }

    println!("public   M' ({} bytes), tr = H(pk)", m_prime.len());
    println!(
        "private  pk ({} bytes), signature ({} bytes)",
        signed.pk.len(),
        signed.signature.len()
    );
    println!("the verifier accepts the signature");

    Ok(())
}
```

## Performance

Zero-knowledge proofs, measured on Apple M3 Max, 16 cores. Build: `--release`, `std parallel blake3 table-math public`. Best of three on an otherwise idle machine. The [Benchmarks](https://oumuamua.dev/hekate/benchmarks) page has the base-protocol figures and the command for each run.

| Workload | Input | Proving | Verify | Proof size | Peak memory |
|:---|:---|:---|:---|:---|:---|
| ML-DSA-44 | FIPS 204 | 433 ms | 10.2 ms | 1,537 KiB | 249 MiB |
| ML-DSA-65 | FIPS 204 | 478 ms | 10.1 ms | 1,575 KiB | 236 MiB |
| ML-DSA-87 | FIPS 204 | 624 ms | 11.1 ms | 1,810 KiB | 332 MiB |

## Security

The crate has not been audited and may contain bugs and security flaws, as its README states. Hekate proves 100 bits
of soundness at every parameter set, below the security level of each, which makes the proof the weaker link; the
verified signature is still full ML-DSA.

## License

`hekate-pqc` is AGPL-3.0-only. Commercial licenses are available from Oumuamua Labs at
[info@oumuamua.dev](mailto:info@oumuamua.dev). The [README's Usage section][usage] builds an ML-DSA-65 host program,
and the API reference is on docs.rs.

[example]: https://github.com/oumuamua-labs/hekate/blob/main/hekate/examples/mldsa.rs
[usage]: https://github.com/oumuamua-labs/hekate/blob/main/hekate-pqc/README.md#usage