# seedfall


<!-- docs/README.md -->

# Documentation

seedfall runs your Go system in a simulated world, breaks it on purpose (crashes, lost messages, half-written files), and lets you replay any failure exactly. These pages are grouped by what you want to do. If you are new, read the first one and stop there for now.

## Start here

- [Getting started](getting-started.md): find, shrink, fix and prove a real bug in about five minutes, using an example that is included.
- [Installing seedfall](install.md): every way to install it, and how to check the install worked.
- [FAQ](faq.md): short answers, such as how seedfall differs from other tools and what it cannot test.
- [Troubleshooting](troubleshooting.md): look up an error message and see how to fix it.

## Find a bug

- [Networking](networking.md): let your nodes talk to each other inside the simulation.
- [Properties and checks](properties.md): write the statements your system must keep true, such as "an acknowledged write is never lost".
- [Storage engines that need mmap or flock](compat.md): test databases such as bbolt, pebble and badger.
- [Config files, profiles and seeded disks](config.md): keep several test setups in one file and start nodes from an existing disk.
- [Feedback-guided exploration](explore.md): hunt for bugs that need two rare events in one run.
- [BUGGIFY](buggify.md): mark places in your own code where seedfall may force a rare path.
- [Mutation testing your checks](mutate.md): find out whether your checks would notice a real bug.
- [Running Antithesis SDK code](antithesis.md): run programs that already use the Antithesis Go SDK.
- [Use your Gostman collections as workloads](gostman.md): reuse API checks you already wrote.

## Understand a failure

- [Timelines, logs and time-travel debugging](timeline.md): see a failing run as a diagram, a filtered log or a step-by-step debugger.
- [Causality analysis](cause.md): find which fault actually made a seed fail.
- [Inspecting the disk at the moment of failure](inspect.md): see which bytes were saved and which a crash would lose.
- [Proving a fix with `seedfall verify`](verify.md): show that a fix works, and pin the bug so it cannot come back.
- [Triage reports](reports.md): group many failing seeds into a short list of bugs.

## Use in CI

- [Running seedfall in CI](ci.md): the GitHub Action, machine-readable output, time limits and `go test`.
- [Using seedfall from AI coding agents](agents.md): the MCP server and skills that let an agent run seedfall for you.

## Reference

- [Configuration and faults](faults.md): every `seedfall.json` field and every fault seedfall can inject.
- [Properties, linearizability and determinism](properties.md): the full `sim` API for checks.
- [Triage reports](reports.md): findings, classification, failure artifacts, notifications and utilization.
- [Troubleshooting](troubleshooting.md): the error catalog, keyed by exact message.
- [How seedfall works](how-it-works.md): the simulated clock, the disk and network models, checking, shrinking and speed.
- [Testing seedfall itself](testing.md): what the project's own tests prove.
- [Findings](findings/README.md): bugs seedfall found in open-source projects, with replay commands.

## About the project

- [Contributing](../CONTRIBUTING.md): development setup, tests and commit style.
- [Roadmap](../ROADMAP.md): what is planned and what is not done yet.
- [Security policy](../SECURITY.md) and [code of conduct](../CODE_OF_CONDUCT.md).


<!-- docs/agents.md -->

# Using seedfall from AI coding agents

This page is for people who let an AI coding agent, such as Claude Code, Cursor or Codex, do the testing work. seedfall can talk to the agent directly through an MCP server (a standard way for an agent to call tools) and ships skills (step-by-step instructions the agent follows). Use it to let the agent find a bug, shrink it, fix it and prove the fix.

`seedfall mcp` serves seedfall's core operations over the [Model Context Protocol](https://modelcontextprotocol.io) on stdio. An agent such as Claude Code, Cursor or Codex can then sweep seeds, replay a failure and shrink it on its own, then use the exact fault schedule and trace to fix the bug and prove the fix. No API key and no hosted service are involved: the agent you already use does the reasoning.

## Setup

Install the binary first. Every integration below runs it:

```sh
go install github.com/kunalgoesbyken/seedfall/cmd/seedfall@latest
```

### Skills

The skills follow the [Agent Skills](https://agentskills.io/specification) format, so any agent that reads `SKILL.md` files can use them. To install them with the [`skills` CLI](https://github.com/vercel-labs/skills):

```sh
npx skills add kunalgoesbyken/seedfall
```

### MCP server

Claude Code:

```sh
claude mcp add seedfall -- seedfall mcp
```

Cursor, or any client that reads an `mcpServers` file:

```json
{
  "mcpServers": {
    "seedfall": { "command": "seedfall", "args": ["mcp"] }
  }
}
```

Config paths in tool calls are resolved against the server's working directory, which is normally your project root. Every tool that takes `config` also takes an optional `profile` and a `set` list of `path=value` overrides, the same as `-profile` and `-set` on the command line ([config.md](config.md)).

## Tools

| Tool | Arguments | Returns |
|---|---|---|
| `seedfall_init` | optional `dir`, `config`, `nodes`, `workload`, `dry_run` | The module's `main` packages and which become nodes, the packages that block a `GOOS=wasip1` build (compile errors and cgo, each with its import chain and the shim that covers it), `compat_shims` for every dependency `compat_overlay` would swap, the starter config and its starter profiles, the files written, and the next steps. See [onboarding](#onboarding-a-new-module) |
| `seedfall_run` | `config`, `seeds` (for example `1-200`), optional `rotate`, `check`, `skip_pinned`, `until_novelty`, `batch`, `timeout` | First the [pinned regressions](verify.md#pinned-regressions), stopping at one that fails again. Then seeds passed, the lowest failing seed with its reason, [classification](reports.md#classification), the faults before the failure, the trace tail, a replay command and `artifacts_dir` ([failure artifacts](reports.md#failure-artifacts)), plus property coverage, `seeds_per_second`, `virtual_seconds_per_wall_second` and `utilization` ([reports.md](reports.md#utilization)), and, with `faults.buggify` on, `buggify_sites` ([buggify](buggify.md#coverage)). With `until_novelty`, `stopped` and the `exploration` growth table ([explore.md](explore.md#stopping-a-plain-sweep)) |
| `seedfall_explore` | `config`, optional `seeds`, `rounds`, `batch`, `until_novelty`, `budget`, `explore_seed`, `keep_going`, `corpus` | Feedback-guided search: every round with the new signals and functions it added, the stop reason, the corpus size, property coverage, throughput, and the first failure with `artifacts_dir` and a replay command ([explore.md](explore.md)) |
| `seedfall_replay` | `config`, `seed`, optional `faults` file | The same failure view for one seed, or the trace tail if it passes, with a `note` when a shrunk schedule's shorter duration ended the run before the workload finished. A failure view of a run that recorded operations also names its `history_file` and, on a linearizability violation, its `timeline_file`. Every result has the run's `determinism_hash` and its `events` from `sim.Event` or `lifecycle.SendEvent` |
| `seedfall_logs` | `config`, `seed`, optional `faults`, `node`, `grep`, `from`, `to`, `net_trace`, `limit` | The run's trace lines filtered by node, regular expression and virtual time, each with its node, instance and time, and a node's slog JSON output parsed into `fields`, plus how many lines matched ([timeline.md](timeline.md#logs)) |
| `seedfall_trace_search` | `config`, `seed`, `pattern`, optional `faults`, `context` (default 3), `node`, `from`, `to`, `net_trace`, `limit` | Each line that matches the regular expression (on the given nodes, inside the virtual time window) with `context` trace lines of every node before and after it, as windows of numbered lines with their virtual time, node and instance, overlapping windows merged, plus how many lines matched ([timeline.md](timeline.md#searching-the-trace)) |
| `seedfall_debug` | `config`, `seed`, optional `faults`, `at`, `net_trace`, `commands` | Replays to `at`, runs each debugger command (`where`, `net`, `faults`, `ls`, `stat`, `cat`, `step`, `until <regex>`, `to <time>`, `branch`, `log`, `grep`) and returns each output and the final state of every node ([timeline.md](timeline.md#debugger)) |
| `seedfall_shrink` | `config`, `seed`, optional `faults` (a schedule file, for a failure found by `seedfall_explore`), `budget` (runs such as `300`, or time such as `10m`) | The original and minimal sizes (faults, duration and, with [`sim.Budget`](properties.md#workload-size), workload operations), the runs used, whether the budget ran out, the path of the saved schedule, and the failure view under that schedule with its replay command ([shrinking](how-it-works.md#shrinking)) |
| `seedfall_faults_edit` | `config`, `seed`, optional `faults`, `remove`, `shift`, `add`, `out` | Edits a fault schedule to test a hypothesis: `remove` takes positions counting from 1, `shift` takes `{"fault": 2, "by": "-50ms"}` (a count such as `"+2"` for a fault that fires at a disk operation, read, buggify hit, counted call or udp datagram), `add` takes faults in the [schedule format](faults.md#editing-a-schedule). Starts from `faults`, else `.seedfall/seed-N.faults.json`, else the seed's own faults, checks every fault against the config and writes nothing if one is wrong. Returns the numbered schedule, the file written (`out`, or the file it came from) and the replay command |
| `seedfall_inspect` | `config`, `seed`, optional `faults`, `at`, `node`, `path` | Every node's disk at the failure or at virtual time `at`: per file the live and durable sizes, the byte ranges a crash would lose, whether its directory entry is durable, the last torn write, and removed entries a crash would bring back. With `path`, one file's durable content as text or a hex dump ([inspect.md](inspect.md)) |
| `seedfall_check` | `history`, optional `model` | Re-checks a recorded history file against a model: the verdict, each anomaly with its cycle, and on a linearizability violation the HTML timeline file ([properties.md](properties.md#history-files)) |
| `seedfall_verify` | `config`, `seed` and optional `faults`, and/or `report`; optional `seeds`, `check_seeds`, `mutate`, `app_mutants` | Whether the fix holds: each replayed schedule, the fresh sweep with its confidence, the determinism check and the mutants, plus a Markdown proof block for the PR ([verify.md](verify.md)) |
| `seedfall_mutate` | `config`, optional `seeds` (default `1-100`), `only`, `app`, `mutants` | Sweeps the seeds unmutated, then once per [mutant](mutate.md) (disk, rename, truncate, network and clock guarantees), or with `app` once per [source mutant](mutate.md#source-mutants) of the node packages: each mutant's `outcome` (`killed`, `survived`, `not exercised` or `did not build`), its `location` and change for source mutants, the seed and reason that killed it, and how often the operation was weakened |
| `seedfall_pin` | `config`, `seed`, optional `faults` | Pins the seed's schedule (the one `seedfall_shrink` saved, the given file, or else the seed's own faults) into `seedfall-regressions/` as a permanent regression, and returns the file and whether it passes now, with the failure view if not ([verify.md](verify.md#pinned-regressions)) |
| `seedfall_doctor` | none | Checks the Go version, `GOOS=wasip1` builds, `net_overlay` against the installed Go, a writable build cache and working directory, and free memory, returning the seedfall build and each check as `ok`, `warn`, `fail` or `skip` with a fix ([install.md](install.md#check-the-install)) |
| `seedfall_findings` | optional `report` (default `.seedfall/report.html`), `history`, `status` (comma separated: `new`, `ongoing`, `regressed`, `resolved`, `not seen`) | Reads a triage report from `seedfall run -report` without running anything, the same as `seedfall findings`: each finding with the given statuses with its status, failing seeds, rate, classification and example failure with replay and shrink commands, findings not seen this time, unmet properties, and the run history of that config from `.seedfall/history.jsonl` ([reports.md](reports.md)) |
| `seedfall_cause` | `config`, `seed`, optional `points`, `branches` | The probability of failing from each moment of the run, with the faults between moments, so the agent can see which event made the failure inevitable ([cause.md](cause.md)) |

Every result is structured JSON, so the agent can read the seed, the faults and the trace directly.

### The same operations on the command line

Every tool has a command, so a person can repeat what the agent did and an agent without MCP can shell out:

| Tool | Command |
|---|---|
| `seedfall_init`, `seedfall_run`, `seedfall_explore`, `seedfall_replay`, `seedfall_logs`, `seedfall_debug`, `seedfall_shrink`, `seedfall_cause`, `seedfall_inspect`, `seedfall_check`, `seedfall_verify`, `seedfall_mutate`, `seedfall_pin` | `seedfall init`, `run`, `explore`, `replay`, `logs`, `debug`, `shrink`, `cause`, `inspect`, `check`, `verify`, `mutate`, `pin` |
| `seedfall_trace_search` | `seedfall trace grep -seed N -e re [-context 3]` |
| `seedfall_faults_edit` | `seedfall faults -seed N [-remove 2] [-shift 1=-50ms] [-add '{...}'] [-out file]` |
| `seedfall_findings` | `seedfall findings [-status new,regressed] [-json]` |
| `seedfall_doctor` | `seedfall doctor [-json]` |

`seedfall schema` prints the whole surface as JSON: every command with each flag's name, type, default and usage, and every MCP tool with its description and input and output JSON Schemas, plus the prompts and resources. Generate client bindings or check an agent's calls against it:

```sh
seedfall schema | jq '.commands[] | select(.command == "seedfall faults") | .flags[].name'
seedfall schema | jq '.mcp_tools[] | select(.name == "seedfall_faults_edit") | .inputSchema'
```

## Prompts and resources

The server also serves what an agent needs in order to work without guessing:

| Kind | Name | Contents |
|---|---|---|
| Prompt | `seedfall-setup`, `seedfall-properties`, `seedfall-triage`, `seedfall-fix-and-prove` | The four [skills](#skills), so MCP clients without skill support get the same workflows |
| Resource | `seedfall://schema/config` | JSON Schema of `seedfall.json`, generated from the config types, with every field's default |
| Resource | `seedfall://docs/<name>` | Each page of these docs, for example `seedfall://docs/properties` for the property API and `seedfall://docs/faults` for what each fault does |

## Onboarding a new module

`seedfall init` (MCP: `seedfall_init`) is the first step in a repository that has never run seedfall:

```sh
seedfall init -n                     # report only
seedfall init                        # write seedfall.json and seedfall/workload/main.go
seedfall init -node ./cmd/server     # choose the nodes yourself; repeatable
seedfall init -json                  # the same report as JSON
```

It runs `go list` twice. The first run uses `GOOS=wasip1 -export -deps`, so every package is compiled for wasip1, and any package that fails is reported with its compiler error and the import chain from the node that pulls it in. The second uses `GOOS=linux CGO_ENABLED=1` and lists the dependencies that contain cgo files. Every `main` package that imports `net` becomes a node. `net_overlay` is turned on unless every node already uses `sim`.

The scaffolded workload follows the pattern every example shares: write keys, remember which ones were acknowledged, then read each one back after the faults. Its `put` and `get` return `errors.ErrUnsupported` until the agent implements them against the service's API. Until then the sweep fails with `the workload got acknowledged writes` never true, so an unwired workload can never pass. Existing files are never overwritten.

On a fresh copy of `examples/kvlog` with its configs removed, `seedfall init -node ./server` writes a config and a workload. Wiring `put` and `get` to kvlog's line protocol takes about twenty lines. The first sweep then fails on seed 1 with `acknowledged write lost`, and shrink brings it down to the same two faults as the [getting started guide](getting-started.md).

## Skills

The `skills/` directory holds four skills. They follow the order of a real adoption, and every command in them runs as written:

| Skill | Use it to |
|---|---|
| `seedfall-setup` | Install, run `seedfall init`, clear the wasip1 blockers, wire the workload and run the first sweep |
| `seedfall-properties` | Read the storage and replication code, write `sim` properties for its durability and consistency promises, and grade them with `seedfall mutate` until every exercised mutant is killed |
| `seedfall-triage` | Classify, shrink, find the decisive fault with `cause`, inspect the disk, and confirm the explanation with a replay of an edited schedule |
| `seedfall-fix-and-prove` | Fix the cause, replay the saved schedule, sweep, run `seedfall verify -mutate -md proof.md` and paste the proof into the pull request |

## The `seedfall hook` command

`seedfall hook` is a small command that reads a Claude Code hook payload (JSON with `cwd` and `stop_hook_active`) from stdin. It does nothing unless `SEEDFALL_HOOK_SEEDS` is set, for example to `1-20`. It is not installed for you; you only get it by pointing your own hook setup at it.

When the variable is set and `seedfall.json` exists in the payload's `cwd` (or the file named by `SEEDFALL_HOOK_CONFIG`), the command replays the [pinned regressions](verify.md#pinned-regressions), then sweeps those seeds, under the profile named by `SEEDFALL_HOOK_PROFILE` if it is set. On a failure, or a property that was never reached or never true, it prints the seed with the replay and shrink commands to stderr and exits with code 2. If `stop_hook_active` is true it exits 0 without running, so it cannot loop.

## Docs for models

The site serves [`llms.txt`](https://seedfall-lemon.vercel.app/llms.txt), an index of these docs and the skills, and [`llms-full.txt`](https://seedfall-lemon.vercel.app/llms-full.txt), their full text. `bash scripts/site-llms.sh` generates both from `docs/` and `skills/`.

## A verification loop

Ask the agent to treat a seed sweep as the definition of done for storage or replication changes:

1. Run `seedfall_run` over a few hundred seeds before changing anything, to record the baseline.
2. When a seed fails, run `seedfall_shrink` and read the minimal fault schedule. It usually names the exact window: "crash during disk op #56", then "crash". `seedfall_cause` shows which of those faults made the failure likely, and `seedfall_faults_edit` with `out` plus `seedfall_replay` tests a guess, such as dropping a fault or moving a crash one disk operation earlier.
3. Fix the code, then `seedfall_replay` the saved schedule until it passes.
4. Run `seedfall_verify` with the seed and schedule and paste its `markdown` proof block into the pull request.

Shrunk schedules are small enough that an agent can reason about them step by step. `examples/kvlog` is a good first exercise: its `seedfall.always.json` shrinks to two faults.


<!-- docs/antithesis.md -->

# Running Antithesis SDK code

Antithesis is a commercial testing platform with its own Go SDK, a library for writing checks inside your program. If your code already uses that SDK, seedfall runs it unchanged and turns each SDK call into a seedfall check. Read this page if you are coming from Antithesis or share code with a team that uses it.

Code instrumented with the [Antithesis Go SDK](https://github.com/antithesishq/antithesis-sdk-go) runs under seedfall unchanged. Assertions become seedfall properties, `lifecycle.SetupComplete` becomes seedfall's setup signal, and `random.GetRandom` draws from the seed.

`examples/ledger` has no seedfall imports at all. It uses plain `net` (through `net_overlay`) and only the Antithesis SDK:

```go
lifecycle.SetupComplete(map[string]any{"ledger": addr})
amount := int(random.GetRandom()%100) + 1
assert.Sometimes(unacked > 0, "a crash interrupted a deposit", nil)
lifecycle.SendEvent("deposits finished", map[string]any{"total": total, "acked": acked, "unacked": unacked})
assert.AlwaysGreaterThanOrEqualTo(total, acked, "ledger total covers every acknowledged deposit", map[string]any{"unacked": unacked})
assert.AlwaysLessThanOrEqualTo(total, acked+unacked, "ledger total holds no deposit that was never sent", nil)
assert.SometimesAll([]assert.NamedBool{{First: "interrupted", Second: unacked > 0}, {First: "kept", Second: total > acked}}, "an unacknowledged deposit survived a crash", nil)
```

```
$ seedfall run -c seedfall.json -seeds 1-20
property       seeds reached  seeds true
  sometimes              20          18  a crash interrupted a deposit
  sometimes              20           2  an unacknowledged deposit survived a crash
  always                 20          20  ledger total covers every acknowledged deposit  (smallest margin 0)
  always                 20          20  ledger total holds no deposit that was never sent  (smallest margin 0)
  sometimes              20           5  recovery dropped a partial entry

ok  20 seeds passed (0 hit the time horizon) in 908ms

$ seedfall run -c seedfall.json -profile nofsync -seeds 1-20
FAIL seed 1 at t=2.940793302s (618 scheduler steps, 336ms real)
  client#1: ledger total covers every acknowledged deposit: {"left":4203,"right":5608,"unacked":1729}
```

## How it works

On `wasip1` the SDK has no native Antithesis library to talk to, so it writes each event as a JSON line to the file named by `ANTITHESIS_SDK_LOCAL_OUTPUT`. seedfall sets that variable for every node and serves the path as a virtual file. Each line is decoded as it is written:

| SDK call | seedfall property |
|---|---|
| `assert.Always` | `always`: fails the seed when false, fails the sweep if never reached |
| `assert.AlwaysOrUnreachable` | `always_or_unreachable`: fails the seed when false |
| `assert.Sometimes` | `sometimes`: fails the sweep if never true |
| `assert.Reachable` | `reachable`: fails the sweep if never reached |
| `assert.Unreachable` | `unreachable`: fails the seed when reached |
| `assert.AlwaysGreaterThan`, `AlwaysGreaterThanOrEqualTo`, `AlwaysLessThan`, `AlwaysLessThanOrEqualTo` | `always`, with the smallest margin in the property table |
| `assert.SometimesGreaterThan`, `SometimesGreaterThanOrEqualTo`, `SometimesLessThan`, `SometimesLessThanOrEqualTo` | `sometimes`, with the largest margin in the property table |
| `assert.AlwaysSome` | `always`: at least one named boolean is true |
| `assert.SometimesAll` | `sometimes`: every named boolean is true |
| `lifecycle.SetupComplete` | ends the setup phase when `faults_after_setup` is on |
| `lifecycle.SendEvent` | an [event](properties.md#events): a trace line with the details as JSON, returned by `seedfall_replay` |

The SDK's details map appears as JSON in the failure message; the numeric variants add `left` and `right`, and the grouped variants add each named boolean. seedfall's source catalog recognizes every `assert.*` call above with a constant message, so Antithesis assertions that never run are reported too.

The margin of a numeric assertion comes from the SDK's own guidance records. Like Antithesis, the SDK only reports a new value when it gets closer to failing (for `Always`) or closer to true (for `Sometimes`), so the smallest and largest margins are exact. The SDK also reports each assertion only the first time it passes and the first time it fails in a process, so the number of hits is lower than with `sim` assertions; seeds reached and seeds true are unaffected.

`sim` has the same variants with the same names ([properties.md](properties.md#numeric-and-grouped-properties)), and `sim.Event` matches `lifecycle.SendEvent`.

`random.GetRandom` and `random.RandomChoice` read `crypto/rand`, which seedfall feeds from the seed, so they replay exactly and draw from the same source as `sim.Random` and `sim.RandomChoice`. Antithesis custom faults are commands its platform runs from outside your program and have no SDK call to map; mark the same spots with `sim.Buggify` instead ([buggify.md](buggify.md)).

## What you get compared with Antithesis

The same assertions and the same setup signal, run locally or in CI for free, with seed replay, shrinking, causality analysis and triage reports. What you don't get: Antithesis runs arbitrary containers in a deterministic hypervisor, while seedfall runs Go programs that build for `wasip1`.


<!-- docs/buggify.md -->

# BUGGIFY: faults inside your code

Most seedfall faults hit your program from the outside: a crash, a broken disk, a cut network. BUGGIFY lets you mark spots inside your own code where seedfall may force a rare path on purpose, such as a lost reply, a retry or an error return. Use it when the bug you fear lives in your own error handling, which outside faults rarely reach.

Every other seedfall fault comes from outside the process: crashes, torn writes, partitions. `sim.Buggify` lets you mark places in your own code where the simulator may force the rare path, such as a dropped reply, a retry, an error return, a minimal quorum or an extra delay. The idea comes from FoundationDB's `BUGGIFY`, which FoundationDB credits for many of its deepest bugs.

```go
v := c.apply(req)
if sim.Buggify("reply lost after apply") {
	return
}
reply(conn, v)
```

Outside the simulator `Buggify` always returns false, so the site costs one function call in production.

## Turning it on

Sites never fire unless the config asks for it:

```json
{ "faults": { "buggify": true } }
```

With `swarm` as well, each seed turns buggify on or off along with the other fault types.

## How a site decides

| Step | Rule |
|---|---|
| Enable | The first time a site is reached in a run, it is enabled with probability 0.25 and stays enabled or disabled for the rest of that run |
| Fire | Each time an enabled site is reached, it fires with probability 0.25 for `sim.Buggify(site)`, or `p` for `sim.BuggifyWithProb(site, p)` |
| Quiet | A site never fires during `sim.QuietFor`, during the recovery phase of `liveness` or the `finally` check, or, with `faults_after_setup`, before `sim.SetupComplete` |

A site is identified by its name, so keep names constant. Both decisions use random streams keyed by the seed and the site name (and, for firing, the node), so adding a site or reaching another site more often never changes when an existing site fires. Most seeds run with only some sites enabled, which explores combinations that firing every site everywhere would hide.

## Replay and shrink

Each firing is recorded as a fault with the node, the site and which hit it was, counted per node and site:

```
faults before the failure (1):
  465.631ms  buggify "reply lost after apply" fires on counter at hit #35
```

```json
{ "at": "465.631252ms", "kind": "buggify", "node": "counter", "site": "reply lost after apply", "until": "0s", "op": 35 }
```

When a schedule is replayed with `-faults`, a site fires exactly at the hits the schedule lists and nowhere else, so `seedfall shrink` removes firings like any other fault, and you can hand-edit a schedule to add or drop one. Replaying a schedule needs `"buggify": true` in the config, and with `swarm` it must be on for that seed: otherwise every site returns false. The trace shows when each site is first reached and whether it is enabled for the run, and every firing.

## Coverage

seedfall catalogs `sim.Buggify` and `sim.BuggifyWithProb` calls whose site is a string literal, and after a sweep with `buggify` on it prints how often each site was reached, enabled and fired:

```
buggify  seeds reached  seeds enabled  seeds fired  fired
                    20              6            6     88  reply lost after apply
                    20              5            5    110  slow apply
```

A site marked `never reached` (with its location) is code no seed ran; `never fired` means it ran but never fired: no seed enabled it, or its rate was too low for the hits it got, so sweep more seeds or raise its probability. Neither fails the sweep: pair a site with a `sim.Sometimes` on the path it opens when you want that path to be required. The same counts are in `buggify_sites` in `run -json` and in the MCP `seedfall_run` result.

## Structured randomness

`sim.Random()` returns a random `uint64` and `sim.RandomChoice(items)` returns one element of a slice (an empty slice fails the run, since there is nothing to return). Inside the simulator both read `crypto/rand`, which seedfall feeds from a stream keyed by the seed, the node and its restart count, so a choice replays with the seed. `RandomChoice` rejects out-of-range draws, so every element is equally likely. Outside the simulator they use `crypto/rand`.

```go
if sim.BuggifyWithProb("slow apply", 0.5) {
	time.Sleep(sim.RandomChoice([]time.Duration{time.Millisecond, 5 * time.Millisecond, 50 * time.Millisecond}))
}
```

The Antithesis SDK's `random.GetRandom` and `random.RandomChoice` read the same source, so Antithesis-instrumented code gets the same replayable choices with no changes. See [antithesis.md](antithesis.md).

## Example

[`examples/buggify`](../examples/buggify) is a counter service whose client retries an increment when the reply does not arrive. Without buggify nothing ever drops a reply and every seed passes; with it, `reply lost after apply` makes the retry apply twice and the sweep fails, and the fixed server, which remembers applied request ids, passes.

## Limits

- A site's name is its identity: two call sites with the same name share one enable decision and one hit count per node.
- Sites named by a non-literal string still fire and are recorded, but cannot be cataloged in advance.
- `seedfall cause` re-randomizes when sites fire after each branch point, not which sites are enabled, so a seed's enabled set is fixed for that seed.


<!-- docs/cause.md -->

# Causality analysis

When a seed fails, you know it failed but not always which event decided it. `seedfall cause` replays the run from many points and shows when the failure became likely and which fault tipped it over. Use it after `shrink` when the short fault list still leaves you asking which fault matters.

`seedfall shrink` tells you which faults are *needed* for a failure. `seedfall cause` tells you *when the failure became likely*, and which event made it so.

```sh
seedfall cause -c seedfall.always.json -seed 1
```

```
seed 1 fails at t=2.891820635s: client#1: acknowledged write lost: k96=v96, server now answers "NONE"

chance of failing when everything after a moment is re-randomized (20 futures each):

         0s     5%  ██
  292.108ms     5%  ██                              <- after 292.108ms  partition [client] from the rest until 627.143ms
  722.955ms     0%
  757.268ms     0%
  757.268ms    75%  ███████████████████████         <- after 757.268ms  crash server during disk op #56, restart at 1.121388s
  1.084433s    75%  ███████████████████████
    1.7052s    65%  ████████████████████
    1.7052s   100%  ██████████████████████████████  <- after 1.7052s  crash server, restart at 1.942589s
  2.711082s   100%  ██████████████████████████████

biggest jump: 0% -> 75% at 757.268ms  <- after 757.268ms  crash server during disk op #56, restart at 1.121388s

440 runs in 24.296s
```

(Abridged: the full output has one row per moment.)

Read it from top to bottom. Before anything happens, a random future of this world fails 5% of the time. The partition changes nothing, so it is a bystander. The crash in the middle of disk operation #56 takes the odds from 0% to 75%: that is when the torn record lands on disk. The second crash makes the failure certain. Even before reading any code, you know which event to look at.

## How it works

For each moment *T*, seedfall replays the seed exactly up to *T*. At the first scheduler step at or after *T*, it re-keys every random stream: scheduling, network latency, disk tearing, I/O faults, what `random_get` hands each node (so `crypto/rand` and `sim.Random`, but not Go's runtime-seeded `math/rand`), and the remaining fault schedule. Then it lets the run continue into a new future. Running many such branches from the same moment estimates the probability of failing from that state.

This needs no snapshots. Because replay is exact, "the state at *T*" is reproduced by running the seed to *T*. That is the same property Antithesis's multiverse debugging relies on, with deterministic replay standing in for VM snapshots.

Moments are chosen evenly across the run (`-points`, default 16), plus just before and just after every fault. Each moment gets `-branches` futures (default 20), so the default costs a few hundred runs, all in parallel.

Branches are also the basis of [feedback-guided exploration](explore.md), which keeps branching from runs that reached something new.

## From an agent

The MCP server exposes the same analysis as `seedfall_cause`, returning the curve as JSON with the faults between consecutive moments. See [agents.md](agents.md).


<!-- docs/ci.md -->

# Running seedfall in CI

This page shows how to run seedfall automatically on every pull request or on a schedule: the GitHub Action, machine-readable output, time limits and sweeps started from `go test`. Use it once seedfall works on your laptop and you want it to guard your main branch.

## GitHub Actions

```yaml
jobs:
  simulate:
    runs-on: ubuntu-latest
    permissions:
      contents: read
      pull-requests: write
    steps:
      - uses: actions/checkout@v4
      - uses: kunalgoesbyken/seedfall@main
        id: seedfall
        with:
          config: seedfall.json
          seeds: 1-500
          check: "true"
          comment: "true"
```

The inputs below other than `config`, `profile`, `seeds`, `check`, `go-version`, `report` and `artifact-name` are newer than v0.2.0, hence `@main` until the next release.

### Inputs

| Input | Default | Meaning |
|---|---|---|
| `command` | `run` | `run`, `verify` or `mutate` ([below](#verify-and-mutate)) |
| `config` | `seedfall.json` | Path to the world description |
| `profile` | | Profile from the config's `profiles` to merge over it ([config.md](config.md#profiles)) |
| `seeds` | | Seed or inclusive range. Empty uses the command's own default: `run` sweeps `1-200`, `mutate` `1-100`, and `verify` as many fresh seeds as 95% confidence needs |
| `rotate-seeds` | `false` | With `run`, move `seeds` forward by its own width for each workflow run ([below](#rotating-seeds)) |
| `check` | `false` | With `run`, run every seed twice and fail at the first host call or trace line that differs |
| `args` | | Extra flags for the command, separated by spaces, such as `-timeout 10m`, `-only fsync_noop` or `-seed 1`. Quoting is not interpreted |
| `version` | | seedfall release to download, or `latest` ([below](#which-seedfall-runs)) |
| `go-version` | `stable` | Go version for building your nodes, and seedfall when it is built from source |
| `report` | `true` | With `run`, sweep every seed and upload an HTML triage report. `false` stops at the first failure |
| `artifact-name` | `seedfall-report` | Name of the uploaded artifact, also used to keep each job's cache and pull request comment apart. Make it unique per job in a matrix |
| `cache` | `true` | Keep the run history and compiled modules between runs ([below](#history-between-runs)) |
| `comment` | `false` | Post or update one pull request comment with the outcome. Needs `pull-requests: write` |
| `webhook` | | Slack or Discord incoming webhook URL, best from a secret. Posts the report's new and regressed findings with `seedfall report notify` |
| `file-issues` | `false` | File a GitHub issue for each finding without an open one, with `seedfall report issue` |

An input that does not apply is an error rather than being ignored: `check` or `rotate-seeds` with `verify` or `mutate`, `comment` with `report: "false"`, and `webhook` or `file-issues` with `report: "false"` or a `verify` or `mutate` command.

The job fails if any seed or [pinned regression](verify.md#pinned-regressions) fails. The triage report (see [reports.md](reports.md)) is uploaded as an artifact, together with the [failure artifacts](reports.md#failure-artifacts) under `failures/`.

### Outputs

| Output | Meaning |
|---|---|
| `status` | `passed`, `failed`, or `error` when seedfall could not finish, for example a config that does not build. With `report: "false"` a `run` that cannot start also reads `failed`, because nothing distinguishes the two |
| `failing-seed` | With a `run` report, the seed to look at first: a pinned regression that fails again, else the first regressed, new, then ongoing finding. Empty on a clean run |
| `findings` | With a `run` report, how many findings the report has |
| `report-path` | The HTML report on the runner, or the Markdown from `verify` or `mutate`. Runner temp is cleared when the job ends |

```yaml
      - if: failure() && steps.seedfall.outputs.status == 'failed'
        run: echo "replay with seed ${{ steps.seedfall.outputs.failing-seed }}"
```

The job summary shows the same Markdown as the [pull request comment](#pull-request-comments), with seedfall's output folded below it. When seedfall cannot finish, such as a config that does not build or a `mutate` baseline that already fails, the summary says so with the last lines of output. Problems also appear as error annotations on the run and the pull request's changed files. A finding from a property with a constant message is annotated at its source line, from the same catalog that reports properties that were never reached. Other failures, such as a crash or a `sim.Assert`, are annotated without a file. GitHub only shows a limited number of annotations per step, so failing regressions come first, then regressed, new and ongoing findings, then unmet properties.

### Which seedfall runs

With `version` empty, the action uses the release that matches the ref in `uses:`, so `@v1.2.3` downloads v1.2.3 for the runner's platform and checks it against the release's `checksums.txt`. A checksum mismatch fails the job. If the ref has no release, such as a branch, a commit or a release older than the automated pipeline like v0.2.0, seedfall is built from the action's source instead. Windows runners and `uses: ./` always build from source. The job log has a notice saying whether seedfall was installed from a release or built from source.

Set `version: v1.2.3`, or `latest`, to run a specific release regardless of the ref. An explicit version never falls back: a missing release fails the job, and it needs a Linux or macOS runner and a released action. Go is set up either way, because seedfall compiles your nodes with it.

### History between runs

New, ongoing, resolved and regressed need the run history ([reports.md](reports.md#history-new-ongoing-resolved-regressed)), so with `cache` on the action restores and saves `.seedfall/history.jsonl` and `.seedfall/cache` next to the config, with `actions/cache`. It saves even when the sweep fails, since that is the run whose history matters most.

The key is the config file's hash, the `artifact-name`, the branch and the run, and restoring falls back to the newest entry for that config and name from this branch, then from any branch the run can read, so a pull request starts from its base branch's history. Changing the config starts a new history. An `extends` parent is not part of the hash. Keep `artifact-name` unique per job, or jobs in a matrix overwrite each other's history.

Set `cache: "false"` if you keep `.seedfall/history.jsonl` some other way, such as committing it.

### Pull request comments

`comment: "true"` posts one comment per job and edits it on later pushes, so a pull request does not collect one per run. It lists new, regressed and resolved findings, ongoing ones, failing pinned regressions and unmet properties, each failure with its replay command, and links the workflow run. It is the job summary's Markdown, so with `verify` or `mutate` it is the proof or the mutant table, and when seedfall cannot finish it says so. A clean run also updates it, so a stale failure does not linger. Only a comment written by the token's own account is edited, so a comment someone else posts with the same marker is left alone. The comment never includes seedfall's raw output; that stays in the job summary.

The job needs `pull-requests: write`. Pull requests from forks run with a read-only token, so the action logs a warning and the job's result is unaffected. `seedfall report comment` does the same from any CI, and `seedfall report github` writes the annotations and outputs ([reports.md](reports.md#github)).

### Verify and mutate

`command: verify` runs [`seedfall verify`](verify.md), and `args` names what to verify:

```yaml
      - uses: kunalgoesbyken/seedfall@main
        with:
          command: verify
          config: seedfall.fixed.json
          args: -seed 1 -faults testdata/torntail.faults.json -mutate
          comment: "true"
```

`command: mutate` runs [`seedfall mutate`](mutate.md) and fails if a mutant survives:

```yaml
      - uses: kunalgoesbyken/seedfall@main
        with:
          command: mutate
          seeds: 1-50
          args: -only fsync_noop,net_dup_chunk
```

Both write Markdown to the job summary and the artifact (`proof.md`, `mutants.md`). `failing-seed` and `findings` stay empty, because neither command writes a triage report.

### Rotating seeds

`rotate-seeds: "true"` keeps exploring new schedules. Run number `n` sweeps the range `n - 1` widths after `seeds`: with `seeds: 1-200`, run 1 sweeps 1-200, run 2 201-400, and run 8 1401-1600. Re-running a job keeps its run number, so it sweeps the same seeds. Every failure names its seed, so it stays exactly reproducible, and [pinned regressions](verify.md#pinned-regressions) still replay on every run.

Outside the action, `seedfall run -seeds 1-200 -rotate N` sweeps the Nth range after `-seeds`, and refuses a rotation past the largest seed.

### Nightly sweep

A template for a scheduled sweep, with alerts and issues for new and regressed findings:

```yaml
name: nightly-simulation
on:
  schedule:
    - cron: "17 3 * * *"
  workflow_dispatch:
jobs:
  simulate:
    runs-on: ubuntu-latest
    timeout-minutes: 60
    permissions:
      contents: read
      issues: write
    steps:
      - uses: actions/checkout@v4
      - uses: kunalgoesbyken/seedfall@main
        with:
          seeds: 1-500
          rotate-seeds: "true"
          args: -timeout 45m
          webhook: ${{ secrets.SEEDFALL_WEBHOOK }}
          file-issues: "true"
```

The history is what limits alerts to new and regressed findings, so leave `cache` on. The message links the workflow run, and each issue names the seed, the replay command, the seedfall version and the commit ([notifications and issues](reports.md#notifications-and-issues)).

### Several configs

Run a matrix with a unique `artifact-name` per job:

```yaml
jobs:
  simulate:
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        include:
          - { name: storage, config: examples/ledger/seedfall.json, seeds: 1-60 }
          - { name: upgrade, config: examples/upgrade/seedfall.json, seeds: 1-50 }
    steps:
      - uses: actions/checkout@v4
      - uses: kunalgoesbyken/seedfall@main
        with:
          config: ${{ matrix.config }}
          seeds: ${{ matrix.seeds }}
          artifact-name: seedfall-${{ matrix.name }}
```

This repository's own [`ci.yml`](../.github/workflows/ci.yml) sweeps several examples this way, and runs `verify` and `mutate` too.

## Machine-readable output

`seedfall run -json` sweeps every seed in the range and prints one JSON object per line, then a summary object. Seeds run in parallel but the lines come out in seed order, so the output is the same for any `-j`.

```sh
seedfall run -c seedfall.always.json -seeds 1-100 -json | jq -c 'select(.type == "seed" and .passed == false)'
```

```json
{"type":"seed","seed":1,"passed":false,"finished":false,"failure":{"class":"assert","node":"client"},"reason":"client#1: acknowledged write lost: k96=v96, server now answers \"NONE\"","virtual_seconds":2.8918212,"faults":3,"host_calls":6810,"determinism_hash":"53786fa3165d442b"}
```

| Field | Meaning |
|---|---|
| `type` | `seed` or `summary` |
| `seed`, `passed`, `finished` | The seed, whether it passed, and whether the workload finished before the time horizon |
| `failure` | `class`, plus `node` and `property` when known, the same key the triage report groups by |
| `reason` | The failure message |
| `virtual_seconds` | Simulated time the run covered |
| `faults` | Faults that happened during the run |
| `host_calls`, `determinism_hash` | How many host calls the run made, and the running hash over them ([determinism check](properties.md#determinism-check)). It covers only simulated values, so the same seed and guest binary should give the same hash on any machine, and a CI matrix can compare it across operating systems to check |

Before the seed lines comes one `{"type": "regression", ...}` line per [pinned regression](verify.md#pinned-regressions) and `-seeds-file` seed, with `source`, `seed` and `passed`, plus `failure`, `reason`, `classification` and `artifacts` when it fails again.

The summary has `passed`, `failed`, `unfinished`, `regressions_failed`, `unmet_properties` and `properties`, the same coverage table `seedfall_run` returns over MCP, with a `problem` on each property that was never reached or never true and a `margin` on each numeric property. With `faults.buggify` on it also has `buggify_sites`: each `sim.Buggify` site with `seeds_reached`, `seeds_enabled`, `seeds_fired`, `fired` and a `problem` of `never reached` or `never fired`, which does not change the exit code. The exit code is 1 if any seed or regression failed or any property is unmet. `-json` cannot be combined with `-report`.

## Time budgets

`seedfall run -timeout 10m` stops starting seeds after ten minutes of wall-clock time, so a CI job can use a wide range and take whatever fits:

```sh
seedfall run -seeds 1-1000000 -timeout 10m -report .seedfall/report.html
```

Seeds already running finish, so the sweep can run slightly past the limit, and [pinned regressions](verify.md#pinned-regressions) always run and count toward it. The run prints `stopped: time limit reached after N of M seeds`, the same text is `stopped` in the JSON summary, report and `seedfall_run` result, and the exit code is decided as usual: 0 if every seed that ran passed and every property was met. A property that needs more seeds than fit fails as `never reached`, as it would with a shorter range, so give the sweep enough time, or [pin](verify.md#pinned-regressions) a seed that reaches the rare path. Each seed stays exactly replayable, but which seeds ran depends on the machine's speed, so compare runs by seed and not by count.

## Rotating seeds outside GitHub

`seedfall run -seeds 1-200 -rotate N` sweeps the Nth range of the same width after `-seeds`, so any CI system can pass its build number and explore new seeds on each run while every failure stays replayable by seed. `-rotate 0` is the plain range. The run prints `rotation N: seeds A-B`, and the report's `seeds` is the rotated range. MCP's `seedfall_run` takes the same value as `rotate`.

## `go test`

```go
import "github.com/kunalgoesbyken/seedfall/seedfalltest"

func TestDurabilityUnderCrashes(t *testing.T) {
	seedfalltest.Sweep(t, "seedfall.json", "1-100")
}
```

`Sweep` first replays every [pinned regression](verify.md#pinned-regressions) for the config. A failure reports the seed, the reason, the trace tail, the classification, a replay command and the [failure artifacts](reports.md#failure-artifacts) folder. A `Sometimes` property that is never satisfied also fails the test.

Three more helpers turn known bugs into tests, each replaying for the config's full duration and expecting a pass:

```go
func TestPinnedRegressions(t *testing.T) {
	seedfalltest.Pinned(t, "seedfall.json")
}

func TestTornTailStaysFixed(t *testing.T) {
	seedfalltest.Replay(t, "seedfall.json", "testdata/torntail.faults.json")
}

func TestKnownSeeds(t *testing.T) {
	seedfalltest.Seeds(t, "seedfall.json", []uint64{1, 9})
}
```

`Pinned` runs each schedule in `seedfall-regressions/` as a subtest, and skips when there is none. `Replay` takes any schedule file with a `seed`, such as one written by `seedfall shrink`. `Seeds` runs each seed with its own faults as a subtest. `examples/kvlog/seedfall_test.go` uses all four.

## Speed

Runs are independent, so a sweep scales with cores: `seedfall run -j N` defaults to every CPU. Light servers take tens of milliseconds per seed; a 3-node hashicorp/raft cluster takes a few seconds. Each guest is compiled once per process and every seed reuses the compiled module, so per-seed cost is booting the nodes and running them. Compiled modules are also cached in `.seedfall/cache`, one entry per set of guest binaries, and only the 8 most recently used entries are kept, so the cache stays bounded however often you rebuild. Add that directory to your CI cache to skip compilation; the first build of a large guest such as nats-server takes about a minute.


<!-- docs/compat.md -->

# Storage engines that need mmap or flock

Some storage libraries, such as bbolt, pebble and badger, use operating system features called `mmap` and `flock` that seedfall's sandbox does not have. This page explains how seedfall swaps in stand-ins at build time so you can still test the real library. Read it when `seedfall init` or a build tells you a dependency will not compile.

Some storage libraries don't build or run for `GOOS=wasip1` because they call `mmap`, `flock` or other syscalls that WASI doesn't have. With `compat_overlay`, seedfall gives them `wasip1` versions at build time, either a shim for that exact library or the [generic `mmap` and `flock` shim](#the-generic-mmap-and-flock-shim), so you test the library you ship, unmodified:

```json
{ "compat_overlay": true }
```

| Library | Without `compat_overlay` | With it | Example |
|---|---|---|---|
| `go.etcd.io/bbolt` v1.5 | doesn't build: no `MaxMapSize` for `GOARCH=wasm`, then `bolt_unix.go` needs `syscall.Flock` and `unix.Mmap` | runs; 300 seeds pass, `NoSync` is caught, and it found a [missing directory fsync](findings/bbolt-create-dir-fsync.md) | [`examples/bboltkv`](../examples/bboltkv) |
| `github.com/cockroachdb/pebble/v2` v2.1 | doesn't build: `vfs` has no `wasip1` file system (its generic lock file refers to an undefined `defFS`), `rawalloc` has no `maxArrayLen` for `wasm`, and prometheus/procfs v0.10 calls `syscall.Statfs` | runs; needs `strict_dirs` (see below) | [`examples/pebblekv`](../examples/pebblekv) |
| `github.com/dgraph-io/badger/v4` v4.9 | builds, but `Open` fails: ristretto's `mmap` returns `ENOSYS` on `wasip1` | runs, with small memtable and value log sizes | [`examples/badgerkv`](../examples/badgerkv) |
| `github.com/blevesearch/mmap-go` v1.0.4 | doesn't build: its only mapping code is `//go:build` unix | runs through the generic shim; a writable mapping, `msync` and `mmap_early_writeback` work | [`examples/mmapwal`](../examples/mmapwal) |
| `github.com/edsrzf/mmap-go` v1.2.0 | builds, then `mmap` returns `ENOTSUP` from its `wasm` file | runs through the generic shim, which replaces the `wasm` file | swap the import in [`examples/mmapwal`](../examples/mmapwal) |
| `github.com/gofrs/flock` v0.13 | builds, then returns `ErrUnsupported` | runs through the generic shim, which replaces `flock_others.go` | [`examples/mmapwal`](../examples/mmapwal) |
| `golang.org/x/exp/mmap` | runs without a shim, reading the whole file | runs through the generic shim, with a real shared mapping | |
| `github.com/hashicorp/memberlist` v0.7 | doesn't build: `go-sockaddr` has no route lookup for `wasip1` | runs, with `net_overlay`; the shim answers as `go-sockaddr` does on other platforms without a route table, and a node binds and advertises its own IP | [`examples/memberlist`](../examples/memberlist) |

## What the shims do, and why crash results stay real

A shim only replaces calls that WASI can't make. Every write still goes to a file, and every durability point is still a real fsync on seedfall's simulated disk, so crashes, torn writes and fsync errors behave as they do for any other code.

- **Read-only `mmap`** (bbolt) becomes a heap copy of the file, re-read on every remap. bbolt writes pages with `pwrite` and syncs with `fdatasync`, never through the mapping. A `MAP_SHARED` mapping sees those writes immediately, so the shim copies each successful `pwrite` into the heap image too. The file stays the only source of truth after a crash.
- **Shared `mmap`** (badger through ristretto's `z` package, the generic shim) becomes a heap buffer that seedfall's disk knows about. A `pwrite` to the file updates every shared mapping of it, and pages written through a writable mapping reach the page cache at `msync`, at `munmap`, when the file is read with `pread` or mapped again, when it is fsynced, and when the process exits cleanly. `fsync` and `fdatasync` make every dirty page of the file durable. `MS_SYNC` flushes only the range it is given, then fsyncs the file; `MS_ASYNC` does not fsync. Truncating a file clears any part of a mapping past the new size. A `MAP_PRIVATE` mapping is a snapshot. Dirty pages that were never `msync`ed are lost on a crash unless [`mmap_early_writeback`](#early-writeback-of-mapped-pages) keeps them.
- **`flock` and file locks** become an in-process lock table. Each node is one process, and a crash starts a fresh process, so this matches what the lock guarantees.
- **`madvise`, `mlock` and disk-usage queries** are no-ops or report "unsupported". They are hints that don't change what is on disk.
- **Route lookups** (`go-sockaddr`) report that no route is known, as the library does on `js` and `plan9`. Only the automatic choice of a private IP depends on them.

## The generic mmap and flock shim

Most libraries put their mapping code in a file constrained to unix, and it calls `unix.Mmap`, `syscall.Mmap`, `unix.Flock` or `syscall.Flock`. You don't need a shim for each one. With `compat_overlay`, seedfall adds `Mmap`, `Munmap`, `Msync`, `Mlock`, `Munlock`, `Madvise` and `Flock` to `syscall` on `wasip1`, and a matching `golang.org/x/sys/unix`. It then finds files in your dependencies that are excluded on `wasip1`, would build on Linux, and call one of those four functions, and compiles them for `wasip1`. If such a file conflicts with a stub the library already builds on `wasip1`, like `gofrs/flock`'s `flock_others.go`, the stub is removed, but only when the file declares everything the stub declares. It does not touch your own module, or a file whose name ends in `_linux`, which normally assumes much more of Linux.

A file that uses anything else missing on `wasip1`, such as `unix.Fallocate`, fails to compile and the build error names the symbol. Run `seedfall init -n` to see which dependencies are covered: every `wasip1_blockers` entry has a `shim` line naming the shim or saying `none: needs a shim`, and `compat_shims` lists every dependency `compat_overlay` will touch, including ones like `gofrs/flock` that compile but fail at run time. `init` turns on `compat_overlay` when it finds any. `flock` is held by a table inside the node's process, keyed by inode: a lock is released by `LOCK_UN`, by closing the file descriptor that holds it, or when the process dies. A blocking `Flock` retries on a virtual 1 ms sleep; because `syscall` cannot import `time`, the overlay reaches `time.Sleep` through one `go:linkname`, the only one in seedfall.

## Early writeback of mapped pages

A kernel can write back any dirty page of a shared mapping at any time, so a program must not assume unsynced mapped data stayed volatile. With `"mmap_early_writeback": 0.5` in `faults`, each dirty page a crash finds in a writable shared mapping is treated as already written back with that probability, so it survives the crash where it would otherwise be lost. Each page is recorded as a `mmap_early_writeback` fault with the node and a `mapped page #N` count, so it replays, shrinks and edits like any other runtime disk fault. [`examples/mmapwal`](../examples/mmapwal) shows a checkpoint-and-checksum design that assumes unsynced pages can't reach the disk: it passes without the fault and fails with it.

Written-back pages are the page's content at the moment of the crash. A page written back earlier and dirtied again would have older content on a real kernel; that outcome is not generated.

## How it works

The shims are Go files embedded in seedfall, one directory per import path under [`engine/compat`](../engine/compat). At build time seedfall runs `go list -deps` for your nodes. For each dependency package with a shim, it copies the dependency's module into `.seedfall/compat`, adds the shim files, and removes every file the shim replaces. It builds with `-modfile` pointing at a copy of your `go.mod` that has a `replace` for each copied module. Your `go.mod`, `go.sum` and module cache are not touched. (`go build -overlay` can't be used here: Go refuses overlays for files in the module cache.)

Nothing is patched by text. A file is replaced when it declares something the shim declares, and then every top-level function, method, type, variable and constant it declares must be in the shim. If a new release adds a declaration to a replaced file, the build stops with an error that names it:

```
compat overlay: go.etcd.io/bbolt/bolt_unix.go declares fdatasync2, which the wasip1 shim does not provide; this version is not supported yet
```

Adding support for another library is adding a directory of `.go.txt` files. The generic shim adds `seedfall_mmap_wasip1.go` to `syscall` with the same `-overlay` mechanism as `net_overlay`, so the first build after a Go upgrade recompiles the standard library's `syscall` once.

## Pebble and directory fsyncs

Pebble records which manifest is current with an empty marker file. It creates the file and fsyncs the directory, but never fsyncs the empty file itself. On a real filesystem the directory fsync makes it durable. seedfall's default disk model drops every file that was never fsynced on a crash, so pebble would fail on its first restart with `database already exists and is not pristine`. Run pebble with `"strict_dirs": true`, where directory fsyncs decide which entries survive, as on a real filesystem.

## Not covered

- A mapping whose bytes are only read by another process. Each node is one process, so a mapping is only ever coherent with the node's own `pwrite` calls.
- Two mappings of one file see each other's writes only after one of the flushes above, because there is no page fault to hook.
- Mapping a file after its last name is unlinked: `Mmap` returns `EBADF`.
- `seedfall inspect` shows mapped writes only once they have reached the page cache, for the same reason.
- `mremap`, and code that needs more of `syscall` or `x/sys/unix` than the functions above. The build error names what is missing.
- Libraries seedfall doesn't have a verified shim for: `github.com/boltdb/bolt`, `github.com/hashicorp/raft-boltdb` before its `v2` (which uses bbolt), `github.com/dgraph-io/ristretto` before `v2`, and `github.com/cockroachdb/pebble` before `v2` (a `v2`-style shim made it build, but acknowledged writes were lost on restart, so it isn't shipped).
- Libraries that need cgo, such as RocksDB bindings or `mattn/go-sqlite3`.


<!-- docs/config.md -->

# Config files, profiles and seeded disks

One `seedfall.json` can hold many variations of your test: a base setup, named profiles, ready-made fault presets and one-off command-line overrides. This page also covers starting nodes from an existing disk and restarting them into a new version of your program. Use it when you want to test more than one scenario without copying files around.

One `seedfall.json` can hold every variant you test: a base config, named profiles that change a few fields, fault presets instead of hand-tuned rates, and one-off overrides from the command line. Nodes can start from an existing disk instead of an empty one, get files from the host, and restart into a new version of their program.

## Layers

A config is built from up to four layers, each merged over the one before:

1. the file named in `"extends"`, if any, itself built the same way
2. the file you pass with `-c`
3. the profile you pass with `-profile name`
4. every `-set path=value`, in order

Merging works the same way at every layer:

- objects merge key by key, so `{"faults": {"crash_on_io": 0.1}}` changes one rate and keeps the rest
- lists of named entries, such as `nodes` and `workloads`, merge by `name`: an entry with a known name merges into it, a new name is appended
- anything else, including `args` and other lists, replaces the value

Fields that no layer sets keep their defaults, as listed in the `seedfall://schema/config` MCP resource.

The merged config is checked once, before anything is built or run, and a config that fails the check does not load:

- a key that is not a config field is an error, in the file, in a profile and in `-set`, so a typo such as `crash_per_sc` cannot silently leave a fault off
- every probability (`crash_on_io`, `fsync_eio`, `write_eio`, `write_enospc`, `read_eio`, `read_corrupt`, `lost_write`, `misdirected_write`, `mmap_early_writeback`, `udp_loss` and `udp_dup`) is between 0 and 1, and every `_per_sec` rate is 0 or more
- every range (`latency`, `links[].latency`, `restart_after`, `partition_for`, `clog_for`, `clog_delay`, `slow_for`, `pause_for` and `disk_latency`) is `[min, max]` with `0 <= min <= max`
- `duration` and `watchdog` are positive, and `clock_jump_max` is 0 or more
- a node sets `pkg` or `wasm`, not both

### extends

```json
{
  "extends": "seedfall.json",
  "nodes": [{ "name": "server", "args": ["-sync", "always", "-repair"] }],
  "faults": { "bitrot_per_sec": 0.5 }
}
```

`extends` names another config file, relative to the file that extends it, and can chain. A file that extends itself, directly or through others, is an error. Paths inside the config, such as `pkg`, `wasm`, `files` and `disk`, are resolved from the directory of the file you pass with `-c`, so keep extended files in the same directory as the configs that use them. `examples/kvlog` keeps one file per variant this way, each a few lines over `seedfall.json`, because the getting started guide and CI name those files.

### profiles

```json
{
  "nodes": [{ "name": "counter", "pkg": "./counter" }],
  "workload": { "name": "client", "pkg": "./client" },
  "faults": { "buggify": true },
  "profiles": {
    "fixed": { "nodes": [{ "name": "counter", "args": ["-dedupe"] }] },
    "off": { "faults": "none" }
  }
}
```

```sh
seedfall run -c seedfall.json -profile fixed -seeds 1-20
```

A profile is a partial config merged over the file. Asking for a profile that does not exist fails and lists the ones that do. Every command that takes `-c` takes `-profile`, and so do the MCP tools (`"profile": "fixed"`). `seedfall init` writes three starter profiles: `strict`, `resilient` and `everything`.

A profile is part of the config's identity everywhere seedfall prints or saves it:

- replay and shrink commands carry it: `replay: seedfall replay -c seedfall.json -profile fixed -seed 2`
- failure artifacts go to `.seedfall/failures/seedfall.fixed-seed-2/`, the same folder a separate `seedfall.fixed.json` would use
- `seedfall pin` records the profile and `-set` overrides in the pinned file (`"profile": "fixed"`), and a pinned schedule is replayed only by runs with the same config file, profile and overrides
- `-set` overrides add a short hash of the overrides to artifact folder and pinned file names, `seedfall.fixed.set-1a2b3c4d-seed-2`, so a run with overrides never replaces the files of a run without them
- reports, proofs and `seedfall hook` print the full config reference

`seedfall hook` reads the profile from `$SEEDFALL_HOOK_PROFILE` ([agents.md](agents.md#the-seedfall-hook-command)).

### -set

```sh
seedfall run -set faults.crash_per_sec=2 -set duration=10s -seeds 1-50
seedfall run -set 'nodes.server.args=["-sync","always"]' -seeds 1-50
seedfall replay -seed 7 -set faults=resilient
```

`-set path=value` overrides one value after every other layer, and can repeat. The path is a dot-separated list of keys. Inside a list, a part is either the `name` of an entry or its index, so `nodes.server.env.MODE` and `nodes.0.env.MODE` both work. Missing objects along the path are created. The value is read as JSON when it parses as JSON (`2`, `true`, `["-x"]`, `{}`) and as a plain string otherwise (`10s`, `resilient`). To set a string that looks like JSON, quote it: `-set 'nodes.server.env.PORT="7000"'`. When the JSON reading does not fit the field, such as the number in `-set nodes.server.env.PORT=7000` for an `env` value, which must be a string, the value is used as a plain string instead.

## Fault presets

```json
{ "faults": "resilient" }
{ "faults": { "preset": "high_availability", "crash_per_sec": 2, "clog_per_sec": 0 } }
```

A preset fills in a documented fault level. Fields set next to it override it, and the string form is shorthand for `{"preset": name}`. Each level adds to the one before:

| Preset | Adds |
|---|---|
| `none` | no faults |
| `durability` | `crash_per_sec` 0.5, `crash_on_io` 0.002, `torn_writes`, `reorder_writes`, `strict_dirs`, `mmap_early_writeback` 0.1 |
| `resilient` | `pause_per_sec` 0.1, `slow_per_sec` 0.1, `reset_per_sec` 0.1, `clock_jump_per_sec` 0.05 |
| `high_availability` | `partition_per_sec` 0.2, `clog_per_sec` 0.2, `swizzle_per_sec` 0.05, `udp_loss` 0.01, `udp_dup` 0.01 |
| `everything` | `fsync_eio` 0.01, `write_eio`, `write_enospc`, `read_eio`, `read_corrupt`, `lost_write` and `misdirected_write` 0.005 each, `corrupt_on_crash`, `bitrot_per_sec` 0.05, `buggify` |

Durations, topologies and clog modes keep their defaults, and every rate is per node per second, per disk operation for the I/O faults, or per datagram for `udp_loss` and `udp_dup`, as in [faults](faults.md). The levels are seedfall's own, named after the fault tolerance levels Antithesis offers, not a copy of them. `high_availability` and `everything` include partitions, clogs and swizzles, which need at least two nodes that take faults, workload included. `everything` includes faults such as corrupted reads that only a system with checksums can survive.

A layer that names a preset starts its faults from that preset, and fault fields from earlier layers are dropped, so a profile with `"faults": "none"` turns every fault off even when the base config sets rates. A layer without a preset merges its fault fields as usual. On the command line, `-set faults=none` replaces the faults the same way, while `-set faults.preset=none` changes only the preset and keeps the fault fields set so far, which still override it. The preset in effect shows up as `faults.preset` in the triage report JSON and in the HTML report's fault table.

## Seeded disks and files

Every node starts with an empty disk unless its entry says otherwise:

```json
{
  "name": "ledger",
  "pkg": "./v1",
  "disk": "image",
  "files": { "etc/ledger.conf": "fixtures/atomic.conf" }
}
```

- `disk` names a host directory. Its files, directories and symlinks are copied onto the node's disk, the directory itself becoming `/`.
- `files` maps a path on the node's disk to a host file. A file listed here replaces the same path from `disk`.

Both are read from the host once, when the config loads, and copied into memory, so a run never touches the host disk and stays deterministic. The copied files are durable and synced before the node first starts, as if an earlier life had written and fsynced them: a crash never loses them, and `seedfall inspect` shows them as durable from t=0. Directories leading to them are durable too, even with `strict_dirs`. Symlinks and other special files in `disk` are rejected. The trace opens with a line per seeded node, `ledger's disk starts with 2 durable files, 86 bytes`, and the config hash in failure artifacts covers the bytes of every seeded file, so changing a fixture changes `config_sha256`.

`seedfall inspect -out dir` exports each node's durable disk as `dir/<node>/`, in exactly the layout `disk` reads, so a failing state can become the starting point of new runs:

```sh
seedfall inspect -seed 21 -out state
seedfall run -set nodes.ledger.disk=state/ledger -seeds 1-20
```

## Upgrades

```json
{ "name": "ledger", "pkg": "./v1", "upgrade_to": "./v2" }
```

`upgrade_to` names a second Go package for the node. seedfall builds both, the node starts as `pkg`, and every start from its first restart on runs `upgrade_to` instead, over whatever the old version left on disk. Restarts come from crash faults, `crash_on_io` and `supervise`. The trace marks the switch with `start ledger#2, upgraded to ./v2`. `upgrade_to` takes a package, not a prebuilt `wasm` file, and `seedfall mutate -app` mutates only `pkg`.

Together with `disk`, this tests the upgrade path FoundationDB's restart tests cover: real old data, a crash, and the new version's recovery code. [examples/upgrade](../examples/upgrade) seeds a v1 ledger, upgrades it to v2 on the first crash, and catches an in-place migration that a crash leaves half done.


<!-- docs/explore.md -->

# Feedback-guided exploration

A plain sweep tries seeds one after another, which is slow for a bug that needs two rare things to happen in the same run. `seedfall explore` keeps the runs that reached something new and builds on them. Use it when ordinary sweeps pass but you suspect a deeper bug.

A plain sweep draws a fresh random seed every time. A failure that needs two rare things to happen in the same run, each with odds of one in a thousand, needs on the order of a million seeds. `seedfall explore` looks for that kind of failure with feedback: it keeps the runs that reached something new, and spends further runs going deeper from there instead of starting over.

```sh
seedfall explore -c seedfall.json -seeds 1-8 -rounds 30 -batch 8
```

```
round 1   runs 8     +4 signals (4)  +625 functions (625)  corpus 4  failures 0  551ms
    new: property "level 1 reached" = true
    new: property "level 2 reached" = true
    new: property "level 3 reached" = true
    new: property "level 4 reached" = true
round 2   runs 16    +0 signals (4)  +0 functions (625)  corpus 4  failures 0  935ms
round 3   runs 24    +1 signals (5)  +0 functions (625)  corpus 5  failures 0  1.289s
    new: property "level 5 reached" = true
round 4   runs 32    +1 signals (6)  +2 functions (627)  corpus 5  failures 1  1.628s
    new: property "level 6 reached" = true

stopped: failure found
FAIL seed 6 at t=923.003008ms (924 scheduler steps, 56ms real)
  client#1: the vault opened after 6 consecutive lucky draws
```

That is [examples/explore](../examples/explore): 20 plain seeds never reach level 6 (and the sweep passes), while exploration finds it in 32 runs. A failure is reported the usual way, and the artifact is an ordinary schedule file.

## How it works

Round 1 runs the `-seeds` range and any entries left in the corpus by earlier runs. Every run reports **signals**:

| Signal | Meaning |
|---|---|
| `property "msg" = true` | a property fired with this outcome, optionally `during crash,partition`: the fault kinds with an open window when it first fired |
| `fault crash server` | a fault of this kind applied to this node, including a `buggify` firing with its site |
| function | a function reached for the first time, per node, counting every function in the binary (the Go runtime included, so some of them are the runtime reacting to the run). This is coarse, function-entry coverage, not basic blocks |

A run that adds a signal or a function joins the corpus as a schedule: its seed, recorded faults and branches. Every further round draws `-batch` children, one at a time from the exploration's own seed:

- pick a corpus entry, more often when it holds rare signals
- with odds 3 of 5, branch at the moment just after one of its signals fired, more often a rare one, and re-randomize the future. This is the checkpoint step: a run that reached the rare state continues from there, so a rare state followed by another rare event no longer needs both to happen in the same attempt
- with odds 1 of 5, re-key one stream (`sched`, `net`, `disk`, `disklatency` or `random`) from a random moment
- otherwise add, remove or shift a fault

Branching uses the machinery [`seedfall cause`](cause.md) already had, with branches now recorded in the run and chained, so a child of a child branches again. A branch at virtual time *T* re-keys the streams at the first scheduler step at or after *T*. Nothing is snapshotted: replay is exact, so reaching *T* again means re-running the seed.

The exploration stops at the first of these:

| Flag | Stops after |
|---|---|
| a failure | the first failing run, unless `-keep-going` |
| `-rounds N` | N rounds |
| `-budget 10m` | that much wall-clock time, checked between rounds |
| `-until-novelty N` (default 8) | N rounds in a row that added nothing |

## Determinism

The choices come from `-explore-seed` (default 1) and every result is merged in a fixed order, so a given corpus and flags produce the same rounds at any `-j` as long as a `-budget` does not cut them short: a `-budget` depends on the machine's speed, so use `-rounds` for an exploration that must repeat exactly in CI.

Every failure is a seed plus a schedule file, so nothing is lost for the rest of the tools:

```sh
seedfall replay  -seed 6 -faults .seedfall/failures/seedfall-seed-6-explore-504fa1fb9883/faults.json
seedfall shrink  -seed 6 -faults .seedfall/failures/seedfall-seed-6-explore-504fa1fb9883/faults.json
seedfall inspect -seed 6 -faults .seedfall/failures/seedfall-seed-6-explore-504fa1fb9883/faults.json
seedfall pin     -seed 6 -faults .seedfall/failures/seedfall-seed-6-explore-504fa1fb9883/faults.json
```

Those commands and the report's replay and shrink lines use the file because the seed alone would not reproduce the run. See [the schedule format](faults.md#editing-a-schedule).

## Corpus

Corpus entries are written to `.seedfall/corpus/<config>/<seed>-<id>.json` and replayed in the first round of the next `seedfall explore`, so a search keeps building where it left off. Pass `-corpus dir` to keep them somewhere committed, like Go fuzz testdata. An entry whose faults no longer fit the config (a node was renamed, for example) or that cannot be read is skipped and counted as stale. Delete the directory to start over.

## What re-keying does not reach

Re-keying a run changes the random streams seedfall owns: the scheduler, the network, the disk, I/O faults, buggify firings and what `random_get` returns to the guest, which reaches `crypto/rand` and `sim.Random`. Go's `math/rand` and `math/rand/v2` top-level functions are seeded once, when the process starts, and keep their own sequence, so a branch does not change what they return in a process that is already running. Workload randomness that should re-roll on a branch has to come from `crypto/rand` or `sim.Random`.

## Stopping a plain sweep

`seedfall run -until-novelty N` stops a sweep once N batches of seeds in a row added nothing, so a wide range does not need to be run in full once coverage has flattened out. `-batch` sets the seeds per batch (default 20) and the verdict for each seed is the same as without the flag; only how many seeds run changes, and the point a run stops does not depend on `-j`:

```sh
seedfall run -seeds 1-5000 -until-novelty 5 -batch 50
```

```
round  runs  new signals  signals  new functions  functions
  1     4     3            3        624            624
  2     8     1            4        1              625
  3     12    0            4        0              625
stopped: seed range finished
```

The same growth table is in the JSON output (`exploration`), `seedfall_run` and the **Exploration** section of the [triage report](reports.md).

## Throughput

Every sweep reports runs per second and virtual time simulated per wall second, the kind of efficiency numbers a deterministic simulation lives on. They are in the last lines of `seedfall run`, the JSON summary as `seeds_per_second` and `virtual_seconds_per_wall_second`, and the report header.

Numbers from one Windows 11 machine, `-j 2`, seedfall built with this repository's Go toolchain:

| Example | Seeds | Time | Note |
|---|---|---|---|
| `examples/kvlog` `seedfall.fixed.json` | 20 | 1.84 s to 2.12 s, 39 to 45x virtual time | without feedback instrumentation |
| `examples/kvlog` `seedfall.fixed.json` | 20 | 1.90 s to 2.13 s | with `-until-novelty`, which adds the function bitmap: no measurable slowdown |
| `examples/natscluster` | 3 | 15.2 s at `-j 1` | a 3-node cluster, about 5 s a seed |

A CPU profile of kvlog (10 seeds, `-j 1`, taken with a one-off build because `-cpuprofile` is refused on Windows) spent 55% of its samples in the guest's compiled code, 22% in wazero's call path to and from the guest, and 3.7% instantiating modules; the per-step watchdog timer did not appear in the top of the profile.

`seedfall run -cpuprofile cpu.pprof` is meant to write a Go pprof profile on platforms where Go's profiler can unwind through wazero's compiled code; it has not been verified on Linux or macOS. seedfall refuses it on Windows: the Go runtime crashes unwinding those frames, consistently with parallel guests and intermittently at one guest, reported with a `fatal error` from `runtime.sigprof`.

There is no snapshotting. `seedfall cause` and every branched run re-execute the seed from the start, in parallel on `-j` workers.

## From an agent

The MCP tool `seedfall_explore` takes the same options and returns the rounds, the stop reason and the failure. `seedfall_run` accepts `until_novelty` and `batch`. See [agents.md](agents.md).


<!-- docs/faq.md -->

# FAQ

Short answers to the questions people ask most, with links to the pages that go into detail. Start with the first section if you are comparing seedfall to something you already know.

Two words come up a lot. A **seed** is a number that decides everything random in one run, so the same seed always gives the same run. A **fault** is something that goes wrong on purpose, such as a crash or a lost message.

## How is seedfall different from Antithesis?

Antithesis runs any kind of program, in any language, inside a special virtual machine that can replay everything exactly. seedfall only runs Go programs, inside one process, with a simulated disk and network. In exchange, seedfall runs on your laptop and in CI with no service and no account, and it is open source.

If your program already uses the Antithesis Go SDK (a library for writing checks in your code), it runs under seedfall unchanged. The SDK's `assert.Always`, `Sometimes`, `Reachable`, the numeric and grouped variants, `lifecycle.SetupComplete` and `lifecycle.SendEvent` become seedfall properties (checks), setup and trace events. `seedfall cause` uses the same idea as Antithesis's multiverse debugging: it looks at how likely the failure was from each moment of the run. Instead of VM snapshots it replays exactly from the start. See [Antithesis compatibility](antithesis.md).

## How is it different from gosim?

[gosim](https://github.com/jellevandenhooff/gosim) is also deterministic simulation testing for Go, with simulated machines, a network, a file system and crashes. Deterministic means the same input always gives the same run. gosim rewrites your program and its dependencies so they run on its own simulated runtime, at the level of system calls.

seedfall does not rewrite code. It compiles your program with the normal Go toolchain for `GOOS=wasip1` (a WebAssembly target, explained [below](#why-wasip1)) and controls everything random at that boundary: time, randomness and waiting, plus its own file system and network calls. Each node is a separate WebAssembly instance, so a crash kills the whole process and a restart boots a fresh one over the disk that survived. Check gosim's own documentation for its current features instead of relying on this page.

## Why not `testing/synctest`?

`testing/synctest` is part of Go's standard library. It runs a test's goroutines (Go's lightweight threads) in a "bubble" with a fake clock. The clock jumps ahead whenever every goroutine in the bubble is waiting. This makes time-based unit tests fast and repeatable inside one `go test` process.

It does not simulate a disk or a network, crash or restart processes, inject faults, or record a run you can replay and shrink. The order in which goroutines interleave still comes from the real scheduler.

seedfall is for whole services: several nodes as separate processes on one virtual clock, with crashes, torn writes (a write that a crash leaves half saved), fsync errors (fsync is the call that forces data onto the disk), partitions (nodes that cannot reach each other) and clock faults. Any failure replays from its seed. The two fit together: use `synctest` for the timing logic of one component, and seedfall for what your service does when the machine fails under it.

## Does seedfall replace `go test -race`?

No. On `wasip1` the Go runtime runs one thing at a time, so goroutines never really run in parallel. The overlapping memory accesses that the race detector looks for never happen there. seedfall's `random`, `pct` and `calls` preemption strategies do find ordering bugs, such as a check-then-act race between goroutines, but they do not detect data races the way `-race` does. Keep running `-race` on your unit tests. seedfall's own CI does.

## How does it compare with Jepsen?

Jepsen tests real deployments of a database, on real or virtual machines, in any language. It injects faults into the real operating system and network, then checks the recorded history for consistency problems. It finds bugs in the system as shipped, but a failing run cannot be replayed exactly.

seedfall borrows from Jepsen. Its network partition shapes follow Jepsen's "nemeses". It records histories in Jepsen's invoke and completion shape. It checks `sim.Txn` histories for the same Elle anomalies (`G0`, `G1a`, `G1b`, `G1c`, `G-single`, `G2`, which are named kinds of transaction inconsistency).

The difference is that every seedfall run is deterministic. A failure comes with a seed, an exact fault schedule and a trace, and `seedfall shrink` cuts the schedule down to the faults that matter. The cost is that seedfall tests a Go program on a simulated disk and network, not the real kernel and the real binary. The checker for **linearizability** (the rule that concurrent operations must look as if they happened one at a time, in an order that fits real time) is described in [properties](properties.md#linearizability).

## Why `wasip1`?

`wasip1` is a Go build target: `GOOS=wasip1` compiles your program to WebAssembly that talks to the outside world through WASI, a small, standard system interface. For seedfall this has a useful property. The Go runtime on `wasip1` is single-threaded and has no asynchronous preemption, and a program reaches the outside world for time, randomness and waiting through only three WASI calls: `clock_time_get`, `random_get` and `poll_oneoff`.

seedfall implements those three calls itself. So the seed decides map iteration order, `select` choices, `math/rand`, crypto randomness and every clock read. File and network calls are seedfall's too. The result is exact replay with the standard toolchain: no forked Go runtime, no `linkname` tricks and no source rewriting outside the opt-in overlays, so new Go releases keep working. Each node runs as its own [wazero](https://wazero.io) instance, so a crash is a real process death. See [how it works](how-it-works.md).

## Does seedfall change my code?

Not by default. Two opt-in settings change how things are built, never your files:

- `net_overlay` adds `wasip1` files to the standard library's `net` package at build time, so unmodified code can use the simulated network.
- `compat_overlay` swaps a dependency's `mmap` and `flock` files for stand-ins, in a copy under `.seedfall/compat`.

Neither touches your source, `go.mod`, `go.sum` or module cache. Instead of `net_overlay` you can call `sim.Listen` and `sim.Dial`, which fall back to `net.Listen` and `net.Dial` outside the simulator. See [networking](networking.md) and [compat](compat.md).

## What can't seedfall test?

The README has a short version of this list under [When it's not a fit](../README.md#when-its-not-a-fit). The full list:

- **Code that does not build for `wasip1`.** There is no cgo (Go code that calls C). Dependencies that need `mmap` or `flock` work through `compat_overlay`, but files named `_linux.go` and code that uses other unix calls still need a hand-written stand-in. Libraries that need cgo, such as RocksDB bindings or `mattn/go-sqlite3`, cannot run.
- **Time-based preemption.** seedfall counts function calls instead of time. A goroutine that spins is interrupted after about four million calls. A loop that makes no function call is interrupted only with `preempt.loops`. Even then the runtime switches goroutines only when a function is entered, so a call-free loop keeps the node's other goroutines from running until it makes a call.
- **Every possible ordering of goroutines.** Inside a node, the ordering comes from the Go scheduler under a seeded random source. The preemption strategies sample orderings rather than list all of them. `pct`'s probability bound is a guide, not a guarantee. None of them detects data races.
- **Every file system.** `fs_model` covers ext4 `data=ordered`, an aggressive independent-pages model, and ext2 or btrfs directory reordering. XFS, `data=journal` and `nodelalloc` have no model of their own. A single directory operation is always atomic, and `Chmod` is not modelled.
- **Some network features.** UDP multicast is not simulated, and `WriteMsgUDP` with out-of-band data returns `ENOTSUP` ([networking](networking.md#udp)).
- **Memory shared between processes.** A memory mapping is consistent only with its own node's writes ([compat](compat.md#not-covered)).

Speed is a limit too. Idle virtual time is free, but the CPU time your code uses and the time to start each node are real. Short runs of large programs are dominated by start-up cost ([how it works](how-it-works.md#speed)).

## Which platforms does it run on?

Linux, macOS and Windows. seedfall's tests run on all three in CI.

## How many seeds should I run?

Enough that a failure at the rate you care about would have shown up. `seedfall verify` works this out for 95% confidence. With no known failure rate it asks for 299 seeds. A sweep's utilization section tells you whether more seeds are likely to find anything new ([verify](verify.md), [reports](reports.md#utilization)). For bugs that need two rare events in one run, `seedfall explore` is better than more plain seeds ([explore](explore.md)).

## A failure looks wrong. Is it a seedfall bug?

First check the failure's classification. Failures marked `nondeterministic` or `timeout` are explained in [troubleshooting](troubleshooting.md#failures-that-are-not-your-systems-bug). If seedfall produced an outcome that a real machine could not, open a false positive issue and include the replay command and the fault schedule.


<!-- docs/faults.md -->

# Configuration and faults

This is the reference for `seedfall.json`: every field, and every fault seedfall can inject, such as crashes, partly written disk writes, lost network messages and clock jumps. Use it to look up what a setting does or to design the failures you want to test. If you are new, start with [getting-started.md](getting-started.md).

A world is described in a JSON file, `seedfall.json` by default. Paths inside it are relative to the file. One file can extend another, hold named profiles selected with `-profile`, take `-set path=value` overrides and start from a fault preset such as `"faults": "resilient"`; see [config.md](config.md).

```json
{
  "nodes": [
    { "name": "n1", "pkg": "./node", "args": ["-id", "n1"] },
    { "name": "n2", "pkg": "./node", "args": ["-id", "n2"] }
  ],
  "workload": { "name": "client", "pkg": "./client" },
  "duration": "60s",
  "latency": ["1ms", "5ms"],
  "supervise": true,
  "faults": {
    "crash_per_sec": 0.5,
    "restart_after": ["10ms", "500ms"],
    "partition_per_sec": 0.2,
    "partition_for": ["50ms", "1s"],
    "torn_writes": true,
    "crash_on_io": 0.005,
    "fsync_eio": 0.01,
    "strict_dirs": true,
    "clock_skew": "200ms",
    "pause_per_sec": 0.2,
    "clock_jump_per_sec": 0.05,
    "buggify": true,
    "swarm": true
  }
}
```

## World

| Field | Default | Meaning |
|---|---|---|
| `nodes[]` | | Crashable nodes. Each has a `name`, then either `pkg` (a Go package, built for wasip1 automatically) or `wasm` (a prebuilt module), plus optional `args`, `env`, `faults`, `disk`, `files` and `upgrade_to`. `disk` and `files` copy a host directory and host files onto the node's disk before it first starts, durable and synced, and `upgrade_to` names a package the node runs from its first restart on ([seeded disks](config.md#seeded-disks-and-files), [upgrades](config.md#upgrades)). `"faults": false` keeps every fault away from the node: it is never crashed, paused, slowed or skewed, its disk never fails, and partitions and clogs never cut its links, like Antithesis's fault exclusions. `sim.Buggify` sites in its own code still fire |
| `workload` | | The checker. Same fields as a node. It takes none of the per-node faults (crashes, pauses, clock skew and jumps, slowdowns, resets, disk faults) unless `faults.include_workload` or its own `"faults": true` says so; partitions and clogs reach it like any node. The run passes when it exits 0 |
| `workloads[]` | | Several workloads instead of, or next to, `workload`. Each is a client like `workload`, and the run passes when every one of them has exited 0. See [Faults on the workload](#faults-on-the-workload) |
| `finally` | | A check that starts only after every workload has exited 0, with all faults stopped and the network healed. Same fields as a node; it never takes faults. The run passes when it exits 0, and its properties count like any other. See [properties.md](properties.md#liveness-recovery-and-finally-checks) |
| `liveness.within` | `0s` (off) | Liveness mode. At `duration` the faults stop, partitions, clogs, slowdowns and pauses end, and crashed nodes restart at once; then the workload (and the `finally` check, if any) must finish within `within`, or the run fails with class `liveness` |
| `duration` | `30s` | Virtual-time horizon, and with `liveness` the end of the fault period. A run that reaches it without failing counts as passed and is reported as "hit the time horizon"; with `liveness`, reaching it starts the recovery phase instead |
| `latency` | `["1ms", "10ms"]` | Per-chunk network delay range |
| `links[]` | | Per-link latency overrides, each `{"from": "n1", "to": "n2", "latency": ["20ms", "80ms"]}`. Links are one-way; leave out `from` or `to` to match any node, so `{"to": "n3", ...}` slows everything sent to `n3`. The first matching entry wins. See [Network faults](#network-faults) |
| `faults_after_setup` | `false` | Suppress all faults until a node calls `sim.SetupComplete()` |
| `supervise` | `false` | Restart a node that exits with an error, after `restart_after`. Go panics (exit code 2) still fail the run, and so does a workload that exits with an error, even under `include_workload` |
| `net_overlay` | `false` | Route plain `net.Listen` / `net.Dial` through the simulated network. See [networking.md](networking.md) |
| `compat_overlay` | `false` | Build dependencies that need `mmap` or `flock` with `wasip1` shims: a shim for bbolt, pebble or badger, or the generic shim for any dependency that calls `Mmap` or `Flock`. See [compat.md](compat.md) |
| `watchdog` | `30s` | Real-time limit for one node to run without yielding. Catches busy loops and livelocks. With `preempt.loops`, a busy loop parks like any other node and a run that never finishes fails on `liveness` instead, which does not depend on the host |
| `preempt.strategy` | `none` | When the running goroutine is preempted inside a node: `none` only at the end of a 4,194,304-call time slice, `random` after a seeded 1 to 4,096 counted calls, `pct` at `depth` - 1 seeded change points per node, each recorded as a `preempt` fault, `calls` every `preempt.calls` counted calls. See [how-it-works.md](how-it-works.md#strategies) |
| `preempt.interleave` | `false` | Shorthand for `"strategy": "random"`. While it is `true`, `strategy` can only be `random` or `none`, and `none` still means `random`, so a profile that switches strategy sets `interleave` to `false` |
| `preempt.depth` | `3` | `pct`: the bug depth d to look for, giving d - 1 change points per node |
| `preempt.steps` | `1048576` | `pct`: the change points are drawn over each node's first `steps` counted calls. The trace's last `pct:` line shows how many each node ran |
| `preempt.calls` | `4096` | `calls`: counted calls between preemptions, at most 4,194,304 |
| `preempt.loops` | `false` | Count loop iterations as well as function calls, so a loop without calls is preempted, uses virtual time and lets other nodes run. Costs guest CPU. See [how-it-works.md](how-it-works.md#loops) |

Every node sees the environment variables `SEEDFALL=1` and `SEEDFALL_NODE=<name>`, so `sim.Enabled()` and `sim.Node()` work.

## Faults

All faults come from the seed. Faults that depend on what the program does, such as which disk operation a crash lands on, are recorded when they happen so that shrinking and replay are exact.

| Field | Default | Meaning |
|---|---|---|
| `preset` | | Start from a built-in fault level, `none`, `durability`, `resilient`, `high_availability` or `everything`, each adding to the one before; fields set next to it override it, and `"faults": "resilient"` is shorthand for `{"preset": "resilient"}`. The values each level sets are in [config.md](config.md#fault-presets) |
| `crash_per_sec` | `0` | Rate of crashes per node, at random points in time |
| `restart_after` | `["10ms", "1s"]` | Downtime after a crash, and the delay before a supervised restart |
| `partition_per_sec` | `0` | Rate of network partitions. A partition splits all nodes, workload included, into groups that cannot reach each other. A new partition replaces the previous one |
| `partition_for` | `["50ms", "2s"]` | Partition duration. TCP traffic across the cut is held and delivered after the heal; UDP datagrams are dropped |
| `partition_topologies` | `["half"]` | Shapes a partition can take; each partition picks one at random. `half` (two random sides), `one` (isolate one node), `majority` (a random majority against the rest), `majorities_ring` (every node sees a majority, and no two nodes see the same one) and `random_groups` (two or more random groups). See [Network faults](#network-faults) |
| `clog_per_sec` | `0` | Rate of clogs. A clog hits one direction of one link, or everything a node sends, receives, or both, and lasts `clog_for` |
| `clog_for` | `["100ms", "2s"]` | Clog duration, also the length of a swizzle |
| `clog_modes` | `["stop", "slow", "jam"]` | Modes a clog can take; each clog picks one at random. `stop` refuses new connections and holds traffic, `jam` holds connections and traffic without any error, `slow` adds `clog_delay` to every message. `stop` and `jam` drop UDP datagrams instead of holding them |
| `clog_delay` | `["10ms", "200ms"]` | Extra latency per message of a `slow` clog, drawn once per clog |
| `swizzle_per_sec` | `0` | Rate of swizzles (FoundationDB's swizzle-clogging): a random subset of nodes is clogged one node at a time, then unclogged in a different random order |
| `reset_per_sec` | `0` | Rate of connection resets per node. Every open connection of the node is reset at once, as if a middlebox dropped them; the process keeps running and both ends see `ECONNRESET` |
| `udp_loss` | `0` | Probability that a UDP datagram is dropped. Each loss is recorded as a `udp_drop` fault with the sender and its datagram number. See [UDP datagrams](#udp-datagrams) |
| `udp_dup` | `0` | Probability that a UDP datagram is delivered twice, the copies with independent latencies. Each one is recorded as a `udp_dup` fault |
| `slow_per_sec` | `0` | Rate of slowdowns per node: a gray failure where the node stays up but everything it does takes longer |
| `slow_for` | `["500ms", "5s"]` | Slowdown duration |
| `slow_factor` | `10` | Largest slowdown. Each slowdown picks a factor between 1 and this value |
| `torn_writes` | `false` | A crash keeps a random in-order prefix of unsynced writes, possibly ending in a partial write |
| `reorder_writes` | `false` | A crash writes dirty pages back out of order, as the kernel does between fsyncs, within the limits of `fs_model`. This finds a commit record or header that reaches the disk before the data it points to. Combine with `torn_writes` to also tear the last write kept in each page. See [File system models](#file-system-models) |
| `fs_model` | `ext4_ordered` | Which crash states `reorder_writes` may produce: `ext4_ordered`, `page_independent` or `dir_reorder`, which needs `strict_dirs`. Setting it without `reorder_writes` is an error. See [File system models](#file-system-models) |
| `crash_on_io` | `0` | Probability that a node crashes *during* each disk operation. This is how you hit the window between a write and its fsync |
| `fsync_eio` | `0` | Probability that a file fsync fails with `EIO`. The unsynced writes stay readable but are dropped from durable storage, and the next fsync succeeds (Linux "fsyncgate" semantics) |
| `disk_bytes` | `0` | Size of each node's disk in bytes; `0` means unlimited. A write that does not fit writes what fits and returns the short count, and the next write fails with `ENOSPC`. See [Disk faults](#disk-faults) |
| `write_eio` | `0` | Probability that a file write fails with `EIO` and writes nothing |
| `write_enospc` | `0` | Probability that a file write fails with `ENOSPC` and writes nothing, however much space is free, as with a quota or a thin-provisioned volume |
| `read_eio` | `0` | Probability that a file read fails with `EIO` |
| `read_corrupt` | `0` | Probability that a file read returns one flipped bit. The disk holds the right bytes, so reading again returns them |
| `lost_write` | `0` | Probability that a file fsync succeeds but one 4 KiB page it should have written keeps its old content on disk. The program keeps reading the new content until a crash |
| `misdirected_write` | `0` | Probability that a file fsync succeeds but one page lands at another page offset of the same file, overwriting what was there, while the intended page keeps its old content |
| `corrupt_on_crash` | `false` | Each crash flips one bit in every file whose pending writes cover bytes that are on disk after the crash, somewhere in those bytes, as a sector half-written when the power failed |
| `bitrot_per_sec` | `0` | Rate of bit rot per node: one bit of durable data, in a random file at a random offset, flips |
| `disk_latency` | `["0s", "0s"]` | Extra time each fsync takes, drawn per fsync. Slow nodes stretch it |
| `mmap_early_writeback` | `0` | Probability that a dirty page of a writable shared mapping is already written back when a node crashes. Needs a shared mapping through `compat_overlay`. Recorded as a `mmap_early_writeback` fault. See [compat.md](compat.md#early-writeback-of-mapped-pages) |
| `strict_dirs` | `false` | Directory entries survive a crash only after the parent directory is fsynced (strict POSIX) |
| `clock_skew` | `0` | Each node's wall clock is offset by a seeded amount in `[-skew, +skew]`. The monotonic clock is untouched, so timers and `time.Since` are unaffected |
| `pause_per_sec` | `0` | Rate of process pauses per node. A paused node stops running, like a long GC pause or a stalled VM, then resumes without crashing. Its connections stay open and messages queue up |
| `pause_for` | `["100ms", "3s"]` | Pause duration |
| `clock_jump_per_sec` | `0` | Rate of wall-clock jumps per node. Each jump moves the node's wall clock forward or back by up to `clock_jump_max`; the monotonic clock is untouched |
| `clock_jump_max` | `10s` | Largest clock jump in either direction |
| `buggify` | `false` | Let `sim.Buggify` and `sim.BuggifyWithProb` sites in your code fire. Each site is enabled in a quarter of runs and then fires at its own rate; every firing is recorded as a `buggify` fault with its node, site and hit number. See [buggify.md](buggify.md) |
| `include_workload` | `false` | Give the workloads the per-node faults too: crashes, pauses, clock skew and jumps, slowdowns, connection resets and disk faults. A crashed workload restarts as a fresh process after `restart_after`, with the same name and its disk as the crash left it. See [Faults on the workload](#faults-on-the-workload) |
| `swarm` | `false` | Swarm testing. Each seed turns every fault type on or off and rescales its rate between 0 and 2× the configured value, so faults that hide each other get explored separately |

## Faults on the workload

By default the workload is the one process that never crashes, so a client's own retry, idempotency and session logic is never tested: what happens when a client restarts halfway through a write and sends it again? Set `"include_workload": true` to change that:

```json
"workload": { "name": "client", "pkg": "./client" },
"faults": { "include_workload": true, "crash_per_sec": 0.3, "pause_per_sec": 0.3 }
```

- A crashed workload restarts as a fresh process after `restart_after`, like a node. It keeps its name, so `sim.Node()` and any client id derived from it stay the same, and it finds its disk as the crash left it. A client that saves its progress there can resume; one that keeps it in memory starts over.
- A workload crash does not end the run. The run passes only when the last incarnation of every workload exits 0.
- Operations the crashed workload had recorded with `sim.Put`, `sim.Get`, `sim.Invoke` or `sim.Txn` and not yet completed stay open, and the trace says how many (`client#1 died with 2 operations in flight, their outcome is unknown`). The history check treats an open write as one that may take effect at any time after it started, and drops open reads, so the check stays sound under every [model](properties.md#other-models).
- Per node, `"faults": true` or `false` overrides the default: `true` on one of several workloads faults only that one, and `false` on a node keeps it out of every fault, network faults included.

`workloads[]` runs several clients side by side, each its own process, so one can crash while the others keep going:

```json
"workloads": [
  { "name": "writer", "pkg": "./client", "args": ["-mode", "write"], "faults": true },
  { "name": "reader", "pkg": "./client", "args": ["-mode", "read"] }
]
```

[`examples/liveness`](../examples/liveness) has a client that saves its progress and resends the add in flight after a crash. Without request deduplication on the server, one crash during an add applies it twice.

## Network faults

Every network fault is directional underneath: it decides what happens to traffic from one node to another. A connection needs both directions to open, so a stopped direction either way refuses a dial, and a jammed one holds it.

| Mode | New connections | Data in flight | Errors the program sees |
|---|---|---|---|
| partition, or clog `stop` | refused | held, delivered after the heal | `ECONNREFUSED` on dial |
| clog `jam` | accepted only after the clog lifts | held, delivered after the clog lifts | none, only timeouts |
| clog `slow` | accepted `clog_delay` later when the slow direction points at the listener | arrives `clog_delay` later, in order | none |

A clog targets one of four shapes, chosen at random: one link in one direction (`n1 -> n2`), or a node's inbound, outbound, or inbound and outbound traffic. A one-way partition, where `n1` can hear `n2` but `n2` cannot hear `n1`, is a `stop` clog on one link or an outbound clog on one node. Faults stack: a slow clog over a partition adds its delay to the held traffic.

Partition topologies follow Jepsen's nemeses. `half` is the original random split and stays the default, so existing seeds keep their schedules. `majority` needs at least 3 nodes and `majorities_ring` at least 4, workload included; the config is rejected otherwise. A ring partition is written as overlapping groups, and two nodes can talk only if some group holds both.

A slowdown by factor F stretches everything the node waits for: its timers and sleeps take F times as long, every message it sends or receives takes F times its latency, and a goroutine that spins is parked F times as long. The node still reads the true time, so it sees its own timeouts fire late, the way an overloaded machine does. CPU work between two waits stays free, as it is for every node in seedfall.

`sim.QuietFor` and the recovery phase of `liveness` heal every partition, clog and slowdown at once.

In a fault schedule, the new kinds look like this:

```json
{ "at": "1.2s", "kind": "partition", "groups": [["n1", "n2"], ["n2", "n3"], ["n3", "client"], ["client", "n1"]], "until": "2s" }
{ "at": "1.5s", "kind": "clog", "from": "n1", "to": "n2", "mode": "stop", "until": "3s" }
{ "at": "1.6s", "kind": "clog", "node": "n3", "dir": "out", "mode": "slow", "delay": "80ms", "until": "2.4s" }
{ "at": "2.1s", "kind": "net_reset", "node": "n2", "until": "2.1s" }
{ "at": "2.5s", "kind": "slow", "node": "n1", "factor": 4.5, "until": "6s" }
```

`dir` is `in`, `out` or `both`. A swizzle shows up as a run of `both` clogs in `stop` mode. Like every other planned fault, each one replays and shrinks on its own, appears in the trace, `seedfall cause` and the report, and joins swarm testing.

### UDP datagrams

TCP traffic is a byte stream, where the kernel retransmits and deduplicates, so a program never sees a packet dropped or repeated on a connection. A UDP program does. `udp_loss` and `udp_dup` are probabilities per datagram, drawn from their own stream of the seed, so they take no draws from any other fault:

```json
{ "faults": { "udp_loss": 0.05, "udp_dup": 0.02 } }
```

A partition or a clog that stops or jams a link also drops a datagram sent across it, rather than holding it for the heal, and a `slow` clog delays it. Datagrams that a link or a missing socket drops are consequences of the rest of the schedule, so they are not faults of their own: only `udp_loss` and `udp_dup` choices are recorded. They count per sender node, from 1, across restarts:

```json
{ "at": "2.1s", "kind": "udp_drop", "node": "n1", "to": "n2", "op": 17, "until": "0s" }
{ "at": "2.2s", "kind": "udp_dup", "node": "n2", "to": "n3", "op": 9, "until": "0s" }
```

`op` is the number of the datagram the sender sent, and the fault fires on that datagram whatever its destination; `to` is a record of where it went. Both replay exactly, shrink like any fault recorded at runtime, can be edited with `seedfall faults`, and join swarm testing. They do not apply when `faults` is off for either end of the datagram, or during a quiet period or the recovery phase. Semantics of sockets and addresses are in [networking.md](networking.md#udp).

## Disk faults

## File system models

`reorder_writes` turns on out-of-order writeback at a crash. `fs_model` says which states a crash may then leave behind. A model that is too weak reports bugs your file system cannot produce; one that is too strong misses bugs it can. The models follow Table 1 of ALICE ([All File Systems Are Not Created Equal](https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-pillai.pdf), OSDI '14), which measured these properties on real file systems.

| `fs_model` | File contents | Directory operations (`strict_dirs`) | Matches |
|---|---|---|---|
| `ext4_ordered` (default) | Appends and truncates of one file persist as an in-order prefix, split at 4 KiB page boundaries. Overwrites of existing bytes persist per page in any order, independently of the appends. Bytes past the surviving file size are not kept | An in-order prefix of the pending operations, under `torn_writes` | ext4 `data=ordered` |
| `page_independent` | Any subset of the dirty pages of a file, in order within each page. A later appended page can survive without an earlier one, leaving zeros in the gap | As `ext4_ordered` | Aggressive: useful to find code that depends on append order, but it reaches states ext4 `data=ordered` does not. ALICE records this for ext2, ext3 and ext4 in `writeback` mode, not for `ordered` |
| `dir_reorder` | As `page_independent` | Each pending operation survives independently, so a rename can persist without the create before it | ext2 and btrfs, where ALICE found directory operations persist out of order |

Details that follow from these rules:

- Models apply per file. Different files are independent, so an append to one file can survive while an earlier append to another is lost. ALICE records `Append -> Any op` failing on ext4 `ordered` for this reason (delayed allocation).
- Under `ext4_ordered` a crash that keeps an overwrite past the surviving file size keeps nothing of it, because that page was never part of the file on disk.
- A single directory operation is atomic in every model, as on btrfs. ext2 can also tear one rename so that both names or neither survive; that is not modelled.
- Plain `torn_writes` without `reorder_writes` does not use `fs_model`: it keeps an in-order prefix of all pending writes.

[`examples/symswap`](../examples/symswap) shows the difference. It publishes each generation by renaming a symlink over `current`, and fsyncs the new generation's file but not its directory entry first. Under `ext4_ordered` it passes, because a journal keeps directory operations in order. Under `dir_reorder` the rename can survive without the create, and `current` points at nothing.

Crashes, torn writes, `reorder_writes` and `fsync_eio` test what survives a crash. The faults below test what a storage engine does when the disk itself misbehaves: it fills up, it fails an operation, or it hands back or keeps the wrong bytes. These are the paths that WAL recovery and checksum code exist for, and the ones that are hardest to reach with a real disk.

```json
"faults": {
  "crash_per_sec": 0.5,
  "torn_writes": true,
  "disk_bytes": 1048576,
  "write_eio": 0.01,
  "read_eio": 0.01,
  "read_corrupt": 0.05,
  "lost_write": 0.01,
  "misdirected_write": 0.01,
  "corrupt_on_crash": true,
  "bitrot_per_sec": 0.2,
  "disk_latency": ["1ms", "20ms"]
}
```

| Fault | What the program sees | What is on disk afterwards |
|---|---|---|
| `disk_bytes` | A short write, then `ENOSPC` on the next write. Overwrites inside a file always fit, and space comes back when files shrink or are removed | What fitted |
| `write_eio`, `write_enospc` | The write fails | Nothing from that write |
| `read_eio` | The read fails | Unchanged |
| `read_corrupt` | One bit flipped in the bytes returned by one read | Unchanged |
| `lost_write` | fsync succeeds, and reads return the new content | One page has its old content; zeros if the page is new. The next fsync that rewrites the page writes it in full |
| `misdirected_write` | fsync succeeds, and reads return the new content | The intended page has its old content, and another page of the file holds the new one |
| `corrupt_on_crash` | After the restart, one flipped bit per file among the bytes that were being written | Same |
| `bitrot_per_sec` | The flipped bit, from the moment it happens, unless that byte has a pending write | One flipped bit |
| `disk_latency` | fsync takes longer | Unchanged |

How each one is modelled, and where it stops:

- **Disk usage** is the sum of every file's size on the node. Holes left by `Truncate` or by writing past the end count in full, so sparse files use more space than on ext4 or XFS. Directories and metadata use none. A `Truncate` that grows a file is never refused.
- **`ENOSPC` reaches your code as `ENOSPC`.** wazero's WASI layer has no `ENOSPC` and reports `EIO` for it, so seedfall rewrites the result of `fd_write` and `fd_pwrite` when the simulated disk was full, and `errors.Is(err, syscall.ENOSPC)` works in the guest.
- **Read and write errors** apply to file reads and writes only. Directory listings, `stat`, `open` and `Truncate` never fail.
- **Corrupted reads** flip one bit in the buffer of one read, as a bad cable or controller would. A checksum plus a retry handles them; a checksum alone turns them into an error.
- **Lost and misdirected writes** pick one dirty page of the file being fsynced. The page cache keeps the right content, because the drive acknowledged the write, so the program only notices after a crash, or never if the page is rewritten first. A misdirected write stays inside the file; writes landing in another file are not modelled. A file needs at least two pages for a misdirected write.
- **Crash corruption** damages only bytes that were being written when the node crashed. With plain crashes, unsynced writes are dropped, so it matters only where they survive: with `torn_writes`, `reorder_writes` or `crash_on_io`. If the damaged range overlapped older durable data, that data is what flips.
- **Bit rot** picks a byte uniformly over all durable data on the node, so large files are hit more often.
- **Latency** applies to file and directory fsyncs only, not to reads or writes, which go to the page cache. The whole node waits, because a wasip1 guest runs every goroutine on one thread.

Every one of them comes from the seed and replays exactly. The rates are drawn per operation, like `crash_on_io`, and each firing is recorded with its node and operation number: `disk op #N` counts the node's writes, truncates and fsyncs, and `disk read #N` counts its reads. Which page or bit is hit comes from a stream keyed by the seed, the fault kind, the node and that number, so it does not change when shrinking removes other faults. Bit rot is planned in time like a crash. In a fault schedule they look like this:

```json
{ "at": "1.942589003s", "kind": "read_corrupt", "node": "server", "op": 3, "path": "data/kv.log", "offset": 70, "until": "0s" }
{ "at": "912.496ms", "kind": "write_eio", "node": "server", "op": 67, "path": "data/kv.log", "until": "0s" }
{ "at": "2.601158s", "kind": "lost_write", "node": "server", "op": 232, "path": "data/kv.log", "until": "0s" }
{ "at": "5.259168s", "kind": "misdirected_write", "node": "server", "op": 558, "path": "data/kv.log", "offset": 4096, "until": "0s" }
{ "at": "657.015787ms", "kind": "bitrot", "node": "server", "path": "data/kv.log", "offset": 22, "until": "657.015787ms" }
{ "at": "36ms", "kind": "mmap_early_writeback", "node": "server", "op": 3, "path": "data/pages", "offset": 65536, "until": "0s" }
```

The other kinds are `write_enospc` and `read_eio`. A recorded fault fires at the operation its `kind`, `node` and `op` name, and bit rot fires at `at`. `path`, `offset` and `target` are filled in by the run so that you can read the schedule, and are left out when they are 0. `seedfall inspect` lists every damaged range of a file under `corrupted ranges`, and with `disk_bytes` shows how full each disk is. Disk usage and latency are settings, not faults, so swarm testing leaves them alone and toggles the rest.

[`examples/kvlog`](../examples/kvlog) shows each one: a corrupted read changes an acknowledged value, a checksum with a re-read fixes it, and a lost write, a misdirected write or bit rot breaks a store that keeps one copy, with or without checksums.

## Editing a schedule

A fault schedule (`.seedfall/seed-N.faults.json` from `shrink`, an artifact's `faults.json`, or a pinned regression) is a list of faults that a replay applies instead of drawing new ones. Changing one fault and replaying is the quickest way to test an explanation of a failure. `seedfall faults` makes the change and checks it:

```sh
seedfall faults -c seedfall.always.json -seed 1 -faults torntail.faults.json -remove 1 -out hypothesis.json
seedfall replay -c seedfall.always.json -seed 1 -faults hypothesis.json
```

```
seed 1, 1 faults from torntail.faults.json, wrote hypothesis.json
  1    802ms  crash server, restart at 802ms
duration 991ms
replay: seedfall replay -c seedfall.always.json -seed 1 -faults hypothesis.json
```

On kvlog's `seedfall.always.json`, seed 1 fails with `torntail.faults.json`, still fails with the crash during disk op #56 moved one operation earlier (`-shift 1=-1`), and passes once that crash is removed. That pass is within the schedule's shrunk 991ms, and the replay prints a note saying so: it shows the crash is necessary for this failure, not that the store is fixed.

| Flag | Meaning |
|---|---|
| `-faults` | The schedule to start from. Without it, `.seedfall/seed-N.faults.json` next to the config, or, when that file does not exist, the faults seed N draws on its own, which takes one run |
| `-remove N` | Remove the fault at position N, counting from 1 as listed. Repeatable |
| `-shift N=AMOUNT` | Move fault N. A timed fault moves by a signed duration (`2=-50ms`), together with its `until`. A fault that fires at a disk operation, read, buggify hit, counted call or udp datagram (`crash_io`, `fsync_eio`, `write_eio`, `write_enospc`, `read_eio`, `read_corrupt`, `lost_write`, `misdirected_write`, `buggify`, `preempt`, `udp_drop`, `udp_dup`, `mmap_early_writeback`) moves by a signed count of those (`1=+2`), because its `at` only records when it happened. Repeatable |
| `-add JSON` | Add a fault in the format shown in this page, for example `{"at":"1s","kind":"pause","node":"server","until":"1.5s"}`. Repeatable |
| `-out` | Write the result here. Without it, the schedule is written back to the file it came from |

Positions in `-remove` and `-shift` always refer to the schedule as it was before the edit. An edited schedule drops the `shrunk_from` and `shrink_runs` that `shrink` recorded, since it is no longer what shrink found. The result is sorted by `at` and checked against the config before anything is written:

| Check | Applies to |
|---|---|
| `kind` is a fault kind seedfall knows | every fault |
| `node`, `from`, `to`, `side` and `groups` name nodes of the config | every fault |
| `at` is not negative | every fault |
| `at` is not after the end of the run: the schedule's `duration`, else the config's | every fault except those that fire at a disk operation, read, buggify hit, counted call or udp datagram, whose `at` only records when it happened |
| `until` is not before `at` | `crash`, `crash_io`, `partition`, `pause`, `clog`, `slow` |
| `side` or `groups`, not both | `partition` |
| `mode` is `stop`, `slow` or `jam`; `dir` is `in`, `out` or `both` with a `node`, or empty with two different nodes in `from` and `to` | `clog` |
| `node` is set | every kind except `partition` and `clog` |
| `factor` is at least 1 | `slow` |
| `op` is at least 1, a `buggify` fault names its `site`, and a `preempt` fault needs `preempt.strategy` `pct` in the config | faults that fire at a disk operation, read, buggify hit, counted call or udp datagram |

Without any edit, `seedfall faults` only lists and checks the schedule, and writes it only when it came from the seed's own faults, so that there is a file to edit. Over MCP, `seedfall_faults_edit` takes the same edits as JSON ([agents.md](agents.md#tools)).

A schedule file can also hold `branches`, which [`seedfall explore`](explore.md) writes for a failure it found by branching:

```json
"branches": [{ "at": "921.003003ms", "key": 257366709774643251 }, { "at": "1.2s", "key": 9, "stream": "sched" }]
```

Each branch re-keys the seed's random streams at the first scheduler step at or after `at`, in order. Without `stream` it re-keys every stream; with one of `sched`, `net`, `disk`, `io`, `udp`, `disklatency`, `mutant` or `random` it re-keys only that one. Re-keying `io` or `udp` changes nothing in a schedule, because those streams only decide faults and a schedule already fixes them; `mutant` matters only under `seedfall mutate`. `replay`, `shrink`, `inspect`, `debug`, `logs` and `pin` all honor them, and `at` values must not decrease.

## Choosing rates

Start with crashes and torn writes, then add `crash_on_io` around `0.005`, so a few hundred disk operations per run produce one or two mid-operation crashes. Add `fsync_eio`, `strict_dirs` and `reorder_writes` once the basic durability path passes. For consensus and leader-election code, add `partition_topologies` beyond `half`, then `clog_per_sec` and `slow_per_sec`: one-way links and slow leaders are the gray failures that break leases and stale-read checks. For a storage engine, add `disk_bytes` and `write_eio` to test the error paths of every write, then `read_corrupt` and `corrupt_on_crash` to test checksums. `lost_write`, `misdirected_write` and `bitrot_per_sec` lose data that a single copy cannot get back, so use them on replicated systems, or to check that a single node notices and stops instead of serving wrong data. Turn on `buggify` once you have marked sites in your code that should sometimes take the rare path. Turn on `swarm` for long CI sweeps. Use property coverage ([properties.md](properties.md)) to confirm the faults are actually reaching the code you care about.

## Durations

Every duration is a Go duration string, such as `"250ms"` or `"2s"`. Ranges are two-element arrays.


<!-- docs/getting-started.md -->

# Getting started

This walkthrough takes about five minutes. You will run seedfall on a small example server that loses data after a crash. You will find the bug, cut the failure down to its simplest form, fix it and prove the fix. The example is `examples/kvlog`, a key-value server that appends every write to a log file.

A few words you will see:

- A **node** is one program in your system, such as a server. seedfall runs each node as its own process inside a simulation.
- A **workload** is a program that uses your system and checks the answers. It plays the part of a client.
- A **fault** is something that goes wrong on purpose: a crash, a lost message, a half-written file.
- A **seed** is a number that decides everything random in one run, including when the faults happen. The same seed always gives the same run, so any failure can be replayed.

## 1. Install

You need Go 1.25 or newer. seedfall runs on Linux, macOS and Windows.

```sh
go install github.com/kunalgoesbyken/seedfall/cmd/seedfall@latest
seedfall doctor
git clone https://github.com/kunalgoesbyken/seedfall
cd seedfall/examples/kvlog
```

`seedfall doctor` checks your setup and tells you how to fix anything that is missing. Other ways to install (Homebrew, Scoop, a script, Docker) are in [install.md](install.md). Those need a release newer than v0.2.0.

## 2. Look at the example

The file `seedfall.always.json` describes the test: one server, one client and the faults to inject. It extends `seedfall.json` and changes one setting, the server's `-sync` flag. Merged, it reads (shortened):

```json
{
  "nodes": [{ "name": "server", "pkg": "./server", "args": ["-sync", "always"] }],
  "workload": { "name": "client", "pkg": "./client", "args": ["-writes", "200"] },
  "faults": { "crash_per_sec": 0.5, "torn_writes": true, "crash_on_io": 0.005 }
}
```

What this means:

- The server appends `key=value` lines to `data/kv.log`. Before it tells a client "done", it calls **fsync**. Fsync is the operating system call that forces data onto the disk. Without it, a crash can lose data that is only in memory.
- The client writes 200 keys. Then it checks that every key the server acknowledged is still there. The check is a `sim.Assert` call.
- The faults crash the server about every two seconds and allow **torn writes**, where a crash leaves a write only half saved.
- The server's only seedfall-specific code is `sim.Listen`, which opens its network port.

## 3. Run a sweep

A sweep runs the test once per seed. Try seeds 1 to 100:

```sh
seedfall run -c seedfall.always.json -seeds 1-100
```

```
FAIL seed 1 at t=2.891820635s (737 scheduler steps, 445ms real)
  client#1: acknowledged write lost: k96=v96, server now answers "NONE"
```

Seed 1 fails. The server said it saved a key, and after the crashes the key was gone, even though the server uses fsync before every acknowledgement. That is a real bug.

## 4. Shrink the failure

Seed 1 had 33 faults, and most do not matter. `shrink` removes faults and simplifies what is left, while the failure keeps happening:

```sh
seedfall shrink -c seedfall.always.json -seed 1
```

```
faults before the failure (2):
  427.268ms  crash server during disk op #56, restart at 761.268ms
     802ms  crash server, restart at 802ms
...
shrunk from 33 faults, 1m0s, 200 workload ops
         to 2 faults, 991ms, 63 workload ops
```

Two faults are enough. Shrink also made them simpler: the first crash restarts 30ms sooner, the second moved from 1.7s to 0.8s, the run ends at 991ms instead of 60s, and the client sends 63 writes instead of 200. (The client can shrink its own size because it uses [`sim.Budget`](properties.md#workload-size).)

Here is the bug in plain words:

1. The first crash lands in the middle of an append. The last line in the log is left half written.
2. On restart, recovery skips the bad line but keeps appending after it. The next record is glued onto the garbage.
3. The second crash forces another recovery, which can no longer read that record.

To see the whole run, use `seedfall replay -c seedfall.always.json -seed 1`. To replay only the two faults that matter, add `-faults .seedfall/seed-1.faults.json`.

## 5. Fix it and prove it

The fix is to cut off the half-written tail during recovery. The server already has this behind a flag called `-repair`, and `seedfall.fixed.json` turns it on:

```sh
seedfall run -c seedfall.fixed.json -seeds 1-1000
```

```
property       seeds reached  seeds true
  sometimes            1000         994  a crash interrupted the workload
  sometimes            1000         406  recovery found a torn tail

ok  1000 seeds passed (0 hit the time horizon) in 1m28.94s
```

All 1000 seeds pass. The table below the result matters too. It shows that the risky paths really ran: in 406 seeds recovery met a torn tail, and each one was handled correctly. A passing sweep that never reached the risky code would prove little.

## 6. Go further

- `seedfall.fsyncgate.json` makes fsync itself fail (`fsync_eio`). The "fixed" server breaks again, because a failed fsync leaves a hole in the log. `seedfall.rewind.json` adds the fix.
- `seedfall.strict.json` also loses directory changes that were never synced, as POSIX allows.
- Open `.seedfall/failures/seedfall.always-seed-1/timeline.html` after the failing sweep for a diagram of every crash and message. Or step through the run with `seedfall debug -c seedfall.always.json -seed 1 -at 1.7s` ([timeline.md](timeline.md)).
- Each of these config files is a few lines that extend `seedfall.json`. In your own project you can keep such variants as profiles in one file and pick one with `-profile`, or try a ready-made fault preset with `-set faults=resilient` ([config.md](config.md)).

## Use it on your own project

1. Make your nodes reachable inside the simulation. Either change `net.Listen` and `net.Dial` to `sim.Listen` and `sim.Dial`, or set `"net_overlay": true` to run your code unchanged ([networking.md](networking.md)).
2. Write a workload. It is any Go `main` package that uses your system and checks the results with `sim.Assert`, `sim.Always` and similar calls ([properties.md](properties.md)).
3. Describe the test in `seedfall.json` ([faults.md](faults.md)).
4. Run sweeps on your machine, then in CI ([ci.md](ci.md)), and from your coding agent ([agents.md](agents.md)).

`seedfall init` can write a first config and workload for you.

One requirement: your code must build for `GOOS=wasip1`. This is Go's target for WebAssembly System Interface, a small sandbox that lets seedfall control time, randomness and the disk. In practice it means no cgo (Go code that calls C). Libraries that need `mmap` or `flock` (operating system calls for mapping files and locking them) work when you set `"compat_overlay": true`; `seedfall init` turns it on and tells you which dependency is covered ([compat.md](compat.md)).


<!-- docs/gostman.md -->

# Use your Gostman collections as workloads

Gostman is an API testing tool. Its collections list requests and the checks each reply must pass. This page shows how to reuse a collection as seedfall's workload, so the same checks run while seedfall breaks your service. Use it if you already have a Gostman collection.

A [Gostman](https://github.com/kunalgoesbyken/gostman) collection already says what your API promises: each request carries checks such as `res.status equals 200` or `res.body equals {{value}}`. Gostman's Go `runner` package builds for `wasip1`, so a seedfall workload can load the collection and send it while seedfall crashes your service, tears its writes and partitions its network. A check that fails after the faults stop is a broken promise, reported with the request and the check, and replayable from its seed.

[`examples/gostman`](../examples/gostman) is a complete world: `examples/httpkv`'s server and a client that runs the collection in [`examples/gostman/collection`](../examples/gostman/collection).

## The pattern

Split the collection into two folders:

- **Write**: requests that change state. They are sent while faults run and retried until their checks pass, so a pass means the server acknowledged the change.
- **Verify**: requests that check state. They are sent after `sim.QuietFor`, when faults are paused and partitions healed. A request that gets no answer, because the server is still restarting, is sent again. A check that fails on an answer fails the seed.

The client copies the embedded collection onto its simulated disk, loads it and sends one request at a time through a single session:

```go
//go:embed collection
var Collection embed.FS

os.CopyFS(".", Collection)
collection, _ := runner.Load("collection")
session, _ := runner.NewSession(engine.Policy{})
session.Enter(collection, "", "Simulation", nil)
listed, _ := session.Catalog(collection, "Verify")
result := session.Send(ctx, listed[0].Request, listed[0].Folder, vars).Result
sim.Always(!result.Failed, "Gostman checks pass once the faults stop", details)
```

Nodes cannot read files on the host, which is why the collection is embedded. Variables passed to `Send` (`key`, `value`, `deleted_key` in the example) win over the environment, so each round uses fresh keys. The `Simulation` environment points `base_url` at `http://server:8080`, the node name; a `Local` environment points at `127.0.0.1` so the same files run with the Gostman command line.

## Run it

```sh
cd examples/gostman
seedfall run -seeds 1-120
seedfall replay -c seedfall.json -profile nofsync -seed 1
```

With fsync before every acknowledgement every seed passes. With `-fsync=false` the first seed fails once a crash drops an acknowledged write:

```
FAIL seed 1 at t=13.104695555s (108 scheduler steps, 29.398s real)
  client#1: Gostman checks pass once the faults stop: GET http://server:8080/kv/k6 (Verify/Get value)
  res.status equals 200: The value was 404
  res.body equals v6: The value was "404 page not found\n"
```

The client embeds the Gostman runner and its JavaScript sandbox, so each seed takes about a minute of real time; sweeps get their speed from running seeds in parallel.

## Use your own collection

1. Copy `examples/gostman/client` and `collection.go` next to your service's seedfall config, and put your Gostman workspace folder in `collection/`.
2. Add a `Simulation` environment whose base URL uses the node name from `seedfall.json`.
3. Put the requests that write in one folder and the requests that check in another, and pass their names with `-write` and `-verify`.
4. Enable `"net_overlay": true` so the runner's plain `net/http` client reaches the simulated network.

The example uses HTTP requests with assertions. Anything that needs the host, such as `{{$file(...)}}`, local commands or an OAuth sign-in in a browser, cannot work inside a node.


<!-- docs/how-it-works.md -->

# How seedfall works

This page explains why the same seed always gives the same run: seedfall controls the clock, the randomness and the scheduling for every node, and simulates the disk and the network. Read it to understand what seedfall can and cannot find, or to decide how far to trust a result. You do not need it to run your first sweep.

## One process, one clock, many nodes

seedfall compiles every node with the stock Go toolchain for `GOOS=wasip1` and runs each one as its own [wazero](https://wazero.io) module instance. On `wasip1` the Go runtime is single-threaded and has no async preemption, and every source of nondeterminism reaches the outside world through three WASI calls. seedfall implements all three in the host, and adds a deterministic preemption point of its own (below):

| WASI call | seedfall behavior |
|---|---|
| `random_get` | A ChaCha8 stream derived from the seed and the node's incarnation. This fixes map iteration order, `select` choice, `math/rand` and crypto randomness. |
| `clock_time_get` | A virtual clock shared by every node. Every read advances it by one nanosecond, so two `time.Now()` calls in a row never return the same value, as on real hardware; wall and monotonic clocks advance together. With `clock_skew` and `clock_jump`, each node's wall clock is offset by a seeded amount; the monotonic clock is never skewed. |
| `poll_oneoff` | Parks the node until its earliest timer or its next network arrival. |

A node gives up control when all of its goroutines are blocked, or when it is preempted after a long run without blocking (see [Preemption](#preemption)). The scheduler runs exactly one node at a time, picks the next one by earliest wake-up time, breaks ties with the seed, and jumps virtual time forward. Ten seconds of `time.Sleep` cost no real time.

There is no `linkname`, no source rewriting and no forked runtime, so new Go releases keep working. The opt-in `compat_overlay` and `net_overlay` are the exceptions: they add wasip1 files to your build ([compat](compat.md)), and the generic `flock` shim uses one `go:linkname` to `time.Sleep`.

## Preemption

Real Go preempts a goroutine that has run for 10ms. On `wasip1` nothing does, so a goroutine that spins without a syscall would starve every other goroutine in its node, and its node would never yield. seedfall loads each Go module with a call counter added to the start of every function. After 4,194,304 counted calls without the node blocking, the counter calls back into the host, which triggers the Go runtime's own cooperative preemption path for the running goroutine (the same `stackguard0` request the runtime's `sysmon` makes on other platforms) and parks the node for 10ms of virtual time, so other nodes run too. The count is part of the execution, so preemption points are as deterministic as everything else. A burst shorter than that costs no virtual time.

### Loops

By default a loop that makes no function call is not counted, so it is never preempted: a call-free spin holds the whole simulation until the real-time `watchdog` stops it, and a long call-free computation takes no virtual time. With `"preempt": {"loops": true}` the counter also runs at the head of every wasm `loop`, which the Go compiler emits for Go loops, so loop iterations count like calls. A node that spins or computes for 4,194,304 counted calls and iterations is then parked for 10ms of virtual time like any other: other nodes keep running, timers and leases on other nodes expire, and a spin that never ends fails deterministically on `liveness` (or runs to the horizon) instead of on the host-dependent watchdog. [`examples/busyloop`](../examples/busyloop) shows both: a leader whose lease expires during a call-free checksum, which only fails with `loops`, and a spin-wait that fails as `liveness` with `loops` and as a real-time `timeout` without.

Two limits. The Go runtime on `wasip1` can switch goroutines only at a function entry, so a goroutine in a call-free loop still keeps the other goroutines of its own node from running until it makes a call; `loops` parks the node, it cannot hand the CPU to a sibling goroutine. And the extra check on every iteration costs guest CPU, which is why it is off by default.

### Strategies

`preempt.strategy` decides when, inside a time slice, the running goroutine is preempted:

| Strategy | Preempts the running goroutine | Randomness |
|---|---|---|
| `none` (default) | only at the end of a 4,194,304-call time slice | none |
| `random` (`"interleave": true` is shorthand) | after a seeded random 1 to 4,096 counted calls, again and again | per instance, from the seed |
| `pct` | at `depth` - 1 change points per node, drawn from the seed over the node's first `steps` counted calls | per node, from the seed, recorded as faults |
| `calls` | every `calls` counted calls | none |

`random` finds shallow races quickly: a check-then-act window that any preemption opens shows up within a few seeds ([`examples/interleave`](../examples/interleave), `interleave.json`). But it preempts every goroutine every few thousand calls, so no goroutine ever runs long without being interrupted. A bug that needs one goroutine to stop inside a window while another runs a long stretch to completion is almost never hit.

`pct` is probabilistic concurrency testing (Burckhardt, Kothari, Musuvathi and Nagarakatte, ASPLOS 2010), as in shuttle's `check_pct`. A run is left alone except at `depth` - 1 seeded change points; at each one the running goroutine is preempted and goes to the back of the Go run queue, and whatever runs next keeps running until it blocks or its time slice ends. For a priority scheduler with n threads and k steps, PCT finds any bug of depth d (one that needs d ordering constraints) with probability at least 1/(n·k^(d-1)) per run. In `examples/interleave`, a checkpointer that copies a journal up to its reserved length instead of its committed length fails on 20 of seeds 1-20 with `pct` at depth 2, on 2 of 20 with `random`, and on none with `none`, because the bug needs the checkpointer to format a long header without being interrupted (`journal.json`).

Every change point that fires is recorded as a `preempt` fault with its node and counted call (`op`), and the trace says so:

```
    0.000s  preempt: pct, depth 2, change points per node: 1, drawn over the first 300000 counted function calls
    0.000s  fault preempt journal#1's running goroutine at counted call 259662
    0.000s  pct: journal ran 271681 counted calls, change points fired: 1
```

In the schedule file it is

```json
{ "at": "10ns", "kind": "preempt", "node": "journal", "until": "0s", "op": 259662 }
```

so replay is exact, `shrink` drops change points the failure does not need, and `seedfall faults` can move one (`-shift 1=-1000`) or remove it to test an explanation. A schedule's `preempt` faults replace the seed's own change points, and they fire only when the config's strategy is `pct`. The last trace line shows how many counted calls each node ran: set `steps` near that number, because change points drawn beyond it never fire.

The bound is a guide for choosing `depth` and `steps`, not a guarantee seedfall gives. seedfall picks only the change points. It cannot see goroutines from the host, so it does not assign them priorities: which goroutine runs after a preemption is the Go scheduler's choice, under the seed's random source. Change points are drawn per node, k is counted in calls (and loop iterations with `loops`), and preemption takes effect at the goroutine's next function call. None of the strategies is a data race detector: they find races that change behaviour, not unsynchronized accesses that happen not to. Run your tests under `go test -race` as well.

## Determinism

Scheduling, network latency, disk tearing, fault timing and I/O faults each draw from their own seeded stream. Removing one fault therefore barely disturbs the rest of the run, which is what makes shrinking work. The same seed produces the same trace byte for byte across processes and machines. `seedfall run -check` verifies this on every seed.

## Disk

Each node gets an in-memory file system mounted at `/` with an explicit durability model. Your code uses plain `os.File`.

- Writes land in the page cache immediately and are visible to reads.
- `Sync` makes the file's pending writes durable.
- A crash keeps only durable data. A file that was never synced disappears.
- With `torn_writes`, a crash also keeps a random in-order prefix of the pending writes, possibly ending in a partial write.
- With `reorder_writes`, a crash writes back dirty pages out of order, as kernel writeback does between fsyncs. Each pending write is split into 4 KiB pages. What may survive depends on `fs_model` ([File system models](faults.md#file-system-models)). The default, `ext4_ordered`, keeps appends and truncates of a file as an in-order prefix and lets overwrites of existing pages survive per page. `page_independent` keeps a random in-order prefix of the writes to each page, with pages chosen independently, and `dir_reorder` also lets each pending directory operation survive independently. With `torn_writes` as well, the last write kept in each page can be partial. Which pages survive is drawn from a stream keyed by the crash itself, its time or its `crash_on_io` disk operation, so shrinking away other faults does not change it.
- `Sync` and `Datasync` behave the same: both make every pending write to the file durable, and neither makes the file's directory entry durable, which is what `strict_dirs` models.
- With `strict_dirs`, creating, renaming or unlinking a file survives a crash only after its parent directory is fsynced. This is strict POSIX, the model used by ALICE and CrashMonkey. Without it, directory entries are durable as soon as they are made, which matches ext4 and XFS in practice.
- With `fsync_eio`, a file `Sync` can fail with `EIO`. The unsynced writes stay readable but are dropped from durable storage, and the next `Sync` succeeds. These are Linux's post-2018 "fsyncgate" semantics.
- Hard links share one inode and count their links, symbolic links are followed by `open`, `stat` and intermediate path components, and `Lstat`, `Readlink`, `Link` and `Symlink` behave as on Linux, including `ELOOP` after 40 hops. A new link is a directory operation like any other: with `strict_dirs` it survives a crash only after its parent directory is fsynced. Symlinks are durable with their directory entry, because a program cannot fsync one.
- `Chtimes` stores times on the file, reads update the access time as `relatime` does, and the times a file had at its last fsync are what a crash restores. Directories report no times. `Chmod` is not modelled: WASI has no call for it, Go's `wasip1` `os.Chmod` only checks that the file exists, and `Stat` reports fixed permission bits.
- With `disk_bytes`, each node's disk has a fixed size. A write that does not fit is cut short and the next one fails with `ENOSPC`.
- `write_eio`, `write_enospc`, `read_eio` and `read_corrupt` fail or corrupt single reads and writes. `lost_write` and `misdirected_write` make a successful fsync leave one page with its old content, or put it at the wrong offset, while the page cache keeps the right bytes. `corrupt_on_crash` flips a bit in the bytes being written at a crash, `bitrot_per_sec` flips durable bits over time, and `disk_latency` makes every fsync wait. Each per-operation fault is recorded with the node's disk operation or disk read number, so it replays and shrinks like `crash_on_io`. See [Disk faults](faults.md#disk-faults).

See [faults.md](faults.md) for every fault type.

## Network

UDP sockets are queues of datagrams with their own seeded latency, sorted by arrival, so they reorder; a held link drops them rather than holding them, and `udp_loss` and `udp_dup` choices are recorded per sender datagram so they replay and shrink like the disk faults. Connections are ordered byte streams with seeded per-chunk latency. Partitions and `stop` or `jam` clogs hold traffic until they heal, `slow` clogs and slow nodes add latency, and a crashed node's connections are reset, as are a live node's when a `net_reset` fault fires. Every fault is a rule on one direction of a link, so one-way partitions fall out of the same code. Every connection is a virtual file registered with Go's own network poller, so blocking reads, deadlines and `Accept` behave exactly like `net`, and nothing polls. See [networking.md](networking.md).

## Crashes and restarts

Every incarnation of a node is a fresh module instance. A crash kills the whole process at a host call, including in the middle of a disk operation with `crash_on_io`, then applies the disk durability model. A restart instantiates the module again over the surviving disk. With `supervise`, a node that exits with an error is restarted the way systemd or Kubernetes would restart it.

## Checking

A run fails when:
- any node calls `sim.Fail`, fails `sim.Assert` or `sim.Always`, or reaches `sim.Unreachable`;
- a `sim.Eventually` condition is still false at its deadline, or, with `liveness`, the workload or the `finally` check has not finished within `liveness.within` of the recovery phase (liveness);
- the workload or the `finally` check exits non-zero;
- a node exits or panics, unless `supervise` restarts it (Go panics always fail);
- every node is blocked with no timer or pending message (deadlock);
- a node runs longer than `watchdog` of real time without yielding (livelock or busy loop; with `preempt.loops`, a spinning node parks like any other and fails on `liveness` instead);
- the recorded `sim.Put` / `sim.Get` / `sim.Invoke` history is not linearizable under the configured model, or the `sim.Txn` history has an isolation anomaly.

A sweep also fails when a cataloged property is never reached, or a `Sometimes` is never true, in any seed.

See [properties.md](properties.md).

## Shrinking

`seedfall shrink` replays a failing seed under smaller and smaller variations and keeps a change only while the run still fails the same way: same class, node, property and message, ignoring numbers. It never trades the bug for a different one, and every schedule it keeps is one it actually ran. It works in passes:

1. **Remove faults by delta debugging** (ddmin). Try half the schedule, then each half on its own, then quarters, eighths and so on down to removing single faults. In `examples/kvlog`, seed 1 goes from 33 faults to the 2 it needs in 16 runs. The last round removes one fault at a time, so the result is 1-minimal: removing any fault left makes the failure go away or change.
2. **Cap the workload** if it sizes itself with [`sim.Budget`](properties.md#workload-size), by bisecting the operation count.
3. **Trim the duration** by bisecting the run's horizon down toward the failure.
4. **Simplify each fault**: shorten crash downtimes, partitions, pauses, clogs and slowdowns (`until` moves toward `at`), shrink clock jumps toward zero, take nodes off the cut side of a partition (a partition into groups keeps its groups), and move planned faults earlier. Faults recorded at run time, such as a crash during a disk operation, keep their operation index; only their downtime shrinks.

Passes 2 to 4 repeat, with another removal round after each, until nothing changes. Times are bisected to within two milliseconds. The shrinker makes no random choices of its own, so a seed always shrinks to the same schedule.

Candidates of one round run at once on `-j` workers (all cores by default), and the shrinker takes the first one that fails, in the order it would have tried them one by one. The schedule and run count are the same for any `-j`. `-budget` stops early: a number (`-budget 300`) counts those runs, so the result is still reproducible, while a duration (`-budget 10m`) is wall-clock time and depends on the machine. With more than one job, a round can also start runs whose results are thrown away. When the budget runs out, shrink saves the smallest failing schedule so far and says it may not be minimal.

The output shows each improvement with the runs used so far and the faults left, then the sizes before and after:

```
  run   16    2 faults  removed 1 of 3 faults
  run   26    2 faults  sim.Budget capped at 107 of 200 operations
  run   43    2 faults  duration 1.965s instead of 1m0s
  ...
shrunk from 33 faults, 1m0s, 200 workload ops
         to 2 faults, 991ms, 63 workload ops
in 191 runs, 14.296s
```

The schedule is saved to `.seedfall/seed-N.faults.json`:

```json
{
  "seed": 1,
  "faults": [
    { "at": "427.268419ms", "kind": "crash_io", "node": "server", "until": "761.268419ms", "op": 56 },
    { "at": "802ms", "kind": "crash", "node": "server", "until": "802ms" }
  ],
  "duration": "991ms",
  "ops": 63,
  "shrunk_from": { "faults": 33, "duration": "1m0s", "ops": 200 },
  "shrink_runs": 191
}
```

`replay`, `inspect` and `verify` take it with `-faults`. `duration` replaces the config's `duration` and `ops` caps `sim.Budget`; leave either out to use the config. A bare JSON array of faults, the format older versions wrote, still works. A replay that passes only because the shortened `duration` ended it before the workload finished prints a note saying so, and `verify` replays schedules for the config's full duration, so a cut-short run never counts as proof of a fix.

## Speed

Virtual time never waits on the wall clock. When every node is blocked, the scheduler jumps straight to the next timer, message or fault; the only real-time limit is the `watchdog`. Real time therefore goes to three things:

- **Guest CPU.** Nodes run as wasm compiled to native code by wazero, with a check on every loop iteration so the watchdog can stop a busy loop. That check costs about a third of guest CPU and is what makes livelocks reportable instead of hanging the run. `preempt.loops` adds seedfall's own counter to every loop head as well. Host calls (clock, `poll_oneoff`, files, network) are a few percent.
- **Booting nodes.** Every start and restart is a fresh module instance: wazero sets up memory and data segments, then the Go runtime and your `main` run. For nats-server this is 0.1-0.3s per start, so short seeds with many crashes are dominated by boots.
- **Compiling, once.** Each guest is compiled once per process and shared by every seed and every node that runs the same binary. Compiled code is cached in `.seedfall/cache`, so later processes only load it. The cache keeps the 8 most recently used sets of binaries and deletes older ones, so rebuilding a guest many times does not fill the disk.

A busy 3-node NATS JetStream cluster under crashes and partitions simulates about 2.5-3x faster than real time; a JetStream node that mostly waits on its client about 7x. Seeds are independent, so `seedfall run -j N` runs N at once.


<!-- docs/inspect.md -->

# Inspecting the disk at the moment of failure

When a test fails after a crash, the cause is often what had and had not reached the disk. `seedfall inspect` shows every node's files at the moment of failure: which bytes were safely saved, which a crash would lose, and where a write was cut short. Use it for durability bugs, such as data that is missing after a restart.

`seedfall replay` tells you what happened. `seedfall inspect` shows you what is on disk when it goes wrong: every file on every node, how much of it is durable, which bytes a crash would lose, which directory entries are not durable yet, and where the last crash tore a write.

```sh
seedfall inspect -c rosedb.json -seed 1
```

```
seed 1 failed at t=3.12130224s: client#1: acknowledged entry 27 lost: server now answers "VAL e141-1111111111111111111111"
disk state at t=3.12130224s, the moment of failure

node server (directory entries are durable once made; torn_writes: a crash may also keep a prefix of the pending writes)
  path                                                   size    durable  state
  data/                                                     -          -  durable
    wal/                                                    -          -  durable
      000000001.SEG                                      4029       4029  durable
        ^ torn by the crash at t=427.268199ms: kept 60 of a 73-byte write at offset 2019
      000000002.SEG                                      3979       3979  durable
      000000003.SEG                                      2054       2054  durable
  2 dirs, 3 files: 10062 bytes durable, 0 bytes pending, 0 entries lost on crash, 0 removed entries that come back

node client (directory entries are durable once made; torn_writes: a crash may also keep a prefix of the pending writes)
  empty disk
```

The crash at 427ms left a 60-byte fragment of entry 26 at offset 2019, and every later entry was appended after it. That is the rosedblabs/wal bug in [findings](findings/rosedblabs-wal-torn-tail.md), visible without reading any code.

## Usage

```sh
seedfall inspect [-c seedfall.json] -seed N [-faults file.json] [-at DURATION] [-node name] [-cat path | -out dir]
```

| Flag | Meaning |
|---|---|
| `-seed` | Seed to replay |
| `-faults` | Replay with a fault schedule from `seedfall shrink` |
| `-at` | Snapshot at this virtual time instead of at the failure, for example `-at 4.4s`. The snapshot is taken at the last scheduler step at or before it. If the run fails or ends first, the snapshot is taken there. |
| `-node` | Only this node |
| `-cat` | Print the durable content of one file: text as is, binary as a hex dump. The file must exist in the durable image. |
| `-out` | Write each node's durable disk image to `dir/<node>/`, so you can open it with the library's own tools, or start new runs from it with `"disk": "dir/<node>"`, a path relative to the config's directory ([seeded disks](config.md#seeded-disks-and-files)); the command prints that path. The target must not exist yet. |

The run is the same as `seedfall replay`: same seed, same faults, same trace. Inspecting changes nothing about it.

## Reading the output

Each file has its live size (what the program reads now) and its durable size (what survives a crash), and one state:

| State | Meaning |
|---|---|
| `durable` | The live content and the durable content are the same, and the name survives a crash |
| `PENDING: N bytes lost on crash at [a,b) ...` | These byte ranges of the live content differ from the durable content: they were written but not fsynced |
| `PENDING truncate` | The file was truncated but not fsynced; a crash restores the old bytes |
| `NOT DURABLE: never fsynced` | Without `strict_dirs`, a file that was never fsynced disappears on crash |
| `NOT DURABLE: entry vanishes on crash` | With `strict_dirs`, the directory entry is not durable until the parent directory is fsynced, even if the file's data is |

A `^ torn by the crash at t=...` line under a file says the last crash kept only part of one write: how many bytes of it, and at which offset. Those partial bytes are now durable and are what recovery code has to cope with.

With `reorder_writes`, a `^ the crash at t=... wrote back pages out of order` line lists the writes that were pending at the last crash, numbered in program order, and says which of them reached the disk: `kept`, `lost`, or `partial` when only some of its pages did. A later write marked `kept` above an earlier one marked `lost` is the reordering your recovery code has to survive. The same list is in `last_writeback` in the MCP inspect output.

With the [disk faults](faults.md#disk-faults), a `^ corrupted ranges` list under a file shows every range a disk fault damaged: a `lost write` or `misdirected write` that a successful fsync left with its old content, a bit flipped by `bit rot` or by `crash corruption`, and each `corrupted read` that returned a flipped bit while the disk held the right bytes. It is a history: an entry stays after the program overwrites the range or a later fsync rewrites the page in full. The last 8 are shown, and the full list is in `damage` in the MCP inspect output. With `disk_bytes`, a `disk_bytes: N of M bytes used` line follows the totals.

```
    kv.log                                               5727       5727  durable
      ^ corrupted ranges:
        t=5.259168049s misdirected write: [4096,5005) kept its old content on disk, and its page landed at offset 0 instead
```

With `strict_dirs`, a file that was unlinked or renamed away while its parent directory was not fsynced is listed separately as an entry that a crash brings back. Renaming a temporary file over an existing one without fsyncing the directory shows up as the new name `NOT DURABLE` and the old content coming back.

The durable image is the disk a crash would leave without `torn_writes` or `reorder_writes`. With `torn_writes`, a crash can also keep an in-order prefix of the pending writes and, with `strict_dirs`, of the pending directory operations. With `reorder_writes`, what it can keep depends on `fs_model`, which the node line names: `fs_model` is also a field of the MCP inspect output, and each file reports `symlink` and `links` there. With `inspect -out`, a symlink is written as a symlink; on Windows without the privilege to create one, it is written as a file holding its target. Hard links are written as separate files.

## Examples

NATS JetStream, the stream that vanishes ([finding](findings/nats-stream-meta-checksum-crash.md)):

```sh
cd examples/natsjs
seedfall inspect -c seedfall.always.json -seed 40 -faults metasum.faults.json
```

```
          EVENTS/                                           -          -  durable
            meta.inf                                      517        517  durable
            meta.sum.tmp                                    6          6  durable
              ^ torn by the crash at t=158.20724ms: kept 6 of a 16-byte write at offset 0
            msgs/                                           -          -  durable
              1.blk                                      7702       7702  durable
```

`meta.inf` exists, `meta.sum` does not, and only a torn `meta.sum.tmp` is left. NATS skips a stream without a checksum on restart, and because `meta.inf` exists it never writes `meta.sum` again, so the 1.blk messages acknowledged since are skipped on every later restart.

tidwall/buntdb, one step before the crash that empties the database ([finding](findings/tidwall-buntdb-shrink-fsync.md)):

```sh
cd examples/buntdb
seedfall inspect -c seedfall.shrink.json -seed 27 -at 4.417s -node server
```

```
  data/                                                     -          -  durable
    db                                                   1255          0  NOT DURABLE: never fsynced, vanishes on crash
```

The AOF shrink renamed its rewritten file into place without fsyncing it: 1255 bytes live, none durable. At the failure, `db` holds only the 211 bytes that the crash at 4.417s happened to keep.

## From an agent

The MCP server exposes the same snapshot as `seedfall_inspect`, with the per-file sizes, volatile byte ranges, entry durability and last tear as JSON, and optionally one file's durable content. See [agents.md](agents.md).

## Limitations

- The snapshot covers the simulated disk only, not process memory or in-flight network messages. `seedfall debug -at` stops the run at the same moment and also shows the messages in flight, the active faults and each node's live file content ([timeline.md](timeline.md#debugger)).
- The last tear is recorded per file. A later write over the same range does not clear it.
- `-cat` prints the whole file. Pipe it through `tail` for large files.


<!-- docs/install.md -->

# Installing seedfall

This page shows every way to install seedfall and how to check that it works. If you have Go, the quickest way is `go install`. Skip the rest unless you want a package manager or a signed release.

seedfall is a single program. It also needs Go (1.25 or newer) on your machine, because it builds your code before running it. Commands that run your code need Go: `run`, `replay`, `shrink` and the matching MCP tools. Commands that only read things do not need Go: `seedfall findings`, `version`, `help` and `schema`.

**Which of these work today.** Homebrew, Scoop, the install script and Docker all install from a release made by `.github/workflows/release.yml`. The latest release, v0.2.0, is older than that workflow. It has only bare binaries, with no archives and no `checksums.txt`. Until a newer release is cut, use `go install`. The signing, SBOM, cask, manifest and image steps of the release pipeline have not run yet, so the commands below that depend on them show what the setup is meant to produce. They have not been checked against a published release.

## Quickest: go install

```sh
go install github.com/kunalgoesbyken/seedfall/cmd/seedfall@latest
```

This needs Go 1.25 or newer. It works for every release, including those from before the automated pipeline.

## Homebrew

```sh
brew install kunalgoesbyken/tap/seedfall
```

The package depends on Go. Apple has not notarized seedfall's binaries, so macOS would normally refuse to start them. The package therefore clears the "quarantine" flag on its own binary after installing.

## Scoop (Windows)

```powershell
scoop bucket add seedfall https://github.com/kunalgoesbyken/homebrew-tap
scoop install seedfall
```

The package depends on Go.

## Install script (Linux and macOS)

```sh
curl -fsSL https://seedfall-lemon.vercel.app/install.sh | sh
```

The script picks the download for your system, checks its SHA-256 checksum (a fingerprint of the file) against the release's `checksums.txt`, and installs to `~/.local/bin`. It stops with an error if the checksum does not match. The script is `scripts/install.sh`, so you can read it first.

Settings, all optional:

- `SEEDFALL_VERSION=v0.3.0` installs a specific release.
- `SEEDFALL_INSTALL_DIR` changes where it is installed.
- `SEEDFALL_BASE_URL` downloads from a mirror.

## Docker

```sh
docker run --rm -v "$PWD:/work" ghcr.io/kunalgoesbyken/seedfall run -seeds 1-200
```

The image is built on the official `golang` image, so it can build your code without Go on your machine. Files the container writes, including `.seedfall/`, belong to root unless you pass `--user`.

## Check the install

```sh
seedfall version
seedfall doctor
```

`seedfall version` (or `--version`; add `-json` for scripts) prints the release, commit, build date, Go version and platform. A build without version-control data, such as `go install` of a tagged module, has no commit or date lines. The same version is written into `report.json`, every `.seedfall/history.jsonl` entry, failure artifacts, pinned regressions and the `seedfall verify` proof block, so a bug report can name the exact build.

`seedfall doctor` checks:

- the Go version;
- that `GOOS=wasip1` builds (`wasip1` is the WebAssembly System Interface target seedfall compiles your code for);
- that `net_overlay` patches and builds against your Go (`net_overlay` lets unmodified code use the simulated network);
- that the Go build cache and the current directory are writable;
- the free memory.

For anything wrong it prints a fix. It exits with code 1 only if a check fails. A warning, such as low memory or an unsupported `net_overlay`, still exits 0. `-json` prints the same checks, and so does the `seedfall_doctor` MCP tool. Free memory is measured on Linux and Windows and shown as `skip` elsewhere.

`seedfall help` lists every command, and `seedfall help run` prints the flags and defaults of one command. `-h` and `--help` also work. All of these exit 0.

## Verifying a release

This section is for people who want proof that a download is genuine. Each automated release publishes:

- `checksums.txt`, the list of file fingerprints;
- `checksums.txt.sigstore.json`, a Sigstore bundle: a signature, made without a long-lived key, by the release workflow;
- an SBOM (a list of the software inside) for each archive;
- a GitHub build provenance attestation, a signed record of where and how the file was built.

First verify the signature on the checksums, then check an archive against them:

```sh
cosign verify-blob checksums.txt \
  --bundle checksums.txt.sigstore.json \
  --certificate-identity-regexp '^https://github.com/kunalgoesbyken/seedfall/\.github/workflows/release\.yml@refs/tags/v' \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com
sha256sum --ignore-missing -c checksums.txt
```

Or check the provenance with the GitHub CLI:

```sh
gh attestation verify seedfall_linux_amd64.tar.gz --repo kunalgoesbyken/seedfall
```

The install script checks SHA-256 only. That catches a damaged download but not a tampered release. Use one of the commands above for that.

## Cutting a release (for maintainers)

Pushing a tag that starts with `v` runs the release workflow. It builds Linux, macOS and Windows on amd64 and arm64 with GoReleaser, signs and attests the files, publishes the GitHub release, and pushes the Homebrew cask, the Scoop manifest and the Docker image.

- The repository needs a `HOMEBREW_TAP_TOKEN` secret with write access to `kunalgoesbyken/homebrew-tap`, which holds both the `Casks/` directory and the Scoop `bucket/`.
- Release notes are grouped from commit subjects that start with `Add` or `feat`, and `Fix` or `fix`.
- A tag with a prerelease suffix, such as `v0.3.0-rc1`, is marked as a prerelease. It leaves the cask, the Scoop manifest and the `latest` image alone.


<!-- docs/mutate.md -->

# Mutation testing your checks

A passing sweep only means something if your checks would notice a real problem. `seedfall mutate` weakens the simulated disk, network or clock one guarantee at a time, or changes your own source code, and tells you whether your checks catch it. Use it to find checks that are too weak.

A sweep that passes is only meaningful if your workload would notice when a guarantee breaks. `seedfall mutate` tests that directly: it weakens the simulated disk, network or clock under your nodes, one guarantee at a time, and checks whether your sweep catches it.

```sh
seedfall mutate -c seedfall.always.json -seeds 1-30
```

```
baseline: seeds 1-30 pass

  fsync_noop     killed     seed 1: client#1: stream EVENTS lost after restart, 133 acknowledged messages gone
                 file fsync returns success without making anything durable

  dirsync_noop   not exercised (the operation never ran, or has no effect in this configuration)
                 directory fsync does nothing (matters with strict_dirs)

  osync_ignored  killed     seed 1: client#1: stream EVENTS lost after restart, 133 acknowledged messages gone
                 writes to O_SYNC and O_DSYNC files are no longer synchronous

every exercised mutant was killed
```

That run is NATS JetStream (`examples/natsjs`). Both guarantees NATS relies on are protected by the workload: when either one silently stops working, acknowledged messages are lost and the sweep fails.

## Mutants

| Mutant | What breaks |
|---|---|
| `fsync_noop` | File `fsync` reports success but makes nothing durable |
| `dirsync_noop` | Directory `fsync` does nothing. Only observable with `strict_dirs`, where directory entries need it to survive a crash |
| `osync_ignored` | Writes to files opened with `O_SYNC` or `O_DSYNC` stop being synchronous |
| `fsync_corrupts` | File `fsync` makes the data durable with one bit flipped: the first byte of the last write it covers. Reads see the right data until a crash, then the flipped one |
| `rename_not_atomic` | A rename over an existing file is not durable until the next successful fsync of any file or directory on that disk. A crash before then loses both names, so neither the old nor the new version exists after the restart. A rename to a new name is unchanged |
| `truncate_not_durable` | `fsync` makes writes durable but skips truncations, including `O_TRUNC`. Reads see the shorter file until a crash, then the old length comes back with the old bytes past the new data |
| `net_drop_after_close` | When a connection is closed, the last chunk written to it that the peer has not read yet is dropped, so the peer sees end of file without it |
| `net_dup_chunk` | 5% of connection writes, chosen from the seed, arrive twice in a row |
| `monotonic_jump` | `clock_jump` faults move the monotonic clock along with the wall clock, so `time.Since` and timers see time run backwards or leap ahead. Needs `clock_jump_per_sec` |

Mutants need no changes to your code. Each one weakens only the nodes that take faults: the disk mutants their disks, the network mutants the data they receive, and `monotonic_jump` their clocks. The workload is affected only with `include_workload`, and the `finally` check never. A run with a mutant replays exactly like any other: the duplicated writes come from their own seeded stream.

Run some of them with `-only`:

```sh
seedfall mutate -c seedfall.json -seeds 1-20 -only net_dup_chunk,truncate_not_durable
```

`-md mutants.md` also writes the result as a Markdown table, for a pull request or job summary; the [GitHub Action](ci.md#verify-and-mutate) uses it. `-only` picks among these runtime mutants and cannot be combined with `-app`. Over MCP the tool is `seedfall_mutate`, with `config`, optional `seeds` (default `1-100`) and `only`. It returns each mutant's `outcome`, the `killed_by_seed` and `reason` when killed, the `seeds_passed` and how many times the operation was `weakened`.

### The new mutants on `examples/ledger`

```
$ seedfall mutate -c seedfall.json -seeds 1-20
baseline: seeds 1-20 pass

  fsync_noop            killed     seed 1: client#1: ledger total covers every acknowledged deposit: {"left":4660,"right":5506,"unacked":1831}
  ...
  truncate_not_durable  SURVIVED   20 seeds passed although the operation was weakened 5 times
                        fsync makes writes durable but not truncations, so a crash brings back the old length and the bytes past it

  net_dup_chunk         killed     seed 18: client#1: ledger total holds no deposit that was never sent: {"left":8387,"right":8119}
                        a seeded 5% of connection writes are delivered twice, which TCP never does
  ...
1 mutants survived: your workload does not notice those guarantees disappearing
```

A duplicated `ADD` is applied twice and the upper bound on the total catches it. `truncate_not_durable` survives because the ledger cuts off a torn final entry with `Truncate` at every start, so a truncation that does not persist only brings back bytes that the next recovery drops again: a survivor you can explain as equivalent. In `examples/liveness`, `rename_not_atomic` survives 991 weakenings for a similar reason: when a crash loses the client's progress file, the client resends adds the servers have already deduplicated.

## Source mutants

The mutants above break the world under your program. `-app` breaks the program itself: seedfall parses the Go files of every node package (not the workload or the `finally` check), lists every place it can make one of three changes, picks `-mutants` of them (default 10) with the first seed of the range, and rebuilds the node once per mutant through a `go build -overlay`, so your files are never touched:

| Change | What it does |
|---|---|
| `flip_comparison` | Negates one comparison: `<` and `>=`, `>` and `<=`, `==` and `!=` |
| `skip_error_return` | `if x != nil { ...; return ... }` becomes `if false && x != nil`, so the early return never runs |
| `skip_sync` | `f.Sync()` becomes a call that returns `nil` without syncing |

```
$ seedfall mutate -c seedfall.fixed.json -seeds 1-10 -app -mutants 4
baseline: seeds 1-10 pass

  server/main.go:95     SURVIVED   10 seeds passed (or the mutated code never ran)
                        complete < len(data) -> complete >= len(data)

  server/main.go:97     killed     seed 1: server#2 crashed: module closed with exit_code(2)
                        err != nil -> err == nil

  server/main.go:157    killed     seed 1: client#1: acknowledged write lost: k61=v61, server now answers "NONE"
                        err != nil -> err == nil

  server/main.go:197    SURVIVED   10 seeds passed (or the mutated code never ran)
                        cmd[0] == "PUT" -> cmd[0] != "PUT"

2 mutants survived: your workload does not notice those guarantees disappearing
```

That is `examples/kvlog`. The survivor at line 197 is a real blind spot: with the comparison flipped, the server answers every `PUT` with an error, the client counts no write as acknowledged, and nothing asserts that writes are ever acknowledged, so the sweep still passes. The survivor at line 95 only changes the condition of a `sim.Sometimes`, which records coverage and never fails a seed.

seedfall cannot tell whether a mutated line ever ran, so a source mutant has no "not exercised" verdict: a survivor may be dead code. A mutant that does not compile (for example a `Sync` method with no error result) is reported as `did not build` and does not count as a survivor. The same seed range and `-mutants` count pick the same mutants every time. Each mutant costs one `go build` and one sweep, so start with a small count. `seedfall verify -app-mutants N` adds the same mutants to a proof ([verify.md](verify.md)), and over MCP `seedfall_mutate` takes `app` and `mutants`.

## Verdicts

- **killed**: some seed failed, so your workload notices this guarantee disappearing. That is the goal.
- **SURVIVED**: every seed passed even though the operation was weakened. Either your checks miss the broken guarantee (acknowledged data loss, a duplicated request, a timeout computed from a clock that ran backwards), or your faults never hit the window where it matters. Raise `crash_per_sec` or `crash_on_io`, lengthen the run, or strengthen the invariant. `seedfall mutate` exits non-zero when any mutant survives.
- **not exercised**: the weakened operation never ran, or had no effect in this configuration. For example, `dirsync_noop` without `strict_dirs`.

The baseline must pass first; otherwise mutants would be killed by the existing bug.


<!-- docs/networking.md -->

# Networking

Nodes in seedfall talk over a simulated network, so seedfall can delay, drop and cut messages between them. This page explains the two ways to connect your code to it: call seedfall's `sim.Listen` and `sim.Dial`, or leave your code alone and turn on `net_overlay`. Read it when nodes cannot reach each other or you are wiring up a new project.

seedfall gives every node a simulated network: ordered TCP byte streams and unordered UDP datagrams with seeded latency, per-link latency overrides, partitions that hold TCP traffic until they heal and drop UDP datagrams, one-way clogs that stop, jam or slow a link, slow nodes, and connection resets when a peer crashes or a reset fault fires. Node names are host names, so a node named `server` is reachable at `server:7000`.

How each network fault behaves and how to configure it is in [faults.md](faults.md#network-faults).

There are two ways to connect your code to the simulated network.

## Option 1: `sim.Listen` and `sim.Dial`

```go
import "github.com/kunalgoesbyken/seedfall/sim"

ln, err := sim.Listen("tcp", ":7000")
conn, err := sim.Dial("tcp", "server:7000")
pc, err := sim.ListenPacket("udp", ":7100")
```

`sim.Listen` and `sim.Dial` take `tcp`, `tcp4` or `tcp6`, and `sim.ListenPacket` takes `udp`, `udp4` or `udp6`; any other network, such as `unix`, is an error in the simulator and outside it, so a node does not behave differently in production. They return a standard `net.Listener`, `net.Conn` and `net.PacketConn`. Outside the simulator they call `net.Listen`, `net.Dial` and `net.ListenPacket`, so production builds are unaffected. This works on every Go version seedfall supports, and it is how most of the examples are written. A connection also has `CloseRead` and `CloseWrite`, reached with a type assertion to an interface that declares them.

If a library takes a custom dialer or listener, pass these in. hashicorp/raft's `NewNetworkTransport` accepts a `StreamLayer` built on them, and NATS clients accept `nats.SetCustomDialer`.

## Option 2: zero code changes with `net_overlay`

```json
{ "net_overlay": true }
```

With `net_overlay`, unmodified programs that call `net.Listen`, `net.Dial`, `net.ListenPacket`, `net.ListenUDP` and `net.DialUDP` use the simulated network, and so do `net/http` servers and clients, and libraries such as hashicorp/raft's stock `NewTCPTransport` and hashicorp/memberlist. `examples/httpkv` is a plain `net/http` server and client with no seedfall imports in the server, and `examples/memberlist` is an unmodified memberlist cluster gossiping over simulated UDP.

How it works: on `wasip1`, Go's `net` package uses an in-process fake network. At build time, seedfall reads that package from your own `GOROOT` and builds an overlay with `go build -overlay`. It makes four exact-text patches: `socket()` is renamed so a seedfall version can wrap it, `accept()` gets a hook for seedfall listeners, and `setReadBuffer` and `setWriteBuffer` accept any size for simulated sockets, because the simulated queues have no size. Then it adds one file to package `net` that sends TCP and UDP sockets to the simulator. Node names resolve through a simulated `/etc/hosts`, and `localhost` means the node itself.

If a future Go release changes those internals, the build fails with a clear "this Go version is not supported yet" error instead of misbehaving. Verified on Go 1.27.

## Addresses, port 0 and half-close

Both options behave the same way:

- Listening or binding on port 0 picks a free port from `49152`..`65535`, in a sequence kept per node, and `Addr()` or `LocalAddr()` returns the real port.
- Every dial takes its own port from the same range, so an accepted connection's `RemoteAddr()` is the dialer's real address and matches the dialer's `LocalAddr()`. Under `net_overlay` an address is the node's IP from the simulated `/etc/hosts`, such as `10.77.0.2:49152`. Through `sim` it is the node name, such as `client:49152`.
- `CloseWrite` sends EOF to the peer after the data already written, and the other direction keeps working. Writing after `CloseWrite` fails with `EPIPE`. `CloseRead` makes every later read return EOF.

## UDP

A UDP socket on one node talks to any other through the same link table as TCP, and every datagram draws its own latency, so datagrams overtake each other whenever the latency range allows it.

| Condition | What happens to a datagram |
|---|---|
| Partition, or clog `stop` or `jam`, in the sending direction | Dropped. Nothing holds it for the heal |
| Clog `slow` | Arrives `clog_delay` later |
| Slow node | Latency is stretched, as for TCP |
| No socket bound to the address when it is sent, or one connected to a different address | Dropped. A connected sender gets the equivalent of ICMP port unreachable: unless a partition or clog cuts the path back, its next read or send after a round trip fails with `ECONNREFUSED`, once. An unconnected sender hears nothing |
| `udp_loss` | Dropped, recorded as a `udp_drop` fault |
| `udp_dup` | Delivered twice with independent latencies, recorded as a `udp_dup` fault |

Datagram boundaries are kept: a read returns one datagram and discards whatever does not fit in the buffer. A socket's queue has no limit, so `SetReadBuffer` and `SetWriteBuffer` succeed and change nothing, and a sender is never blocked. A crash closes the node's sockets and drops what was queued for them, and `net_reset` faults do not touch UDP, because a datagram socket has no connection to reset. Multicast is not simulated, and `WriteMsgUDP` with out-of-band data and raw reads with flags return `ENOTSUP`.

## Seeing the traffic

`-net-trace` on `run`, `replay`, `logs` or `debug` adds every dial, accept, message sent and message read to the trace, with its connection, size, send and arrival time, and whether a partition or clog held it. UDP sockets show up as `binds udp`, each datagram as `udp <socket>` lines, and a lost one says why. Every failure's `timeline.html` draws the same messages as arrows between nodes. See [timelines and logs](timeline.md).

## Without either

Go's unmodified `net` package on `wasip1` is an in-process fake. A `net.Listen` succeeds but can never be reached from another node. If nodes cannot reach each other, enable `net_overlay` or switch to `sim`.


<!-- docs/properties.md -->

# Properties, linearizability and determinism

A property is something your system must always (or eventually) get right, such as "an acknowledged write is never lost". This page covers how to write properties with the `sim` package, how to check recovery, and how to check a recorded history of operations for linearizability (concurrent operations behaving as if they happened one at a time, in some order). Use it when you write or improve your workload.

## Failing a run

```go
sim.Fail("replica diverged")
sim.Assert(got == want, fmt.Sprintf("acknowledged write lost: %s=%s", key, want))
```

`Fail` and `Assert` stop the run with a message. Outside the simulator they panic, so the same code works in ordinary tests.

## Properties with coverage

A green sweep only means something if the dangerous paths actually ran. Properties are tracked across every seed and printed after a sweep:

```go
sim.Always(len(log) >= committed, "log never shrinks below the commit index", len(log), committed)
sim.Sometimes(tornTail, "recovery found a torn tail")
sim.Reachable("a node restored from a snapshot")
sim.Unreachable("two leaders in the same term", term)
```

| Function | Fails the seed when | Fails the sweep when |
|---|---|---|
| `Always(cond, msg, details...)` | `cond` is false | it was never reached |
| `AlwaysOrUnreachable(cond, msg, details...)` | `cond` is false | |
| `Unreachable(msg, details...)` | it is called | |
| `Sometimes(cond, msg, details...)` | | it was never reached, or `cond` was never true |
| `Reachable(msg, details...)` | | it was never reached |
| `Eventually(cond, msg, within)` | `cond()` is still false after `within` of virtual time, as a `liveness` failure | it was never reached |

```
property       seeds reached  seeds true
  sometimes             400         400  a crash interrupted the workload
  sometimes             400         172  recovery found a torn tail

ok  400 seeds passed (0 hit the time horizon) in 1m32s
```

A property is identified by its message, so keep messages constant and pass changing values as details. Details appear in the failure message but do not create a new property. A `Sometimes` that is never satisfied means your faults never reached that path: raise a fault rate, lengthen `duration`, or change the workload.

Properties are evaluated in any node, not only the workload. Outside the simulator, `Always`, `Unreachable` and `Eventually` panic on violation and the others do nothing.

### Numeric and grouped properties

The comparison and grouped forms match the [Antithesis SDK](antithesis.md) and say more than a plain boolean:

```go
sim.AlwaysGreaterThanOrEqualTo(len(log), committed, "log never shrinks below the commit index")
sim.SometimesGreaterThan(backlog, 100, "the queue backs up past 100")
sim.AlwaysSome(map[string]bool{"primary": p >= 0, "backup": b >= 0}, "some replica answers")
sim.SometimesAll(map[string]bool{"crashed": crashed, "recovered": recovered}, "a crashed node caught up")
```

| Function | Same as |
|---|---|
| `AlwaysGreaterThan(left, right, msg, details...)`, also `OrEqualTo` | `Always(left > right, ...)` (`>=`) |
| `AlwaysLessThan(left, right, msg, details...)`, also `OrEqualTo` | `Always(left < right, ...)` (`<=`) |
| `SometimesGreaterThan(left, right, msg, details...)`, also `OrEqualTo` | `Sometimes(left > right, ...)` (`>=`) |
| `SometimesLessThan(left, right, msg, details...)`, also `OrEqualTo` | `Sometimes(left < right, ...)` (`<=`) |
| `AlwaysSome(named, msg, details...)` | `Always` that at least one value in the `map[string]bool` is true |
| `SometimesAll(named, msg, details...)` | `Sometimes` that every value in the map is true |

`left` and `right` are any Go number type. On failure the details are JSON, `{"left":41,"right":40}` for the comparisons and the named booleans for the grouped forms, with any extra details under `"details"`.

For the comparisons seedfall also keeps a margin: `left - right` for `GreaterThan`, `right - left` for `LessThan`, so a positive margin is on the true side. An `always` comparison reports its smallest margin over every hit and seed, which is how close it came to failing; a `sometimes` comparison reports its largest, which is how close it came to being true. A margin of 0 on an `OrEqualTo` assertion means the boundary was hit exactly:

```
property       seeds reached  seeds true
  always                 20          20  no acknowledged add is lost  (smallest margin 0)
  sometimes              20           0  the queue backs up past 100  (largest margin -37)  <- never true (client/main.go:41)
```

The margin is also in `-json`, the MCP `seedfall_run` result (`margin`) and the HTML report.

### Events

```go
sim.Event("client resumed", map[string]int{"next add": done})
```

`sim.Event(name, details)` records a moment in the run without asserting anything. The details are encoded as JSON. Each event is a trace line (`event client resumed from client#2: {"next add":39}`), so it sits in order between the faults and the program output, and `seedfall_replay` returns the run's events as a list. Outside the simulator it does nothing. `lifecycle.SendEvent` from the Antithesis SDK is recorded the same way.

### The property catalog

Before a sweep, seedfall scans the Go source of every node and the workload for calls to these functions, including the numeric and grouped forms, with a constant message, so it knows about properties even if no seed ever executes them. A property that is never reached is reported with its location and fails the sweep:

```
property       seeds reached  seeds true
  reachable               0           0  compaction ran  <- never reached (node/main.go:12)
  always                  5           5  invariant holds

FAIL 1 properties were never reached or never true in 5 seeds
```

An `Always` that never runs proves nothing, so it has to be reached too. Calls whose message is not a string literal are still tracked once they run, but they cannot be cataloged in advance.

## Liveness: recovery and finally checks

Safety properties say nothing bad happens. Liveness properties say something good eventually happens, and they can only be checked once the faults stop. A cluster with a stuck leader, or a node that never reconnects after a network blip, passes every safety check: it just stops making progress, and a run that stops making progress only hits the time horizon.

Liveness mode adds a recovery phase to every run:

```json
"duration": "20s",
"liveness": { "within": "10s" }
```

For the first `duration`, faults fire as usual. Then the recovery phase starts: every remaining fault is suppressed, every partition, clog and slowdown ends, paused nodes resume, and crashed nodes restart at once instead of waiting out their downtime. From then on the workload has `within` of virtual time to finish. If it does not, the run fails with class `liveness`:

```
FAIL seed 1 at t=15s (2255 scheduler steps, 404ms real)
  liveness: client did not finish within 10s of the recovery phase starting at 5.000s

trace:
    4.172s  fault reset 1 connections of primary#1
    5.000s  recovery: the fault period ended; faults stop, partitions, clogs, slowdowns and pauses end, 0 crashed nodes restart now, everything must finish by 15.000s
   15.000s  FAIL  liveness: client did not finish within 10s of the recovery phase starting at 5.000s
```

That failure shrinks like any other: `seedfall shrink` cuts it to the faults that leave the system stuck, here a single connection reset. Liveness failures are grouped apart from safety failures in reports, as `liveness · client`.

### Eventually

`sim.Eventually` checks a condition that must become true, rather than one that must always hold:

```go
sim.Eventually(func() bool { return leader() != "" }, "a leader is elected", 5*time.Second)
```

It calls `cond` until it returns true, sleeping `within/100` of virtual time between calls, and returns true. If `cond` is still false after `within`, the run fails with class `liveness`, the property's message and `not true within 5s`. It is a property like the others: it is cataloged from the source, shows up in the coverage table as `eventually`, and fails the sweep if no seed ever reaches it. Outside the simulator it uses real time and panics when the condition never holds.

### Finally checks

A `finally` program runs once, after every workload has exited 0, the way Antithesis runs `finally_` commands:

```json
"workload": { "name": "client", "pkg": "./client" },
"finally": { "name": "check", "pkg": "./check" }
```

When the last workload exits, the recovery phase starts (if `liveness` has not started it already) and then the check starts. It never takes faults, it sees every node through a healed network, and the run passes when it exits 0. With `liveness`, it too must finish within `within` of the recovery phase. Its properties are cataloged and counted like the workload's, so this is the place for end-state checks: replicas converge, every acknowledged write is readable, nothing was applied twice.

```go
var p, b int
sim.Eventually(func() bool {
	p, b = count("primary:7000"), count("backup:7000")
	return p >= 0 && p == b
}, "primary and backup report the same count", 5*time.Second)
sim.AlwaysLessThanOrEqualTo(p, adds, "no add is applied twice")
sim.AlwaysGreaterThanOrEqualTo(p, adds, "no acknowledged add is lost")
```

[`examples/liveness`](../examples/liveness) shows all three: a primary that never reconnects to its backup fails liveness mode, a server without request deduplication fails the finally check once the client is crashed mid-request, and the fixed pair passes.

### Quiet periods

`sim.QuietFor(d)`, called from any node, starts a quiet period from inside the program: it suppresses every fault for `d` of virtual time and heals any active partition, lifts every clog and ends every slowdown. Unlike the recovery phase, nodes that are already down still restart on schedule. The trace records each suppressed fault. `examples/raftkv/client` uses this to check that the cluster recovers after the workload.

```go
sim.QuietFor(10 * time.Second)
started := time.Now()
waitUntilServed()
sim.Always(time.Since(started) < 10*time.Second, "cluster serves reads again within the quiet period")
```

## Faults at your own code sites

`sim.Buggify("site")` returns true at seeded points when `faults.buggify` is on, so the simulator can force a retry, an error return or a delay inside your code. A quiet period stops sites from firing too. See [buggify.md](buggify.md).

## Waiting for setup

With `"faults_after_setup": true`, no faults fire until some node calls `sim.SetupComplete()`. Use it when bootstrapping, such as electing the first leader or creating a stream, is not what you want to test.

## Workload size

Wrap the number of operations your workload performs in `sim.Budget` so that `seedfall shrink` can make it smaller:

```go
writes := flag.Int("writes", 200, "number of writes")
flag.Parse()
n := sim.Budget(*writes)
for i := range n {
	// one operation
}
```

`sim.Budget(n)` returns `n` in normal runs and outside the simulator. When a shrunk schedule sets `ops`, it returns at most that many, and the trace says so: `client#1: sim.Budget capped at 63 of 200 operations`. Shrink only tries this when a node called `sim.Budget` in the failing run, and bisects the cap down to the fewest operations that still fail the same way. Use the returned value everywhere the count matters, including messages and checks such as "all `n` writes were acknowledged". `examples/kvlog/client` does this.

## Linearizability

Workloads can record operations from any number of concurrent clients. When the workload finishes, seedfall checks the history with [Porcupine](https://github.com/anishathalye/porcupine) against the model named in `seedfall.json` (`kv` when there is no `checker`). Linearizability checking is NP-complete, and a history with many operations of unknown outcome can take Porcupine longer than any test should run. After 30 seconds of real time seedfall gives up on that seed, notes "gave up checking N operations for linearizability" in the trace, and neither passes nor fails it on linearizability. A seed that hits this limit says nothing about the history, so keep workloads short enough to check, or give fewer operations an unknown outcome.

```go
op := sim.Put(clientID, "k1", "v7")
reply, err := client.Put("k1", "v7")
switch {
case err != nil:          op.Unknown()
case reply == "redirect": op.Failed()
default:                  op.Ok("")
}

op = sim.Get(clientID, "k1")
value, err := client.Get("k1")
if err != nil {
	op.Unknown()
} else {
	op.Ok(value)
}
```

- `Ok(output)` means the operation took effect. For a read, `output` is what was read, with `""` meaning absent.
- `Unknown()` means it may or may not have taken effect, such as a timeout. Unknown writes may land any time after they start; unknown reads are dropped.
- `Failed()` means it definitely did not take effect, such as a redirect to the leader.

On a violation, seedfall writes an interactive timeline to `.seedfall/seed-N.history.html`.

### Other models

`sim.Put` and `sim.Get` are shorthands for `sim.Invoke(client, f, key, value)`, which records any operation. Pick the model in `seedfall.json`:

```json
"checker": { "model": "queue" }
```

| Model | Operations: `sim.Invoke(client, f, key, value)`, then `op.Ok(output)` | Checked as |
|---|---|---|
| `kv` (default) | `put` with a string value; `get` with the string read as output, `""` for absent | A linearizable register per key |
| `cas` | `put` and `get` as in `kv`, plus `cas` with value `[]string{old, new}` and output `true` if it swapped, `false` if the value was not `old` | A linearizable compare-and-set register per key, for locks and leases |
| `append` | `append` with a string value; `read` with the whole list as output, a `[]string` | A linearizable append-only log per key |
| `queue` | `enqueue` with a string value; `dequeue` with the item taken as output, `""` when empty | A linearizable FIFO queue per key: no item lost, delivered twice or out of order |
| `set` | `add` with a string value; `read` with the members as output, a `[]string` in any order | A linearizable grow-only set per key |
| `counter` | `add` with an integer value; `read` with the integer read as output | A linearizable counter per key |
| `list-append` | `sim.Txn(client, mops...)`, see [transactions](#transactions) | Serializability, with Elle-style anomaly detection |

Every model checks each key on its own. An unknown `dequeue` stays in the history with any result allowed, since it may have removed an item; unknown pure reads (`get`, `read`) are dropped. An operation the model does not have, or an input or output of the wrong type, fails the run as an `assert` that names the operation, for example `history (model queue): operation "put" is not one of dequeue, enqueue`, so a typo cannot silently weaken the check.

```go
op := sim.Invoke(client, "cas", "leader-lock", []string{"", me})
swapped, err := locks.CompareAndSwap("leader-lock", "", me)
if err != nil {
	op.Unknown()
} else {
	op.Ok(swapped)
}
```

### Transactions

With `"checker": {"model": "list-append"}`, workloads record transactions over append-only lists, the workload Elle uses, and seedfall infers the dependencies between them:

```go
mops := []sim.Mop{sim.Read("x"), sim.Append("y", "c1-17")}
op := sim.Txn(client, mops...)
err := db.Txn(func(tx *Tx) {
	mops[0].Value = tx.List("x")
	tx.Append("y", "c1-17")
})
if err != nil {
	op.Unknown()
} else {
	op.Ok(mops)
}
```

`Ok` takes the same micro-ops back, with every read's `Value` set to the list it returned (a `[]string`). Appended values must be unique per key. seedfall takes each key's version order from its longest read, builds write-write, write-read and read-write edges between transactions, finds the strongly connected components with Tarjan's algorithm, and searches them breadth-first for one short cycle of each kind:

| Anomaly | Meaning |
|---|---|
| `G0` | A cycle of write-write edges: two transactions' appends interleave in different orders on different keys |
| `G1a` | A committed transaction read an append made by a transaction that `Failed()` |
| `G1b` | A transaction read a list ending in an intermediate append of another transaction, which appended to that key again later |
| `G1c` | A cycle of write-write and write-read edges with at least one write-read edge |
| `G-single` | A cycle with exactly one read-write edge, such as read skew |
| `G2` | A cycle that needs two or more read-write edges, such as write skew |
| `internal` | A transaction's read does not match its own earlier reads and appends |
| `incompatible-order` | Two reads of a key where neither is a prefix of the other, such as after a lost append |
| `duplicate-elements` | A read that contains the same element twice |
| `duplicate-append` | The same value appended to a key twice, which makes the history impossible to analyse |
| `garbage-read` | A read returned an element nobody appended |

A history with any of these fails as `isolation`, with one explained example of each kind in the trace:

```
G-single: T4 -rw z-> T0 -wr z-> T6 -ww y-> T4; T4 (client 4, ok) [r z ["4-0"], append y "4-1", r y ["3-0" "1-1" "4-1"]]; T0 ...
FAIL  history of 121 transactions is not serializable: G-single, G2, internal
```

`Tn` is the transaction's `id` in the history file. The check is serializability, not strict serializability: real-time order between transactions is not used. Transactions that returned `Unknown()` or never returned count as possibly committed: their appends are used once someone reads them, and their reads are ignored.

### History files

Every failing `run`, `replay` and `shrink`, and every passing `replay`, writes the recorded history to `.seedfall/seed-N.history.jsonl`, one event per line in Jepsen's invoke and completion shape:

```json
{"index":0,"type":"invoke","process":1,"f":"enqueue","key":"q","value":"1-0","time":8,"id":0}
{"index":4,"type":"ok","process":1,"f":"enqueue","key":"q","value":null,"time":648261,"id":0}
```

`type` is `invoke`, then `ok`, `info` (unknown) or `fail`; an operation that never returned has no completion line. `time` is virtual nanoseconds, and `id` pairs an invocation with its completion. A completion's `value` is the output for `ok` and the input otherwise. For `list-append`, `value` holds the micro-ops as `[f, key, value]` triples, the same layout as Elle's list-append micro-ops (seedfall's keys and values are strings). Over MCP, the failure view names the files as `history_file` and `timeline_file`.

Re-check a stored history, or check it against a different model, without running anything:

```sh
seedfall check -history .seedfall/seed-1.history.jsonl -model queue
```

It prints the verdict and every anomaly, writes the timeline next to the history file (or to `-timeline`) on a linearizability violation, and exits 1 when the history fails. The MCP tool is `seedfall_check`.

### Your own Porcupine model

For a data type none of the models cover, read a history file in Go and check it with your own [Porcupine](https://github.com/anishathalye/porcupine) model:

```go
f, _ := os.Open(".seedfall/seed-1.history.jsonl")
ops, err := engine.ReadHistory(f)
ok := porcupine.CheckOperations(myModel, engine.PorcupineOperations(ops))
```

`PorcupineOperations` drops failed operations and gives unknown and pending ones a return time after the end of the history. Each operation's `Input` and `Output` are its `engine.HistoryOp`, with the raw JSON `Value` and `Output` and the `Status`; your `Step` should accept any output when `Status` is not `ok`.

## Determinism check

```sh
seedfall run -seeds 1-200 -check
```

Every seed runs twice, and the sweep fails if the two runs diverge. Run it in CI to make sure nothing in your program escapes the simulator.

The comparison does not wait for a difference to reach the trace. Every run keeps a running hash over its host calls: clock reads, `random_get` lengths, sleeps and `poll_oneoff`, file opens, stats, reads, writes, truncates, syncs, renames, links, symlinks and directory changes, `mmap`, `msync` and `munmap` calls, network listens, dials, accepts, reads, writes and closes, and the `sim` property, event, history, `Buggify`, `SetupComplete`, `QuietFor` and `Budget` calls, each with its node instance, arguments and virtual time. The hash is saved every 4,096 calls. When the two runs differ, seedfall finds the first window of 4,096 calls where they differ, runs the seed twice more recording that window, and reports the first call that differs, in the form `host call N: <call in one run> vs <call in the other>, after <last common call>; host calls <window> (...)`. Each call reads as instance, call, target, argument and virtual time, for example `server#1 random_get(8) at 1.204s` or `server#1 fd_write data/log(37) at 1.204s`. Every `-check` failure is a `nondeterminism` failure.

If the extra runs do not reproduce the difference, the report names the window instead. If the host calls agree but the traces do not, it falls back to the first differing trace line.

The final hash is printed at the end of `seedfall replay` (`determinism hash 4c9ab008f72df649 over 9126 host calls`) and is the `determinism_hash` field of every `-json` seed line and of `seedfall_replay`. The hash covers only simulated values, so two machines that build the same guest binary should get the same hash for the same seed; comparing the field from CI runs on different machines checks that. A different Go toolchain or source tree produces a different binary and may change the hash.


<!-- docs/reports.md -->

# Triage reports

A big sweep can find many failing seeds that come from only a few bugs. Reports group them into findings, label each one as new or old, remember history between runs, and can post to Slack, Discord or GitHub. Use this page when you run seedfall at scale or in CI and want to triage instead of reading one failure at a time.

```sh
seedfall run -c seedfall.json -seeds 1-500 -report .seedfall/report.html
```

With `-report`, a sweep keeps going after the first failure, groups every failing seed into findings, and writes an HTML report plus a JSON version next to it (`report.json`). The `-report` path must not end in `.json`, since that is where the JSON version goes. The terminal prints a summary:

```
16 of 60 seeds failed, 1 findings, in 4.867s
  new       assert · client                             16 seeds  e.g. seed 1  bug
report: .seedfall/report.html
```

## Findings

Failures are grouped by what failed, not by message text: the failure class (`property`, `assert`, `crash`, `exit`, `watchdog`, `deadlock`, `liveness`, `linearizability`, `isolation`, `nondeterminism`), the node, and, for properties, the property name. Use `sim.Always` with a constant message to get one finding per invariant.

For each finding the report shows:
- how many seeds failed and the rate, with findings under 1% marked rare;
- up to ten example seeds;
- ready-to-run `replay` and `shrink` commands;
- the faults before the failure and the trace of the lowest failing seed. seedfall re-runs that seed to get them, which works because replays are exact;
- that seed's [timeline](timeline.md), embedded from its artifact folder, with a link to open it on its own.

## Classification

Every finding, and the failure `seedfall run` stops at, gets a class that says whether it is worth blocking on:

| Class | Meaning |
|---|---|
| `bug` | Replaying the seed fails again with the same trace. A real, reproducible failure of the system under test |
| `nondeterministic` | The replay diverges from the original run: something in the harness or the system leaks host nondeterminism. The first diverging trace line is shown |
| `timeout` | The real-time watchdog fired. This depends on host speed and load, not only on the seed. With `preempt.loops` a busy loop fails on `liveness` instead |

```
FAIL seed 1 at t=2.892s ...
class: bug
```

Classification replays only the failure that `run` reports and one representative seed per finding, so it adds one run per finding, never one per seed. It appears in the terminal summary, in the HTML report, as `classification` in `report.json`, and in the MCP `seedfall_run` and `seedfall_replay` results, so CI and agents can block on `bug` and quarantine the rest.

## History: new, ongoing, resolved, regressed

Every report appends a line to `.seedfall/history.jsonl`, keyed by config path. Findings are classified against that history:

| Status | Meaning |
|---|---|
| `new` | Never seen before for this config |
| `ongoing` | Seen in earlier runs and still failing |
| `not seen` | Absent from this run, but not enough clean seeds yet to be sure it is fixed |
| `resolved` | Absent for enough consecutive clean seeds to be 95% confident it is fixed |
| `regressed` | Failing again after it was resolved |

"Enough" depends on how often the finding used to fail. A finding that failed in a fraction *p* of seeds needs *n ≥ ln(0.05) / ln(1 − p)* clean seeds, counted across runs since it was last seen. A bug that failed 1 seed in 4 is resolved after 11 clean seeds; one that failed 1 seed in 100 needs 299.

```
  new       assert · client          16 seeds  e.g. seed 1
  ongoing   assert · client          15 seeds  e.g. seed 61
  not seen  assert · client          not seen in 5 seeds, but 11 are needed to be 95% sure it is fixed
  resolved  assert · client          not seen in 20 seeds since it failed 15 of 60
  regressed assert · client           6 seeds  e.g. seed 1
```

A line of the file that is not valid JSON is an error that names the file and the line (`.seedfall/history.jsonl line 12: ...`), not something skipped, since skipping it would make findings look new or resolved by mistake. Delete that line to carry on.

Keep `.seedfall/history.jsonl` between CI runs (cache or commit it) to get this classification on every pull request. The [GitHub Action](ci.md#history-between-runs) caches it for you.

## Reading findings back

`seedfall findings` reads the last report and the run history without running anything:

```sh
seedfall findings                          # .seedfall/report.html
seedfall findings -status new,regressed    # only what needs attention
seedfall findings -report ci/report.json -json
```

```
.seedfall/report.html: 1 of 6 seeds failed (seeds 1-6 of seedfall.always.json), 3 runs in history
  new       assert · client                              1 seeds  16.67%  e.g. seed 1
            client#1: acknowledged write lost: k96=v96, server now answers "NONE"
            replay: seedfall replay -c seedfall.always.json -seed 1
```

It lists each finding with its status, failing seeds, rate, example seed, reason and replay command, then the earlier findings this run did not see (`resolved` or `not seen`) and the properties that were never reached or never true. `-status` takes a comma-separated list of the statuses above and applies to both lists, `-history` points at a history file other than the one the report names, and `-json` prints the same object the `seedfall_findings` MCP tool returns, with every finding's example failure, trace tail, shrink command and artifacts folder, and every run of that config in the history.

## Properties and fault profile

The report also lists every property with how many seeds reached it and how many saw it true, flagging properties that were never reached or never true, and the fault profile the sweep ran with. Its header names the seedfall version, the Go version and, when the config is in a git repository, the commit it was run at. Schedules pinned with `seedfall pin` are replayed before the sweep and listed in a **Regressions** section ([pinned regressions](verify.md#pinned-regressions)); a regression that fails again fails the run.

## Exploration and throughput

A report from `seedfall run -until-novelty` or `seedfall explore -report` has an **Exploration** section: one row per batch or round with the runs so far, the new signals and functions it added, and the corpus size, so you can see where coverage flattened out, plus why it stopped. Every report's header and JSON (`seeds_per_second`, `virtual_seconds_per_wall_second`) also state throughput. A finding that needs a schedule to reproduce, as `seedfall explore` findings do, carries `schedule_file` in its example and its replay and shrink commands use it; `seedfall verify -report` replays that schedule instead of the bare seed ([explore.md](explore.md)).

## Utilization

A report from `seedfall run` has a **Utilization** section (`utilization` in `report.json`, in the `-json` summary and in the `seedfall_run` result) that answers whether to keep sweeping:

- `batches` splits the seeds that ran into up to ten ranges of nearly equal size, with how many new property outcomes each added. An outcome is a property being reached, being true or being false, and it counts toward the lowest seed that showed it, so the table is the same whatever order parallel runs finished in.
- `speedup_min`, `speedup_median` and `speedup_max` are virtual seconds per real second for one seed, including time spent waiting for a CPU under `-j`.
- `advice` is one sentence, also printed as `utilization:` at the end of the run, saying whether the last batches still added outcomes: more seeds are likely to help if the last batch did, may help if a new outcome came in the later half, and are unlikely to if the later half was quiet. Under ten seeds it says there are too few to compare. It is a heuristic over property outcomes only: it cannot see a bug no property or invariant catches, so read `No new property outcome` as "this config has stopped widening coverage", not as "no bugs remain".

`seedfall explore` reports have the Exploration section instead, because its runs are branches of earlier runs rather than a seed range.

On a terminal, `seedfall run` also shows a progress line on stderr, updated every second and erased when the sweep ends: seeds done, seeds per second, failures, estimated time left and virtual speedup. With `-until-novelty` the estimate is an upper bound, since the sweep can stop early. It is off with `-json`, with `-v`, and when stderr is not a terminal, so piped output and CI logs stay clean.

## Failure artifacts

Every failure seedfall reports gets a folder you can attach to an issue or upload from CI:

```
.seedfall/failures/seedfall.always-seed-1/
  report.json            what failed, classification, seedfall and Go versions, config hash, commit, replay command
  trace.txt              the full trace
  faults.json            the run's fault schedule, replayable with seedfall replay -faults
  history.jsonl          the recorded operations, when the workload records any
  linearizability.html   the timeline, on a linearizability violation
  timeline.html          a space-time diagram of nodes, messages, faults and operations with a trace explorer
  timeline.mmd           the same run as a Mermaid sequence diagram
  disk/<node>/           each node's durable disk image at the failure, as inspect -out exports it
```

`timeline.html` and `timeline.mmd` are described in [timelines and logs](timeline.md). The HTML triage report embeds each finding's `timeline.html` under the finding, linked relative to the report, so keep the report and `.seedfall/failures/` together when you move or upload them.

seedfall writes it by replaying the failing seed once more and capturing the disks at the failure, so it costs one run per reported failure, not one per seed. `seedfall run` writes it for the failure it stops at, `run -report` for the example seed of each finding (the report links it), `replay` for a failing replay, `shrink` for the minimal schedule, and a failing [pinned regression](verify.md#pinned-regressions) for itself. The folder is named after the config and the seed, `<config>-seed-N`, so two configs in one directory keep separate folders. `<config>` is the file name without `.json`, then `.<profile>` for a profile and `.set-<hash>` for `-set` overrides, a short hash of the overrides in order, as in `seedfall.fixed.set-1a2b3c4d-seed-2`. A run from the seed alone goes to `<config>-seed-N`; a replay from a schedule file to `<config>-seed-N-schedule`, a shrunk schedule to `<config>-seed-N-shrunk` and a pinned one to `<config>-seed-N-pinned`, so they do not overwrite each other. A new failure of the same seed replaces the folder. `run -json` writes artifacts only for failing regressions, not for every failing seed.

`report.json` has `reproduced`, which is false when the replay did not fail the same way as the reported run, `classification` ([above](#classification)), `seedfall_version` (from the binary's build information), `config_sha256` (of the resolved config after `extends`, the profile and `-set`, plus the bytes of every file seeded onto a node's disk), `commit` (`git rev-parse HEAD` in the config's directory, so uncommitted changes are not reflected) and `replay`, a command that replays `faults.json` exactly:

```sh
seedfall replay -c seedfall.always.json -seed 1 -faults .seedfall/failures/seedfall.always-seed-1/faults.json
```

Over MCP, failures from `seedfall_run`, `seedfall_replay` and `seedfall_shrink` carry the folder as `artifacts_dir`.

## Notifications and issues

Two commands turn a report into alerts and issues, so a nightly sweep needs no glue code:

```sh
seedfall report notify -report .seedfall/report.html -webhook "$SEEDFALL_WEBHOOK" -link "$CI_RUN_URL"
seedfall report issue  -report .seedfall/report.html -repo owner/name
```

`report notify` posts one message with the report's `new` and `regressed` findings, each with its failing seeds, rate, example seed, reason and replay command, to an incoming webhook. The body is `{"text": ..., "content": ...}`, the fields Slack and Discord incoming webhooks read, and the message is cut to Discord's 2000-character limit with a count of the findings left out. `-webhook` defaults to `$SEEDFALL_WEBHOOK`, and errors never print the URL, which holds the webhook's secret. Each finding sent is recorded in `.seedfall/history.jsonl` against the report it came from, so posting the same report twice sends nothing the second time; an `ongoing` finding is never sent. Because new and regressed come from that history, keep the file between CI runs (see [above](#history-new-ongoing-resolved-regressed)), or every run's findings are new and every run notifies. `-dry-run` prints the message instead.

`report issue` files one GitHub issue per finding with the [`gh` CLI](https://cli.github.com), titled `seedfall finding: <key>`, for example `seedfall finding: assert · client`. The body has the counts, status and class, the reason, the replay and shrink commands, the example seeds, the faults before the failure, the trace tail, the artifacts folder, and the seedfall version, commit and Go version. Before filing, it reads the titles of the repository's 1000 most recent open issues and skips a finding whose title is among them, so a finding has one open issue whether or not the history is saved, and gets a new one if it comes back after its issue was closed. `gh` needs to be logged in, or `GH_TOKEN` set, with permission to write issues. `-dry-run` prints each issue without calling `gh`.

The HTML report has a **Copy issue markdown** button on every finding with the same body, and the text itself under it, for filing by hand in any tracker.

## GitHub

Two more commands read a report for GitHub, and the [GitHub Action](ci.md#github-actions) runs both:

```sh
seedfall report github  -report .seedfall/report.html
seedfall report comment -report .seedfall/report.html -repo owner/name -pr 12 -marker storage -link "$RUN_URL"
```

`report github` prints one `::error` workflow command per problem, most urgent first: pinned regressions that fail again, regressed, new and ongoing findings, then properties that were never reached or never true. A finding from a [property](properties.md) with a constant message, and an unmet property, carry the `file` and `line` of the call, as a path relative to the working directory. Run it from the repository root. A location outside that directory, such as a dependency in the module cache, is left off. It then appends `failing-seed` and `findings` to `-output`, default `$GITHUB_OUTPUT`, or prints them when neither is set. `-md file` also writes the Markdown that `report comment` would post, for a job summary or a later `report comment -body file`.

`report comment` posts the report to a pull request as a [`gh`](https://cli.github.com) comment, or `-body file` posts a Markdown file instead, such as a `verify -md` proof, with `-link` added at the end. It lists new, regressed, resolved and ongoing findings with replay commands, failing pinned regressions and unmet properties, with the most urgent sections first. Each comment starts with a hidden marker from `-marker`, and a later call with the same marker edits that comment instead of adding one, so give each job in a matrix its own. Failure text sits inside code spans so it cannot mention anyone or inject Markdown, and a comment too long for GitHub is cut with a note. `-dry-run` prints the comment.


<!-- docs/testing.md -->

# Testing seedfall itself

This page is for people who work on seedfall itself, or who want to know why its results can be trusted. It lists the tests that check seedfall's model of crashes, faults and replay, and how to run them. You do not need it to use seedfall.

seedfall is only useful if its own model of crashes, faults and replay is right, so that model has its own tests. This page lists what they check and how to run them.

## What the tests check

| Area | Test file | What it proves |
|---|---|---|
| Disk durability | `engine/memfs_test.go` | Synced writes survive a crash, unsynced writes and never-synced files do not, `O_SYNC` makes every write durable, an unsynced truncate is undone |
| Torn writes | `engine/memfs_test.go` | A torn crash keeps an in-order prefix of the pending writes, the last one possibly cut mid-way, and records the tear |
| Out-of-order writeback | `engine/memfs_test.go` | Writes split at 4 KiB page boundaries, pages persist independently (a later page can survive without an earlier one), and writes to one page persist in order |
| fsync `EIO` | `engine/memfs_test.go` | A failed fsync drops the pending writes while they stay readable, and a retried fsync does not bring them back |
| Disk faults | `engine/diskfaults_test.go` | `disk_bytes` cuts a write short and then refuses it, flagged so the guest gets `ENOSPC`, while overwrites still fit; a failed write writes nothing but counts as a disk operation; a corrupted read flips the returned buffer and never the stored data; a lost write keeps the old page on disk (zeros for a new page) and a misdirected write puts the page at another offset, while the page cache keeps the new content, and rewriting the page later writes it in full; crash corruption flips exactly one bit inside the bytes that were being written; bit rot flips one stored bit; `fsync_corrupts` flips only the durable copy; a misdirected write is chosen from the seed and operation number and replays from its recorded fault |
| File system calls | `engine/memfs_test.go` | `OpenFile` flags, `Mkdir`, `Rename`, `Unlink`, `Rmdir` and `Readdir` return the POSIX errors and results |
| `strict_dirs` | `engine/namespace_test.go` | New entries need the parent directory fsynced to survive, a rename reverts without a directory fsync, and a torn crash recovers an in-order prefix of directory operations |
| Fault schedules | `engine/faults_test.go` | Schedules are identical for the same seed and differ across seeds, stay inside the time horizon and in order, never crash the workload unless asked, and never plan runtime-only faults; swarm rates stay in `[0, 2 x rate)`, swarm mixes are deterministic per seed, and partition sides are never empty |
| Network faults | `engine/netfaults_test.go` | Every partition topology has the promised shape (a ring gives each node a distinct majority), the default `half` topology keeps the old schedule, a one-way clog holds one direction only, `jam` accepts late without an error, `slow` adds its delay, per-link latency overrides apply one way, a reset breaks both ends, including connections waiting to be accepted, while the listener stays open, a slow node stretches its latency and timers, `sim.QuietFor` heals clogs, swizzles clog one node at a time and unclog in random order, and bad settings, including network faults on a single-node config, are rejected |
| Scheduler | `engine/sched_test.go` | The next step is the earliest one; at the same time a planned fault goes before a restart and a restart before a resume; every resume due at that time is a candidate for the seeded scheduler; a paused node waits for its pause to end |
| Shrinking | `engine/shrink_test.go`, `cmd/seedfall/shrink_test.go` | Against a fake runner, `Shrink` keeps the original failure, ignores a different failure, and returns a 1-minimal schedule; delta debugging finds one needed fault among 64 in fewer runs than removing one at a time; downtimes, clock jumps, partition sides and fault times shrink to just what the failure needs, while faults recorded at run time keep their operation; the duration and a `sim.Budget` workload are trimmed, and a workload without `sim.Budget` is left alone; the result and run count are the same for 1, 3 and 8 jobs; a run or time budget stops it with the failure intact; failure matching ignores numbers only. Schedule files round-trip, the older fault arrays still read, and a passing replay gets a note only when a shortened duration ended it before the workload finished |
| Network | `engine/net_test.go` | Messages on one connection arrive in order under random latency, reads wait for arrival, a partition holds messages until it heals, close delivers EOF after data, and a crash resets every connection |
| Linearizability | `engine/history_test.go` | Every model (`kv`, `cas`, `append`, `queue`, `set`, `counter`) accepts and rejects known histories, including unknown, pending and failed operations; operations a model does not have, and inputs or outputs of the wrong type, are rejected; a history survives the JSONL round trip and re-checks the same; a custom Porcupine model checks a history through `PorcupineOperations` |
| Transactional anomalies | `engine/elle_test.go` | The list-append checker finds `G0`, `G1a`, `G1b`, `G1c`, `G-single`, `G2`, internal inconsistency, incompatible orders, duplicate elements and appends, and garbage reads in minimal histories, passes serializable ones and reads of unknown transactions, explains the cycle, and rejects malformed transactions |
| End to end | `engine/guest_test.go` | A small guest in `engine/testdata/guest` runs under crashes, partitions, torn writes, out-of-order writeback, crashes during disk operations and pauses: two runs of a seed give byte-identical traces, `-check` passes, a sweep finds the same failing seeds with 1 or 4 jobs, a failure replays exactly from its saved fault schedule, and a shrunk schedule keeps the failure, replays exactly and is 1-minimal. `sim.Budget` caps the client's writes when a schedule sets `ops`, the trace shows the cap, the run is shorter and replays exactly. Under clogs, swizzles, resets, slow nodes and partition topologies, two runs of a seed and a replay of its fault schedule give byte-identical traces. Under every disk fault the same holds, a full disk and `write_enospc` reach the guest as `syscall.ENOSPC`, and a failure caused by a lost write shrinks to a schedule that keeps the lost write and replays exactly |
| Liveness and workload faults | `engine/liveness_test.go` | Against the guest: with `liveness`, a workload that never finishes fails as `liveness` at `duration + within` and without it only hits the horizon; the recovery phase restarts a node that would stay down and heals a partition, so the workload finishes; a `finally` check starts only after the workload, with no fault after it, and its `sim.Eventually` counts as a property; an `Eventually` that never holds fails as `liveness` with its message; `include_workload` crashes and pauses the client, open operations are reported and stay sound for linearizability, and a replay of the recorded faults is byte-identical; every one of several workloads must finish. Without the guest: `supervise` never restarts a workload that exits with an error, `"faults": false` keeps a node out of every planned fault and every partition, the workload is a fault target only when asked, configs with `workloads[]`, `finally` and `liveness` are validated, and `sim.Eventually` is cataloged |
| Assertions and events | `engine/assertions_test.go`, `sim/sim_test.go` | The catalog finds numeric and grouped assertions with their message at the right argument; Antithesis guidance records keep the smallest margin for `always` and the largest for `sometimes`, and guidance without an assertion creates nothing; `lifecycle.SendEvent` becomes a trace event; margins aggregate across seeds; outside the simulator the numeric and grouped forms fail with JSON details and `sim.Event` does nothing |
| Determinism hash | `engine/hostcalls_test.go` | The host-call hash is stable, checkpointed every 4,096 calls and sensitive to field boundaries, and a divergence report names the first differing call with the call before it, including a run that ends early |
| Mutants | `engine/mutation_test.go` | `rename_not_atomic` loses both names in a crash before the next fsync in loose and strict mode, but not a rename to a new name or one a later fsync closed; `truncate_not_durable` brings back the old tail; `net_drop_after_close` drops only an unread last chunk; `net_dup_chunk` duplicates a seeded share of writes and replays them identically; network mutants skip nodes that take no faults; `monotonic_jump` moves the monotonic clock only when active; `-only` parses and rejects typos. `engine/appmutant_test.go`: source mutants find comparisons, early error returns and `Sync` calls and still parse, the selection is seeded and ordered, and a mutant's overlay merges with the `net_overlay` one |
| Preemption | `engine/preempt_test.go` | Strategy validation; loop counting adds the countdown after every `loop` header while decoding LEB immediates, `br_table` and `0xfc` opcodes, and rejects unsupported opcodes; the loop-counted guest compiles; with `preempt.loops` a call-free loop of three time slices takes at least 30ms of virtual time and without it almost none; `pct` finds a goroutine race, records its change points as `preempt` faults that replay exactly, an empty schedule fires none, shrinking keeps one, every change point fires at its counted call across time-slice parks and sleeps and replays the same, and a `preempt` fault is rejected unless the strategy is `pct`; `calls` preempts deterministically |
| Confidence math | `report/report_test.go` | `SeedsToConfirm` and the detectable failure rate against known values, findings moving through new, ongoing, not seen, resolved and regressed across runs, and the JSON report against a golden file |
| Proof rendering | `verify/verify_test.go` | How many seeds a proof needs, and the text and Markdown proof blocks against golden files |

`scripts/regress.sh` then runs every example except `badgerkv` against its expected pass or fail result, replays saved fault schedules, and checks that replays are identical.

## Running them

```sh
go test ./...                 # everything, including the wasip1 guest build
go test -short ./...          # skip the tests that build and run a wasip1 guest
go test -race ./...           # what CI runs; needs cgo
go test ./report ./verify -update   # rewrite golden files after an intended change, then review the diff
go run honnef.co/go/tools/cmd/staticcheck@latest ./...
go run golang.org/x/vuln/cmd/govulncheck@latest ./...
bash scripts/regress.sh       # every example; takes hours
```

govulncheck also reports standard library vulnerabilities, so run it with the latest Go patch release, as CI does with `go-version: stable`.

## CI

| Workflow | When | What |
|---|---|---|
| `ci.yml` | every push to `main` and every pull request | gofmt, `go vet`, staticcheck, govulncheck, the site checks (`scripts/site-check.sh` and an up-to-date `site/llms.txt` and `site/llms-full.txt`); `go test -race ./...` on Ubuntu, macOS and Windows; and two example sweeps through the GitHub Action with `-check` |
| `regress.yml` | nightly, or by hand | `bash scripts/regress.sh` |
| `codeql.yml` | every push to `main`, every pull request, weekly | CodeQL analysis of the Go code |

Dependabot opens weekly updates for the root module and the GitHub Actions. The examples are left alone on purpose: each pins the library version its findings were made against.


<!-- docs/timeline.md -->

# Timelines, logs and time-travel debugging

After a failure you want to see what happened. This page covers the four views seedfall gives you of one run: a timeline diagram, a sequence diagram, filtered logs and a step-by-step debugger. Use it when the failure message alone does not explain the problem.

A failing seed replays exactly, so you can look at it as many times and in as many ways as you like. seedfall gives you four views of one run:

| View | Command | What it shows |
|---|---|---|
| Timeline | `seedfall replay -html timeline.html`, and `timeline.html` in every [failure artifact](reports.md#failure-artifacts) folder | A space-time diagram: one lane per node, every connection and message as an arrow, fault intervals shaded, recorded operations as bars, properties and events as markers, next to a filterable trace |
| Sequence diagram | `seedfall replay -html timeline.mmd`, and `timeline.mmd` in every artifact folder | The same run as a Mermaid `sequenceDiagram`, for an issue or a pull request |
| Logs | `seedfall logs -seed N -node server -grep re -from 1s -to 2s` | The trace filtered by node, pattern and virtual time, with app output interleaved with engine events and slog JSON parsed into fields |
| Debugger | `seedfall debug -seed N -at 1.7s` | A prompt paused at a moment of the run: node states, the live disk, in-flight messages and active faults, then step, run until a pattern, or branch into a different future |

`seedfall trace grep` finds a pattern and shows the lines of every node around each match, and `seedfall trace diff` compares two traces and shows where they first part ways. Logs, trace search and the debugger are also MCP tools, and the timeline is in every artifact folder the MCP tools name.

## The trace

Every run already traces node starts, crashes, faults and checks, plus every line each node writes to stdout or stderr, stamped with the virtual time it was written:

```
    0.000s  start server#1
    0.000s  server#1| serving 0 keys on :7000
    0.292s  fault partition [client] | rest, heals at 0.627s
    0.757s  fault crash server#1 during disk op 56, restart at 1.121s
```

`server#2` is the second process started on node `server`, after its first crash. With `-net-trace` on `run`, `replay`, `logs` or `debug`, the trace also has every connection, message sent and message read:

```
    1.120s  net client#1 dials server:7000, refused
    1.121s  start server#2
    1.121s  server#2| serving 26 keys on :7000
    1.130s  net client#1 dials server:7000 conn 57, arrives 1.132s
    1.130s  net client#1 -> server#2 conn 57: 12 bytes, arrives 1.132s
    1.132s  net server#2 accepts conn 57 from client#1
    1.132s  net server#2 <- client#1 conn 57: 12 bytes sent at 1.130s
    1.132s  net server#2 -> client#1 conn 57: 3 bytes, arrives 1.137s
```

A message sent while a partition or a clog holds the link says `held by a partition or clog`, and a duplicate from the `net_dup_chunk` mutant says `a duplicate`. UDP datagrams appear as `udp <socket>` lines, and one that never arrived says `lost` and why: a partition or clog, no socket bound to the address, a socket connected to another address, or a `udp_drop` fault. `-net-trace` adds lines to the trace only: it does not change the schedule, the determinism hash or the result, so a seed fails the same way with and without it. A failure replayed with `-net-trace` writes those lines into its artifact `trace.txt` as well.

## Timeline

```sh
seedfall replay -c seedfall.always.json -seed 1 -html timeline.html
```

`timeline.html` is one self-contained file with no network fetches, so it opens from a CI artifact or an email attachment. Every failure seedfall reports also gets one in its artifact folder, next to `trace.txt`, and the [triage report](reports.md) embeds it under each finding.

The diagram has one column per node with virtual time flowing down:

| Mark | Meaning |
|---|---|
| Green line | A process of the node is alive, from its start to its crash or exit, labelled with its instance (`server#2`) |
| Arrow | A connection (`connect`, purple) or a message (data, blue; EOF, yellow; reset, red) from the sender at the time it was sent to the receiver at the time it was first read. A dashed arrow was never read: it was dropped by a crash, a reset or the end of the run. Hover for the connection, size and times |
| Shaded box | A fault interval over the nodes it hits: a crash until the restart, a pause, a slowdown, a clog, a clock jump, or a partition over every lane |
| Bar | An operation recorded with `sim.Put`, `sim.Get`, `sim.Invoke` or `sim.Txn`, from invocation to completion, green when ok, red when failed, yellow when unknown. Concurrent operations of one node sit side by side |
| Dot | A `sim.Event`, the first time a `Sometimes` or `Reachable` property is true, or the first time an `Always` or `Eventually` property is checked |
| Red line | The failure, with its reason |

Rows are the distinct moments something happened, labelled with their virtual time, so a run with long idle stretches stays compact; the spacing is not proportional to time.

The trace explorer beside it lists every trace line. Above both are a node toggle per node (plus `engine` for lines that belong to no node), toggles for lives, messages, operations, faults and marks, a `from` and `to` window in Go duration syntax (`1.5s`, `200ms`), and a `grep` box that filters trace lines with a JavaScript regular expression. Clicking a trace line scrolls the diagram to its moment.

## Sequence diagram

```sh
seedfall replay -c seedfall.always.json -seed 1 -html timeline.mmd
```

A path ending in `.mmd` writes Mermaid instead of HTML:

```
sequenceDiagram
  participant p0 as server
  participant p1 as client
  Note over p0: 0.000s start server#35;1
  p1->>p0: 0.000s conn 2 connect, read 0.003s
  p1->>p0: 0.000s conn 2 10 bytes, read 0.003s
  p0->>p1: 0.003s conn 2 3 bytes, read 0.007s
  p1-->>p0: 0.007s conn 2 eof, read 0.009s
```

It has the node lives, messages (`->>` read, `-->>` an EOF or reset, `-x` never read or a lost datagram), faults, events, properties and the failure, in time order. Recorded operations are only in the HTML timeline. GitHub renders a ` ```mermaid ` block in issues and pull requests; a run with thousands of messages makes a diagram too tall to read there, so cut it to the moments around the failure first.

## Logs

```sh
seedfall logs -c seedfall.always.json -seed 1 -node server
```

```
    0.000s  start server#1
    0.000s  server#1| serving 0 keys on :7000
    0.757s  fault crash server#1 during disk op 56, restart at 1.121s
    1.121s  start server#2
    1.121s  server#2| serving 26 keys on :7000
    1.705s  fault crash server#2, restart at 1.943s
    1.943s  start server#3
    1.943s  server#3| serving 60 keys on :7000
8 of 12 trace lines; seed 1: FAIL client#1: acknowledged write lost: k96=v96, server now answers "NONE"
```

| Flag | Meaning |
|---|---|
| `-seed`, `-faults` | The run to replay, as for `replay` |
| `-node` | Only lines that belong to these nodes, comma separated: their output, starts, crashes, faults aimed at them and, with `-net-trace`, the messages they send and read. Lines about the whole run, such as a partition or the end of the workload, belong to no node and are left out |
| `-grep` | Only lines matching this Go regular expression |
| `-from`, `-to` | Only lines in this virtual time window, for example `-from 1.5s -to 2s` |
| `-json` | One JSON object per line instead of text |
| `-net-trace` | Add connections and messages to the trace first |

The summary line goes to stderr, so `seedfall logs ... > server.log` keeps only the trace. With `-json`, each line has `at`, `at_ns`, `node`, `instance`, the full trace `line` and, for a node's own output, `output`. When that output is a JSON object, such as a line from `slog.NewJSONHandler`, it is parsed into `fields`:

```json
{"at":"100.000013ms","at_ns":100000013,"node":"app","instance":"app#1","line":"    0.100s  app#1   | {\"time\":\"2026-01-01T00:00:00.100000012Z\",\"level\":\"INFO\",\"msg\":\"put\",\"key\":1}","output":"{\"time\":\"2026-01-01T00:00:00.100000012Z\",\"level\":\"INFO\",\"msg\":\"put\",\"key\":1}","fields":{"key":1,"level":"INFO","msg":"put","time":"2026-01-01T00:00:00.100000012Z"}}
```

slog's `time` field is the guest's wall clock, which seedfall simulates from 2026-01-01 (and skews or jumps under clock faults); `at` is the virtual time the line was written. Other slog handlers' text output comes through as `output` without `fields`.

## Searching the trace

`logs -grep` keeps only the matching lines. To see what happened around each match, across every node, use `seedfall trace grep`:

```sh
seedfall trace grep -c seedfall.always.json -seed 1 -e crash -context 1
```

```
     4     0.292s  fault partition [client] | rest, heals at 0.627s
>    5     0.757s  fault crash server#1 during disk op 56, restart at 1.121s
     6     1.121s  start server#2
     7     1.121s  server#2| serving 26 keys on :7000
>    8     1.705s  fault crash server#2, restart at 1.943s
     9     1.943s  start server#3
2 matches of 12 trace lines, 2 shown; seed 1: FAIL client#1: acknowledged write lost: k96=v96, server now answers "NONE"
```

Matches are marked `>`, each line carries its number in the run's trace (the same as the artifact's `trace.txt` for that run) and its virtual time, windows that touch or overlap are merged, and separate windows are divided by `--`. `-e` is a Go regular expression. `-node`, `-from` and `-to` narrow which lines can match, as for `logs`, while the context lines come from every node. `-context` sets the lines before and after each match (3 by default), `-limit` the most matches shown (200), `-net-trace` adds connections and messages first, and `-json` prints the windows as one JSON object with the same line fields as `logs -json` plus `n` and `match`.

## Debugger

```sh
seedfall debug -c seedfall.always.json -seed 1 -at 1.7s
```

`debug` replays the seed and stops before the first scheduler step after `-at` (the same moment `seedfall inspect -at` snapshots), then reads commands:

```
paused at t=1.696068226s before scheduler step 379
  server       server#2     blocked
  client       client#1     runnable at 1.702612857s
(seedfall 1.696068226s) until fault crash
    1.705s  fault crash server#2, restart at 1.943s
paused at t=1.705199634s before scheduler step 382
  server                    down until 1.942588993s
  client       client#1     runnable at 1.706780887s
(seedfall 1.705199634s) net
  conn 125  server#2 -> client#1: eof, sent at 1.705199634s, arrives at 1.706780887s
(seedfall 1.705199634s) stat server data/kv.log
data/kv.log on server: 527 bytes, 527 durable, directory entry durable: true
```

| Command | Effect |
|---|---|
| `where` | Virtual time, the next scheduler step, and each node's state: `runnable` at a time, `blocked` with no timer or message due, `paused` or `down` until a time, `exited` |
| `log [n]` | The last `n` trace lines, 20 by default |
| `grep <regex>` | Every trace line so far that matches |
| `ls [node]` | Every node's disk, or one node's, in the [inspect](inspect.md) format: live and durable sizes, what a crash loses, torn writes and damage |
| `stat <node> <path>` | One file's size, durable size, the byte ranges a crash loses and its damage |
| `cat <node> <path>` | The file's live content, what the node reads now, as text or a hex dump (`inspect -cat` shows the durable content instead) |
| `net` | Every message still in flight with its sender, receiver, size, send and arrival time, and connections not yet accepted |
| `faults` | Active faults and the next scheduled one |
| `step [n]` | Run `n` scheduler steps, 1 by default |
| `until <regex>` | Run until a new trace line matches, then stop right after it |
| `to <duration>` | Run until the next step is after this virtual time |
| `branch [key]` | Re-randomize everything after now with this key, 1 by default: the scheduler, network and disk randomness, guest randomness and the faults still to come, as [`seedfall cause`](cause.md) does. One branch per session |
| `quit` | End the session |

Commands after `step`, `until` and `to` print the trace lines that ran and the new position. Nothing runs between commands, and the run is the same one `replay` produces, so the state you see is the state the failing run had. Once the run ends, inspection commands still work on the final state.

The debugger stops between scheduler steps, not inside a node's code: it shows what a crash at that moment would see, not a goroutine's stack. For source-level stepping, rebuild the node natively and reproduce with the faults from `faults.json`.

## Comparing traces

```sh
seedfall trace diff .seedfall/failures/seedfall.always-seed-1 after-fix.txt
```

Each side is a trace file (an artifact's `trace.txt`, or `seedfall logs` output saved to a file) or an artifact folder, which means its `trace.txt`. It prints the line where the traces first differ with the matching lines before it (`-context 3`), and exits 1, or says they are identical and exits 0. `-context` goes before the two paths. Here `a.txt` is the trace of seed 1 and `b.txt` the trace of the same seed under its shrunk schedule, both saved with `seedfall logs`:

```
$ seedfall trace diff a.txt b.txt
the traces diverge at line 4 (a.txt has 12 lines, b.txt has 12)

      0.000s  start server#1
      0.000s  start client#1
      0.000s  server#1| serving 0 keys on :7000
-     0.292s  fault partition [client] | rest, heals at 0.627s
+     0.000s  client#1: sim.Budget capped at 63 of 200 operations
```

Use it after shrinking to see where the shrunk schedule leaves the original run, after a fix to see the first moment the run behaves differently, or on two machines to find where a nondeterministic run splits (`run -check` does that for you within one machine).

## Over MCP

`seedfall_logs` takes `config`, `seed` and optionally `faults`, `node`, `grep`, `from`, `to`, `net_trace` and `limit` (200 by default), and returns the matching lines with the same fields as `logs -json`, how many matched and how many the trace has. `seedfall_trace_search` takes `config`, `seed`, `pattern` and optionally `faults`, `context`, `node`, `from`, `to`, `net_trace` and `limit`, and returns the same windows as `trace grep -json`. `seedfall_debug` takes `config`, `seed`, optionally `faults`, `at`, `net_trace` and a `commands` list run in order (`["until fault crash", "net", "ls server"]`), and returns each command's output and the final state. Failures from `seedfall_run`, `seedfall_replay` and `seedfall_shrink` name the artifact folder, which holds `timeline.html` and `timeline.mmd`. See [agents.md](agents.md#tools).


<!-- docs/troubleshooting.md -->

# Troubleshooting

This page lists the errors and failure messages seedfall prints, with what causes each one and how to fix it. Find yours by its exact text. Parts in angle brackets, such as `<pkg>`, change from case to case. Commands print errors as `seedfall: <message>` and exit with code 1.

Do this first:

1. Run `seedfall doctor`. It checks the Go version, a `wasip1` build, `net_overlay`, the build cache, the working directory and free memory. For every check that is not `ok` it prints a fix.
2. In a new project, run `seedfall init`. It lists every package that will not build for `wasip1` (the WebAssembly target seedfall compiles your code for) and shows the chain of imports that pulls each one in.

## Setup and Go version

### Go is too old

```
  fail  go            <installed> is older than go<version>
        fix: install go<version> or newer from https://go.dev/dl/
```

`seedfall doctor` prints this when your Go is older than the version in seedfall's own `go.mod` (currently `go1.25.0`). Install that version or newer.

### No go command

```
  fail  go            no working go command on PATH: <error>
```

seedfall builds each node with your Go toolchain, so `go` must be on your `PATH`.

1. Install Go from https://go.dev/dl/.
2. Open a new terminal and run `go version` to check.
3. Run `seedfall doctor` again.

Until this passes, `seedfall doctor` skips the `wasip1 build`, `net_overlay` and `build cache` checks. If you use `net_overlay` or the generic compat shim, the same problem shows up as `go env GOROOT: <error>`.

### The net overlay does not support this Go version

```
net overlay: expected one "<anchor>" in <file>, found <n>; this Go version is not supported yet
```

With `"net_overlay": true`, seedfall patches a few functions in Go's own `net` package for `wasip1` (`net_fake.go`, `fd_fake.go` and `sockopt_fake.go`). Each patch looks for one exact line in `$GOROOT/src/net`. If a new Go release changed that line, seedfall refuses to patch instead of patching the wrong place. `seedfall doctor` shows this as a `warn` on the `net_overlay` check.

Fix it in one of two ways:

- Use a Go version that seedfall supports.
- Turn off `net_overlay` and call `sim.Listen` and `sim.Dial` in your code instead. They need no patch ([networking](networking.md)).

```
net overlay: <error>
```

seedfall could not read the files it patches from `$GOROOT/src/net`. Your Go install is missing its standard library source. Reinstall Go from https://go.dev/dl/.

## Building nodes for wasip1

### A node does not build

```
build <pkg>: exit status 1
```

For every `pkg` in the config, seedfall runs `GOOS=wasip1 GOARCH=wasm go build`. The compiler's own errors are printed above this line. The usual causes:

- **cgo.** cgo (Go code that calls C) is off under `wasip1`, so a package with cgo files does not build. `seedfall init` lists these under `cgo packages`, with a `cgo files: <files>` line and the chain `via <main> -> ... -> <pkg>`. Replace each with a pure-Go library, or stub it behind a build tag. Libraries such as RocksDB bindings or `mattn/go-sqlite3` cannot run under seedfall.
- **`mmap`, `flock` and other unix calls.** An error such as an undefined `syscall.Mmap`, `unix.Mmap` or `syscall.Flock` means the code uses operating system calls that WASI does not have. (`mmap` maps a file into memory. `flock` locks a file.) `seedfall init` lists each one under `wasip1 blockers` with a `shim:` line.
  - If the line names a shim, set `"compat_overlay": true` ([compat](compat.md)).
  - If it says `none: needs a shim, see docs/compat.md`, the dependency needs a hand-written shim, an upgrade, or a `go.mod` replace with an in-process version, as `examples/flockshim` does for `gofrs/flock`.
- **Platform-specific code in your own packages.** Move it behind build tags so that a `wasip1` version builds. `compat_overlay` never changes your own module.

### A compat shim does not match the library version

```
compat overlay: <pkg>/<file> declares <names>, which the wasip1 shim does not provide; this version is not supported yet
```

A shim replaces whole files, and only if it provides every top-level name those files declare. The version of the library you use declares something the shim does not, so seedfall stops instead of building a half replacement. Either pin the library to the version listed in [compat](compat.md), or add the missing declarations to the shim under `engine/compat` ([CONTRIBUTING](../CONTRIBUTING.md#adding-a-compat-shim)).

### golang.org/x/sys is not downloaded

```
compat overlay: golang.org/x/sys is not downloaded; run go mod download golang.org/x/sys
```

The generic shim adds `wasip1` versions of `Mmap` and `Flock` to a copy of `golang.org/x/sys/unix`, so that module must be in your module cache. Run the command from the message in the folder that holds your `go.mod`.

```
compat overlay: finding golang.org/x/sys: <error>
```

`go list -m golang.org/x/sys` failed in the config's folder. Run it yourself to see why. Usually your `go.mod` does not require `golang.org/x/sys`, or a module download fails.

### Not inside a module

```
compat overlay: <dir> is not inside a Go module
compat overlay: <pkg> is not part of a module
```

`compat_overlay` builds with a copy of your `go.mod` that adds a `replace` for each shimmed module. So the config's folder must be inside a Go module, and every shimmed package must come from one. Run seedfall from a folder with a `go.mod`, with module mode on (not `GO111MODULE=off`).

```
compat overlay: go mod edit: <error>: <output>
```

seedfall could not write the `replace` lines into its copy of `go.mod` under `.seedfall/compat`. The text after the colon comes from `go mod edit`. Check that `.seedfall` is writable and that your `go.mod` is valid.

### preempt.loops cannot instrument the binary

```
preempt.loops: function <n>: unsupported wasm opcode 0x<op>
preempt.loops: function <n>: unsupported wasm opcode 0xfc <sub>
```

With `"preempt": {"loops": true}`, seedfall reads every function of the compiled program and adds a counter after each `loop`. It hit an instruction it does not know, which a newer Go compiler may produce. Turn `preempt.loops` off and report your Go version in an issue.

## Config

These errors come from a check that runs before anything is built.

```
config: workload.name is required
config: every node needs a name
config: duplicate node name "<name>"
config: node "<name>" needs pkg or wasm
config: node "<name>" has an invalid pkg "<pkg>"
```

The workload and every node need a unique `name`. Every node also needs either a `pkg` (a Go package path, which seedfall builds for you) or a `wasm` file. [Configuration and faults](faults.md) lists every field.

```
config: node "<name>" sets both pkg and wasm, use one
<file>: json: unknown field "<name>"
```

A node names either a `pkg`, which seedfall builds into a `wasm` file, or a prebuilt `wasm`, never both. An "unknown field" is a key that is not part of the config. Look for a typo in the file, in a profile or in a `-set`.

```
config: faults.<name> must be between 0 and 1, got <value>
config: faults.<name> must not be negative, got <value>
config: <range> must be [min, max] with 0 <= min <= max, got [<min>, <max>]
config: duration must be positive, got <value>
config: watchdog must be positive, got <value>
config: faults.clock_jump_max must not be negative, got <value>
```

A number is out of range. A probability is outside 0 to 1, a `_per_sec` rate is negative, a range has a negative or reversed end, or a duration is not positive. [Config](config.md) says which rule covers which field.

```
config: no profile "<name>", have <profiles>
config: no profile "<name>", the config has no profiles
```

`-profile` named a profile that is not in the config's `profiles`. The first form lists the ones that exist ([config](config.md#profiles)).

```
config: -set "<expr>" is not path=value
config: -set <key>: <path> is not an object or a list
```

`-set` takes `path=value`. The path walks objects by key and lists by element name or index. The value is JSON or a bare string ([config](config.md#-set)).

```
config: <file> extends itself
<file>: extends must be the path of another config file
```

`extends` must name a different config file ([config](config.md#extends)).

```
config: preempt: unknown strategy "<name>", want one of <strategies>
config: preempt: interleave is shorthand for strategy random, but strategy is <name>
```

`preempt.strategy` is not one of the strategies listed, or `interleave` was combined with a different strategy ([how it works](how-it-works.md#strategies)).

```
bad seed range "<range>": seed 18446744073709551615 is the largest uint64, so the count of seeds or the next seed would wrap around, end the range at 18446744073709551614 or lower
```

A `-seeds` range cannot end at the largest 64-bit number. The sweep could not tell the end of the range from a wrap-around to seed 0.

```
the module cannot be instrumented for preemption or feedback: <reason>
```

`preempt.strategy`, `preempt.loops` and the feedback used by `explore` need a call counter that seedfall adds to Go `wasip1` programs. A prebuilt `wasm` from another toolchain, or one that does not import `sched_yield`, cannot take it. Build the node from Go, or turn those settings off.

```
-json and -report cannot be combined
timeout cannot be negative
```

`run` writes either one JSON object per seed or an HTML report, not both. `-timeout` must be zero (no limit) or positive.

```
report path <path> ends in .json, which is where the JSON report goes; use a .html path
```

`-report` names the HTML report. The JSON version is written next to it, with `.json` in place of the extension. An HTML report cannot go to a `.json` path, because it would be overwritten.

```
<file> line <n>: <json error>
```

A line of `.seedfall/history.jsonl` is not valid JSON, for example because an editor or a merge damaged it. `report`, `findings` and `report notify` refuse to read a history they cannot trust. Delete or repair the line named in the message ([history](reports.md#history-new-ongoing-resolved-regressed)).

```
listen <network>: the simulator supports only tcp, tcp4, tcp6
listen <network>: the simulator supports only udp, udp4, udp6
dial <network>: the simulator supports only tcp, tcp4, tcp6
```

`sim.Listen`, `sim.ListenPacket` or `sim.Dial` was given a network type the simulator does not have, such as `unix`. Use `tcp` or `udp` ([networking](networking.md#option-1-simlisten-and-simdial)).

## Failures that are not your system's bug

Every reported failure is classed as `bug`, `nondeterministic` or `timeout` ([reports](reports.md#classification)). The last two need a different fix from a bug.

### Watchdog

```
watchdog: <node>#<n> ran for more than 30s of real time without yielding (livelock or busy loop)
```

Classed as `timeout`. One node ran for longer than `watchdog` (default `30s`) of real time without ever waiting. Only one node runs at a time, and virtual time barely moves while it runs, so a loop that never waits freezes the whole simulation. The usual cause is a loop with no function call, which the default preemption cannot interrupt, or a very long calculation. The result depends on how fast and how busy your machine is, so the same seed may pass on a faster machine or with a lower `-j`.

To fix it:

1. Set `"preempt": {"loops": true}`. Loops with no function call are then interrupted and use up virtual time. A spin that never ends then fails as `liveness`, which does not depend on your machine ([how it works](how-it-works.md#loops), [`examples/busyloop`](../examples/busyloop)).
2. If the node really needs more real time, raise `watchdog`.
3. Or lower `-j`, so fewer nodes share the CPU.

### Nondeterminism

```
nondeterminism: two runs of seed <n> diverge at host call <n>: <call> vs <call>, after <call>; host calls <a>-<b> (...)
nondeterminism: two runs of seed <n> diverge at trace line <n>: "<line>" vs "<line>"
```

With `-check` (and in `verify`), every seed runs twice. The two runs made a different host call or wrote a different trace line. The first form names the first call that differs, with the node instance, call, target, argument and virtual time ([properties](properties.md#determinism-check)).

```
nondeterministic (replay diverges at trace line <n>: "<line>" vs "<line>")
nondeterministic (replay diverges at outcome: "<reason>" vs "<reason>")
```

seedfall replays a failure to classify it, and the replay did not match the original run.

seedfall controls everything a program normally reads: time, randomness, scheduling, disk and network. All of it replays exactly. So a difference means something from outside got in. Check these, in order:

1. Did your program's binary change between the runs? A rebuilt package, another Go toolchain or a different source tree makes a different binary and can change the run.
2. Did input from the host change? Examples are seeded disk images or fixture files that the config reads.
3. Did the watchdog or a `-timeout` limit fire in one run and not the other? Both depend on real time.

If none of these applies, it is a bug in seedfall. Open a bug report with the `-check` output, the config and the seed.

### Deadlock

```
deadlock: every node is blocked with no timer or pending message
deadlock: every node has exited
```

Classed as `bug`. In the first message every node is waiting and nothing can wake one. In the second, no node is left to run before the workload finished.

The first is often a real bug. For example, a retry loop waits for a reply after a partition dropped the connection, and it never set a deadline. It is also what you see when nodes cannot reach each other at all. Without `net_overlay` or `sim.Listen`, Go's `net` package on `wasip1` is a fake that lives inside one process, so a listener on one node cannot be reached from another ([networking](networking.md#without-either)).

The second usually means the nodes exited and nothing restarts them.

### Liveness

```
liveness: <node> did not finish within <within> of the recovery phase starting at <time>
```

With `liveness` on, faults stop at the recovery phase, the network heals and crashed nodes restart. The workload or the `finally` check then has `liveness.within` to finish. A system that never recovers has a real bug. If it recovers but slowly, raise `within` ([properties](properties.md#liveness-recovery-and-finally-checks)).

### A node exits or panics

```
<node>#<n> exited
<node>#<n> crashed: <error>
```

The first line means a node, other than the workload or the `finally` check, exited with status 0. A server that returns from `main` counts as a failure. The second means a node exited with an error or panicked. With `"supervise": true`, seedfall restarts a node that exits with an error after `restart_after`, as systemd would. A Go panic (exit code 2) always fails the run ([faults](faults.md#world)).


<!-- docs/verify.md -->

# Proving a fix with `seedfall verify`

After you fix a bug you need evidence that the fix works. `seedfall verify` replays the failing run, sweeps many fresh seeds, checks that the run is repeatable and writes a proof for your pull request. Pinned regressions then keep the bug from coming back. Use it as the last step before you open a pull request.

`seedfall verify` is the definition of done for a change that fixes a seedfall failure, whether a person or an AI agent wrote it. It answers one question with evidence: is the failure gone, and how sure are we?

```sh
seedfall verify -c seedfall.fixed.json -seed 1 -faults .seedfall/seed-1.faults.json -mutate -md proof.md
```

```
verify seedfall.fixed.json (seedfall v1.2.3)
  pass  replay seed 1 with .seedfall/seed-1.faults.json  passes, twice, with identical host calls and traces
  pass  fresh sweep, seeds 2-300                         299 of 299 pass: 95% confidence that a failure with rate >= 0.997% would have shown up
  pass  determinism, seeds 2-11                          every seed ran twice with identical host calls and traces
  pass  mutant fsync_noop                                killed by seed 2
  pass  mutant dirsync_noop                              not exercised
  pass  mutant osync_ignored                             not exercised
  pass  mutant fsync_corrupts                            killed by seed 2
PASS
```

Against the unfixed config the same command stops at the first check and exits 1:

```
verify seedfall.always.json (seedfall v1.2.3)
  FAIL  replay seed 1 with .seedfall/seed-1.faults.json  seed 1 FAILS [bug]: client#1: acknowledged write lost: k60=v60, server now answers "NONE"
  skip  fresh sweep                                      an earlier check failed
  skip  determinism                                      an earlier check failed
FAIL
```

## What it checks

In order, stopping at the first stage that fails:

1. **Replay.** Every failing schedule you name is replayed and must pass now. Each replay runs twice and must produce identical host calls and traces, so a pass cannot be luck.
2. **Fresh sweep.** New seeds, starting after the highest seed already known, must all pass. By default verify runs as many as needed for 95% confidence that a failure with the historical rate would have shown up: *n = ⌈ln(0.05) / ln(1 − p)⌉*, the same rule the [triage report](reports.md) uses to call a finding resolved. A finding that failed 27.5% of seeds needs 10 clean seeds; when no rate is known, verify assumes a rare failure (1%) and runs 299. `-seeds` overrides the range.
3. **Determinism.** The first `-check` fresh seeds (default 10) run twice and must produce identical host calls and traces, as with `run -check`.
4. **Mutants** (with `-mutate`). The [mutants](mutate.md) run over the fresh seeds, and every exercised mutant must still be killed. This catches a "fix" that passes by weakening the checks. With `-app-mutants N`, N [source mutants](mutate.md#source-mutants) of the node packages run too, each as a row naming its line and change, and each one that builds must be killed. If the node packages cannot be read to list the source mutants, a `source mutants` row fails the proof.

Any failure is printed with its [classification](reports.md#classification), so a determinism leak is not mistaken for the bug coming back.

## What to verify

| Flags | Replays |
|---|---|
| `-seed N` | seed N with its generated faults |
| `-seed N -faults file.json` | seed N under a saved schedule, for example one written by `seedfall shrink`. Its faults and `ops` cap are kept, but it runs for the config's full `duration`: a shrunk schedule's shorter duration could end the run before the workload checks anything |
| `-report .seedfall/report.html` | every example seed of every finding in a [triage report](reports.md), plus any schedule `shrink` saved for those seeds in `.seedfall/`. The findings' failure rates set the sweep size |

`-seed` and `-report` can be combined. Point `-c` at the config of the code you changed; the report can come from an earlier run of the same or another config.

Every schedule [pinned](#pinned-regressions) for the config is replayed too, as a `replay pinned seed N with seedfall-regressions/...` row, without being named.

```
$ seedfall verify -c seedfall.fixed.json -report .seedfall/report.html
verify seedfall.fixed.json (seedfall v1.2.3)
  pass  replay assert · client seed 1                                     passes, twice, with identical host calls and traces
  pass  replay assert · client seed 1 with .seedfall/seed-1.faults.json   passes, twice, with identical host calls and traces
  pass  replay assert · client seed 12                                    passes, twice, with identical host calls and traces
  ...
  pass  fresh sweep, seeds 41-50                                          10 of 10 pass: 95% confidence that a failure with rate >= 25.9% would have shown up (historical rate 27.5%)
  pass  determinism, seeds 41-50                                          every seed ran twice with identical host calls and traces
PASS
```

## Pinned regressions

A fixed bug should stay fixed. `seedfall pin` copies a failing seed's schedule into `seedfall-regressions/`, next to the config, a directory you commit:

```sh
seedfall pin -c seedfall.fixed.json -seed 1 -faults torntail.faults.json
```

```
pinned seed 1 (2 faults, from torntail.faults.json) to seedfall-regressions/seedfall.fixed-seed-1.json
it passes now; seedfall run, verify and seedfalltest replay it first and fail if it fails again
```

Without `-faults`, pin takes the schedule `seedfall shrink` saved in `.seedfall/seed-N.faults.json`, or else the seed's own faults, recorded fault by fault so the pinned faults stay the same if the fault rates change later. The file is a schedule in the usual format with a `pinned` block: the config it belongs to, the finding and reason if it fails now, where it came from, the seedfall version and the date. It is named `<config>-seed-N.json`, so two configs in one directory can pin the same seed; `<config>` carries the profile and a hash of any `-set` overrides, as artifact folders do ([config](config.md#profiles)). Pinning a schedule that still fails is allowed, and the commands below fail until the bug is fixed, the way a test written before its fix does.

A pinned schedule keeps its faults and `ops` cap but runs for the config's full `duration`, as `-faults` does in verify, so a shrunk schedule's short duration cannot end the run before the workload checks anything. The same file replays exactly with `seedfall replay -c C -seed N -faults seedfall-regressions/<file>`.

Pinned schedules are replayed, in parallel, before anything else by:

| Where | What happens |
|---|---|
| `seedfall run` | A `regressions` table comes first. One that fails again stops the run before the sweep with its failure, classification, [artifacts](reports.md#failure-artifacts) and replay command, and exit code 1 |
| `seedfall run -report` | The sweep still runs, the report gets a **Regressions** section, and a failing regression fails the run |
| `seedfall run -json` | One `{"type": "regression", ...}` line per regression before the seed lines, with `source`, `seed`, `passed`, and on a failure `failure`, `reason`, `classification` and `artifacts`; the summary counts `regressions_failed` |
| `seedfall verify` | A `replay pinned` row each, which must pass twice |
| `seedfalltest.Sweep` and `seedfalltest.Pinned` | The test fails with the regression's failure ([ci.md](ci.md#go-test)) |
| `seedfall hook` and `seedfall_run` over MCP | The regression's failure is reported before any sweep |

A file in `seedfall-regressions/` without a `pinned.config`, for example a schedule copied in by hand, is replayed for every config in that directory. `run -pinned=false` skips them; over MCP, `skip_pinned`.

`run -seeds-file known-bad.txt` replays a list of seeds, each with its own faults, the same way before the sweep. The file holds seeds separated by spaces or lines, with `#` comments.

## The proof block

`-md proof.md` writes the result as Markdown for the pull request description:

```markdown
### seedfall verify: PASS

Config `seedfall.fixed.json`, seedfall `v1.2.3`, reproduce with `seedfall verify -c seedfall.fixed.json -seed 1 -faults .seedfall/seed-1.faults.json -mutate`

| | Check | Result |
|---|---|---|
| pass | replay seed 1 with .seedfall/seed-1.faults.json | passes, twice, with identical host calls and traces |
| pass | fresh sweep, seeds 2-300 | 299 of 299 pass: 95% confidence that a failure with rate >= 0.997% would have shown up |
| pass | determinism, seeds 2-11 | every seed ran twice with identical host calls and traces |
| pass | mutant fsync_noop | killed by seed 2 |
| pass | mutant dirsync_noop | not exercised |
| pass | mutant osync_ignored | not exercised |
| pass | mutant fsync_corrupts | killed by seed 2 |
```

## Flags

| Flag | Default | Meaning |
|---|---|---|
| `-c` | `seedfall.json` | Config of the code under test |
| `-seed` | | Failing seed to replay |
| `-faults` | | Fault schedule for `-seed` |
| `-report` | | Triage report (`.html` or `.json`) whose findings to replay |
| `-seeds` | enough for 95% confidence | Fresh seed range to sweep |
| `-check` | `10` | Fresh seeds to run twice for the determinism check |
| `-mutate` | off | Also require every exercised mutant to be killed |
| `-app-mutants` | `0` | Also rebuild the nodes with this many [source mutants](mutate.md#source-mutants), picked from the first fresh seed, and require every one that builds to be killed |
| `-md` | | Write the Markdown proof block to this file |
| `-j` | all CPUs | Parallel runs |

The exit status is 0 only when every check passes.

## From an agent

The MCP tool `seedfall_verify` takes the same inputs (`config`, `seed`, `faults`, `report`, `seeds`, `check_seeds`, `mutate`) and returns each check as structured JSON, the overall `passed` verdict, and the proof block as `markdown`. See [agents.md](agents.md).


<!-- skills/seedfall-fix-and-prove/SKILL.md -->


# Fix a seedfall failure and prove it

The fix is done when `seedfall verify` passes, not when one replay goes green. Below, `C` is the config that failed, `N` the seed, and `S` the schedule from `seedfall shrink`, `.seedfall/seed-N.faults.json`.

## 1. Fix the cause, not the symptom

Change the code that triage identified: fsync before acknowledging, truncate a torn tail during recovery, fsync the directory after a rename, stop acknowledging after a failed fsync. Do not change `C`, the workload's checks or the fault rates to make the failure go away. A fix that weakens the checks fails step 4 anyway.

## 2. Replay until it passes

```sh
seedfall replay -c C -seed N -faults S
seedfall replay -c C -seed N
```

Both must end with `seed N: ok, ... steps`. Seeds and schedules replay exactly, so a pass here is not luck. If it still fails, read the new failure: it may be the same bug further along, or a second bug the first one was hiding.

## 3. Sweep

```sh
seedfall run -c C -seeds 1-200
```

A new failure on another seed is a new finding. Triage it before going on.

## 4. Verify

```sh
seedfall verify -c C -seed N -faults S -mutate -md proof.md
```

If the failures came from a triage report, use `-report .seedfall/report.html` instead of, or as well as, `-seed`. Verify stops at the first stage that fails:

1. **Replay.** Each named schedule passes, twice, with identical host calls and traces.
2. **Fresh sweep.** Enough new seeds for 95% confidence at the failure's historical rate. Without a rate, verify assumes 1% and runs 299 seeds. `-seeds` overrides the range.
3. **Determinism.** `-check` fresh seeds (default 10) run twice with identical host calls and traces.
4. **Mutants** (`-mutate`, `-app-mutants N`). Every exercised mutant is still killed, so the fix did not pass by making the checks blind. `-app-mutants` also rebuilds the nodes with N source mutants.

It prints `PASS` or `FAIL` and exits 0 or 1. Over MCP, `seedfall_verify` with `{"config": "C", "seed": N, "faults": "S", "mutate": true}` returns the same verdict, and its `markdown` field holds the proof block.

## 5. Put the proof in the pull request

Paste `proof.md`, or the MCP `markdown` field, into the pull request description unchanged, under a heading such as `## Crash-safety proof`. It names the config, the replayed schedules, the seed ranges and the confidence, so a reviewer can rerun the exact command it shows.

## 6. Keep it fixed

- Pin the schedule as a permanent regression and commit the file:

  ```sh
  seedfall pin -c C -seed N
  git add seedfall-regressions/
  ```

  Pin takes `S` (or `-faults` another file) and writes `seedfall-regressions/<config>-seed-N.json`. Over MCP, `seedfall_pin` with `{"config": "C", "seed": N}`. It reports whether the schedule passes now; after a real fix it must. From then on `seedfall run`, `seedfall verify`, `seedfall hook` and `seedfalltest.Sweep` replay it before every sweep and fail if the bug comes back.
- Run the sweep from `go test` with `seedfalltest.Sweep(t, "seedfall.json", "1-100")`, and the pinned schedules alone with `seedfalltest.Pinned(t, "seedfall.json")`, from `github.com/kunalgoesbyken/seedfall/seedfalltest`, or in CI with the `kunalgoesbyken/seedfall` GitHub Action, whose `command: verify` input runs the same proof on a pull request.


<!-- skills/seedfall-properties/SKILL.md -->


# Write properties that catch real durability bugs

A passing sweep proves only what the workload checks. Find the service's promises, check each one, prove that the faults reached the dangerous paths, then break the disk on purpose and confirm the checks notice.

## 1. Find the promises

Read the code, not the README. For each item below, note the file and line:

- **Acknowledgement.** Where does the service answer OK, return 2xx or ack a producer? What must already be fsynced at that point: the data file, the directory entry, the index?
- **Recovery.** What does startup do with a torn last record, a missing file, a leftover temp file or a half-finished compaction?
- **Atomic replace.** For each write-temp-then-rename, is the file fsynced before the rename, and is the parent directory fsynced after it?
- **Deletes and compaction.** Can a crash bring back deleted data, or lose data that had been copied?
- **Replication.** When is a write committed? Can a follower serve stale reads? Can two leaders coexist?

Write each promise as one sentence, for example "every acknowledged write is readable after any number of crashes".

## 2. Turn each promise into a check

The full reference is the MCP resource `seedfall://docs/properties` (docs/properties.md).

| Promise | Check |
|---|---|
| Acknowledged writes survive | The workload records each acknowledged write, then reads it back after the faults: `sim.Assert(got == want, "acknowledged write lost: "+key)` |
| State never goes backwards | In the node: `sim.AlwaysGreaterThanOrEqualTo(len(log), committed, "log never shrinks below the commit index")`. The numeric forms (`AlwaysGreaterThan`, `AlwaysLessThan`, `SometimesGreaterThan`, ... and their `OrEqualTo` variants) put `left` and `right` in the failure and report a margin: the smallest one shows how close an `always` came to failing |
| One of several things holds | `sim.AlwaysSome(map[string]bool{"primary": p >= 0, "backup": b >= 0}, "some replica answers")`; `sim.SometimesAll(...)` for a combination that must happen at least once |
| Something must never happen | `sim.Unreachable("two leaders in the same term", term)` |
| A dangerous path actually ran | `sim.Sometimes(tornTail, "recovery found a torn tail")`, `sim.Reachable("a node restored from a snapshot")` |
| Concurrent clients see a linearizable history | Wrap each call: `op := sim.Put(client, key, value)`, then `op.Ok("")`, `op.Unknown()` on a timeout, or `op.Failed()` when it definitely did not apply. Use `sim.Get` for reads |
| A lock, queue, log, set or counter behaves like one | Set `"checker": {"model": "cas"}` (or `queue`, `append`, `set`, `counter`) in seedfall.json and record each call with `sim.Invoke(client, f, key, value)`, for example `sim.Invoke(c, "cas", "lock", []string{"", me})` then `op.Ok(swapped)`, or `sim.Invoke(c, "dequeue", "q", nil)` then `op.Ok(item)`. The table of operations per model is in docs/properties.md, Other models |
| Transactions are serializable | Set `"checker": {"model": "list-append"}`, record each transaction with `op := sim.Txn(client, sim.Read("x"), sim.Append("y", unique))`, and pass the micro-ops back with each read's `Value` set to the list it returned: `op.Ok(mops)`. Appended values must be unique per key. Failures name the anomaly (`G-single`, `G2`, ...) and the cycle |
| The system recovers | Set `"liveness": {"within": "10s"}` in seedfall.json: after `duration` the faults stop, crashed nodes restart, and a workload that does not finish within 10s fails as `liveness`. Inside a program, `sim.Eventually(func() bool { return served() }, "cluster serves reads again", 10*time.Second)` |
| The end state is right | A `"finally": {"name": "check", "pkg": "./check"}` program runs after the workload with faults stopped; check convergence and exactly-once effects there with `sim.Eventually` and `sim.Always` |
| Client retries are safe | `"include_workload": true` in `faults` crashes and pauses the workload too. Derive request ids from `sim.Node()` and saved progress, so a restarted client resends the same id, then check in `finally` that nothing was applied twice |

Rules:
- Keep messages constant string literals and pass changing values as extra arguments. seedfall catalogs literal messages before the sweep, and an `Always` or `Reachable` that no seed reaches fails the sweep.
- Add a `Sometimes` for each fault-dependent path you care about. The coverage table then proves the faults reached it.
- Use `sim.Event("name", details)` to mark a moment (a recovery finishing, a leader change) in the trace without asserting anything; triage then reads it next to the faults.
- Properties can live in nodes. Outside the simulator, `Always`, `Unreachable` and `Eventually` panic on violation and the others do nothing, so only put invariants in node code that must hold in production too.

## 3. Sweep and read the coverage table

```sh
seedfall run -c seedfall.json -seeds 1-100
```

Over MCP: `seedfall_run`, which returns `properties` with `seeds_reached`, `seeds_true`, a `problem` for each one and a `margin` for numeric ones.

- An `always` numeric property whose smallest margin stays far from 0 never got near failing: the faults may not be stressing it. A margin of exactly 0 on an `OrEqualTo` means the boundary was reached.

- A `Sometimes` that is never true means the faults never reached that path. Raise `crash_on_io` (around 0.005 to 0.02), set `torn_writes`, lengthen `duration`, or make the workload write more.
- If no outside fault can reach a path (a lost reply after a successful apply, an error return, a minimal quorum), mark it in the service with `if sim.Buggify("site") { ... }` and set `"buggify": true` in `faults`. The sweep then lists each site as reached, enabled and fired; see the MCP resource `seedfall://docs/buggify` (docs/buggify.md).
- If goroutines inside one node share state, sweep with `"preempt": {"strategy": "random"}` for short check-then-act windows and `"strategy": "pct"` for bugs that need one goroutine to stall while another runs a long stretch; set `preempt.steps` near the counted calls the trace's `pct:` line reports. Add `"loops": true` when the code has call-free loops (checksums, spin-waits). See `seedfall://docs/how-it-works`, section Preemption.
- A failure here may be a real bug. Switch to the `seedfall-triage` skill.

If a sweep keeps passing but a rare state or a deep `Sometimes` stays out of reach (a property the coverage table shows as never true, a bug that needs two rare things in one run), run `seedfall explore -c C` before raising the seed count. It branches from runs that reached something new, and a failure comes with a schedule file for shrink and replay. Randomness in the workload that should re-roll on a branch has to come from `crypto/rand` or `sim.Random`, not `math/rand`.

## 4. Grade the checks with mutants

```sh
seedfall mutate -c seedfall.json -seeds 1-30
```

The baseline must pass first. Then each mutant weakens one disk, network or clock guarantee under the nodes. Run a subset with `-only rename_not_atomic,net_dup_chunk`, or over MCP with `seedfall_mutate`:

| Mutant survived | Meaning | Fix |
|---|---|---|
| `fsync_noop` | Nothing checks that acknowledged data survives a crash, or crashes never land between a write and its fsync | Read back every acknowledged write after crashes. Raise `crash_on_io` and set `torn_writes` |
| `dirsync_noop` | Directory fsyncs are untested | Add `"strict_dirs": true` to `faults`, then check data that depends on a create or rename |
| `osync_ignored` | Writes to `O_SYNC` files are untested | Check the data written through those files |
| `fsync_corrupts` | Nothing compares the data read back after a crash with what was acknowledged | Read back every acknowledged value after crashes and compare it byte for byte, not only its presence |
| `rename_not_atomic` | Nothing checks a file replaced by rename (state, manifest, snapshot) after a crash | Read back the replaced file after crashes and assert it holds either the old or the new version. Raise `crash_on_io` so crashes land right after a rename |
| `truncate_not_durable` | Nothing checks a file's length after a crash that followed a truncation | Read back truncated or `O_TRUNC`-rewritten files after crashes and compare their whole content |
| `net_drop_after_close` | A response or final message cut off by a close goes unnoticed | Check that every request the client counts as done really got its full answer, and that the server applied every message sent before a close |
| `net_dup_chunk` | A duplicated request or message is not caught | Assert upper bounds too (nothing applied twice, `sim.AlwaysLessThanOrEqualTo(total, sent, ...)`), not only that acknowledged data survived |
| `monotonic_jump` | Timeouts and leases never meet a clock that runs backwards, or nothing checks what they protect | Turn on `clock_jump_per_sec`, then check lease-protected reads with a linearizability checker |

`not exercised` means the operation never ran, or had no effect in this config. That is fine when the service never uses it, such as `dirsync_noop` without `strict_dirs`, or `monotonic_jump` without `clock_jump_per_sec`.

Then mutate the service's own code: `seedfall mutate -c seedfall.json -seeds 1-20 -app -mutants 10` flips comparisons, skips early error returns and skips `Sync` calls in the node packages, one rebuild per mutant. A surviving source mutant names a line and a change the checks do not notice; it may also be dead code, so read the line before strengthening the workload.

Repeat steps 2 to 4 until every exercised mutant is killed, or until you can state why a survivor is equivalent, for example data the service never promises to keep. `seedfall mutate` exits 1 while any mutant survives.

## 5. Widen the fault model

Once the basic sweep and the mutants pass, add one fault class at a time and sweep again: `fsync_eio` (around 0.01), `strict_dirs`, `partition_per_sec`, then `pause_per_sec` and `clock_jump_per_sec` for lease and timeout logic, and for consensus or leader election `partition_topologies`, `clog_per_sec` and `slow_per_sec` (one-way links, jammed links and slow leaders), and for gossip or any other UDP protocol `udp_loss` and `udp_dup`. For storage code, add the disk faults next: `disk_bytes` and `write_eio` for write error paths, `read_corrupt` and `corrupt_on_crash` for checksums, and on replicated systems `lost_write`, `misdirected_write` and `bitrot_per_sec` (see the MCP resource `seedfall://docs/faults`, section Disk faults). Set `swarm` for long CI sweeps. A fault class that breaks the service is a finding, not noise: triage it.


<!-- skills/seedfall-setup/SKILL.md -->


# Set up seedfall in a Go module

seedfall builds each node (a Go `main` package) for `GOOS=wasip1`, runs every node on one simulated clock, and crashes, tears and partitions them from a seed. The workload is another `main` package: it drives the nodes and checks invariants with `sim.Assert` and friends. Setup is done when a 20-seed sweep runs and its property table shows that the workload got acknowledged writes and that a fault interrupted it.

## 1. Install

```sh
go install github.com/kunalgoesbyken/seedfall/cmd/seedfall@latest
seedfall doctor   # Go version, wasip1 builds, net_overlay, caches, memory; over MCP, seedfall_doctor
```

## 2. Inspect and scaffold

From the module root:

```sh
seedfall init -n      # report only, write nothing
seedfall init         # write seedfall.json and seedfall/workload/main.go
```

Add `-json` for the structured report. Over MCP, call `seedfall_init` with `{"dir": ".", "dry_run": true}`, then without `dry_run`. Init never overwrites: existing files are listed as kept.

Read the report in this order:

1. **wasip1 blockers.** Packages that fail to compile for wasip1, each with the compiler error and the import chain from the node. Nothing else works until these are gone.
   - `own_module: true`: move the platform-specific file behind a build tag and give wasip1 a portable version.
   - A dependency: read its `shim` line. If it names a shim, `compat_overlay` handles it (`seedfall init` turns that on). If it says `none`, upgrade first, since newer versions often build for wasip1, and otherwise add a `replace` in go.mod that points at a small in-process shim, as `examples/flockshim` does.
2. **cgo packages.** cgo is off under wasip1, so these either fail to build or fall back to a stub. Use a pure-Go alternative or stub them behind a build tag.
3. **main packages.** Every `main` package that imports `net` becomes a node. If init picked the wrong ones, such as a CLI, an admin tool or an existing test client, delete `seedfall.json` and rerun with one `-node` per real server, for example `seedfall init -node ./cmd/server`.
4. **next steps.** Follow them in order.

Some dependencies compile but fail at runtime under wasip1. For example, gofrs/flock returns `ErrUnsupported`. `compat_shims` in the report lists the ones `compat_overlay` covers; anything else shows up as a node error in the first run's trace, and gets a shim the same way.

If the module does not require seedfall yet, run `go get github.com/kunalgoesbyken/seedfall@latest`. The workload imports `github.com/kunalgoesbyken/seedfall/sim`.

## 3. Wire the workload

Open `seedfall/workload/main.go` and implement `put` and `get` against the service's real API:

- **Address.** A node is reachable by its name from `seedfall.json`. Set the workload's `-addr` argument in `seedfall.json` to `<node>:<port the service listens on>`. Init guesses port 8080.
- **Network.** If the nodes import `github.com/kunalgoesbyken/seedfall/sim`, dial with `sim.Dial`. Otherwise init turned on `net_overlay`, and plain `net.Dial` and `net/http` reach the simulated nodes. UDP works the same way, through `sim.ListenPacket` or plain `net.ListenUDP` under `net_overlay`; add `udp_loss` and `udp_dup` to the faults for a program that uses it.
- **Acknowledgement.** `put` returns nil only when the service acknowledged the write. Return an error for everything else. Writes whose outcome is unknown are simply not tracked.
- **Timeouts.** Set a deadline on every request (`conn.SetDeadline`, or `http.Client{Timeout: ...}`), so a crash or partition does not block the workload forever.

Keep the two `sim.Sometimes` lines. They prove the workload exercised the service and that faults hit it.

## 4. First sweep

```sh
seedfall run -c seedfall.json -seeds 1-20
```

Over MCP: `seedfall_run` with `{"config": "seedfall.json", "seeds": "1-20"}`.

| Output | Meaning | Next |
|---|---|---|
| `build ...` error | A wasip1 compile error | Go back to step 2 |
| `the workload got acknowledged writes` never true | `put` never succeeded | Check `-addr` and the port. `seedfall replay -c seedfall.json -seed 1` prints every node's output in the trace |
| `a fault interrupted the workload` never true | Faults never reached the workload | Raise `crash_per_sec` or lengthen `duration` |
| `FAIL seed N` with `class: bug` | Possibly a real bug | Use the `seedfall-triage` skill |
| `ok  20 seeds passed` | Setup is done | Use the `seedfall-properties` skill |

Then confirm that nothing leaks host nondeterminism:

```sh
seedfall run -c seedfall.json -seeds 1-20 -check
```

Once 20 seeds pass, harden the faults without editing the base config. Init wrote three profiles into `seedfall.json`; run them in order and treat each failure as a finding for the `seedfall-triage` skill:

```sh
seedfall run -c seedfall.json -profile strict -seeds 1-20       # strict POSIX directory durability
seedfall run -c seedfall.json -profile resilient -seeds 1-20    # adds the resilient fault preset
seedfall run -c seedfall.json -profile everything -seeds 1-20   # every fault, including disk corruption
```

Over MCP, pass `"profile": "resilient"` to any tool. Keep new variants as profiles in the same file, and use `"set": ["faults.crash_per_sec=2"]` or `-set` for a one-off change. If the service must start from existing data, such as a fixture database or a config file, give the node `"disk": "dir"` or `"files": {"guest/path": "host/path"}` instead of baking them into the binary.

The config fields and their defaults are in the MCP resource `seedfall://schema/config`. What each one means is in `seedfall://docs/faults` (docs/faults.md), and profiles, presets, `-set`, seeded disks and upgrades are in `seedfall://docs/config` (docs/config.md).


<!-- skills/seedfall-triage/SKILL.md -->


# Triage a failing seed

Every seedfall failure replays exactly from its seed. Do not guess from the failure message. Narrow the run to the few faults that matter, find where the outcome was decided, look at the bytes, and test the explanation by replaying a variation before you edit code. Below, `C` is the config and `N` the seed.

## 1. Classify

```sh
seedfall run -c C -seeds N
```

The output ends with `class:`.
- `bug`: the replay fails with the same trace. Continue.
- `nondeterministic`: something leaks host nondeterminism, such as real time, unseeded randomness or map iteration feeding I/O. The first diverging trace line is shown; `seedfall run -seeds N -check` goes further and names the first host call that differs (a clock read, a `random_get`, a file or network call) with its node and virtual time. Fix the leak first: it is a harness problem, not the bug.
- `timeout`: the real-time watchdog fired. A busy loop that never yields, or a host that is too slow. Rerun on an idle machine, or raise `watchdog`, before treating it as a bug. To make a busy loop reproducible, set `"preempt": {"loops": true}` with `liveness.within`: the spinning node then parks like any other and fails as `liveness` on the same seed every time.

The line after it, `artifacts: .seedfall/failures/<config>-seed-N`, is a folder with the full trace, a replayable `faults.json`, the operation history, each node's disk image at the failure, and `timeline.html` and `timeline.mmd`, a space-time diagram of every node, message and fault. Read `trace.txt` there instead of rerunning for it, and attach the folder if you file an issue.

Many failing seeds? `seedfall run -c C -seeds 1-500 -report .seedfall/report.html` groups them into findings, each with an example seed. Triage one example seed per finding. `seedfall findings -status new,regressed` reads that report back (findings, their status across runs, unmet properties) without running anything, and over MCP so does `seedfall_findings`.

## 2. Shrink

```sh
seedfall shrink -c C -seed N
```

This writes the minimal schedule to `.seedfall/seed-N.faults.json` and prints it, for example:

```
  427.268ms  crash server during disk op #56, restart at 761.268ms
     802ms  crash server, restart at 802ms
...
shrunk from 33 faults, 1m0s, 200 workload ops
         to 2 faults, 991ms, 63 workload ops
```

Every fault left is needed for the failure. Shrink also shortens downtimes, partitions and pauses, shrinks clock jumps, narrows partition sides and moves faults earlier, so the times that are left matter too. It trims the run's duration and, if the workload sizes itself with `sim.Budget`, its operation count. On a long run, add `-budget 300` (runs) or `-budget 10m` (time); if the output says the budget ran out, the schedule still fails the same way but may not be minimal. `crash ... during disk op #k` means the node died in the middle of its k-th disk operation, usually between a write and its fsync, or between a rename and the directory fsync.

A failure found by `seedfall explore` exists only under its schedule: pass the artifact's file to `seedfall shrink -c C -seed N -faults .seedfall/failures/<name>/faults.json`, and to the replay and inspect commands below (the output of `seedfall explore` prints all of them).

A failure with class `liveness` (the workload or the `finally` check did not finish within `liveness.within`, or a `sim.Eventually` never held) shrinks the same way. The faults left are the ones that leave the system stuck even after the `recovery:` line in the trace, where every fault stops and crashed nodes restart. Read the node output after that line to see which node stopped making progress.

## 3. Find the decisive moment

```sh
seedfall cause -c C -seed N
```

seedfall replays the run up to many moments, re-randomizes everything after each one, and prints the probability of failing from that moment on. The fault just before the jump to near 100% is the cause; faults after it are just how the damage gets observed. Raise `-points` and `-branches` for a finer curve.

Read what each node did around that moment with `seedfall logs -c C -seed N -node server -from 400ms -to 500ms` (add `-net-trace` for every message sent and read, `-grep` for a pattern, `-json` for slog fields). To stop the run there and look around, `seedfall debug -c C -seed N -at 427ms` opens a prompt: `where`, `net` (messages in flight), `faults`, `ls`, `cat` and `stat` on a node's live disk, `step`, `until <regex>` and `branch`. `seedfall trace grep -c C -seed N -e 'crash|fsync' -context 3` shows every node's lines around each match. Over MCP these are `seedfall_logs`, `seedfall_trace_search` and `seedfall_debug` with a `commands` list.

## 4. Look at the disk

```sh
seedfall inspect -c C -seed N -faults .seedfall/seed-N.faults.json
seedfall inspect -c C -seed N -faults .seedfall/seed-N.faults.json -at 427ms
seedfall inspect -c C -seed N -faults .seedfall/seed-N.faults.json -node server -cat data/kv.log
```

Inspect shows each node's files at the failure, or at the virtual time `-at`, with live and durable sizes, the byte ranges a crash would lose, directory entries that are not durable yet, the last torn write, and removed entries a crash would bring back. Take `-at` just before and just after the decisive fault from step 3. `-cat` prints one file's durable content. `-out dir` exports the durable images so the project's own tools can open them.

A `linearizability` or `isolation` failure is about the recorded history, not the disk. The failing run saved it to `.seedfall/seed-N.history.jsonl`, and a linearizability violation also to the timeline `.seedfall/seed-N.history.html`; find the first operation that no order explains. For `isolation`, the trace names each anomaly with its dependency cycle (`T4 -rw z-> T0 -wr z-> T6 -ww y-> T4`) and every transaction on it. `seedfall check -history .seedfall/seed-N.history.jsonl -model M` re-checks the file without running anything, also over MCP as `seedfall_check`.

## 5. Check the hypothesis with a replay

Write the explanation down as one sentence, for example "the crash in op #56 leaves a torn record, and recovery appends after it instead of truncating". Then test it by changing one thing and replaying.

- **Drop a fault.** `seedfall faults -c C -seed N -remove 2 -out hypothesis.json` copies `.seedfall/seed-N.faults.json` without its second fault (`seedfall faults -c C -seed N` alone lists the faults with their positions). Then run `seedfall replay -c C -seed N -faults hypothesis.json`. If it now passes, that fault is necessary. If it still fails, compare the failure message with the original: a different message means you uncovered a second bug, so note it and triage it separately.
- **Move a fault.** `-shift 1=-1` moves a `crash_io` entry one disk operation earlier, and `-shift 2=+20ms` moves a `crash` 20ms later, to put the crash just before or after the suspect operation; then replay again. On a `buggify` entry, the count is which hit of that site on that node fires; on a `preempt` entry (from `preempt.strategy` `pct`) it is the counted call at which that node's running goroutine is preempted, so a failure that survives shrinking with only a `preempt` fault is a goroutine interleaving inside that node. `-add '{"at":"1s","kind":"pause","node":"server","until":"1.5s"}'` adds a fault. Every edit is checked against the config (known nodes, `until` not before `at`, a timed fault inside the run) before it is written, and the schedule format is in `seedfall://docs/faults` under "Editing a schedule".
- **Change the world.** In a copy of `C`, turn off `torn_writes`, or turn `strict_dirs` on or off, and replay the same seed. If the failure needs torn writes, the bug is in recovery parsing. If it needs `strict_dirs`, a directory fsync is missing.

`replay` exits 1 and prints the trace when the seed fails, and ends with `seed N: ok, ... steps` when it passes. Over MCP, use `seedfall_faults_edit` (with `out`), then `seedfall_replay` with `faults`, and `seedfall_shrink`, `seedfall_cause` and `seedfall_inspect`, which take the same arguments as JSON.

`seedfall trace diff .seedfall/failures/<config>-seed-N hypothesis-trace.txt` shows the first line where two traces part, for a replay saved with `seedfall logs ... > hypothesis-trace.txt`.

Then confirm the explanation in the source: find the code that issued the disk operation named in the trace, and the code that read it back on restart.

## 6. Hand off

Record the seed, the minimal schedule file, the decisive fault, what inspect showed, and the replay that confirmed the hypothesis. Then use the `seedfall-fix-and-prove` skill.