Tarski — small enough to verify, expressive enough to run a business
A Datalog extension for declaring ontologies: relations, rules, invariants, and relays. Deliberately not Turing-complete — Tarski stays inside logic fragments where composition, decidability, and cost envelopes are mathematical consequences, not hopes.
The only path from a model's output to the world
LLM output lands in relay namespaces — candidate.* for extractions, proposal.* for actions. No rule may derive accepted truth or an executable intent directly from them: every path must cross an explicit decision.* gate, and the loader checks the whole graph at load time.
Promotion is an inspectable decision rule a developer wrote — here, a bounds check that accepts, and review routing for everything else. Your agent writes this file; tarski verify tells it whether the contract holds.
-- the voice parser is a fallible sensor: its parse arrives -- as candidate.order(item, qty) evidence — nothing more -- acceptance is an explicit decision, not a vibe decision.accepted.orders.line(item, qty) :- candidate.order(item, qty), menu.bounds(item, max), qty <= max. order.line(item, qty) :- decision.accepted.orders.line(item, qty). -- out of bounds → route for review, never submit decision.requires_review.orders.line(item, qty, "reviewer", "order_desk") :- candidate.order(item, qty), menu.bounds(item, max), qty > max. -- the wall: named, checked at every fixpoint invariant pos_only_accepted_lines { never pos.ticket(item, qty), not order.line(item, qty) }
What the fragment buys you
The simplicity developers feel is the surface of structural properties underneath. Because Tarski stays inside well-behaved fragments of logic, the platform can check things about your system that general-purpose code cannot offer.
Bounded blast radius
What any change can affect is bounded by the rule graph's neighborhoods. Recomputation, hydration, and review scope to what a change can actually reach.
Modules that merge safely
Namespace boundaries are computed from the ontology and checked by the platform. Independently developed modules compose — or the merge is rejected with a verdict, before deploy.
Performance before profiling
The shape of a rule determines its worst-case cost. Tarski reports which rules leave the tractable classes — and why — before anything runs. A regression is a semantic diagnosis first.
Indexes and plans are derived from the ontology and declared queries. Tuning can trade constants; it can never trade meaning — every plan must reproduce the exact model and provenance the reference evaluator derives.
Designed to be written by agents, read by humans
You will rarely write Tarski by hand. Coding agents author it against your Scenarios and invariants, iterating on tarski verify until the contract holds.
What matters is that when you do read it — an acceptance rule during an audit, an invariant during sign-off — each statement is small, declarative, and means exactly what it says.