Feynman

Understand how a system behaves, and what each change does to it.

Code tells you what each part does. It rarely tells you what happens when the parts meet: when a reply is lost, a lease runs out mid-write, or two people press the same button. Those are the bugs that reach production, and the questions a newcomer cannot answer by reading.

A Feynman spec is one TypeScript file that writes the behaviour down as a program that runs: the actors and their state, the messages between them, the actions people take, and the rules that must always hold, each step anchored to the code it stands for. From that one file you get:

• A simulator. Add people and machines, press the buttons they would, watch every message travel, lose one, and go back to any moment to try something else.
• A model checker that says how sure it is. It tries every order of events within bounds, with the faults the spec declares (lost messages, duplicates, crashes), then takes long random runs. Rules are safety ("never two holders") or liveness ("every request is answered"), judged under fairness as in TLA+, and a world where the system is stuck is reported too. A broken rule comes with the shortest trace that breaks it, and for liveness the loop it repeats forever; a rule that held says whether every state was explored.
• The flows of every scenario, step by step, and how they change between commits.
• The code behind each step, with its call tree, and a warning when that code changes under the spec.

See it on a real system: axo's remote access, where people pair Macs with a one-time code and open terminals on them through a relay.

Start

Feynman runs on Bun 1.3 or later.

bun add -d @leostera/feynman
bunx feynman check    # type-check, run the scenarios, explore, and judge every rule
bunx feynman dev      # the simulator, reloading as the spec changes
bunx feynman build    # minified standalone .feynman/index.html, plus .gz/.br for static hosting

feynman check --brief gives one line per property; --only P shows one property's counterexample, --json the whole result, and --only P --as-scenario the counterexample as a scenario you can paste into the spec.

Specs live in specs/*.ts and import @leostera/feynman:

import { atMost, budget, defineActor, defineMessage, defineProperty, defineSpec, defineZone, lose } from "@leostera/feynman";

// Faults are steps the spec declares: at most one on any path (`--set faults=2` for two).
const faults = budget("faults", 1);

const Acquire = defineMessage("Acquire");
const Granted = defineMessage("Granted", { token: Number }, { tone: "reply" });

const zone = defineZone({ name: "Cluster" });

const Server = defineActor({
  name: "Lock server",
  zone,
  singleton: true,
  initialState: () => ({ token: 0 }),
  transitions: {
    acquire: {
      on: Acquire,
      description: "Grants the lock with a larger token each time.",
      sends: [Granted],
      run(state, _msg, ctx) {
        state.token += 1;
        ctx.reply(Granted, { token: state.token });
      },
    },
  },
});

const Client = defineActor({
  name: "Client",
  zone,
  symmetric: true,
  initialState: () => ({ token: null as number | null }),
  actions: {
    acquire: {
      with: [atMost(2)], // at most twice per client on any path
      label: "Take the lock",
      description: "Asks the server for the lock.",
      sends: [Acquire],
      run(_state, _inputs, ctx) {
        ctx.send(ctx.the(Server), Acquire, {});
      },
    },
  },
  transitions: {
    granted: { on: Granted, description: "Holds the lock.", run: (state, msg) => void (state.token = msg.token) },
    // The network may lose the grant on its way.
    grantedLost: lose(Granted, { spend: faults }),
  },
});

const oneHolder = defineProperty("oneHolder", {
  description: "Two clients never hold the same token.",
  always: (w) => {
    const tokens = w.all(Client).map((c) => c.state.token).filter((t) => t !== null);
    return new Set(tokens).size === tokens.length;
  },
});

export default defineSpec({
  name: "Lease lock",
  actors: [Server, Client],
  properties: [oneHolder],
});

Every part is a value: messages with the schema of their payload, checked when sent; actors whose steps say what they are on; properties and scenarios. defineSpec puts them together, and says when they do not fit: a message no one receives, an undeclared send, two fair steps on one message. Faults come from the faults library (lose, duplicate, crash, calls whose failure reaches the caller), built on the same steps as everything else.

examples/ has 28 well-known systems (two-phase commit, Raft's vote, chain replication, CRDTs, dining philosophers and more), each with a real bug for the checker to find, the fix beside it, and most with TLA+ and P models that check the checker.

Let your agent write it

Specs are meant to be written by coding agents and read by people. The package ships a skill, skills/feynman/SKILL.md, that teaches an agent to read a codebase, model one behaviour, check it, and report what it found. Pi loads it from the package; other agents can read it at https://feynman.leostera.dev/SKILL.md. A prompt to start from:

Read https://feynman.leostera.dev/SKILL.md, then write a Feynman spec for how works in this repository. Put it in specs/, and run bunx feynman check until every rule holds or you can show a real bug. Report what the spec covers and every verdict.

Verdicts you can trust

Every rule gets one of four verdicts, and Feynman never rounds up:

• ✗ broken, with the trace, found by the search, a random run, or a scenario;
• ✓ holds in every state within the bounds, all of them explored;
• ~ held in the states explored, but a limit stopped the search first;
• ? never tested: nothing reached the situation the rule is about.

The checker is tested against others. On the examples, it finds the same distinct states, the same verdicts and counterexamples of the same length as TLA+'s TLC, and the same verdicts as the P checker (bun run oracles).

This repository

• src/: the DSL and engine (spec), the checker (check), sources and call trees (code), the CLI (cli), the playground kit (play), and the browser view (view).
• examples/: the example specs, and TLA+ and P models of them in examples/oracles/.
• skills/feynman/: the skill. docs/rfds/: the design, one decision at a time.
• sites/feynman.leostera.dev/: the website, and the simulators it publishes.

bun install
bun run test         # everything but the oracles
bun run typecheck
bun run feynman dev  # the examples in the simulator
npm publish          # builds the view, type-checks and tests first

Status: early. The DSL may still change between minor versions.