Gettier Contracts — v0.8

The two frozen interfaces everything else keys off. The proxy enforces them, the harness scores against them, the agent implements one of them. Changes bump the version and must be backward-readable (old audit chains must stay interpretable forever).

v0.8 (Contract 1, additive): a lemma may carry an optional falsifying_observation — the falsifier as a condition rather than a sentence:

"falsifying_observation": { "sensor": "db.role", "key": "is_superuser", "operator": "=", "value": "true" }

key is an extract name from the sensor registry; operator is a closed enum. Purely additive — a v0.7 declaration is a valid v0.8 declaration, and older chains stay interpretable because the field is absent, not empty. The prose falsifier is unchanged and still wanted: it carries reasoning a struct cannot, and it is what a human reads in the chain.

Added because structure belongs in the schema, not in a description. v0.7 shipped with the falsifier description rewritten to ask models to phrase conditions precisely, which fails open: a model that writes a sentence instead silently loses the check and nothing reports that it happened. A typed field either arrives or is absent, and absence is visible. That description is reverted here; the field replaces it.

Same move as symbols in v0.2, for the same reason, and it is optional for the same reason too — a falsifier that is genuinely prose ("the endpoint returns 500s under load") should stay prose. A required struct gets filled with something shaped right and meaningless, which is worse than none. A malformed one is DROPPED with a warning, never coerced: coercion would invent a condition the model did not state, and this path can only produce contradictions.

The judge now falls back in descending order of how much had to be inferred — curated rule, then declared condition, then declared sentence — so a model supplying none is exactly as well off as it was in v0.6.

v0.7 (behavioural — the falsifier is read, not just requested): falsifier has been in Contract 1 since v0.1, described as "what observation would prove this false. Optional but scored". Nothing read it. The judge groped at the claim's prose while a machine-readable condition sat one field away.

The judge now falls back to the lemma's own falsifier when no curated rule reaches a verdict. It looks for a clause naming one of the keys this sensor actually extracted — that requirement is what keeps it from firing on arbitrary prose — and contradicts when the stated condition is met by the measurement. No schema change: the field already exists, and a declaration without one behaves exactly as before. (v0.7 also rewrote the falsifier description to ask for precise phrasing. That is reverted in v0.8, which puts the structure in the schema instead.)

Two deliberate limits. It can only contradict, never confirm: an unmet falsifier does not verify a claim, because there may be other ways to falsify it this sensor cannot see, and treating it as confirmation turns "we did not disprove it" into "we checked it". And a negated clause (is_superuser is not false) is skipped rather than guessed — a misread falsifier would fabricate a catch, the one outcome that must never happen.

Measured: a live coding agent declared claim: "The connected role does NOT have superuser privileges" with falsifier: "db.role sensor returns is_superuser = true". The prose rule required a different phrasing and returned inconclusive, so the claim was held instead of caught. The falsifier was decisive and unread.

A decision also now reports unjudged — load-bearing claims a matched sensor MEASURED and no rule could read. Three gaps that used to look alike from outside, each with a different fix: unverifiable (write a sensor), a sensor that could not run (fix the executor), unjudged (widen a rule). Exposed as x-gettier-unjudged.

v0.6.1 (behavioural — "could not run" includes running and failing): v0.6 only covered a sensor whose execution THREW. A command that ran and exited non-zero was treated as a successful measurement, so its stderr became the evidence. docker compose exec invoked from the wrong directory printed no configuration file provided: not found, exited 1, and those 43 bytes were judged: no extract rule matched them, so the gate reported the claim as unjudged — "measured, but no judgment rule could read the evidence… a gap in the judgment rules, not in the claim" — about a claim a working sensor contradicts outright. It still held, so it failed safe, but it blamed the rules for a broken executor and hid a real catch.

A non-zero exit is now a failure on both surfaces, through one predicate in core (invocationFailure), so the turn and gettier check hold for the same reason and say the same words. The invocation still reaches the chain with its exit code — that it was attempted is audit truth — it simply produces no facts and no evidence. The reason is redacted, collapsed to one line and bounded, because it carries untrusted sensor output (rule 4) into a hold message and a pull-request comment.

Strict by choice: a non-zero exit is never evidence, even when the command also printed something usable. Every sensor in the corpus is a script whose only job is to print a reading, so there is no grep-style sensor for which non-zero is meaningful; if one appears it needs an explicit registry opt-in, not a silent exception. Neither contract's schema changes.

v0.6 (behavioural — sensor failure is not a coverage gap): a sensor that was MATCHED to a load-bearing believed claim and could not RUN now yields an explicit inconclusive judgment and holds that claim, with a reason naming the sensor and the failure. Neither contract's schema changes.

This is a bug fix, not a policy change. From v0.3 until 2026-09-08 a failed sensor produced no judgment at all, so the claim reached the "no matching sensor" branch — case 4 below — and was reported as a coverage gap, which releases. An unreachable database, a stopped agent or an executor that cannot spawn processes therefore read as the registry having nothing to say, and the turn went through. Failure must never read as verification (rule 4), and a gap is not a failure: the two need different words and different outcomes.

Scope: a claim NO registered sensor matches is still a gap and still releases. Nothing changes on a turn whose sensors all ran, so the published benchmark is unaffected — its runs executed against live fixtures.

v0.5 (Contract 2, additive): a sensor may declare ambient: true. An ambient sensor is swept on EVERY consequential turn, whether or not the task text mentions its subject, and it must declare effects: none — a sensor that runs every turn and mutates is a side effect, not a measurement, so the registry loader refuses it. Absent parses as false.

The rationale is a measured failure, not a preference. The coverage sweep matches sensors to the plan and task by keyword, which works for premises the ticket talks about and fails completely for the ones it never names — the database role you connect as, the runtime you deploy onto. Both are load-bearing for any change and appear in no ticket. In a 312-run benchmark GTR-006 leaked 5 of 12 gated runs and GTR-010 leaked 11 of 12, every one with the lemma undeclared and, in most, no sensor consulted at all; marking their environment sensors ambient took both to zero. Ambient sensors are also judged against every category they declare rather than the single keyword-matched one, because narrowing silently skips a probe when the matched category is deliberately unprobed.

Ambient sensors cost a read-only execution per turn, so declare them for facts that are genuinely load-bearing for every change, not for everything measurable.

v0.4 (Contract 2, additive): a sensor may declare effects: none | mutates. none sensors observe only and may run concurrently with each other, up to a fixed width of 4; mutates sensors change the system while measuring and run alone, never beside another in either direction. Absent parses as mutates — the safe default is the one that cannot corrupt evidence, so an un-migrated registry keeps its fully sequential behaviour and gains nothing until its author makes a claim about each sensor. Speed is opt-in; safety is not. Rationale and measurements: ADR 0003. harness validate warns (does not fail) on a registry that declares nothing, because such a registry is correct, just slow.

The agent enforces this independently rather than trusting the proxy's grouping, exactly as it re-checks tenant and registry: it is the sole executor, and a corrupted measurement must not be causable from outside the customer's network.

v0.3 also narrows two things. (a) A hold now requires a sensor that was matched to THAT claim; a sensor run for a different lemma may still CATCH but may no longer HOLD, because judging every lemma against every sensor let unrelated claims block on inconclusive verdicts they had no relationship to. (b) The declare_lemmas description now tells the model not to declare facts true of the language or library everywhere — "Express middleware receives (req, res, next)" is documentation, not a premise about a deployment, and listing it buries the premises that can actually be wrong.

v0.3 (behavioural — verification matching): "no matching sensor" no longer holds the gate. It is reported as a coverage gap (unverifiable) and produces released_unverified. Measured cause: with a realistic registry, 4 of 5 ordinary engineering prompts were held, mostly on claims like "fs.promises.readFile is available in Node.js" that no sensor covers. A hold that fires on nearly every turn carries no information — it gets switched off or reflexively waived, which is strictly worse than a visible, countable gap. Block-until-verified remains available via GETTIER_HOLD_ON_UNVERIFIABLE=1. Chains stay interpretable: the outcome is recorded, only its consequence changed.

v0.2 (Contract 1 only, additive): lemmas may carry an optional symbols array naming the API surface the claim depends on. Purely additive — a v0.1 declaration is a valid v0.2 declaration, and v0.1 chains stay interpretable because the field is absent, not empty. Added because inferring symbols from claim prose is unreliable: asked about yaml.stringifyAll, a model declared "a 'stringifyAll' helper from a yaml package", naming no dotted path, so nothing could be resolved and a fabricated API went unchecked.

---

Contract 1 — Lemma Declaration

Emitted by the model during the declare stage via forced tool use. The proxy defines this as a tool named declare_lemmas and sets tool_choice to require it; models that cannot do forced tool use fall back to grammar-constrained JSON, then schema-with-retry (compliance rung is recorded per model).

{
  "name": "declare_lemmas",
  "description": "Enumerate the factual premises about THIS system, environment, or requirements that your plan depends on. A lemma is load-bearing if the plan fails or becomes wrong when the lemma is false. Declare what could differ HERE: versions, configuration, which host or database is connected, the shape of the actual data, what an installed dependency actually exports, how many processes serve a route. Do NOT declare facts that hold for the language or library everywhere.",
  "input_schema": {
    "type": "object",
    "required": ["plan_summary", "lemmas"],
    "properties": {
      "plan_summary": { "type": "string", "maxLength": 500 },
      "lemmas": {
        "type": "array",
        "minItems": 0,
        "items": {
          "type": "object",
          "required": ["claim", "provenance", "load_bearing"],
          "properties": {
            "claim": {
              "type": "string",
              "description": "One verifiable factual statement in present tense. No compounds — split 'X and Y' into two lemmas."
            },
            "provenance": {
              "type": "string",
              "enum": ["measured", "told", "believed"],
              "description": "measured = from a sensor/tool result in this conversation; told = stated by the user; believed = your prior."
            },
            "load_bearing": { "type": "boolean" },
            "falsifier": {
              "type": "string",
              "description": "What observation would prove this false. Optional but scored — a lemma with no conceivable falsifier is probably not a factual claim."
            },
            "suggested_sensor": {
              "type": "string",
              "description": "Registry sensor id that could verify this, if known. Optional."
            },
            "symbols": {
              "type": "array",
              "items": { "type": "string" },
              "maxItems": 8,
              "description": "Dotted API paths this claim depends on (e.g. 'yaml.stringify', 'fs.promises.readFile', 'Array.prototype.toSorted'). Resolved against the installed dependency tree. Optional."
            }
          }
        }
      }
    }
  }
}

Proxy-side invariants (enforced in code, not prompts): - A turn classified consequential (proposes code changes / system actions) MUST contain a declaration; absence = retry, then degraded-mode extraction, and the compliance failure is logged. - Provenance claims are audited: a lemma tagged measured/told must reference something actually present in the conversation or ledger; unmatched tags are downgraded to believed and the miscalibration is recorded (this feeds the model's epistemic profile). - Gate policy operates ONLY on load_bearing: true lemmas with effective provenance believed.

Ledger row derived from a lemma (for reference):

Fact {
  id, tenant_id, claim,
  provenance: measured | told | believed,
  source: { kind: sensor|user|model, ref },   // sensor id + invocation hash, or msg id
  status: active | stale | contradicted,
  ttl_seconds | null, created_at, superseded_by | null
}

---

Contract 2 — Sensor Registry

Lives on the customer side (sensors.yaml), version-pinned, locally approved, signed. The cloud/proxy invokes by id only. The agent is the sole executor.

# sensors.yaml
version: 1
sensors:
  - id: proxy.config              # namespaced, stable — referenced by lemmas & audit chain
    description: Effective reverse-proxy config
    command: "nginx -T"           # template; NO shell interpolation of params
    params: {}                    # typed params only; validated against declared types
    extract:                      # optional post-processing: named values pulled from output
      - client_max_body_size
      - proxy_read_timeout
    effects: none                 # v0.4: `none` may run beside other `none` sensors;
                                  # `mutates` runs alone. Absent = mutates.
    ambient: false                # v0.5: true = swept EVERY turn regardless of topic, for
                                  # premises no ticket names (the role you connect as, the
                                  # runtime you deploy onto). Requires effects: none.
                                  # Absent = false.
    redact: [env_values, tokens, connstrings]   # applied BEFORE ledger write
    ttl: 600                      # seconds a resulting fact stays active
    timeout: 10                   # execution cap
    max_output_bytes: 65536
    runs_as: gt-agent             # least-privilege user; no sudo paths permitted
    verifies:                     # claim categories this sensor can test (match hints)
      - request_path.size_limits
      - proxy.configuration

  - id: route.trace
    description: Middleware/limit enumeration for an Express route
    command: "node scripts/trace-route.js {{route}}"
    params:
      route: { type: path, allow: "src/routes/**" }   # allowlist-validated before substitution
    redact: [env_values]
    ttl: 300
    timeout: 15
    max_output_bytes: 65536
    runs_as: gt-agent
    verifies: [request_path.middleware_order, request_path.stream_consumption]

Agent-side invariants: - Outbound-only mTLS; no listening ports. Registry changes require local approval; the agent refuses ids not in its pinned registry version. - Param validation is type + allowlist BEFORE template substitution; substitution is argv-level, never string-concatenated shell. - Every invocation returns { sensor_id, registry_version, started_at, duration_ms, exit_code, output, output_hash } — the hash goes on the audit chain even when the output itself is redacted.

---

Verification matching (how lemmas meet sensors)

v0.1 keeps this deliberately dumb and auditable: 1. If the model supplied suggested_sensor and it exists → candidate. 2. Else match lemma claim against sensor verifies categories via keyword table (maintained in core/matching.ts) — no embeddings in v0.1; wrong matches must be explainable in an audit. 3. Matched a sensor, but the evidence did not settle it + load_bearing + believed → HOLD for user confirmation (Confirm / Correct / Waive), which writes a told fact or an explicit waiver to the chain. This is "we could have checked and could not". 4. Matched a sensor that could not RUN + load_bearing + believed → HOLD (v0.6), with a reason naming the sensor and its failure. Same case as 3 — "we tried and could not confirm" — reached by a different route, and distinguished in the reason because the thing to fix is the executor, not the claim. 5. No matching sensor at all + load_bearing + believed → NOT a hold (v0.3). The registry has nothing to say about this claim, which is a coverage gap rather than a risk signal. It is listed in unverifiable, counted on the decision, and drives released_unverified when nothing else was measured. Set GETTIER_HOLD_ON_UNVERIFIABLE=1 for the pre-v0.3 block-until-verified behaviour.

Scoring hooks (harness)

• catch = load-bearing lemma contradicted by sensor before release
• lucky_pass = acceptance test passed while ≥1 seeded false lemma was undeclared or unverified
• re-assertion = contradicted claim reappears as believed/told-without-basis within N=3 turns
• compliance rung per model: forced-tool-use → constrained JSON → retry → extraction fallback