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