Verification Context specification

QWED Verification Context v1.0 and v1.1 spec: the JSON record of a verification, its four context layers, verdict, proof_ref, admission, and attestation.

​

QWED Verification Context specification v1.0

Status: Draft Version: 1.0 Introduced in: QWED v7.1.0

The Verification Context is the atomic record of a QWED verification. It standardizes what is being verified, what it means, how it was proven, on what evidence, and what decision followed, so that every QWED engine, SDK, API, CLI, and client speaks one protocol.

A Verification Context document is a single JSON object that validates against the machine-readable JSON Schema shipped with the spec (spec/v1.0/schemas/verification-context.schema.json). Version 1.1 adds one field, the issuing server’s attestation, and has its own schema.

The schema’s $id is https://qwedai.tech/schemas/verification-context/v1.0. If your validator or schema registry resolves the schema by its $id, register it under this URI. Earlier copies of the schema used https://qwed.dev/schemas/verification-context/v1.0, so update any lookups that still reference the old $id.

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://qwedai.tech/schemas/verification-context/v1.0",
  "title": "QWED Verification Context"
}

​

Design goals

• One protocol. Every verification surface emits the same document shape.
• Fail-closed. Anything not proven is UNVERIFIABLE or BLOCKED, never VERIFIED.
• Truth ≠ admission. A proven verdict and a safe-to-run decision are separate fields.
• Honesty. QWED never claims to have verified intent. It verifies a formal statement and shows exactly what was proven.

​

The verified object

The object of verification is a formal statement (for example, x**2 + 2*x + 1 = (x+1)**2), captured in object.formal_statement.

Two rules govern the object:

• The theory is required interpretation context. A formal statement is only meaningful relative to a theory. x² = 4 over the reals and over integers mod 5 are different propositions. The theory lives in the Interpretation layer (below), not in the object.
• The formalization is exposed but never verified. The mapping from natural language to the formal statement is surfaced in object.formalization for confirmation, but object.formalization.verified is always false. QWED claims “we verified THIS formal statement,” never “we verified your intent.”

​

The four context layers

context captures all information required to correctly interpret, reproduce, and trust a verification:

Layer	Field	Contents	Role
Interpretation	context.interpretation	theory / logic / dialect / algebra domain	Gives the object meaning
Proof	context.proof	verifier + version + configuration + theory scope + trusted dependencies	How the object was discharged; sets proof strength
Evidence	context.evidence	retained evidence + proof_ref	What was checked; evidence integrity
Decision	context.decision	admission	The safe-to-run outcome

​

Interpretation layer

Each engine exposes only the interpretation it needs: a theorem prover records theory and logic, SQL records dialect and parser version, code records language and policy version, symbolic math records the algebra domain.

​

Proof layer

The verifier is the trusted computing base (TCB). A proof discharged by SymPy (large TCB) is a different-strength guarantee than one checked by a small trusted kernel. The Proof layer records the full trust boundary:

• verifier and verifier_version — the exact engine and release.
• configuration — solver flags, timeouts, resource limits.
• theory_scope — the logic or axiom set the discharge is relative to.
• trusted_dependencies — libraries and components inside the TCB.
• outcome_treatment — how unknown/timeout/error outcomes are treated. These never resolve to VERIFIED; they resolve to UNVERIFIABLE or BLOCKED (fail-closed).

​

Evidence layer and proof_ref

context.evidence.evidence is the retained evidence. context.evidence.proof_ref is the evidence commitment: an immutable commitment to the verification evidence. It provides evidence integrity and reproducibility. It is not itself the mathematical proof.

How it is computed:

1. Bound payload: the JSON object {"formal_statement": <object.formal_statement>, "context": <context>}, with context.evidence.proof_ref removed before serialization. object.formalization is deliberately excluded: the commitment binds the formal statement, not how it was derived.
2. Canonical encoding: RFC 8785 (JSON Canonicalization Scheme). UTF-8 with no ASCII-escaping, object keys sorted by UTF-16 big-endian byte order, compact separators, and RFC 8785 §3.2.2 number serialization. NaN and Infinity are rejected, and integers that are not exactly representable as IEEE-754 doubles are rejected (fail-closed).
3. Commitment algorithm: SHA-256 over the canonical bytes, expressed as sha256:<64-lowercase-hex>.

Resolution: a consumer resolves proof_ref by removing the stored value, re-deriving the commitment from the supplied document, and comparing. A resolver must reject a mismatch before any ADMIT decision. Missing, malformed, or mismatched evidence is treated as unverified (fail-closed). A proof_ref that cannot be resolved confers no authority.

​

Verdict

verdict is the truth judgment:

Verdict	Meaning	proof_ref
VERIFIED	The claim was checked and proven.	Non-null (sha256:<64-hex>)
UNVERIFIABLE	Not proven (fail-closed).	null
BLOCKED	Verification could not be attempted or completed (fail-closed).	null

The schema enforces two invariants:

• verdict == VERIFIED ⟹ context.evidence.proof_ref is present and matches ^sha256:[a-f0-9]{64}$.
• verdict ∈ {UNVERIFIABLE, BLOCKED} ⟹ context.evidence.proof_ref is null.

​

Admission (truth ≠ admission)

VERIFIED is a truth guarantee, not an admission guarantee. context.decision.admission is the separate safe-to-run decision, one of ADMIT or DENY, computed from the verdict plus policy.

The critical case: a proven-unsafe artifact is VERIFIED (QWED proved it is unsafe) with admission DENY.

Proven false is the same case. A claim the engine disproves (for example the math claim 2+2=5) is VERIFIED with is_valid: false and admission DENY. It is never UNVERIFIABLE, which means the engine could neither prove nor disprove the claim.

Verdict	Truth	Admission (typical)
VERIFIED, valid	Proven safe	ADMIT
VERIFIED, unsafe	Proven unsafe	DENY
VERIFIED, false	Proven false (counter-proof)	DENY
UNVERIFIABLE	Not proven	DENY (fail-closed)
BLOCKED	Verification failed	DENY (fail-closed)

Execution and shipping consumers gate exclusively on admission == "ADMIT". is_valid contributes to the admission decision but is not an alternative authorization gate. A valid statement can still be denied by policy.

​

Conformance

An implementation conforms to this specification if it:

1. Emits documents that validate against the v1.0 JSON Schema.
2. Upholds the verdict invariants: VERIFIED ⟹ non-null proof_ref; UNVERIFIABLE/BLOCKED ⟹ null proof_ref.
3. Treats proof_ref as an evidence commitment, not a proof of truth.
4. Separates truth from admission and gates execution on admission == "ADMIT" only.
5. Exposes the formalization but never marks it verified.
6. Treats unknown/timeout/error outcomes as fail-closed.

​

Version 1.1 and the issuer attestation

A v1.0 document’s proof_ref is an unkeyed commitment. Anyone can compute it, so anyone can build a document, an ADMIT one included, whose proof_ref resolves. It shows the document is internally consistent, not who issued it.

v1.1 is v1.0 plus one field, attestation: the issuing server’s signature. Everything else in v1.0 applies unchanged. The machine-readable schema is spec/v1.1/schemas/verification-context.schema.json, with $id https://qwedai.tech/schemas/verification-context/v1.1, and the prose spec is spec/v1.1/verification-context.md.

• A v1.1 document must carry attestation, and a v1.0 document must not.
• attestation is a compact ES256 JWT. Its header has typ qwed-context+jwt, which separates it from a verdict’s attestation (qwed-attestation+jwt), and a kid naming the signing key.
• Its claims sign the document hash: the SHA-256 of the canonical encoding of every field except attestation, written as sha256: followed by 64 lowercase hex characters, in both sub and qwed.document_hash. The claims also name qwed.version ("1.1"), qwed.verdict, qwed.admission, and qwed.proof_ref.
• The token lasts as long as a verdict’s attestation (QWED_ATTESTATION_TTL_SECONDS, 24 hours by default). An expired document is obtained again, not trusted.

To verify a v1.1 document, check:

1. The signature, with an ES256 P-256 key from the issuer’s JWKS (GET /.well-known/jwks.json). The verified header’s kid names that key, its typ is qwed-context+jwt, and it names no critical extension (crit).
2. The issuer, and that the token has not expired.
3. That qwed.version and the document’s spec_version are both "1.1", that sub and qwed.document_hash are the hash of this document, and that the verdict, admission, and proof_ref the claims name are this document’s.

The attestation authenticates the document relative to the issuer’s key. It does not validate the formal statement or change the verdict or the admission: a signed DENY document is still DENY. A server needs a configured signing key (QWED_SIGNING_KEY or QWED_SIGNING_KEY_FILE) for its documents to verify after a restart or on another replica.

​

Working with Verification Context documents

Verification Context v1.0 is exposed across every QWED surface as of v7.1.0:

• API: POST /verification-context/from-diagnostic, /validate, and /resolve. from-diagnostic returns signed v1.1 documents, and validate and resolve check the attestation by default. The audit row of each successful from-diagnostic call stores the signed document as returned, so when read back from the audit log it verifies until its attestation expires, while the server keeps the signing key. Only the row’s query is redacted, and the stored document keeps any personal data in the request. See audit row.
• Python SDK: client methods and re-exported types on qwed_sdk, plus to_verification_context() on the verifier classes (Math and the secure code executor convert through create_verification_context_from_diagnostic()). validate_verification_context() and resolve_verification_context() verify the attestation by default. See the Python SDK.
• CLI: the qwed context command group. validate and resolve verify the attestation with --server or --jwks-file by default.
• GitHub Action — verdict, admission, proof_ref, and verification_context outputs.

​

Example document

{
  "spec_version": "1.0",
  "object": {
    "formal_statement": "x**2 + 2*x + 1 = (x+1)**2",
    "formalization": {
      "source_query": "Is x squared plus 2x plus 1 the same as (x+1) squared?",
      "translator": "MathVerifier",
      "verified": false
    }
  },
  "context": {
    "interpretation": {
      "theory": "real arithmetic",
      "logic": "symbolic simplification"
    },
    "proof": {
      "verifier": "MathVerifier",
      "verifier_version": "7.1.0",
      "configuration": {"domain": "real"},
      "theory_scope": "real arithmetic",
      "trusted_dependencies": ["sympy"],
      "outcome_treatment": "unknown/timeout/error resolve to UNVERIFIABLE or BLOCKED"
    },
    "evidence": {
      "evidence": {"simplified_difference": "0"},
      "proof_ref": "sha256:9f2c4a8e1b7d3f6a0c5e9b2d8f1a4c7e3b6d9f2a5c8e1b4d7f0a3c6e9b2d5f81"
    },
    "decision": {
      "admission": "ADMIT"
    }
  },
  "verdict": "VERIFIED"
}