ZK roadmap

The Verdifax audit bundle carries three sub-artifacts that are still flagged as scaffold values today: transcript, zksp_binding, and hardware_attestation. The hardware-attestation scaffold is a platform problem (covered in scaffold-gaps and not addressed here). The first two share a single root cause: the orchestrator does not yet run a real zero-knowledge proving system. This page documents the engineering plan that closes both scaffolds at the same time.

We publish this page because the value of a scaffold gap is in its closure path. A vague "future work" gap is worth one thing; a documented engineering interface, a chosen library, a specific list of acceptance criteria, and a published trait signature the buyer's team can immediately read is worth something different. Anyone reading this can assess what the remaining engineering actually is, and how big it isn't.

What "real" looks like

In a fully-activated Verdifax bundle, the transcript artifact carries the Fiat-Shamir transcript bytes of an actual STARK proof, and the zksp_binding artifact binds that proof to the manifest hash. A third-party verifier holding only the bundle and the open-source verifier library can recompute the proof's commitments, check the FRI low-degreeness proof against the signed checkpoint, and confirm the public inputs match the manifest's sealed fields. The orchestrator's claim that "this AI run executed within the declared policy" becomes a cryptographic proof a regulator can recompute, not a trust statement backed by the orchestrator's signature.

Today the same artifacts carry a deterministic SHA-256 over the R1CS inputs as a placeholder. The hash is byte-stable and replayable, but it is not a zero-knowledge proof. Verdifax is honest about this distinction by leaving the scaffold flag set; the verdifax-verify --strict mode exits non-zero on any scaffolded artifact precisely so a CI pipeline can gate on real activation.

Why winterfell, and why the architecture is prover-agnostic

The chosen reference prover is winterfell, Meta/Novi's pure-Rust STARK library, MIT-licensed, currently in production at Polygon Miden. It was chosen because it is the only candidate that passes both of Verdifax's hard cryptographic constraints:

• No trusted setup. Verdifax's ProverSystemManifest declares trusted_setup_policy = "NO_TRUSTED_SETUP_IN_TRANSITIONAL_HASH_FACADE". Groth16, KZG-PLONK, and other ceremony-based systems are disqualified at this constraint regardless of every other tradeoff.
• Post-quantum survivable. The PostQuantumPostureDeclaration commits to reducing security to a collision-resistant hash family. Pairing-based systems (Groth16, KZG-PLONK) and discrete-log-based systems (Halo2-IPA, Bulletproofs) are disqualified at this constraint.

Once those two filters are applied, winterfell is the only mature Rust crate left standing. Newer STARK libraries (plonky3, stwo) will likely be faster and smaller in 2-3 years, but they are pre-1.0 today and their APIs are still in flux. Pinning to them now would mean re-pinning every two months.

Critically, the prover choice is isolated behind a trait. The integration seam (described in the next section) is generic over the proving backend. A buyer who acquires Verdifax and prefers plonky3, stwo, or a future ZK system can substitute it without changing any other layer of the pipeline. The attestation architecture is prover- agnostic by design: the integration seam is what carries the binding between proof output and manifest hash, so swapping the underlying STARK system does not require revisiting any of the surrounding integration code.

The AIR adapter (task 5.3.3)

Verdifax produces R1CS as part of its existing pipeline. Winterfell consumes AIR (Algebraic Intermediate Representation). The bridge between them is a deterministic transformation, not a re-derivation, because the transcript hash that the existing pipeline produces must remain valid under the new path.

The integration trait is the seam where the work lands. It is intentionally narrow:

/// Bridge from Verdifax canonical R1CS + witness artifacts to a winterfell AIR.
///
/// Implementations must be pure functions of their inputs. No I/O,
/// no clock, no parallelism that affects ordering. This trait is the
/// only place where prover-specific code is allowed to exist outside
/// the `real_zk` feature gate.
pub trait CircuitInterface {
    /// Public inputs the verifier is given (hashes only, no secrets).
    type PublicInputs: serde::Serialize + Eq;

    /// Private witness (matches WitnessArtifact entry order).
    type PrivateWitness: serde::Serialize + Eq;

    /// Build a winterfell AIR from the canonical R1CS.
    ///
    /// The translation is fixed: each R1CS row (A, B, C) becomes one
    /// AIR transition constraint. Wire IDs become trace columns in
    /// the witness artifact's canonical order; entry_count becomes
    /// the trace length, rounded up to the next power of two with
    /// zero rows.
    fn build_air(&self, cra: &CircuitRepresentationArtifact) -> AirDescriptor;

    /// Build the trace from the canonical witness.
    fn build_trace(
        &self,
        witness: &WitnessArtifact,
    ) -> Result<TraceTable, CircuitError>;

    /// Public-input projection. Must depend only on the public-wire
    /// subset declared in the circuit representation artifact.
    fn project_public_inputs(
        &self,
        witness: &WitnessArtifact,
    ) -> Self::PublicInputs;
}

The trait is committed to the codebase today. What is gated on the real_zk Cargo feature is the implementation: under the default build, AirDescriptor and TraceTable resolve to no-op mock types so cargo check works without pulling winterfell as a dependency. Under --features real_zk, the same names resolve to winterfell::Air and winterfell::TraceTable and the prover runs end-to-end.

This separation is deliberate. It means the trait shape and the caller-side code are stable today; the cryptography engineer who fills in the body is working against a frozen interface, not discovering it as they go.

Proof system parameters

When real_zk activates, the prover emits proofs under these fixed parameters:

These parameters are not aspirational. They are the values the real_zk-gated constants will emit into the ProverSystemManifest once the AIR adapter lands. Until then, the manifest honestly declares proving_system = "DETERMINISTIC_R1CS_TRANSITIONAL_PROVER" and the scaffold flag remains set.

Acceptance gates

The transcript and zksp_binding scaffolds flip to is_scaffold: false only when all five of the following gates pass. None is optional.

1. AIR adapter implemented. A real CircuitInterface implementation is committed; the trait body builds a valid winterfell AIR from a canonical R1CS input and the test suite's canonical example circuits prove correctly.
2. Cross-toolchain byte-equality. The same proof bytes are produced on rustc 1.78, 1.79, and 1.80 from byte-identical inputs. CI runs this on every commit that touches the prover tree.
3. Verifier byte-stable. The verifier reaches the same accept / reject verdict on three rustc toolchains from the same inputs.
4. Multi-prover equivalence. A second independent implementation (a slow Python AIR replayer is the planned candidate) is wired into the determinism CI and produces the same proof bytes on the canonical example circuits.
5. Dependency pinning ceremony. Winterfell is pinned to a specific commit hash, not a ^x.y semver. The hash is recorded in Cargo.lock, the real_zk feature documentation, and the project's reproducible-build manifest.

Until all five gates pass, the orchestrator stays on the deterministic R1CS hash facade and the scaffold flag stays set. This is the same honesty posture the project takes everywhere else: declare what's real, declare what isn't, and don't shift between the two asymmetrically.

Effort and ownership

The realistic scope of this work is on the order of 4–8 weeks for a credible first cut, 12–16 weeks to satisfy all five acceptance gates. The bottleneck is not winterfell itself (it is a stable, well-documented library) and is not the orchestrator integration (the trait is already committed). The bottleneck is the AIR adapter implementation, which requires a cryptographer who is comfortable reasoning about R1CS-to-AIR lifting, FRI parameter tuning, and the determinism invariants that Verdifax's other layers depend on. This is PhD-level work or senior applied-cryptography work; it is not generic Rust engineering.

The other long tail (Lean 4 formal-verification theorem, hardware-attestation activation under TPM2/SEV-SNP) is tracked separately under scaffold-gaps.

What this page commits us to

The page above is a public commitment to a specific engineering plan, not a marketing statement. The closure path is named, the library is chosen, the trait is committed, the acceptance gates are enumerated. If a buyer's team reads this and concludes the gaps are bigger than described, the page is wrong and we need to fix it. If they conclude the gaps are smaller than described, we have understated the work and the page is also wrong. Either way, the page exists to be adversarially read.

When the scaffold closes, i.e., the orchestrator code is updated to emit transcript.scaffold.is_scaffold = false and zksp_binding.scaffold.is_scaffold = false, this page will be marked closed with the date, the release version, and a link to the engineering record that activated it. The scaffold-gaps page will gain a corresponding entry.

Until that day, the orchestrator continues to be honest about what it emits, and the verifier continues to surface the scaffold flag. That posture is the asset.