Verification

Status: Stage 6A contract, frozen; Stage 6B implemented for sandbox stages. This page specifies exact semantics for the four verification objects. The sandbox runner, manifest, conformance runner and the SAT verifier are live (see Runtime at the end); review stages execute under Stage 7B (docs/reference/reviews.md → Runtime); external stages wait on their adapters, and a run that reaches one finishes inconclusive. The participant-facing explanation is Verifying Results.

Canonical schemas: Verifier, VerifierContract, VerifierImplementation, VerificationRun. Canonical examples, validated in CI: schemas/examples/verifier-contract.sat.json, schemas/examples/verifier-contract.materials.json, schemas/examples/problem-revision.sat.json. Review stages are specified in the Review reference.

Object roles

ProblemRevision.verifier_contract_id pins exactly one Contract, or null. Null means results are recorded and not checked — an explicit state, not an omission.

The compatibility rule

The rule is normative, not behavioural: what matters is whether the Contract's intended acceptance semantics changed, not whether the outcomes a checker produces changed. There is no heuristic compatibility guessing.

Correcting a non-conforming implementation stays under the same Contract even when it changes the outcomes that implementation produces. If a Contract requires all 91 clauses to be satisfied and v1 wrongly accepts an assignment that fails one, v2 rejecting that assignment is a fix rather than a new Contract; the Contract's semantics did not change, v1 was non-conforming. Runs v1 produced are revoked and re-examined as needed.

Deciding that assignments naming variables outside the instance are now rejected, where the Contract previously allowed them, is a change to the normative semantics and requires a new Contract and a new revision.

Conformance

A Contract carries conformance_fixtures: known inputs with known expected outcomes, published as part of the Contract itself.

An Implementation may execute authoritative verification only while its conformance.status is passed — every applicable fixture reproduced its expected_result, and expected_score where the Contract declares one. Conformance is recorded, not asserted.

• A sandbox stage must carry fixtures sufficient to test its declared success and failure semantics. Where the stage can distinguish malformed or unverifiable input from substantive failure, include an inconclusive fixture. Three fixture classes per stage is the right target where the distinctions are meaningful — the SAT Contract below uses all three — but it is not a universal requirement, because some verifiers have no natural inconclusive case.
• error is not an expectable fixture outcome: it reports a failure of TfP's machinery, which is not behaviour to pin.
• conformance.failures records each fixture that did not reproduce, with expected and actual results. A failing implementation stays registered and inspectable.
• differential_against_implementation_id optionally records differential testing against a previous implementation of the same stage, on inputs beyond the fixtures.

Verification therefore has two levels: an Implementation passes its Contract's fixture suite, and only then does it check Submissions.

Reference inputs: slots on the Contract, bindings on the revision

A Contract declares named reference_inputs slots — the CNF instance an assignment must satisfy, the theorem statement a proof must close, the inventory snapshot a recipe must draw from — and does not contain the bytes. A ProblemRevision binds each slot to exact content-addressed bytes in verifier_input_bindings. One SAT Contract therefore serves every SAT Problem, each revision binding instance to a different CNF, all comparable under one conformance suite; without the split every instance would need its own Contract.

At ProblemRevision publication TfP enforces that every required slot is bound exactly once, no unknown slots are bound, the bound media type and size satisfy the slot's constraints, the bytes exist, and the server-computed hash and size match. Bindings are immutable with the revision. Conformance fixtures bind their stage's selected slots to fixture bytes, so the conformance suite exercises the real interface. Sandbox stages see bound bytes read-only at /input/reference/{key}/.

A binding may instead be a link (ProblemRevision 1.2.0): the binding carries url, an absolute https:// address where the content lives, and TfP stores no bytes for the slot. Its content_hash and size_bytes are then the author's statement about the content at that URL — TfP does not fetch it and never checks them; readers compare what they download against them. The slot's media type and size limits still apply. A linked slot is listed with its URL everywhere the revision's inputs appear (the Problem page, reference_resources, the submission page, the review casefile, the revision package), and the reference endpoint redirects to the URL, but sandbox stages do not mount it: /input/reference/{key}/ is absent for that slot, so a checker that needs the content must have the bytes bound as a stored binding. Conformance fixtures always bind bytes. Authoring convention: reference/<key>.link.json.

This is an approved extension to the ProblemRevision schema. It is deliberately minimal: there is no general Resource object.

A slot can be declared sealed: until release, only Problem managers and sandbox stages explicitly selecting that slot can read its bytes. Every sandbox stage in a sealed Contract declares reference_input_slots; public format checks therefore receive only their public inputs. Protected-stage logs and evidence are withheld until label release, while final scores have an independent score_release policy. See Sealed reference inputs.

Stages: an ordered plan, not a workflow language

A Contract's stages are an ordered list. Stages run in order, each must pass before the next is attempted, and a run reaches verified only when every stage has passed.

That is the whole control model: the stages are any finite ordered sequence of sandbox, review and external in any order and multiplicity (no cap, no fixed order), run strictly sequentially, with no parallel stages, no branching, no conditionals, and no user-supplied control flow. Sequential means only that stage N+1 runs after stage N passes. A Contract is a verification plan, not a workflow program. Several cheap diagnostic checks belong inside one sandbox implementation, reported in that stage's evidence, rather than as extra stages. Composability lives in the ReviewProtocol; the Contract stays deliberately plain.

The kind records who ran the check, which is what a reader needs to know how much to trust a pass. Whether an external stage is an institution's acceptance API, a physical measurement, or a future-world outcome, and how long it takes, belongs in the stage's title, description_md, external_system, and evidence schema — not in the kind. An ORD deposition is sandbox (structurally valid ORD?) → review (faithful to the source paper?) → external (does ORD accept it?); each stage establishes only its own statement, and stopping at the first non-pass avoids consuming scarce review capacity on a Submission that already failed a cheap check.

Sandbox stages

A sandbox stage may declare an evidence_schema: a JSON Schema that /output/evidence/summary.json must satisfy, so evidence is structured and comparable across implementations of the same Contract. Only sandbox stages carry conformance fixtures and implementations.

Review stages

A review stage carries review_protocol_id, pinning one immutable ReviewProtocol. The protocol's final outcome maps accept → verified, reject → refuted, unresolved → inconclusive. Changing the pinned protocol changes the Contract's acceptance semantics, so it is a new Contract. Full semantics: Review reference.

External stages and rule_owner

An external stage names the external_system and declares rule_owner, a machine-readable field with two values:

The schema enforces both conditional requirements. This field is what prevents an author-controlled endpoint from manufacturing the claim that TfP independently verified something: with rule_owner: contract the endpoint cannot decide the outcome, and with rule_owner: partner the run says plainly that the partner decided. Transport (how TfP reaches the external system and retrieves evidence) is specified when external stages are implemented; the Contract fixes only who and what.

A run that reaches a stage TfP cannot execute finishes, with result inconclusive and the unavailable mechanism recorded as the reason. It does not stay running waiting for a mechanism that may be months away. When the mechanism becomes available, re-examination is an explicit new run.

Derived state

Per the platform's derived-state rule, nothing about verification is stored on the Submission, and there are no stored "current" pointers:

Latest run and latest substantive verdict are separate because a later inconclusive or error does not erase an earlier verified or refuted. A failure of TfP's machinery is not evidence about the work.

Interfaces show both, hierarchically: the current verdict is primary and the most recent check is secondary information beneath it — Verified · latest re-check Sep 3: verification error. No additional canonical state is needed to express that.

A run against a Contract other than the one the Attempt's revision pins is history, not current state: it answers a different question.

Run lifecycle

status:   queued ──► running ──► finished
result:                          verified | refuted | inconclusive | error

revoked is not a status. Revocation is a separate write-once block on an already-finished run: the run keeps its status and its result, and gains a record stating that the claim no longer stands.

status is workflow state; result is the outcome. They are separate fields because "waiting on a check" is a fact about the run, not a finding about the Submission. A run in progress carries no result at all, and a run that reaches a stage TfP cannot execute finishes inconclusive rather than remaining open.

• status transitions are forward-only. result, score, evidence_md, and finished_at are written exactly once, at the transition to finished.
• After finished, the run is immutable except for the write-once revocation block and operator-only log redaction.
• A run that cannot complete still finishes, with result error. A run never remains silent.
• Runs are never deleted, and a re-examination is a new run.

Results

The canonical values stay as they are; the right-hand column is the plain-language label interfaces should use.

score is non-null only when the Contract's result_kind is score and the entire run has finished with result: verified. The last successful score stage supplies that score; a subsequent review pause retains it internally but exposes no final score until review succeeds. Stage results have no score field. A sealing policy may additionally defer publication of the final score and protected evaluation verdicts.

Triggers

Registering a new implementation never re-verifies history implicitly. Reruns are always explicit and always additive.

Stage results and per-kind evidence

A run appends one stage_results entry per stage attempted, in Contract order. A list shorter than the Contract's plan is itself information: it says where acceptance got to.

Each entry carries a mechanism block with exactly one non-null member matching its kind, because a proof checker, a review panel, and a physical assay are not evidenced the same way:

• sandbox — the verifier_implementation_id, that implementation's content_hash, the runtime_image_digest actually executed (never a tag, which can move), the backend TfP selected to run it, the exit code, the duration (so a near-timeout pass is visible as one), and the digest of everything written under /output/evidence/.
• review — the review_process_id, review_protocol_id, and protocol_hash of the frozen protocol snapshot. The ReviewProcess record carries the full evidence: assignments, reviewer identities or agent configurations, structured responses, rationale, citations, and every reducer step. See the Review reference.
• external — the external system, their durable reference, the rule_owner copied from the Contract, an optional evidence_hash for anything TfP stored, and the User who attested the outcome, with a timestamp.

Evidence durability

A finished run is self-contained. inputs.artifacts records, per Contract role, the artifact_id, the server-computed content_hash, and the size_bytes of each Artifact examined.

This is what survives withdrawal. When a participant later withdraws an Artifact and TfP deletes the bytes, the run still names exactly which bytes were checked, under which Contract, by which mechanism, with what evidence. The record states what was checked; it does not promise the bytes remain re-checkable. Withdrawal makes the Submission ineligible, so the run stops contributing to the current verdict, and the run itself remains readable.

Stage logs are stored by TfP (served from /verifications/{id}/stages/{stage_key}/log), not as participant Artifacts. They are therefore not withdrawable: the evidence behind a claim cannot be removed by the party the claim is about. log.truncated records capture-ceiling truncation rather than hiding it.

Operator redaction. A verifier can print a credential or personal data by accident, so log.redaction exists: operator-only removal of log content, with a reason from a closed list (secret_material, personal_data, legal_requirement). Participants cannot invoke it.

The redaction record is append-only and retains original_content_hash, original_size_bytes, redacted_at, and redacted_by_user_id, so the run can state that a log of that hash and length existed and was redacted, without retaining the content. A run's inputs, artifact hashes, stage results, result, and evidence_md are never redactable, so redaction cannot be used to reach around Artifact withdrawal or to remove semantic evidence.

Withholding protected-stage logs and evidence_md until label release is not redaction: nothing is removed. Public validation diagnostics remain readable; combined run evidence is withheld when it would disclose a protected stage. These output projections apply to managers too; authenticated manager access to reference bytes is separate. At release, authorized readers see the retained record (Sealed reference inputs).

Revocation

revocation is write-once and additive. It records revoked_at, revoked_by_user_id, and reason_md; the run's inputs, stage results, evidence, and logs all remain readable.

• Revoking a run removes it from the current verdict. It does not turn the run into a refutation.
• Yanking an implementation does not revoke its runs. A superseded implementation leaves its results standing; an implementation found to disagree with its Contract requires each affected run to be revoked explicitly, with a reason.
• Yanking a Contract stops it being offered for new ProblemRevisions. Existing pins keep resolving and past runs keep their meaning.

Sandbox execution interface

A VerifierImplementation is a digest-pinned OCI image with an entrypoint, resource requirements (vcpu, memory_mb, disk_mb, timeout_seconds), and network: none. It declares requirements and never a backend: TfP selects a compatible execution backend at run time and records it on the run, so verification claims do not depend on which provider ran them, and a provider can supply capacity without any author republishing. Images are pre-loaded by TfP; nothing is fetched during a run.

A script checker (schema 0.4.0, an approved extension of this object) is the same Implementation with the image being one of TfP's own script runtimes (runtime.image_ref = tfp-runtime/python:1, its digest the actual OCI image pinned in the runtime catalogue) and one more immutable block, program {filename, content_hash, size_bytes}: the author's one source file, stored content-addressed, mounted read-only at /input/checker/checker.py beside the inputs and run by the runtime's fixed command. program is part of content_hash, so a changed script is a new Implementation. It stays under the same Contract only if normative acceptance semantics are unchanged; changed criteria require a new Contract and ProblemRevision. Fixtures are regression evidence, not proof of equivalence. The runtime catalogue pins the actual OCI image digest globally; a deployment can enable that image, but cannot redefine the name. Authoring and lifecycle: Script checkers.

Every backend presents the same filesystem:

/input/manifest.json            read-only: run id, contract, stage, revision,
                                submission summary, artifact and reference
                                entries with hashes, prior stage results
/input/artifacts/{role}/...     the Submission's Artifacts, by Contract role
/input/reference/{key}/...      only the stage's selected stored reference inputs,
                                by slot; a slot bound by link (the binding carries
                                url) is never mounted and is absent here

/output/result.json             required: {"result": "verified" | "refuted" | "inconclusive",
                                "score"?, "reason"?, "findings"?: [...]}
/output/evidence/...            optional; hashed and preserved; summary.json
                                must satisfy the stage's evidence_schema if one
                                is declared

An implementation may emit verified, refuted, or inconclusive. error is reserved for TfP's execution machinery: a non-zero exit, a missing or malformed result.json, or an exhausted limit is recorded by the runner as error or inconclusive, never as refuted. score is accepted only when the stage's effective result_kind is score and the result is verified. A sandbox stage may override the Contract's scored default with pass_fail, for example for public format validation. The manifest carries that effective stage kind. Isolation, the exact manifest schema, and the runner protocol are specified under Runtime.

Submission requirements

submission_requirements defines what makes a Submission verifiable, never what makes it valid. A Submission that does not satisfy them produces an inconclusive run with the unmet requirement recorded — a mismatch is a statement about the packaging, not the work.

Artifacts map to required_artifacts roles by the Submission's artifact_ids order, so a Contract never dictates filenames. A Contract's declared media_types filter is a convenience; an implementation must validate content, because media_type is participant-declared and stored canonicalized.

Preflight is not verification

A ProblemRevision may pin a Skill that tells the solver how to run the same check locally before submitting. That is encouraged and it is not authoritative: the solver controls that environment. The authoritative check runs on TfP's side, after the Submission exists.

This needs no object of its own. Preflight instructions live in the pinned Skill, which is already immutable and already versioned.

tfp verify is that preflight for any Problem whose revision pins a Contract:

tfp verify <problem> --artifact <role>=<path>… [--summary <text> | --summary-file <path>] [--revision <n>] [--json]

The tfp bundle comes from get_authoring_toolkit, open to every connected User; tfp login --mcp signs it in from an agent. The command reads the revision and its bound reference inputs (a slot bound by link is skipped with a printed note, as TfP would not mount it either), checks the Submission requirements (a miss is reported the way TfP would record it: inconclusive, with no stage run), then runs each sandbox stage in order with the same manifest, mount paths, builtin backend and interpretation as a VerificationRun, against the stage's current conformance-passed implementation (a custom image runs under Docker when a daemon answers), stopping at the first stage that does not pass. Review and external stages are reported, never run. While sealed inputs remain protected, the command runs the public sandbox stages before the first protected stage and reports that stage and the remainder as not run locally. It never downloads sealed bytes, including for a manager. After release it can run those stages normally. The exit code is 0 when every stage it reached passed, 1 otherwise, 2 for a usage error. Local preflight creates no Submission and consumes no submission quota. The run TfP creates on create_submission remains the authoritative one.

Worked examples

Both examples are checked in under schemas/examples/ and validated against the schemas in CI.

SAT: one Contract, many Problems

verifier-contract.sat.json. The SAT Solver Dogfood Problems ask for a satisfying assignment to a CNF instance. This is what Stage 6B builds against.

Verifier — @tfp/sat-assignment (vfr_…), the methodology family.

VerifierContract v1, result_kind: pass_fail, one reference slot:

"reference_inputs": [
  { "key": "instance", "required": true, "media_types": ["text/plain"],
    "max_bytes": 10485760,
    "description": "The CNF instance in DIMACS format that the submitted assignment must satisfy." }
]

statement_md — A result is verified when the submitted assignment file, parsed as SAT-competition v-line format, assigns every variable of the bound CNF instance and satisfies all of its clauses. Assignments mentioning variables outside the instance are rejected. This establishes that the instance is satisfiable and that this assignment witnesses it. It does not establish that the assignment is unique or minimal.

One sandbox stage, assignment_check, with an evidence_schema requiring clauses_total and clauses_satisfied. One Submission role, assignment (text/plain, ≤ 1 MiB).

Four conformance fixtures, each binding instance to small.cnf and assignment to a different file:

The last two pin the distinction most easily collapsed: an assignment that breaks the Contract's stated rule (refuted) versus a file the checker could not read at all (inconclusive).

ProblemRevision (problem-revision.sat.json) pins the Contract and binds the slot:

"verifier_contract_id": "vct_01jf90aa4rrc",
"verifier_input_bindings": [
  { "key": "instance", "content_hash": "sha256:…", "size_bytes": 4821, "media_type": "text/plain" }
]

Five hundred SAT Problems are five hundred revisions binding instance differently, under one Contract and one conformance suite.

VerifierImplementation v1 binds stage_key: "assignment_check", pins its image by digest, declares 1 vCPU / 4096 MB / 600 s / network: none, records source_uri / source_revision / license, runs the four fixtures, and records conformance: {status: "passed", fixtures_total: 4, fixtures_passed: 4}. Only then is it the stage's current implementation.

The flow. An Attempt uploads solution.txt and creates a Submission referencing it. TfP creates a run with trigger: submission, freezing inputs.artifacts = [{role: "assignment", artifact_id: "art_…", content_hash: "sha256:…", size_bytes: 512}], mounts the bound instance at /input/reference/instance/, executes the stage on a selected backend, and the run finishes verified with the backend, image digest, exit code, duration, and evidence digest recorded.

Later. The participant withdraws the Artifact. Its bytes are deleted, the Submission becomes ineligible, and the run stops contributing to the current verdict. The run remains: it still says which Contract was satisfied, by which implementation, on bytes with that exact hash.

Later still. The implementation is found to accept assignments naming out-of-range variables. A fixture pinning that case is added to the Contract, v1 fails conformance, v2 replaces it, and every affected run is revoked individually with that reason. The Contract's normative semantics never changed, so no ProblemRevision moved.

Materials synthesis: sandbox → review → external

verifier-contract.materials.json. A Problem asks for a synthesis recipe that, executed by the A-Lab at Lawrence Berkeley National Laboratory, yields a target phase.

Three reference slots: inventory_snapshot, furnace_envelope, target_phase. Three stages:

The lab's own assessment is a finding in the evidence. The stage result is TfP's, computed from the Contract's rule. Had the Contract instead declared rule_owner: partner, the run would say plainly that the A-Lab decided. Conformance fixtures exist only for recipe_check: valid_recipe, unbalanced, garbage (not JSON → inconclusive).

A candidate that fails recipe_check never reaches the reviewer, and a recipe the reviewer declines never reaches the furnace — cheap checks first, scarce capacity last.

Invariants JSON Schema cannot express

These are contract requirements that the schema files cannot state and that Stage 6B must therefore enforce in code, with tests:

• A Contract with any sandbox stage carries at least one fixture for that stage. Fixture sufficiency for a stage's declared semantics is a judgment made at publication, not a machine-checkable rule; only the presence of at least one fixture is enforceable.
• Every conformance_fixtures[].stage_key names a sandbox stage of the same Contract, and every fixture role is a declared required_artifacts role.
• Every VerifierImplementation.stage_key names a sandbox stage of its Contract.
• Exactly one member of a stage result's mechanism block is non-null, and it matches that stage's kind.
• score is non-null on a run only when the Contract's result_kind is score and the run's result is verified; the Contract's score block is non-null exactly when result_kind is score.
• Stage keys are unique within a Contract; fixture keys and reference-input keys likewise.
• Every fixture binds every required reference slot selected by its stage, and binds no unknown or unselected slot; every ProblemRevision verifier_input_bindings entry names a declared slot, every required slot is bound exactly once, and the bound media type and size satisfy the slot's constraints.
• A review stage's review_protocol_id resolves to a non-yanked ReviewProtocol whose purpose is acceptance and whose subject_kind is submission.
• An implementation's limits.network is none.
• Only an implementation with conformance.status = 'passed' executes an authoritative run.

Explicitly not in Stage 6A

Kept out of 6A:

• No verification status on Submission. It is derived from runs.
• No workflow language. Contract stages are an ordered plan: no branching, no conditionals, no user-supplied control flow.
• No external transport. How TfP reaches an external system and retrieves evidence is specified with the external-stage adapters. 6A fixes rule_owner, external_system, evidence_schema, and acceptance.
• No verifier reputation, ranking, or leaderboards. A run settles a Contract's statement; it does not score people.
• No partial credit beyond the Contract's own declared score scale.
• No implicit re-verification. A new implementation never rewrites the past; reruns are explicit records.
• No preflight object. Solver-side checking lives in the pinned Skill.
• No sandbox runtime. The filesystem interface and result values are fixed above; isolation, the manifest schema, backend selection, and the runner protocol are Stage 6B.
• No MCP write surface for verification. Agents do work and submit; they do not adjudicate their own results. Read tools for runs come with 6B.

Runtime (Stage 6B)

What the implementation fixed beyond 6A, all within the frozen model.

The manifest

/input/manifest.json is version tfp.verification-manifest/v0.1, an object with exactly: version, run_id, verifier_contract_id, stage_key, problem_revision_id, submission {id, summary_md, summary_included} (summary text only when the Contract accepts text and the Submission gave one), artifacts[] {role, artifact_id, path, filename, content_hash, size_bytes, media_type}, reference[] {key, path, filename, content_hash, size_bytes, media_type}, prior_stage_results[] {stage_key, kind, result}, result_kind, and the implementation's limits. Paths are absolute inside the sandbox; an implementation reads the manifest for paths rather than listing directories. The schema is MANIFEST_SCHEMA in apps/worker/src/verification-contracts.ts, and a test asserts every manifest handed to a stage validates against it. Conformance fixtures present the same manifest with cfx_-prefixed run and revision ids.

Mounts and names

Role and slot keys are Contract keys. A participant's filename is reduced to one safe path segment (no separators, no traversal, no control characters, no leading dot; an unsafe name falls back to a synthetic one), so an Artifact can neither escape its role directory nor collide with the manifest. /input/** is read-only; /output/** is writable within limits.disk_mb; the captured log is bounded at 256 KiB and log.truncated records the cut; evidence is bounded at 8 MiB and a stage that exceeds it is error.

How the runner interprets an outcome

Before any stage executes, the runner re-reads every input Artifact and reference blob and re-hashes it against the record frozen at run creation; different bytes than recorded finish the run error with nothing executed. A withdrawn Artifact finishes it inconclusive. A run whose execution keeps faulting is finished error after three attempts by the queue consumer or the hourly sweep; it is never left queued. One executor holds a run at a time (a lease that outlives the largest stage timeout), stage results are appended compare-and-set, and a Submission whose run was never created gets one from the sweep.

Backends

Backend selection is by runtime.image_digest only; the tag in image_ref is display. Two backends exist, tried in order:

A script checker (tfp-runtime/python:1 with a program) uses the same tfp-runner backend as custom images. Its catalogue pins a real OCI digest and a fixed command; deployments cannot redefine the name. The program is mounted at /input/checker/checker.py. Implementations hash the real image digest and source bytes. Stage results record the resolved linux/amd64 image digest. Each invocation uses a fresh container identity and destroys it after collecting outputs, including retries, fixtures and custom images. The application uses /run-isolated and requires the trusted runner's fresh-container-v1 response marker; existing runners need an operator rollout. Missing program bytes are an operational failure, never a verdict.

Every run records which backend ran on the stage result, as the model requires. The SAT implementation in production is tfp-builtin; its conformance (4/4) is re-recorded by every seed run.

Read surface

• Web: /verifications/{id} (the canonical run page), /verifications/{id}/stages/{stage_key}/log.
• API: GET /api/verifications/{id}, GET /api/submissions/{id}/verification (derived state plus every run), GET /api/verifier-contracts/{id} (with implementations and their conformance), GET /api/verifier-implementations/{id}, GET /api/verifiers. Revisions now carry verifier_input_bindings.
• MCP (schemas/mcp-tools.json 0.7.0): get_verification, list_verifications, get_verifier_contract, the resource tfp://verifications/{id}, and create_submission returns verification_run_id. The lookup tools are read-only; create_submission submits work for evaluation.

Sweeps are recovery, never latency

Every scheduled sweep in verification (sweepQueuedRuns, sweepPendingConformance, the review sweeps) exists for a lost queue message or a dead consumer. The normal path is event-driven: a Submission enqueues its run; a custom Implementation enqueues its conformance the moment it is created and the message retries every few seconds until its runner is available; an Implementation passing re-enqueues every run that was waiting on it. An author or solver should see seconds, and a sweep firing on user-visible work is a bug to investigate, not expected behaviour.

Remaining execution limitations

Operator log redaction (the record shape exists; no endpoint yet) and external-stage adapters are not implemented. Custom-image runners are available through the registered runner path described in Backends. Reruns (/admin/rerun-verification), revocation (/admin/revoke-verification) and implementation yanking (/admin/yank-implementation) are operator actions behind the admin secret, not participant or agent actions. Conformance runs keep only their latest logs; the record carries counts and failures, not evidence hashes.