A language for application logic · pre-M0

Declare the laws.
The compiler proves them.

Tessera is declarative and deterministic. You write types, rules and laws. The compiler builds the implementation and proves every law, or hands you the exact state and call that breaks it.

Read the spec Star on GitHub

seed 0x7e55e1a · same seed, same mosaic, every browser

Errors are counterexamples.

Forget one ownership check and the build doesn't say "something's wrong". It shows you the failing state, the call that broke the law, and one suggested fix, in JSON for agents and plain text for people.

todo.tes

rule complete(by: Principal, id: Id<Task>) {
  let t = tasks[id] or fail NotFound
  // require t.owner == by.id or fail NotFound
  tasks[id].status = Done(clock.now)
    unless t.status is Done
}

law done_once: forall t in tasks.
  t.status is Done => t.status.at >= t.created
// law isolation: only an owner changes their tasks

prove complete(by, id) is idempotent
example complete(bob, alice_task) fails NotFound

tessera check --json

{ "code": "E-LAW-001",
  "law":  "todo.isolation",
  "rule": "todo.complete",
  "counterexample": {
    "state": { "tasks": [
      { "id": 1, "owner": "alice" } ] },
    "call":   "complete(by: bob, id: 1)",
    "effect": "tasks[1].status changed by bob"
  },
  "hint": "add `require t.owner == by.id
           or fail NotFound`" }

refuted

Three concepts. That's the language.

A small core means fewer wrong outputs from the models writing it, and less for the people reviewing it.

Type

Types are constraints, not just shapes. Refinements become compile errors, and the solver uses them.

Int[1..100] Text matching email Secret<Text>

Rule

An atomic state change: preconditions, then declared writes. All reads see the state before the rule. Failures are values.

require … or fail NotFound

Law

An invariant that must hold after every rule. Laws are what humans review: short, and where the errors are expensive.

forall t in tasks. …

Built for code you didn't write.

AI writes most new code now. Reading it all line by line doesn't scale, but verifying it does. People review the types, laws and examples, and the solver checks the rule bodies.

P1Deterministic everywhereSame state and inputs, same outputs, bit for bit, on every backend.

P3No ambient effectsTime, randomness, IO and secrets are declared needs. Every input is logged, and every run replays.

P4Review where it countsHumans review types, laws and examples. Machines write rule bodies.

P5Errors you can act onConcrete failing inputs with stable codes, in human form and JSON.

P7Hashes are identityOne canonical form per definition. Renaming or reformatting doesn't change the hash.

P8One oracleThe interpreter defines the semantics. Every backend is differential-tested against it.

One IR. One oracle. No JIT.

Every stage reads the same typed, hashed Core IR. A solver result of Unknown fails the build. Packages are git URLs plus tags, pinned by commit and IR hash, with no central registry.

source ─▶ AST ─▶ Core IR (typed, hashed) ─┬─▶ Interpreter   semantic oracle · dev loop
                                          ├─▶ Verifier      Z3 / cvc5 · proven · refuted · unknown = fail
                                          └─▶ Dataflow IR ─▶ Low IR ─▶ C · Wasm · LLVM IR

Roadmap

Nothing has been compiled or benchmarked yet. Each milestone has a gate, and claims about speed are hypotheses to test in M4 and M6.

Milestone	Delivers	Gate
M0 Spec & corpus	20 example programs, semantics cases, open questions settled	Human sign-off on laws and examples
M1 Interpreter	Parser, formatter, type checker, interpreter. Todo runs in the REPL	All examples pass
M2 Verifier	SMT encoding, counterexamples, fast and full modes	Zero false proofs on a seeded-bug suite
M3 Store, CLI, HTTP	Todo app with auth on SQLite	End-to-end tests, store parity
M4 AOT via C	Lowering and C emission	Parity on every example, first benchmark
M5 Wasm & web	Wasm backend, web surface	Browser build passes the same examples
M6 Optimizer & packages	Fusion, e-graphs, index selection, git-native packages	Parity kept, benchmarks improve, hashes stable

Help with M0: example programs, semantics cases, and settling open questions.

Declare the laws.The compiler proves them.