Determinism & replay

Tarski’s determinism claims are precise, and each one is enforced by an executable gate — not a design intention. This page states exactly what holds.

Byte-exact replay

Facts are never written directly; they are derived by evaluating an append-only observation log with a digest-identified evaluator. A clean-database replay of recorded observations reproduces the same derived model — the same facts, intents, provenance edges, and checkpoint digests. Resume-from-checkpoint equals clean replay, and multi-hop agent deliberations replay with identical digests from a clean store.

Two engines, one output

Evaluation runs on the incremental (semi-naive) engine by default: work scales with the size of each change, not the length of history. The naive full-recomputation engine remains the correctness authority, the verification engine, and the rollback target.

The contract between them is bit-identical canonical output — facts, intents, assertions, retractions, contradictions, invariant verdicts, provenance edges with exact justification sets, and checkpoint digests. Not “equivalent”: identical.

tarski verify --cross-engines

replays every selected fixture through both engines and fails on any divergence. The same parity harness runs continuously in CI over every fixture-bearing example and is release-blocking. Delta-proportionality (the incremental engine doing dramatically less work on warm updates) is itself enforced by a CI regression floor.

If you ever need it, TARSKI_EVALUATOR_ENGINE=naive selects the naive engine per process — no data migration, because incremental carry state is in-memory only. An incremental-path error automatically retries naively once and records the reason.

Query determinism

A query result is a pure function of the canonical query IR, its bindings, the snapshot identity (lineage_id, evaluator_digest, committed_head), and the caller’s projection. Re-execution reproduces the same result_digest byte for byte; explain artifacts are digest-stable; and CLI, API, and MCP doors produce byte-identical results for the same query at the same head. Even denials are byte-equal on empty versus seeded stores — a denial can never leak whether hidden data exists.

Index neutrality

Indexes accelerate; they never mean anything. Index presence, absence, or rebuild never changes query results, derived facts, or any canonical digest — tested by enabled-versus-dropped digest comparison, a three-state corpus parity gate, and crash-recovery kill tests. Covering index families are derived automatically from your app’s declared workload, and tarski index drop is always safe. See the CLI reference.

Hosted/local parity

One semantic runtime contract spans local evaluation, the shadow reference evaluator, managed Cloud’s evaluation guest, BYOC, and entitled full-local hosts: for one frozen evaluation package and observation history, all accepted hosts derive the same canonical tuples with provenance. Packages that cannot load are refused at admission — at deploy time, not on the first production event.

Hosted query parity is certified, not assumed: parity receipts compare canonical rows, ordering, digests, support witnesses, typed denials, and redaction state across authorities before capability discovery reports query operations as available. A hosted lineage’s health honestly separates “observation accepted” from “projection committed” (committed / pending / trapped), and a trapped lineage never loses data — the log is immutable, and a corrected evaluator replays it.

Provider record/replay

External provider envelopes (HTTP, LLM) are captured with redaction and replay identity, so LLM-assisted behavior verifies deterministically without live provider state. Model context is assembled from digest-stamped sections whose digests join the provider request digest — a capture envelope proves byte-for-byte what a model saw.

The authority hierarchy

• Engine level — the naive evaluator is the correctness authority; the incremental engine must match it bit-identically.
• Activation level — exactly one committed activation per lineage may execute effects; shadow and compare evaluators derive but never act.
• Runtime level — managed Cloud (or your accepted BYOC/enterprise/local authority) is the semantic authority for current evidence; after an app is hosted, local replay is diagnostic parity evidence, not production effect authority.