formalizr

Property-based fuzzing for stateful specifications.

formalizr lets you write a small, executable model of a system — its state, its requests, its responses, and the pure handlers that connect them — and then uses that model as a test oracle. It fuzzes the model against invariants, compares it byte-for-byte against your real implementation, stress-tests concurrency for linearizability, drives load tests, and audits production hardening. One specification, six kinds of tests.

The model is the spec. If the implementation and the model ever disagree, formalizr hands you a deterministic seed and the exact diff.

Why model-based testing

Hand-written tests encode the cases you thought of. A model encodes the rules, and the fuzzer explores the cases you didn't.

You describe the system once as a state machine:

• State — a Zod schema plus an initialState() factory.
• Requests / Responses — discriminated unions keyed by a kind field, wrapped in a uniform protocol envelope.
• Handlers — pure functions (state, request) → response that mutate the model state. This is your reference implementation, kept deliberately simple.

From that single description formalizr can:

| Command | What it proves | | ----------- | --------------------------------------------------------------------------- | | fuzz | The model upholds your invariants; the implementation matches the model. | | seed | Reproduce and inspect a single trace's end state. | | replay | Re-run every seed that has ever failed until they're fixed. | | linearize | Concurrent operations against the implementation are linearizable. | | perf | The implementation holds latency/error thresholds under k6 load. | | audit | Production endpoints are locked down: auth gates, JWKS, JWT attack surface. |

Installation

bun add @tomperez98/formalizr

formalizr runs on Bun and uses Zod v4 for schemas.

Optional, per command:

• linearize builds a small Go checker (lincheckr) on install. It needs a Go toolchain available; the binary is compiled via the postinstall script.
• perf shells out to k6, which must be on your PATH.

Core concepts

The protocol envelope

Every request and response shares a uniform shape, built with reqSchema and resSchema:

import { reqSchema, resSchema } from "@tomperez98/formalizr";
import { z } from "zod/v4";

// Request: kind + head (corrId, version, optional auth, optional debugTime) + data
const IncrReq = reqSchema("incr", z.object({}));

// Response: kind + head (corrId, status, version, branch) + data
const IncrOk = resSchema("incr", 200, "ok", z.object({ count: z.number() }));

• kind is the discriminant that routes a request to its handler.
• head.corrId is a correlation UUID that responses must echo.
• head.status / head.branch describe the outcome. Every distinct kind:status:branch triple is a coverage target the fuzzer tracks.
• head.debugTime is a test-only logical clock (see setOnTick), rejected in production.

The MBT model

You assemble a model by constructing an MBT and chaining configuration:

import { MBT, noAuth } from "@tomperez98/formalizr";
import { z } from "zod/v4";

const CounterState = z.object({ count: z.number() });

const CounterReq = z.union([
  reqSchema("incr", z.object({})),
  reqSchema("decr", z.object({})),
]);

const CounterRes = z.union([
  resSchema("incr", 200, "ok", z.object({ count: z.number() })),
  resSchema("decr", 200, "ok", z.object({ count: z.number() })),
  resSchema("decr", 400, "below_zero", z.object({ error: z.string() })),
]);

const counter = new MBT({
  state: CounterState,
  initialState: () => ({ count: 0 }),
  requests: CounterReq,
  responses: CounterRes,
  handlers: {
    incr: (state, req) => {
      state.count++;
      return {
        kind: "incr",
        head: { corrId: req.head.corrId, status: 200, version: "1.0.0", branch: "ok" },
        data: { count: state.count },
      };
    },
    decr: (state, req) => {
      if (state.count <= 0) {
        return {
          kind: "decr",
          head: { corrId: req.head.corrId, status: 400, version: "1.0.0", branch: "below_zero" },
          data: { error: "cannot decrement below zero" },
        };
      }
      state.count--;
      return {
        kind: "decr",
        head: { corrId: req.head.corrId, status: 200, version: "1.0.0", branch: "ok" },
        data: { count: state.count },
      };
    },
  },
})
  .addGenerator({
    incr: (rng, state, step, coverage) => noAuth({}),
    decr: (rng, state, step, coverage) => noAuth({}),
  })
  .addInvariant("count is never negative", (prev, current) => {
    if (current.count < 0) throw new Error(`count went negative: ${current.count}`);
  });

The type system enforces coherence at compile time: response kinds must cover all request kinds, every request kind needs a handler and a generator, and the initialState() factory must match the state schema. Several tests in src/__tests__/todo.test.ts exist purely to assert those @ts-expect-error guarantees.

Generators

A generator produces the data (and optional auth) for one request kind. It receives the RNG, the current model state, the step index, and the coverage seen so far — so it can bias toward untested branches or generate state-aware requests (e.g. picking an id that already exists).

.addGenerator({
  "todo.create": (rng) => noAuth({ ownerId: `u${Math.floor(rng() * 3)}`, title: "x" }),
  "todo.get":    (rng, state) => {
    const existing = state.todos[Math.floor(rng() * state.todos.length)];
    return noAuth({ ownerId: existing?.ownerId ?? "u0", id: existing?.id ?? crypto.randomUUID() });
  },
})

Use withAuth(token, data) when a kind needs an authenticated request.

Invariants

Invariants are predicates over (prev, current, step) that must hold after every step. They run against both the model and the implementation, so a violated invariant tells you whether the bug is in your spec or your code.

.addInvariant("todos stay unique per owner", (_prev, state) => {
  const seen = new Set();
  for (const t of state.todos) {
    const key = `${t.ownerId}:${t.id}`;
    if (seen.has(key)) throw new Error(`duplicate ${key}`);
    seen.add(key);
  }
});

The Target adapter

A Target is the bridge between the model and a real running implementation. It translates each protocol message into a call against your system and returns the system's response in the same envelope:

import type { Target } from "@tomperez98/formalizr";

const httpTarget: Target<State, Req, Res> = {
  name: "http",
  dispatch: async (req) => {
    const res = await fetch(`http://localhost:3000/rpc`, {
      method: "POST",
      headers: { "content-type": "application/json" },
      body: JSON.stringify(req),
    });
    return res.json();
  },
  // debug hooks — used only in development mode:
  start: async (req) => post(req),  // spin up / connect
  reset: async (req) => post(req),  // wipe to initialState
  stop:  async (req) => post(req),  // tear down
  snap:  async (req) => post(req),  // return full state for comparison
  tick:  async (req) => post(req),  // advance the logical clock
  jwks:  async (req) => post(req),  // serve .well-known/jwks.json (audit)
};

counter.addTarget(httpTarget);

The magic is in snap: after every step formalizr snapshots both the model state and the implementation state and asserts they are deep-equal. Combined with the response comparison, this catches divergence the instant it happens — not three requests later when it surfaces as a symptom.

snap, start, reset, stop, and tick are debug endpoints. In production they must be locked down (return 404), which is exactly what the audit command verifies.

Optional configuration

• .setIdempotent() — replays every request twice and asserts the state is unchanged the second time, for both model and implementation.
• .setOnTick(fn) — model a logical clock; fuzz/seed randomly advance it.
• .setPartitionKey(fn) — group operations by key so linearize checks each partition independently.
• .setPublic("kind", ...) — mark request kinds that don't require auth (the rest are treated as private by audit).
• .setPerf({ httpRequest }) — map a request to a raw HTTP call for perf.
• onSnap — normalize state before comparison (e.g. sort arrays whose order is not part of the contract).

Running tests

There are two ways to drive a model.

1. As a CLI

Call await mbt.cli() at the end of a spec file and run it directly:

// counter.spec.ts
// ...build `counter` as above, add a target...
await counter.cli();

# Fuzz the model + implementation (100 traces × 50 steps by default)
TARGET=http bun counter.spec.ts fuzz

# Require full coverage of every kind:status:branch, else exit 1
TARGET=http bun counter.spec.ts fuzz --strict

# Reproduce one trace deterministically and print the end state
TARGET=http bun counter.spec.ts seed --seed 12345 --steps 50

# Re-run everything in .failing-seeds.json; drops the ones now fixed
TARGET=http bun counter.spec.ts replay

# Linearizability across 4 concurrent clients
TARGET=http bun counter.spec.ts linearize --clients 4 --ops 20

# k6 load test (requires setPerf and k6 on PATH)
TARGET=http bun counter.spec.ts perf --rate 50 --duration 30

# Production hardening audit
MODE=production TARGET=http bun counter.spec.ts audit

TARGET selects a registered target by name. MODE=production is a safety switch: fuzz, seed, linearize, and perf refuse to run destructive traffic against a production target, while audit is the one command meant for production.

2. Inside a test runner

The same model plugs into bun:test:

import { test } from "bun:test";

test("counter", counter.run(async (req, snap, tick) => {
  await req({ kind: "incr", head: { corrId: crypto.randomUUID(), version: "1.0.0" }, data: {} });
  const state = await snap();      // asserts model == impl
  await tick(1);                   // advance the clock
}));

mbt.run(fn) returns a test function. In MODE=production the body is skipped entirely, so the same spec file is safe to ship.

What every trace checks, for free

On each step, with a target attached, formalizr asserts:

1. The model response validates against the response schema.
2. The model handler echoed the request's corrId and kind.
3. Every invariant holds (against the model state).
4. The implementation response deep-equals the model response.
5. The implementation state (via snap) deep-equals the model state.
6. Every invariant holds (against the implementation state).
7. If idempotent: replaying the request changes nothing.

Any failure prints the seed, step, request, expected vs. actual, and a diff, and appends the seed to .failing-seeds.json.

The agentic feedback loop

This is where formalizr earns its keep when a coding agent is doing the work.

An agent writing a stateful service without a spec is flying blind: it generates plausible code, writes a handful of tests that pass because they encode the same assumptions as the code, and declares victory. The bugs live in the cases nobody enumerated — the concurrent decrement, the delete-then-get, the auth gate that fires after validation instead of before.

formalizr closes that gap with a tight, machine-readable loop:

1. Model first. The agent writes the small pure model — a few dozen lines of handlers over a Zod state schema. This is far easier to get right than a distributed implementation, and it forces the agent to make the contract explicit: every status, every branch, every invariant, written down.

2. Implement against the model. The agent builds the real system behind a Target adapter. The model is now an independent oracle the implementation has never seen.

3. Fuzz. fuzz explores thousands of randomized traces. When the implementation diverges, the agent doesn't get a vague "test failed" — it gets the exact seed, step, request, model output, impl output, and a diff. The failure is deterministic and reproducible with seed --seed N. That precision is what lets an agent reason about a fix instead of guessing.

4. Fix at the root. Because the divergence is pinned to a single step and a single request kind, the agent fixes the actual rule, not the symptom the way a narrow test would push it to.

5. Replay. Every failing seed is persisted to .failing-seeds.json. replay re-runs the entire failure history and removes the seeds that now pass. Regressions can't sneak back in, and the file is the shrinking to-do list — a persistent, self-pruning backlog the agent works against.

6. Harden. Before shipping, linearize checks concurrency, perf checks latency, and audit checks that debug endpoints are closed and the JWT surface (alg:none, key confusion, embedded JWK, expired/garbage tokens) is rejected. All from the same model.

Why this multiplies an agent's effectiveness:

• Deterministic reproduction. A seed replays the exact trace every time. An agent can iterate on a fix and confirm it against the same failure without flakiness — the single biggest source of wasted agent turns.
• A diff, not a verdict. "Expected count: 0, got count: -1 at step 7 after decr" is directly actionable. "Something is wrong" is not.
• The model is the shared contract. Human and agent argue about the model — small, readable, reviewable — instead of about sprawling implementation details. Once the model is agreed, correctness of the implementation is a mechanical, checkable property.
• Coverage as a stopping condition. --strict fails until every kind:status:branch has been exercised, giving the agent an objective signal for "the fuzzer has actually explored the behavior," not just "it didn't crash."
• The oracle scales with the system. Adding a feature means adding a handler and a generator; the fuzzer immediately explores its interaction with everything else. The agent's test coverage grows automatically with the spec.

The loop turns "did the agent write correct code?" — unanswerable — into "does the implementation match the model, under fuzzing, concurrency, load, and adversarial auth?" — answerable, deterministically, on every run.

Project layout

src/
  index.ts            Public API surface
  protocol.ts         reqSchema / resSchema / isStatus envelope helpers
  rng.ts              Seeded, deterministic RNG + helpers (oneOf, fakeUUID)
  mbt/
    index.ts          The MBT class: builder, trace engine, CLI, all commands
    types.ts          Target, generator, handler, and coverage types
    zod-utils.ts      Schema normalization and kind/status derivation
    lincheckr/        Go linearizability checker (Porcupine-based)
  __tests__/          Model + framework tests (todo, counter, audit, perf, prod)

Development

bun install
bun test          # run the suite
bun run typecheck # tsc --noEmit
bun run check     # biome
bun run build     # emit dist/