chore: repo contract - distilled AGENTS.md, .agents/ layout, verify-temper skill

.agents/skills/deterministic-simulation/SKILL.md

@@ -0,0 +1,56 @@
+---
+name: deterministic-simulation
+description: Deterministic simulation testing (DST), TigerBeetle/FoundationDB style, and DST-driven development. Use when building or testing a stateful system (Temper and anything like it - databases, queues, engines, protocol code), when a task mentions simulation, seeds, fault injection, or invariants, or before writing tests for concurrent/distributed logic. Not for frontend apps.
+---
+
+# Deterministic simulation testing
+
+## What it is
+
+The whole system runs inside a simulator that owns every source of nondeterminism: time, randomness, scheduling, network, disk. One seed drives one execution. The same seed replays the exact same execution, byte for byte. The simulator injects faults (crashes, partitions, delayed and dropped messages, disk errors) while invariants are checked continuously. Different seeds explore different executions; a failing seed is a permanent, replayable reproduction of a bug.
+
+Reference implementations and what each proved:
+- **FoundationDB**: a deterministic simulator running the whole cluster in one process; `BUGGIFY` markers in production code cooperatively inject faults with some probability when simulating; "swizzle-clogging" (clog a random subset of nodes' networks one by one, unclog in random order) finds the deep interleavings. Their bar: if production hits a bug the simulator could have expressed, that is a simulator gap to fix.
+- **TigerBeetle (VOPR)**: an entire cluster of real code under network, storage, and process faults at ~1000x real-time (a virtual clock means simulated time runs as fast as the CPU allows); runs continuously across many cores and seeds; assumes the disk WILL fail - corruption and misdirected reads/writes are in the fault model, not just crashes.
+- **Antithesis**: DST as a service over unmodified systems.
+
+In this repo: the simulator lives in `temper-runtime` (sim module) with `temper-store-sim` as the simulated store; DST suites are `platform_e2e_dst` and `system_entity_dst` in `crates/temper-platform/tests/`.
+
+## What it is NOT - the mistakes agents make
+
+- **Not an integration test.** An integration test runs the system against real dependencies on real time and passes or fails once. A simulation runs thousands of seeded executions against simulated dependencies with faults injected.
+- **Not a mock-based unit test.** Mocks replace the system's parts to isolate one piece. In DST the PRODUCTION CODE runs - all of it, unmodified. Only the environment (clock, network, disk, scheduler, entropy) is simulated.
+- **Not a parallel reimplementation.** You do not write a second version of the logic and compare. The one real implementation runs in the simulator. A simplified MODEL may exist as an oracle to check results against, but the thing under test is always the production code.
+- **Not "tests that use a seed."** If any nondeterminism leaks (a real clock read, an unseeded RNG, thread timing, iteration order of an unordered map), replay breaks and the whole method is void. Determinism is the load-bearing property.
+
+## Requirements on the code under test
+
+- All time via an injected clock. Never read the wall clock directly.
+- All randomness from one seeded source the simulator provides.
+- Single logical thread of execution, or scheduling fully controlled by the simulator.
+- All I/O (network, disk, external services) behind interfaces the simulator can implement.
+- No dependency on unordered iteration, real timers, or ambient environment.
+
+If the code cannot meet these, that is an architecture finding to raise, not a reason to fall back to integration tests.
+
+## DST-driven development
+
+For systems like Temper this replaces test-driven development. The loop:
+
+1. **Define the harness first.** Before implementing, extend the simulator with the scenario: the workload, the faults, and the invariants - the things that must never happen (lost write, double apply, stuck state machine, divergent replicas). Run it. **The invariant must fail now** - a harness that cannot catch the missing behavior proves nothing.
+2. **Implement.** Production code, running inside the simulation.
+3. **Run seeds until the invariants hold.** Not one seed - many. A green run on one seed is one execution, not correctness.
+4. **A failing seed found later is committed as a regression case** and stays in the suite forever.
+5. Fix by root cause. Never fix by weakening the invariant or narrowing the workload.
+
+## Writing good simulations
+
+- Coverage lives in the workload and fault schedule, not the framework. It is easy to build a simulator that explores almost nothing. Vary operation mixes, timings, fault frequencies; check that interesting states are actually reached.
+- Invariants are properties, not examples: "no acknowledged write is ever lost", not "this call returns 3".
+- Keep seeds cheap. A virtual clock costs nothing to advance - simulated hours run in wall-clock seconds. Fast executions buy more seeds per CI run, and more seeds are more coverage.
+- Put cooperative fault points in production code (FoundationDB's BUGGIFY pattern): rare branches - a timeout firing early, a message reordered - taken with small probability only under simulation. The code helps the simulator find its own weaknesses.
+- Report failures as: seed, invariant violated, minimal event trace. The seed IS the bug report.
+
+## Limits - say them, do not hide them
+
+DST cannot catch: bugs in the simulator's model of the environment, behavior of real external systems, real-clock/performance issues, and nondeterminism the harness failed to capture. Code changes invalidate old seeds' meaning (the seed replays a different execution). DST complements live verification; it does not replace the Definition of Done's live run.

.agents/skills/verify-temper/SKILL.md

@@ -0,0 +1,43 @@
+---
+name: verify-temper
+description: Launch the Temper kernel locally and verify a change end to end - build, serve, drive the OData surface, run the verification cascade and DST proof. Use before calling any temper change done.
+---
+
+# Verify temper
+
+## Launch
+
+```bash
+cargo build -p temper-cli                                    # first build is long (~29 crates)
+cargo run -p temper-cli -- serve --port 3600                 # pick a free port; capture the PID
+```
+
+Ready when `GET http://localhost:3600/healthz` returns 200 (unauthenticated liveness; `/observe/health` is behind Observe auth and 401s) and `GET /tdata/$metadata` with `X-Tenant-Id: default` returns CSDL XML.
+
+For authenticated entity reads and dispatches, set `TEMPER_API_KEY=<any local value>` in the environment BEFORE serve - the platform bootstraps a tenant credential from it at startup, and a keyless boot serves 401 on every governed route (that 401 is itself the fail-closed proof).
+
+**ISOLATE**: run from your worktree so state lands in the worktree, not in a shared checkout. Never point at another session's data directory.
+
+## Doctor
+
+- Build fails on `edition 2024`: rustup update; rust-version is 1.85.
+- Port in use: pick another; read the real port from the serve log, not the flag you passed.
+- Serve exits immediately: read the log bottom-up; a spec that fails the L0-L3 cascade at bootstrap names itself.
+
+## Verify a change
+
+Pick the feature file matching what changed (see `features/`):
+
+- `features/serve-and-odata.md` - boot, health, CSDL metadata, entity reads
+- `features/spec-cascade.md` - L0-L3 verification of `.ioa.toml` changes
+- `features/dst-proof.md` - deterministic simulation, seeded reproduction
+
+Always finish with the suite for the crates you touched (`cargo test -p <crate>`), then `cargo test --workspace` before push (the pre-push hook runs it anyway).
+
+## Evidence
+
+Capture into `/tmp/verify-temper/<date>/`: the health response, the metadata head, cascade output, and the DST test result. Hand commands + outputs to the PR, do not assert.
+
+## Teardown
+
+Kill only the serve PID you captured at spawn. Never kill by pattern - other temper worktrees run servers on this machine.

.agents/skills/verify-temper/features/README.md

@@ -0,0 +1,25 @@
+# Feature map
+
+Surface enumeration.
+
+Served route trees (crates/temper-server/src): `/tdata` (OData), `/observe` (UI + health), `/api` (authorize, decisions, policies, audit, repl), `/_admin` (profiling), `/healthz`.
+CLI verbs (temper-cli): Serve, Mcp, Verify, VerifyIoa, VerifyRemote, Init, Codegen, Install, Decide, MigrateTursoToPostgres.
+Plus the DST suites (crates/temper-platform/tests).
+
+| Feature | File | Drive when you changed |
+|---|---|---|
+| Serve + OData | serve-and-odata.md | server, routes, stores, platform bootstrap |
+| Spec cascade | spec-cascade.md | any `.ioa.toml`, temper-spec, temper-verify |
+| DST proof | dst-proof.md | temper-runtime, temper-jit, temper-server sim paths |
+| MCP bridge + REPL | mcp-bridge.md | temper-mcp, temper-sandbox, SDK surface |
+| Observe UI + decisions | observe-ui.md | temper-observe, temper-authz, approval flow |
+
+## Not yet mapped
+
+- `/api` governance routes (authorize, policies, audit) - the Cedar policy/audit surface; decisions is partially covered by observe-ui.md, the rest needs its own file
+- `/_admin` profiling (cpu/wall) - ops-only; drive read-only
+
+- Init/Codegen - scaffolding verbs; drive = run them in a temp dir and build the output
+- Install - app install flow; needs a target app checkout
+- Decide (CLI) - covered indirectly by observe-ui.md's decision flow
+- MigrateTursoToPostgres - one-way ops migration; drive only against scratch data

.agents/skills/verify-temper/features/dst-proof.md

@@ -0,0 +1,16 @@
+# Deterministic simulation proof
+
+## Sub-features
+Seeded runs, fault injection, invariant checking, reproduction.
+
+## Driving it
+```bash
+cargo test -p temper-platform --test platform_e2e_dst           # E2E shared-registry proof
+cargo test -p temper-runtime                                    # sim runtime suite
+```
+
+## What proves it
+The DST suite passes, and a failure reproduces under the same seed (the failing output names the seed; rerunning with it must fail identically). For changed sim-visible code, the determinism guard (`scripts/check-determinism.sh`) reports no new violations.
+
+## Gotchas
+Code that passes tests can still break determinism (wall clock, HashMap order) - the guard and the DST reviewer ruleset in `.agents/agents/dst-reviewer.md` are the check, not the test suite alone.

.agents/skills/verify-temper/features/mcp-bridge.md

@@ -0,0 +1,13 @@
+# MCP bridge and REPL
+
+## Sub-features
+Stdio MCP server, sandboxed Python REPL, `temper.*` API (submit specs, create entities, invoke actions).
+
+## How to get to it (user POV)
+Agent clients (Claude Code, Codex) connect over stdio: `cargo run -p temper-cli -- mcp` proxies to a running serve instance.
+
+## Driving it
+Start serve first, then the bridge. Through the REPL: `await temper.specs("default")`, create an entity, invoke an action, read it back over OData.
+
+## Gotchas
+The bridge proxies - it does not serve. A dead serve behind it turns every call into a transport error that looks like an auth failure.

.agents/skills/verify-temper/features/observe-ui.md

@@ -0,0 +1,13 @@
+# Observe UI
+
+## Sub-features
+Web UI on the serve port: entity browser, pending Cedar decisions, approval flow (`temper decide` is the CLI equivalent).
+
+## How to get to it (user POV)
+Browser at `http://localhost:<port>/observe`. Auth-gated: unauthenticated requests 401 (that is fail-closed, not breakage).
+
+## Driving it
+Browser tooling against /observe after authenticating; or drive the decision flow headlessly: trigger a Cedar-denied action over OData, list pending decisions, approve, re-invoke.
+
+## Gotchas
+`/observe/health` is behind the same auth - use `/healthz` for liveness. A denial that never surfaces as a pending decision is a product finding, not a driver error.

.agents/skills/verify-temper/features/serve-and-odata.md

@@ -0,0 +1,18 @@
+# Serve and the OData surface
+
+## Sub-features
+Boot, health, CSDL metadata, entity-set reads, action dispatch.
+
+## Driving it
+```bash
+cargo run -p temper-cli -- serve --port 3600   # capture PID
+curl -sf http://localhost:3600/healthz
+curl -sf -H 'X-Tenant-Id: default' 'http://localhost:3600/tdata/$metadata' | head -c 400   # CSDL XML
+```
+Read an entity set named in the metadata; dispatch an action via `POST /tdata/<Set>('<id>')/Temper.<Action>` with `X-Tenant-Id`.
+
+## What proves it
+Health 200 with a live process; metadata is CSDL XML listing the bootstrapped entity types; an entity read returns `@odata.context`. A dispatch is proven by reading the entity back and seeing the state move - a 200 on dispatch alone is not a transition.
+
+## Gotchas
+The serve log at bootstrap lists every spec that loaded; a missing entity set means its spec failed the cascade - read the log, not the route.

.agents/skills/verify-temper/features/spec-cascade.md

@@ -0,0 +1,16 @@
+# Spec verification cascade (L0-L3)
+
+## Sub-features
+IOA parse, TransitionTable build, model checking, DST invariants.
+
+## Driving it
+```bash
+cargo run -p temper-cli -- verify --specs-dir <dir-with-specs>    # takes a directory, not a file
+scripts/verify-cascade.sh                                       # all spec dirs, results in .cascade-results/
+```
+
+## What proves it
+The cascade reports each level passed for the changed spec. An edit that adds a state or action must show the new element in the pass output. A deliberately broken guard must FAIL the cascade - if it passes, that is a finding in the verifier, not a success.
+
+## Gotchas
+The `.claude` hook runs this automatically on `.ioa.toml` edits and BLOCKS on failure; running it yourself first avoids losing the edit loop. `.cascade-results/` is local state, never committed.

.claude/agents

@@ -0,0 +1 @@
+../.agents/agents

.claude/commands

@@ -0,0 +1 @@
+../.agents/commands