VerifierImplementation schema
Generated from the canonical schema
schemas/verifier-implementation.schema.jsonbyscripts/generate-schema-docs.mjs— do not edit this page by hand.
Stage 6A contract (proposed). An immutable executable mechanism for one sandbox stage of one VerifierContract: a digest-pinned container image, an entrypoint, resource requirements, and provenance; or, for a script checker, one author program (program, content-addressed) run by a TfP script runtime named in runtime.image_ref (tfp-runtime/python:1), whose digest pins the actual OCI image in the immutable runtime catalogue on every deployment. The Contract defines acceptance semantics; an implementation computes one stage of them and may be wrong. Compatibility rule: if the Contract's normative acceptance semantics are unchanged, a new Implementation is published under the same Contract and no ProblemRevision moves — even when correcting a non-conforming implementation changes the outcomes it produces. Only a change to the normative semantics creates a new Contract and a new ProblemRevision. An implementation may execute authoritative verification only after reproducing the Contract's conformance fixtures for its stage, recorded in conformance. The implementation declares requirements, never a backend: TfP later selects a compatible execution backend and the VerificationRun records which one ran. The filesystem interface is fixed: /input/manifest.json, /input/artifacts/{role}/..., /input/reference/{key}/...; /output/result.json (result ∈ verified | refuted | inconclusive — error is reserved for TfP's execution machinery) and /output/evidence/... (hashed and preserved).
Schema version: 0.4.0 · $id: https://tokensforprogress.org/schemas/verifier-implementation.schema.json
Fields
id
Type: string · Required: yes · Mutable: no · Pattern: ^vfi_[0-9a-z]{10,32}$
Stable opaque identifier — what every VerificationRun it produced records.
Example: "vfi_01jn5p2c9fxk"
verifier_contract_id
Type: string · Required: yes · Mutable: no · Pattern: ^vct_[0-9a-z]{10,32}$
The Contract whose acceptance semantics this implements. An implementation is never shared across Contracts.
Example: "vct_01jf90aa4rrc"
stage_key
Type: string · Required: yes · Mutable: no · Pattern: ^[a-z0-9]+(_[a-z0-9]+)*$
The sandbox stage of that Contract this implements. Only sandbox stages have implementations; the binding is explicit rather than positional.
Example: "assignment_check"
version_number
Type: integer · Required: yes · Mutable: no
TfP's own sequential version within the Contract stage, starting at 1. The stage's current implementation is derived as the highest non-yanked version_number whose conformance has passed; there is no stored pointer, and a non-conforming implementation is never current.
Example: 2
runtime
Type: object · Required: yes · Mutable: no
The pinned execution target: an OCI image identified by digest. Backend selection (which sandbox provider runs it) is not part of the implementation.
runtime.kind
Type: container · Required: yes · Mutable: —
Execution model. v0 defines one: an OCI container image. The enum exists so later models can be added without reinterpreting existing records.
Example: "container"
runtime.image_ref
Type: string · Required: yes · Mutable: —
Human-readable image reference, for display and provenance. A TfP builtin (tfp-builtin/…:n) uses a name hash. A TfP script runtime (tfp-runtime/…:n) uses a friendly catalogue name here, but image_digest pins the actual OCI image, identical on every deployment.
Example: "ghcr.io/tfp/lean4-verifier:4.9.0"
runtime.image_digest
Type: string · Required: yes · Mutable: — · Pattern: ^sha256:[0-9a-f]{64}$
Immutable content digest of the image. This, not the tag, is what executes: a moved tag must not change what a past run meant.
Example: "sha256:9f2b7c1e4a8d6035b1c2ee74d0f39a4b5c6d7e8f90123456789abcdef0123456"
entrypoint
Type: array · Required: yes · Mutable: no
Argument vector invoked inside the container. Inputs are presented on the fixed filesystem interface and the verdict is written to /output/result.json. An argument vector rather than a shell string, so participant-controlled text is never interpolated into a command line.
Example: ["/usr/local/bin/verify"]
limits
Type: object · Required: yes · Mutable: no
Resource requirements the run executes under, pinned rather than set per run so results stay comparable, and used by TfP to select a compatible backend. Exhausting a limit resolves the run inconclusive, never refuted.
limits.vcpu
Type: integer · Required: yes · Mutable: —
CPU cores required.
Example: 1
limits.memory_mb
Type: integer · Required: yes · Mutable: —
Memory ceiling for one run.
Example: 4096
limits.disk_mb
Type: integer · Required: yes · Mutable: —
Scratch disk required.
Example: 4096
limits.timeout_seconds
Type: integer · Required: yes · Mutable: —
Wall-clock ceiling for one run.
Example: 600
limits.network
Type: none · Required: yes · Mutable: —
Network access during execution. v0 accepts only none: a verifier that needs the network is not a sandbox verifier. Images are pre-loaded by TfP; nothing is fetched during a run.
Example: "none"
content_hash
Type: string · Required: yes · Mutable: no · Pattern: ^sha256:[0-9a-f]{64}$
Deterministic digest over this implementation's pinned execution inputs (runtime digest, entrypoint, limits, and any snapshotted harness files), computed server-side.
Example: "sha256:1a2b3c4d5e6f708192a3b4c5d6e7f80912a3b4c5d6e7f8091a2b3c4d5e6f70819"
source
Type: object · Required: yes · Mutable: no
Where the mechanism came from. Provenance is required: participants are asked to accept a machine's verdict, so what produced it must be inspectable.
source.source_uri
Type: string \| null · Required: yes · Mutable: —
Public repository the implementation was built from; null only when there is none to point at.
Example: "https://github.com/tfp/verifiers"
source.source_revision
Type: string \| null · Required: yes · Mutable: —
Exact commit built, never a branch name.
Example: "b41f9e2c7d0a15368e94b2c1f7a08d35e6c9014b"
source.license
Type: string \| null · Required: yes · Mutable: —
SPDX identifier of the implementation's license, when known.
Example: "Apache-2.0"
program
Type: object · Required: no · Mutable: no
Script checkers only (runtime.image_ref names a tfp-runtime/…): the author's one program file, stored content-addressed by TfP and mounted read-only at /input/checker/checker.py beside the run's inputs, where the runtime's fixed command runs it. Absent for a builtin or a container image. Part of content_hash, so a changed script is a new Implementation under the same Contract.
program.filename
Type: string · Required: yes · Mutable: —
The file's name in the authoring package, for display; the sandbox mounts it under the fixed name.
Example: "checker.py"
program.content_hash
Type: string · Required: yes · Mutable: — · Pattern: ^sha256:[0-9a-f]{64}$
SHA-256 of the program bytes, computed server-side; the bytes are served at GET /api/verifier-implementations/{id}/program.
Example: "sha256:7f3a0b2c9d8e1f405162738495a6b7c8d9e0f1a2b3c4d5e6f708192a3b4c5d6e"
program.size_bytes
Type: integer · Required: yes · Mutable: —
Size of the program; a script checker is at most 256 KiB.
Example: 1420
conformance
Type: object · Required: yes · Mutable: yes
Result of running the Contract's conformance_fixtures for this implementation's stage. An implementation may execute authoritative verification only while status is passed. Re-recorded when the Contract's fixtures or the implementation change. A failed implementation stays registered and inspectable.
conformance.status
Type: pending | passed | failed · Required: yes · Mutable: —
pending until the fixture suite has been run; passed only when every fixture for this stage produced its expected_result (and expected_score, where applicable).
Example: "passed"
conformance.checked_at
Type: string \| null · Required: yes · Mutable: — · Default: null
When the fixture suite was last run against this implementation; null while pending.
Example: "2026-09-05T09:25:00Z"
conformance.fixtures_total
Type: integer · Required: yes · Mutable: —
Number of the Contract's fixtures applicable to this stage.
Example: 4
conformance.fixtures_passed
Type: integer · Required: yes · Mutable: —
How many reproduced their expected outcome.
Example: 4
conformance.failures
Type: array · Required: yes · Mutable: —
Each fixture that did not reproduce, with what was expected and what happened. Empty when status is passed.
conformance.differential_against_implementation_id
Type: string \| null · Required: yes · Mutable: — · Default: null · Pattern: ^vfi_[0-9a-z]{10,32}$
Optionally, a previous implementation of the same stage this one was differentially tested against on inputs beyond the fixtures. Fixtures pin the cases someone thought of; differential testing is how disagreements nobody thought of surface. Null when no differential run was performed.
Example: null
created_by_user_id
Type: string · Required: yes · Mutable: no · Pattern: ^usr_[0-9a-z]{10,32}$
The User who registered this implementation.
Example: "usr_01jf90aa4rrc"
created_at
Type: string · Required: yes · Mutable: no
RFC 3339 UTC timestamp of registration.
Example: "2026-09-05T09:20:00Z"
yanked_at
Type: string \| null · Required: yes · Mutable: yes · Default: null
Write-once withdrawal from use. A yanked implementation runs nothing new. Yanking does not by itself revoke the runs it produced: a superseded implementation leaves its results standing, while a non-conforming one requires its affected runs to be revoked explicitly, with a reason.
Example: null
JSON Schema source
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"$id": "https://tokensforprogress.org/schemas/verifier-implementation.schema.json",
"title": "VerifierImplementation",
"description": "Stage 6A contract (proposed). An immutable executable mechanism for one `sandbox` stage of one VerifierContract: a digest-pinned container image, an entrypoint, resource requirements, and provenance; or, for a script checker, one author program (`program`, content-addressed) run by a TfP script runtime named in `runtime.image_ref` (`tfp-runtime/python:1`), whose digest pins the actual OCI image in the immutable runtime catalogue on every deployment. The Contract defines acceptance semantics; an implementation computes one stage of them and may be wrong. Compatibility rule: if the Contract's normative acceptance semantics are unchanged, a new Implementation is published under the same Contract and no ProblemRevision moves — even when correcting a non-conforming implementation changes the outcomes it produces. Only a change to the normative semantics creates a new Contract and a new ProblemRevision. An implementation may execute authoritative verification only after reproducing the Contract's conformance fixtures for its stage, recorded in `conformance`. The implementation declares requirements, never a backend: TfP later selects a compatible execution backend and the VerificationRun records which one ran. The filesystem interface is fixed: /input/manifest.json, /input/artifacts/{role}/..., /input/reference/{key}/...; /output/result.json (result ∈ verified | refuted | inconclusive — `error` is reserved for TfP's execution machinery) and /output/evidence/... (hashed and preserved).",
"x-tfp-version": "0.4.0",
"type": "object",
"additionalProperties": false,
"required": [
"id",
"verifier_contract_id",
"stage_key",
"version_number",
"runtime",
"entrypoint",
"limits",
"content_hash",
"source",
"conformance",
"created_by_user_id",
"created_at",
"yanked_at"
],
"properties": {
"id": {
"type": "string",
"pattern": "^vfi_[0-9a-z]{10,32}$",
"x-mutable": false,
"description": "Stable opaque identifier — what every VerificationRun it produced records.",
"examples": [
"vfi_01jn5p2c9fxk"
]
},
"verifier_contract_id": {
"type": "string",
"pattern": "^vct_[0-9a-z]{10,32}$",
"x-mutable": false,
"description": "The Contract whose acceptance semantics this implements. An implementation is never shared across Contracts.",
"examples": [
"vct_01jf90aa4rrc"
]
},
"stage_key": {
"type": "string",
"pattern": "^[a-z0-9]+(_[a-z0-9]+)*$",
"maxLength": 40,
"x-mutable": false,
"description": "The `sandbox` stage of that Contract this implements. Only sandbox stages have implementations; the binding is explicit rather than positional.",
"examples": [
"assignment_check"
]
},
"version_number": {
"type": "integer",
"minimum": 1,
"x-mutable": false,
"description": "TfP's own sequential version within the Contract stage, starting at 1. The stage's current implementation is derived as the highest non-yanked version_number whose conformance has passed; there is no stored pointer, and a non-conforming implementation is never current.",
"examples": [
2
]
},
"runtime": {
"type": "object",
"additionalProperties": false,
"x-mutable": false,
"required": [
"kind",
"image_ref",
"image_digest"
],
"description": "The pinned execution target: an OCI image identified by digest. Backend selection (which sandbox provider runs it) is not part of the implementation.",
"properties": {
"kind": {
"type": "string",
"enum": [
"container"
],
"description": "Execution model. v0 defines one: an OCI container image. The enum exists so later models can be added without reinterpreting existing records.",
"examples": [
"container"
]
},
"image_ref": {
"type": "string",
"minLength": 1,
"maxLength": 500,
"description": "Human-readable image reference, for display and provenance. A TfP builtin (`tfp-builtin/…:n`) uses a name hash. A TfP script runtime (`tfp-runtime/…:n`) uses a friendly catalogue name here, but image_digest pins the actual OCI image, identical on every deployment.",
"examples": [
"ghcr.io/tfp/lean4-verifier:4.9.0",
"tfp-runtime/python:1"
]
},
"image_digest": {
"type": "string",
"pattern": "^sha256:[0-9a-f]{64}$",
"description": "Immutable content digest of the image. This, not the tag, is what executes: a moved tag must not change what a past run meant.",
"examples": [
"sha256:9f2b7c1e4a8d6035b1c2ee74d0f39a4b5c6d7e8f90123456789abcdef0123456"
]
}
}
},
"entrypoint": {
"type": "array",
"minItems": 1,
"maxItems": 20,
"items": {
"type": "string",
"minLength": 1,
"maxLength": 500
},
"x-mutable": false,
"description": "Argument vector invoked inside the container. Inputs are presented on the fixed filesystem interface and the verdict is written to /output/result.json. An argument vector rather than a shell string, so participant-controlled text is never interpolated into a command line.",
"examples": [
[
"/usr/local/bin/verify"
]
]
},
"limits": {
"type": "object",
"additionalProperties": false,
"x-mutable": false,
"required": [
"vcpu",
"memory_mb",
"disk_mb",
"timeout_seconds",
"network"
],
"description": "Resource requirements the run executes under, pinned rather than set per run so results stay comparable, and used by TfP to select a compatible backend. Exhausting a limit resolves the run `inconclusive`, never `refuted`.",
"properties": {
"vcpu": {
"type": "integer",
"minimum": 1,
"maximum": 16,
"description": "CPU cores required.",
"examples": [
1
]
},
"memory_mb": {
"type": "integer",
"minimum": 64,
"maximum": 16384,
"description": "Memory ceiling for one run.",
"examples": [
4096
]
},
"disk_mb": {
"type": "integer",
"minimum": 64,
"maximum": 65536,
"description": "Scratch disk required.",
"examples": [
4096
]
},
"timeout_seconds": {
"type": "integer",
"minimum": 1,
"maximum": 3600,
"description": "Wall-clock ceiling for one run.",
"examples": [
600
]
},
"network": {
"type": "string",
"enum": [
"none"
],
"description": "Network access during execution. v0 accepts only `none`: a verifier that needs the network is not a sandbox verifier. Images are pre-loaded by TfP; nothing is fetched during a run.",
"examples": [
"none"
]
}
}
},
"content_hash": {
"type": "string",
"pattern": "^sha256:[0-9a-f]{64}$",
"x-mutable": false,
"description": "Deterministic digest over this implementation's pinned execution inputs (runtime digest, entrypoint, limits, and any snapshotted harness files), computed server-side.",
"examples": [
"sha256:1a2b3c4d5e6f708192a3b4c5d6e7f80912a3b4c5d6e7f8091a2b3c4d5e6f70819"
]
},
"source": {
"type": "object",
"additionalProperties": false,
"x-mutable": false,
"required": [
"source_uri",
"source_revision",
"license"
],
"description": "Where the mechanism came from. Provenance is required: participants are asked to accept a machine's verdict, so what produced it must be inspectable.",
"properties": {
"source_uri": {
"type": [
"string",
"null"
],
"format": "uri",
"maxLength": 500,
"description": "Public repository the implementation was built from; null only when there is none to point at.",
"examples": [
"https://github.com/tfp/verifiers"
]
},
"source_revision": {
"type": [
"string",
"null"
],
"maxLength": 100,
"description": "Exact commit built, never a branch name.",
"examples": [
"b41f9e2c7d0a15368e94b2c1f7a08d35e6c9014b"
]
},
"license": {
"type": [
"string",
"null"
],
"maxLength": 100,
"description": "SPDX identifier of the implementation's license, when known.",
"examples": [
"Apache-2.0"
]
}
}
},
"program": {
"type": "object",
"additionalProperties": false,
"x-mutable": false,
"required": [
"filename",
"content_hash",
"size_bytes"
],
"description": "Script checkers only (runtime.image_ref names a tfp-runtime/…): the author's one program file, stored content-addressed by TfP and mounted read-only at /input/checker/checker.py beside the run's inputs, where the runtime's fixed command runs it. Absent for a builtin or a container image. Part of content_hash, so a changed script is a new Implementation under the same Contract.",
"properties": {
"filename": {
"type": "string",
"minLength": 1,
"maxLength": 255,
"description": "The file's name in the authoring package, for display; the sandbox mounts it under the fixed name.",
"examples": [
"checker.py"
]
},
"content_hash": {
"type": "string",
"pattern": "^sha256:[0-9a-f]{64}$",
"description": "SHA-256 of the program bytes, computed server-side; the bytes are served at GET /api/verifier-implementations/{id}/program.",
"examples": [
"sha256:7f3a0b2c9d8e1f405162738495a6b7c8d9e0f1a2b3c4d5e6f708192a3b4c5d6e"
]
},
"size_bytes": {
"type": "integer",
"minimum": 1,
"maximum": 262144,
"description": "Size of the program; a script checker is at most 256 KiB.",
"examples": [
1420
]
}
}
},
"conformance": {
"type": "object",
"additionalProperties": false,
"x-mutable": true,
"required": [
"status",
"checked_at",
"fixtures_total",
"fixtures_passed",
"failures",
"differential_against_implementation_id"
],
"description": "Result of running the Contract's conformance_fixtures for this implementation's stage. An implementation may execute authoritative verification only while status is `passed`. Re-recorded when the Contract's fixtures or the implementation change. A `failed` implementation stays registered and inspectable.",
"properties": {
"status": {
"type": "string",
"enum": [
"pending",
"passed",
"failed"
],
"description": "`pending` until the fixture suite has been run; `passed` only when every fixture for this stage produced its expected_result (and expected_score, where applicable).",
"examples": [
"passed"
]
},
"checked_at": {
"type": [
"string",
"null"
],
"format": "date-time",
"default": null,
"description": "When the fixture suite was last run against this implementation; null while pending.",
"examples": [
"2026-09-05T09:25:00Z"
]
},
"fixtures_total": {
"type": "integer",
"minimum": 0,
"description": "Number of the Contract's fixtures applicable to this stage.",
"examples": [
4
]
},
"fixtures_passed": {
"type": "integer",
"minimum": 0,
"description": "How many reproduced their expected outcome.",
"examples": [
4
]
},
"failures": {
"type": "array",
"maxItems": 100,
"description": "Each fixture that did not reproduce, with what was expected and what happened. Empty when status is `passed`.",
"items": {
"type": "object",
"additionalProperties": false,
"required": [
"fixture_key",
"expected_result",
"actual_result",
"detail"
],
"properties": {
"fixture_key": {
"type": "string",
"maxLength": 60,
"description": "The Contract fixture that failed.",
"examples": [
"malformed_assignment"
]
},
"expected_result": {
"type": "string",
"enum": [
"verified",
"refuted",
"inconclusive"
],
"description": "What the Contract says a conforming implementation must produce.",
"examples": [
"inconclusive"
]
},
"actual_result": {
"type": "string",
"enum": [
"verified",
"refuted",
"inconclusive",
"error"
],
"description": "What this implementation produced.",
"examples": [
"refuted"
]
},
"detail": {
"type": "string",
"maxLength": 4000,
"description": "Human-readable account of the disagreement.",
"examples": [
"Treated an unparseable v-line as a wrong answer rather than an unverifiable submission."
]
}
}
}
},
"differential_against_implementation_id": {
"type": [
"string",
"null"
],
"pattern": "^vfi_[0-9a-z]{10,32}$",
"default": null,
"description": "Optionally, a previous implementation of the same stage this one was differentially tested against on inputs beyond the fixtures. Fixtures pin the cases someone thought of; differential testing is how disagreements nobody thought of surface. Null when no differential run was performed.",
"examples": [
null
]
}
}
},
"created_by_user_id": {
"type": "string",
"pattern": "^usr_[0-9a-z]{10,32}$",
"x-mutable": false,
"description": "The User who registered this implementation.",
"examples": [
"usr_01jf90aa4rrc"
]
},
"created_at": {
"type": "string",
"format": "date-time",
"x-mutable": false,
"description": "RFC 3339 UTC timestamp of registration.",
"examples": [
"2026-09-05T09:20:00Z"
]
},
"yanked_at": {
"type": [
"string",
"null"
],
"format": "date-time",
"x-mutable": true,
"default": null,
"description": "Write-once withdrawal from use. A yanked implementation runs nothing new. Yanking does not by itself revoke the runs it produced: a superseded implementation leaves its results standing, while a non-conforming one requires its affected runs to be revoked explicitly, with a reason.",
"examples": [
null
]
}
}
}