Build backends you can prove, not just deploy
Everything here runs against a deterministic evaluator: the commands are real, the outputs are checkable, and every claim about behavior is one verify away from evidence.
Fast paths
Quickstart
Install the CLI, scaffold an app, and watch verify prove the contract holds.
What is Tarski?
the Agent Native platform for verifiable backends — and what those words mean precisely.
The Tarski language
Relations, rules, invariants, and relay namespaces — small enough to verify.
Client SDK
Append observations, run queries, and subscribe to live results from your app.
Start here
What is Tarski?
the Agent Native platform for verifiable backends — what those words mean, precisely, and how the pieces fit together.
Quickstart
Scaffold a Tarski app, watch verification prove the contract holds, and take the same app to the cloud — in about five minutes.
Installation
Install the tarski CLI, pin versions, keep it updated, and understand what runs locally versus in the cloud.
Project structure
A Tarski app is a directory of text files interpreted by one binary — the manifest, ontology, mappers, helpers, queries, and fixtures, and what each is responsible for.
Examples
The example catalog is a set of executable behavior contracts — each app teaches a specific containment or verification behavior, with fixtures proving the unsafe paths too.
Concepts
The observation-first pipeline
Observations are the only canonical evidence of what happened. Everything Tarski believes or does is computed from an observation history under one evaluator.
Facts, decisions & intents
How Tarski turns fallible evidence into trusted state and authorized action — candidates, proposals, the decision namespace, and the graph-cut safety boundary.
Worldviews & lineages
The identities that keep observation history, semantic meaning, package contents, and mapper output from blurring together — and why effects bind to exactly one of them.
Provenance
The explanation graph — why every candidate, decision, fact, intent, and effect exists, traced back to the observations that support it.
Determinism & replay
What Tarski's guarantees actually claim — byte-exact replay, dual-engine parity, query determinism, index neutrality, and hosted/local parity — and how each is proven.
Build
The Tarski language
A strict Datalog subset for declaring ontologies — relations, rules, decisions, invariants, and the reserved namespaces that make containment structural.
Mappers & observations
The deterministic boundary where raw events become typed evidence — Rhai mappers, pure helpers, and deterministic effect providers.
Entities
One declaration expands into the whole record kit — versioned latest-wins state, fail-closed conflicts, soft delete with revival, and generated read queries.
Scenarios & fixtures
Deterministic observation timelines plus exact expected worlds — the proof model behind tarski verify, blessing, query expectation sidecars, and proof artifacts.
Effects & reconciliation
How Tarski touches the world — declared capabilities, admission identity, retry policies, the effect lifecycle, work queues, and explicit reconciliation.
Declared queries
The named, typed, parameterized read surface over your derived worldview — authoring, exposure, validation, and the query engine underneath.
Reactive queries
Keep a declared query's result current without polling — durable subscriptions, exactly-once delta delivery, held streams, and explicit rehydrates.
Workviews, Collectors & modules
Workflow-shaped inspection and acquisition without a workflow engine — read models, dispatch policy, scenario-driven collection with completion seals, and composable modules.
Scheduling
Standing cron, interval, and one-shot schedules whose exactly-once fires enter the lineage as ordinary observations — never a second source of truth.
Storage
Content-addressed blob storage with backend invariance, quotas and GC — and semantic tiering that keeps observation history at object-storage cost.
Plugins & packages
Installable semantic packs for external systems — designated namespaces, load-checked surface tiers, typed HTTP receipts, and locked package management.
Agents
Authoring with agents
Tarski does not ship a coding agent — it ships the contract surface, diagnostics, and machine-checkable feedback that make any capable agent effective.
Runtime containment
LLMs as tools, never drivers — the relay namespaces, decision gates, invariant backstops, and shared-reality coordination that make containment structural.
The agent query relay
How an LLM agent reads the worldview — proposal, decision, admitted intent, governed effect, and results that re-enter as gated evidence.
Platform
CLI reference
The tarski binary's command surface — scaffold, dev, verify, query, studio, cloud, and the full inspection and maintenance families.
Client SDK
The @tarski/client TypeScript SDK — append observations, run queries, subscribe to live results, and drive typed sessions against local serve or Tarski Cloud.
Studio
The browser surface for inspecting everything Tarski derives and runs — observations, facts, intents, effects, provenance, queries, and cloud state.
Cloud
The managed platform — cloud-first development, deploys with receipts, hosted parity and health, provider bindings, and multi-tenant read models.
Identity & tenancy
How real users, agent sessions, and tenant organizations stay separated — verified identity at ingress, authorization as derived facts, and fail-closed boundaries everywhere.
Versions & releases
Release channels, immutable artifacts, version pinning, and what "preview" means for the platform today.