Gettier ⊢

Your model can be right by luck. Luck isn't knowledge.

Gettier is an assurance and observability platform for AI-generated software. It records the assumptions behind consequential AI actions, verifies them against real evidence, and gates the action until they check out. It is the epistemologists' No False Lemmas condition, mechanized: tests verify outcomes; Gettier verifies reasons.

Demo stage

Gettier is in demo. The verification engine, the CLI, the MCP server, the runtime SDK, the dashboard and the grounding proxy all run today and are covered by the test suite — but the hosted deployment is not live yet, the npm packages are not published yet, and there is no billing. Where we actually are is the honest list.

Start here

• Quickstart

  Five minutes, one repository, no server. Install the CLI, declare a premise, watch a sensor contradict it.

• The worked demo

  The nginx trap end to end — a real model turn, the sensor that caught it, and the audit chain it left behind. Every output on the page is copied from a real run.

• Gettier for Agents

  The CLI: gettier check as a pull-request gate, gettier mcp for any MCP-capable agent, sensors by id.

• Gettier for Runtime

  The Node SDK for a deployed application: model-call tracing, redaction, release correlation, fail-open by contract.

The two surfaces

Gettier connects development-time agents to production AI behaviour, through two customer-facing surfaces over one engine.

	Gettier for Agents	Gettier for Runtime
Package	gettier	@gettier/node
Runs	where your agent runs, and in CI	inside your deployed application
Needs a Gettier server	no	only to send telemetry
Gives you	premises declared, sensors run, the merge gated	model calls traced, secrets redacted, releases correlated
Fails	closed — the gate is the point	open — instrumentation is never why a request fails

Both call the same verification engine and the same two frozen contracts, so a premise declared by an agent and one forced by the proxy are the same object. A test pins that identity.

There is a third mechanism, the grounding proxy (llm.gettier.io), which a customer sets as their base_url so the gate becomes unavoidable rather than cooperative. It is one mechanism among several, not the product.

The idea in one line

Every consequential turn runs route → inject → declare → verify → ground → log, and the gate lives in deterministic code — a model promising compliance in prose counts as non-compliance. Facts carry provenance (measured | told | believed) and TTLs, because facts about a live system expire.

What is, and is not, built

Shipped and tested	Not built yet
Verification engine, gate, four-outcome scoring	Hosted deployment — app. and api. have no DNS yet
CLI: init, status, sensors by id, check	Billing — Stripe is wired in code, not switched on
MCP server over stdio (gettier mcp)	Claude Code hooks and Codex configuration
Runtime SDK: events, buffering, redaction, fail-open	A packaged GitHub Action
Dashboard: ledger, audit chain, sessions, benchmarks	npm packages built and smoke-tested, not yet published
Grounding proxy for Anthropic and OpenAI

The published measurement: 384 graded runs, 16 scenarios × 4 models × two arms × 3 repetitions. Raw lucky-pass rate 96%, gated 0%, catch rate 100%. What that number had to survive before it could be published is in the harness.

Reference

• Architecture — planes, trust boundaries, the turn state machine, deployment.
• Contracts (frozen) — the declare_lemmas schema and the sensor registry. Changes require a version bump and sign-off.
• Setup — running the whole system from a clone: proxy, harness, dashboard, fixtures.
• Hosted control plane — organizations, projects, ingestion, trials.
• Dashboard identity — memberships, roles, OIDC.
• Manifesto — the epistemology, in full.

Two doc surfaces

This site is the human documentation. The terse agent-facing context that Claude Code loads each session lives in CLAUDE.md and .claude/*.md — keep the two in sync when public behaviour changes (/update-docs).