The nine stages

Every Verdifax execution flows through nine deterministic stages, each contributing its hash output to the final sealed manifest. This page walks through each stage in plain English. The full technical specification is in the Section 0 reference.

Stage 1, DOG (Deterministic Oracle Gateway)

The pipeline's front door. DOG admits the payload, derives an envelope identifier, and computes the envelope hash, a sealed snapshot of the input bytes plus the program identity. Nothing is admitted that hasn't been canonically encoded first.

What DOG does: it canonicalizes and hashes the input. Identical inputs always produce the same envelope ID, but each submission is admitted as its own run. Program authorization is a separate gate after policy evaluation and before transport, and it refuses unregistered programs only on deployments that enforce the program registry; elsewhere the declared program identifiers are bound as submitted. What DOG does not check: whether the values inside the input are truthful. A well-formed patient record with fabricated symptoms is admitted the same as a real one, authenticity of content is upstream of the pipeline.

Outputs added to the manifest: envelope_id, envelope_hash.

Stage 2, DTL (Deterministic Transport Layer)

DTL fixes each route's order. Every envelope takes the route's next sequential position, persisted so a restart can never reuse one; reordering, duplicates and a consumed position presented with different content are refused, and a hybrid logical clock that never runs backwards stamps each envelope. The transport hash covers the route, envelope hash, position and clock.

Outputs: sequence_id, transport_hash.

Stage 3, DKEC (Deterministic Kernel Execution Controller)

DKEC dispatches the six kernels that actually do the work. Each slot of the execution ids is the respective kernel's own output, at a fixed position:

  • DSE, Deterministic State Engine
  • TOK, Temporal Ordering Kernel
  • DSC, Deterministic State Continuity
  • NREP, Non-Repudiation Engine Protocol
  • AIVP, Artificial Intelligence Verification Protocol
  • DCAE, Deterministic Compute Attestation Engine

DSE, TOK and DSC execute here; the AIVP slot is the governance stage's sealed PIA hash; the NREP and DCAE slots are identity and closure commitments, because their real operations (signing the finished record, verifying its closure) can only happen after the record exists. DKEC also emits an EPA hash (its sealed execution policy artifact) and an EFA hash (Execution Flow Artifact).

Outputs: epa_hash, efa_hash, six execution_ids.

Stage 4, AER (Attestation Execution Record)

AER is the run's attestation execution record, computed once with the aer.v1 formula from Verdifax's allowed US patent application: a single prefix-isolated SHA-256 over the input, transport, execution control and program hashes, the six kernel output identifiers at fixed positions, and the hardware field. A proof.v1 proof binds it to the hardware field. When a hardware agent is configured, the hardware field is the SHA-256 of an AMD SEV-SNP report taken just before the record and bound to its other fields. The bundle's execution_record section discloses every field so anyone can recompute both.

Outputs: aer_hash.

Stage 5, ZKSP (Zero-Knowledge State Prover)

The cryptographic core. ZKSP runs four steps in lockstep:

  • The ZK transcript step computes a transcript hash. Scaffold today: it is a domain-tagged SHA-256 over the execution record's proof.v1 hash (the R1CS hash facade), not a Fiat-Shamir commitment to the execution trace, and every bundle flags its transcript section as scaffold.
  • The hardware attestation hash field of this stage is a legacy placeholder and is never computed over a quote. The run's real hardware measurement is the execution record's hardware field (Stage 4), which carries a verified AMD SEV-SNP report when a hardware agent is configured.
  • The leakage step produces a leakage bundle hash. Scaffold today: the leakage bundle's two booleans (constant-time compliant, no timing variance observed) are design declarations of the deterministic kernel scheduler, not per-run measurements and not a bound on information leaving an enclave, and every bundle flags its leakage section as scaffold.
  • The formal verifier step runs a deterministic check that the pipeline produced a sealable manifest. Scaffold today: the status field carries the disclosed scaffold token SCAFFOLD_R1CS_HASH_FACADE; separately, every new bundle carries a formal_verification record that references a machine-checked Lean 4 development. That record is sealed by a hash inside the bundle and, on successful runs sealed from run 238 on, bound to the public log by the complete-record anchor. Anything other than the expected status still causes the manifest to be rejected.

Note also: the zero-knowledge proof step (the ZKSP binding in Stage 6) today emits a deterministic R1CS hash facade in place of a real STARK proof.

Outputs: transcript_hash [scaffold], hardware_attestation_hash [legacy placeholder], leakage_bundle_hash [scaffold], formal_verifier_status [scaffold].

See /concepts/scaffold-gaps/ for the specific scaffold-value records the system emits and what activates each.

Stage 6, Proof & State Binding

This stage produces three artifacts that bind the AER + ZKSP results into a single proof bundle:

  • ZKSP binding hash, a SHA-256 over the envelope id, AER hash, program id, registry record hash and formal verifier status. Scaffold today: its proving system is the transitional R1CS hash facade, not a real proof, and every bundle flags its ZKSP binding section as scaffold. It shows registry authorization only on deployments that enforce the program registry; elsewhere it binds the value the caller declared.
  • Migration token hash, a cross-environment portability seal so the proof can be re-verified on a different machine class without ambiguity.
  • Replay fingerprint, a deterministic identifier any re-execution must reproduce.

Outputs: zksp_binding_hash [scaffold], migration_token_hash, replay_fingerprint.

Stage 7, Ledger

The run is anchored into a transparency log. The PoTE (Proof of Temporal Execution) proof hash binds the run to a Merkle inclusion proof in the public ledger. The log entry id is the human-readable reference (Rekor-style).

Outputs: pote_proof_hash, log_entry_id.

Stage 8, Artifact Registry

Every artifact produced by the prior stages is registered into the artifact store. The registry returns a count, registry_artifact_count that must equal the number of artifacts the orchestrator believed it produced. Mismatches abort the run.

Outputs: registry_artifact_count.

Stage 9, DLA / .VFA

The final stage assembles everything into a single file: the .VFA artifact (Verdifax Final Artifact), whose hash is computed from the sealed outputs of every earlier stage. The independent_verified flag is set by an in-process consistency check that this build always sets to true; it is not a third-party verdict. Independent verification is what verdifax-verify does, outside the operator's systems, on the sealed record.

Outputs: final_vfa_hash, independent_verified.

The seal

After Stage 9, every sealed manifest field, including formal_verifier_status, registry_artifact_count and independent_verified, is joined in canonical order and SHA-256'd. The result is the manifest hash, the single 64-character receipt for the run. The operator re-derives it server-side with GET /runs/{id}/verify; the open-source verifier confirms that every section of the audit bundle carries it.

sha256(
  envelope_id . envelope_hash .
  sequence_id . transport_hash .
  epa_hash . efa_hash .
  exec_ids[6] .
  aer_hash .
  transcript_hash . hw_attest_hash . leakage_hash . formal_verifier_status .
  zksp_binding_hash . migration_token_hash . replay_fingerprint .
  pote_proof_hash . log_entry_id .
  registry_artifact_count .
  final_vfa_hash . independent_verified
)  →  manifest_hash

This shows the core field set. Later formula eras append further fields at the tail, including the per-run public-log leaf nonce that every /execute call mints fresh, which is why two separate submissions of identical inputs never share a manifest hash. See What the Manifest Hash proves.

Continue