What is Tarski?

Tarski is a backend development platform for software built by AI coding agents and for systems that contain runtime AI agents. Humans state intent as Scenarios and invariants; agents implement ontology rules and deterministic mappers; Tarski verifies the resulting behavior over an immutable observation log and admits only transitions that satisfy the declared model. Every accepted fact, intent, and effect remains explainable through provenance.

The name is mathematically literal. Alfred Tarski established the semantic notion of truth in a model, and the Knaster–Tarski fixed-point theorem underlies the fixed-point semantics Tarski’s evaluator uses. This is not branding metaphor: Tarski is the platform where models make claims true, fixed points make evaluation deterministic, and evidence makes those claims auditable.

Agent Native, read both ways

“the Agent Native platform for verifiable backends” deliberately reads two ways, and both readings are product surface:

1. Backends developed by AI agents. Coding agents author .ta rules and mappers against a machine-checkable contract — golden fixtures, named invariants, load-time gates. Humans declare boundaries and review evidence, never generated code line by line.
2. Backends that contain, support, and are consumed by AI agents. At runtime, LLMs stay fallible tools behind the candidate.* and proposal.* relay namespaces. Intents are proved satisfiable before touching the world, and independent agents coordinate through the shared derived model.

The readings close into one loop. When a contained runtime agent misbehaves, provenance pins the exact observations that caused it, the counterexample is promoted into a deterministic fixture, an authoring agent iterates until it passes, and verification proves the fix. Production feeds development through a single artifact chain.

One rule underneath everything

Everything Tarski believes or does is computed from an observation history under one evaluator:

observations → typed atom inbox → deterministic evaluator → intent outbox → effects → new observations

State is never mutated; it is derived. The observation log is append-only and canonical. A deterministic mapper turns each observation into typed atoms, the evaluator computes a fixed point over those atoms and your ontology rules, and only committed intent.* rows may be admitted to effects. Effects produce receipts that re-enter the log as new observations.

Because the whole pipeline is deterministic, replay is exact, verification runs the real evaluator, and every derived fact carries provenance edges back to the observations that support it.

The human-checkable contract layer

As agents produce applications directly from intent, the artifacts a human reviews must be small, precise, and executable:

• Scenarios — a timeline of observations and the exact world that must result. They read like product requirements and are executed directly by the production evaluator, so there is no step-definition glue layer where classic BDD drifts.
• Invariants — named, fail-closed statements about states the system must never reach, checked over the fully materialized model at every fixpoint.
• Provenance — the explanation graph. Every fact, decision, intent, and effect traces back to evidence, which makes debugging a walk along edges instead of a read through generated code.

tarski verify runs the whole corpus against the deterministic evaluator and checks every invariant. Green means the declared contract holds — a precise statement about declared behavior, not a vague promise.

What Tarski is not

• Not a mutable-state database. Tarski does not emulate Postgres or Firestore. State is derived from the log, not written in place.
• Not an agent framework. Tarski does not ship a coding agent or an orchestration loop. Your agent — Claude Code, Codex, Devin, or any capable tool — authors against Tarski’s contract surface.
• Not an identity provider. Your app’s IdP keeps login UI, passwords, and MFA. Tarski verifies credentials at ingress and derives authorization from facts. See Identity & tenancy.

The platform surface

Where to go next

Start with the Quickstart to get a verified app running in minutes, then read the observation-first pipeline to build the mental model everything else assumes.