Normative sourceView source on GitHub

Rendered from standard/VSTD-1.md at build time without changing its status. The repository source controls if this presentation differs.

Verifier Standard (VSTD)-1 — Claim Mechanics#

Acronyms: artificial intelligence (AI); conjunctive normal form (CNF); directed acyclic graph (DAG); Davis-Putnam-Logemann-Loveland (DPLL); International Organization for Standardization (ISO); JavaScript Object Notation (JSON); Request for Comments (RFC); Boolean satisfiability problem (SAT); Secure Hash Algorithm 256-bit (SHA-256); satisfiability modulo theories (SMT); trusted computing base (TCB); Coordinated Universal Time (UTC); Unicode Transformation Format, 8-bit (UTF-8).

Reader aid: concept glossary and primary precedents.

Numbered profile: VSTD-1 on the object axis; required closure coordinate: Claim Mechanics (see LADDER.md) Receipt serialization: schema_version = "VSTD-1"; see WIRE_IDENTIFIERS.md Status: Project Specification with Implemented Reference Subset Maintainer: TimeLordRaps Date: 2026-08-21

1. Purpose & Thesis#

VSTD specifies infrastructure for consequential computational claims to carry evidence checkable outside its producer. Conformance is defined by this document, not by the identity of its maintainer.

Modern AI systems, scientific simulators, and autonomous code generators routinely produce complex assertions without an attached, machine-checkable audit trail showing what evidence is offered for those claims. VSTD-1 is a project specification for representing claims, capturing runtime provenance, structuring machine-readable verification receipts, defining reproduction-fidelity states, and separating trusted computing bases from untrusted outputs. It is not a consensus or accredited standard.

2. Scope & Boundaries#

2.1 What VSTD-1 Covers#

2.2 What a VSTD Verification Claim Does NOT Imply#

  1. Universal Truth: Verification is strictly relative to the declared formal system, input formula, and explicit scope.
  2. Unbounded Safety: A verified component does not guarantee overall system safety if surrounding orchestration or unmodeled environmental dynamics fail.
  3. Unchecked Prose: Non-extracted, unverified natural language outside the formal translation grammar is not certified.

3. Epistemic Ontology & Claim Statuses#

Claims conforming to this specification must carry one of the following explicit status labels. Producers and validators MUST downgrade or challenge a claim when applicable evidence is missing or falsified. A historical receipt is immutable: correction is an additive record rather than an in-place rewrite.

StatusDefinition
DEMONSTRATEDThe claim is backed by executable tests or formal proofs that pass in a reproducible environment with recorded execution coordinates. Actor independence is a separate claim.
BENCHMARKEDQuantitative performance or accuracy metrics have been empirically measured against a defined reference baseline.
SUPPORTEDTheoretical derivation or empirical evidence is established, but automated end-to-end continuous verification is partial.
IMPLEMENTED_UNVALIDATEDCode or logic exists on disk, but automated end-to-end verification has not yet run or passed.
INDETERMINATEEvidence is ambiguous, supporting leaves are unspecified, or solver execution timed out.
UNSUPPORTEDNo valid empirical or formal evidence is attached to the proposition.
FALSIFIEDAn executable check, counterexample, or evidence-bound audit refuted the claim.
HYPOTHESISA stated conjecture intended for experimental falsification.
LONG_RANGE_OBJECTIVEA strategic or architectural aspiration requiring substantial future R&D.

4. Claim Representation Schema#

A canonical claim record contains:

5. Independent Verification & Trusted Computing Base (TCB)#

To prevent self-referential confirmation bias (systems verifying their own uninspected outputs), VSTD-1 defines independent-verification role separation as a conformance requirement for claims labeled independent:

Target System (Producer)
       ↓ (Generates derivation / CNF / artifacts)
Independent VSTD-Conformant Auditor
       ↓ (Runs separately implemented DPLL solver + DAG grounding checker in isolated TCB)
Structured VFY Receipt

Independence in this profile is a claim about distinct actors occupying the producer and checker roles. Two executions that return the same result do not prove that separate actors performed them; nor do two processes or machines. Those are artifact and runtime observations. Actor independence requires separately bound evidence, and it never strengthens the checked result merely because an actor is identified or trusted.

Trusted Computing Base Invariant#

An auditor described as independent must:

  1. Share zero solver state or runtime logic with the producer.
  2. Rely exclusively on a minimal, inspectable codebase (e.g. Python standard library).
  3. Explicitly declare its TCB components in every generated receipt.

Running the bundled reference implementation does not by itself establish actor, implementation, or runtime independence. A receipt MUST state the actual separation achieved. If distinct actors are not evidenced, actor independence is NOT_DEMONSTRATED even when two results match. If producer and auditor share relevant logic or state, the result is still inspectable but MUST NOT be labeled independent on that seam.

Serialized EVIDENCED status words and evidence-reference strings are declarations, not validated bindings. A runtime MUST derive independent verification only after an implemented validator resolves the referenced evidence, binds it to the producer and checker executions, and establishes distinct actors plus the claimed implementation and runtime seams. The VSTD 1.2.0 reference runtime implements no such adapter; it therefore treats externally supplied assertions as no stronger than DECLARED, rejects receipts that serialize them as EVIDENCED, and never emits EVIDENCED.

6. Reproducibility Taxonomy#

VSTD-1 defines a five-state reproduction-fidelity taxonomy. The public ReproducibilityLevel name is a compatibility identifier; it does not denote a numbered VSTD profile or assurance strength:

  1. BITWISE_IDENTICAL: Byte-for-byte exact match across all generated files, logs, and artifacts.
  2. CONTENT_IDENTICAL: Canonical JSON representation of stable verification payload matches exactly, ignoring volatile execution fields (timestamps, elapsed wall-clock ms, hostnames).
  3. EVIDENCE_EQUIVALENT: All checks, proofs, SAT assignments, and invariant bounds evaluate to the same truth values and proof certificates, though internal trace order or solver step counts may differ.
  4. RESULT_EQUIVALENT: Summary verification verdict (VERIFIED/FALSIFIED) and primary metrics agree within declared tolerance bounds.
  5. SEMANTIC_REPRODUCTION: The underlying formal proposition is sustained under a separately implemented translation or alternate solver. This does not establish distinct actors.

7. Canonical Receipt Specification & Hashing#

A VSTD-1 receipt separates stable verification content from volatile execution metadata. The receipt kind is explicit:

receipt.json
├── schema_version: "VSTD-1"
├── receipt_kind: "claim_mechanics"
├── receipt_id: "VFY-XXXXXX"
├── canonical_digest: SHA256(canonical_json(stable_payload))
├── claim: {...}
├── evidence: {...}
├── target_result: {...}
├── independent_audit: {...}
├── provenance: {...}
├── reproducibility: {...}
└── execution_metadata: (volatile: timestamps, elapsed_ms, logs)

Canonicalization Algorithm#

  1. Extract stable fields (schema_version, receipt_kind, receipt_id, claim, evidence, target_result, independent_audit, provenance_stable, reproducibility).
  2. Serialize the VSTD-1 JSON subset with alphabetically sorted object keys, compact separators "," and ":", UTF-8 encoding, and no non-finite numbers. This project-specific canonicalization is deterministic for the supported value subset; VSTD-1 does not claim full RFC 8785 conformance.
  3. Compute SHA-256 digest over the serialized bytes.
  4. The digest remains invariant across directory moves, path changes, and reformatting of human-readable reports.

8. Challenge & Correction Model#

  1. Any party may submit a counterexample, failing test, or ungrounded leaf finding.
  2. A validator or reproducer returns failure when the bound content or declared rerun does not match. It does not silently mutate a historical receipt.
  3. The maintainer or integrating system must publish an additive FALSIFIED, INDETERMINATE, or challenged record, preserving the affected receipt's provenance.

9. Implementation Roadmap & Extensibility#