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 checks: the bytes are well-formed, the program is authorized by the registry, and the same input cannot be admitted twice without detection. 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 produces a sequence id and a transport hash that bind the envelope into a totally-ordered log. The same envelope cannot enter the pipeline twice without being detected; the order in which envelopes enter is itself sealed.
Outputs: sequence_id, transport_hash.
Stage 3, DKEC (Deterministic Kernel Execution Controller)
DKEC dispatches the six kernels that actually do the work. Each kernel runs deterministically and emits an execution id:
- 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
DKEC also emits an EPA hash (Execution Proof Artifact) and an EFA hash (Execution Flow Artifact).
Outputs: epa_hash, efa_hash, six execution_ids.
Stage 4, AER (Attestation Execution Record)
AER consolidates the six kernel outputs into a single tamper-evident record. The AER hash seals the kernel-level work and is the input into the cryptographic sealing pipeline that follows.
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, a Fiat-Shamir-style commitment to the entire execution trace.
- The hardware attestation step captures the hardware attestation hash, designed to be a TPM2 quote or AMD SEV-SNP measurement that anchors the run to a specific physical machine. Scaffold today, currently emits a scaffold value; activates on confidential-compute deployment.
- The leakage bound step produces a leakage bundle hash, an upper bound on information that escaped the secure enclave.
- The formal verifier step runs a deterministic check that the pipeline produced a sealable manifest. Scaffold today, the Lean 4 formal verifier development tree is empty; determinism is currently established by deterministic replay rather than formal proof. Anything other than the expected status still causes the manifest to be rejected.
Note also: the zero-knowledge proof step (covered in Stage 4 and earlier output binding) today emits a deterministic R1CS hash facade in place of a real STARK proof.
Outputs: transcript_hash, hardware_attestation_hash [scaffold],
leakage_bundle_hash, 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, ties the ZK transcript to the registry record hash, ensuring the run was authorized by the program registry.
- 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, 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 signed file: the
.VFA artifact (Verdifax Final Artifact). An independent third-party
verifier re-derives the chain and either signs off (independent_verified = true) or rejects.
Outputs: final_vfa_hash, independent_verified.
The seal
After Stage 9, all 18 hash fields plus formal_verifier_status plus
registry_artifact_count plus independent_verified are concatenated
in canonical order and SHA-256'd. The result is the manifest hash.
the single 64-character receipt that anyone can verify.
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
