Weft

Weft weaves deterministic order out of concurrent chaos.

Point it at a compiled Linux binary — no rewrite, no SDK, no special runtime — and one 64-bit seed determines every clock read, every random byte, and every thread interleaving in that process; with a simulated network, every message’s latency, loss, and partition fate is a pure function of the seed too. Record a run and it replays byte-for-byte on any platform Rust runs — a failing seed becomes a permanent, portable bug report. weft fuzz sweeps thousands of fault seeds against invariant checks and shrinks every violation to a minimal (1-minimal, not provably smallest) reproducer. Its built-in workload exercises the framework’s own network core; seed campaigns against your binary are scripted today, not one-command — see docs/fuzzing.md and the Chord campaign scripts for the pattern.

One honest caveat up front, not buried in the docs: in a live multi-process run, which process’s message reaches the simulated network first is OS-scheduled, so re-running the same seed live can reach a different outcome. Record the run you care about — the recording replays identically, always. Details: LIMITATIONS.md §3.

Weft is in the tradition of FoundationDB’s simulator and Antithesis. Unlike sim-first designs (FoundationDB, TigerBeetle) it retrofits onto binaries you already have. Antithesis also runs unmodified software — at the hypervisor level, as a commercial platform; Weft is open source, self-hosted, and intercepts at the libc boundary, with the narrower coverage that implies (docs/comparison.md states the trade-offs in both directions). The name comes from weaving: the weft is the crosswise thread carried through the warp to make fabric.

Status: working, pre-1.0. Interception, deterministic scheduling, simulated network, fault injection, record/replay, and fuzzing with shrinking are all implemented and validated against two protocols with formally-proven bugs (Chord, Raft) in unmodified C. Interfaces may still change — see VERSIONING.md. Read LIMITATIONS.md before you trust a result.

See it work

From a checkout (git clone https://github.com/arnavsinghal09/weft && cd weft), with the weft binary and shim built and on PATH per Install below, and a C compiler present:

$ cc -O2 -o /tmp/chrono examples/chrono.c
$ cc -O2 -o /tmp/race_bank examples/race_bank.c -lpthread
$ weft run --seed 42 -- /tmp/chrono | tail -1
total virtual elapsed: 2800026 us, c11 time 962138923

$ weft run --seed 42 -- /tmp/chrono | tail -1     # same seed
total virtual elapsed: 2800026 us, c11 time 962138923

$ weft run --seed 7  -- /tmp/chrono | tail -1     # different seed
total virtual elapsed: 2800026 us, c11 time 957028369

$ weft run --seed 3 -- /tmp/race_bank 2 2         # a real lost-update race
threads=2 iters=2 expected=4 balance=2 lost=2     # ← fires. every time.

$ weft run --seed 2 -- /tmp/race_bank 2 2
threads=2 iters=2 expected=4 balance=4 lost=0     # ← avoided. every time.

chrono.c mixes every libc clock API and sleeps between iterations; under Weft the sleeps advance virtual time instead of wall time, so it finishes instantly. race_bank.c has a classic split-critical-section bug — under Weft, whether the race fires is not luck, it’s the seed’s choice, and it’s 100% reproducible either way. The full walkthrough, including a network fault, a recorded/replayed run, and the fuzzer, is in the user guide.

Install

From crates.io:

cargo install weft-dst                   # the `weft` binary

The shim is built from a clone (it is a cdylib, not a cargo-installable binary):

git clone https://github.com/arnavsinghal09/weft && cd weft
cargo build --release -p weft-shim       # libweft_shim.so (Linux only)

weft run finds the shim via WEFT_SHIM, or next to the weft binary — copy it beside wherever cargo installed weft (usually ~/.cargo/bin; $CARGO_TARGET_DIR changes the build path too):

cp "${CARGO_TARGET_DIR:-target}/release/libweft_shim.so" "$(dirname "$(command -v weft)")/"

Or skip the copy and pass --shim <path> per run. weft replay and weft fuzz are pure computation and need no shim; they work on every platform, including macOS.

(The crate is weft-dst because the bare name weft is already taken on crates.io by an unrelated project; the installed binary is weft.)

Interception itself needs Linux (x86-64, glibc, dynamically linked targets — see LIMITATIONS.md §1). On macOS, run everything inside Docker; the user guide has the exact container recipe.

What it found

Pointed at our own minimal, uninstrumented C implementation of the 2001 Chord protocol (~300 lines; it knows nothing about Weft), Weft dynamically rediscovered the ring-maintenance flaw Zave proved formally in 2012: 57 of 500 seeded runs violate her correctness-critical invariants under the original protocol rules (55 broken rings, 2 permanently stranded appendages), falling to 8 once published liveness fixes are applied. Pointed at a minimal Raft leader-election implementation, it reproduced the dissertation’s votedFor-persistence edge case — 3 of 300 runs elect two leaders in the same term when vote state isn’t persisted across a crash restart, 0 of 300 once it is. Both studies, including where detection has a measurable blind spot, are in docs/case-study/CREDIBILITY_SUMMARY.md.

Documentation

Rendered docs site: https://arnavsinghal09.github.io/weft/ — the documents below as a browsable book.

Contributing

DEVELOPMENT.md is a complete onboarding path: clone, build, run the full sanitizer/fuzz suite, make a first change. Ground rules and quality gates are in CONTRIBUTING.md. Design decisions already made are recorded in PROJECT_NOTES.md. Security reports go through SECURITY.md.

License

Dual-licensed under MIT or Apache-2.0, at your option.

Weft user guide

From zero to reproducing a distributed-systems bug. Every command in this guide is copy-pasteable and was verified end-to-end in a clean container. When something needs Linux, the guide says so and gives the Docker form.

Contents: Quickstart · Concepts in 60 seconds · Worked example 1: taming a racy program · Worked example 2: simulated network + record/replay · Worked example 3: fuzz and shrink · Case study walkthrough: breaking Chord · Where to go next

Quickstart

Weft’s interception runtime is Linux-only (x86-64, glibc, dynamically linked targets — see ../LIMITATIONS.md §1). On macOS or Windows, run everything below inside Docker; the commands are identical inside the container.

On Linux (needs Rust ≥ 1.84 and a C compiler):

git clone https://github.com/arnavsinghal09/weft && cd weft
cargo build --release --workspace
cc -O2 -o /tmp/chrono examples/chrono.c
./target/release/weft run --seed 42 -- /tmp/chrono
./target/release/weft run --seed 42 -- /tmp/chrono   # byte-identical output
./target/release/weft run --seed 7  -- /tmp/chrono   # different timeline

On macOS / anywhere with Docker (one container, everything inside):

git clone https://github.com/arnavsinghal09/weft && cd weft
docker run --rm -it -v "$PWD":/work -w /work \
  -e CARGO_TARGET_DIR=/work/target/linux rust:1.84-bookworm bash
# now inside the container:
cargo build --release --workspace
cc -O2 -o /tmp/chrono examples/chrono.c
target/linux/release/weft run --seed 42 -- /tmp/chrono

What you should see: chrono.c mixes every libc clock API, formats real dates, and sleeps between iterations. Under Weft it (a) finishes instantly — sleeps advance virtual time, not wall time; (b) prints the same timestamps, dates, and values every run with --seed 42; (c) prints a different-but-equally-stable timeline with any other seed.

If output varies between two same-seed runs, the target escaped interception — check it is dynamically linked (file <binary> must not say “statically linked”) and not a Go binary (LIMITATIONS.md §1).

Concepts in 60 seconds

• One seed is the whole universe. --seed N determines every timestamp, every random byte, every thread-scheduling decision within a process, and every network fate. A single process with the same seed always produces the same run; a live multi-process cluster can still diverge in arrival order (see below) — but a recorded run always replays identically. A failing seed, once recorded, is a permanent bug report.
• Nothing is recompiled. The shim (libweft_shim.so) is LD_PRELOADed into your unmodified binary and interposes on libc: time, randomness, pthreads, UDP sockets, file sync.
• The broker is the network. With --net, UDP traffic is diverted to a seeded broker that decides every message’s latency, loss, and partition fate as a pure function of the seed.
• Recordings replay exactly. --record captures the broker order — the only non-seed input — so weft replay reproduces the run byte-for-byte, on any platform, forever. (Live cluster re-runs of the same seed are not identical — see LIMITATIONS.md §3c; record what you care about.)
• The fuzzer closes the loop. weft fuzz sweeps seeds, checks invariants, and shrinks every distinct violation to a minimal reproducer.

Worked example 1: taming a racy program

examples/race_bank.c has a textbook lost-update bug: it reads a balance under a lock, releases the lock, then re-locks to write back. Natively the race fires or not at the whim of the OS. Under Weft, the interleaving is the seed’s choice:

cc -O2 -o /tmp/race_bank examples/race_bank.c -lpthread

# seed 3: the race fires. Every time.
target/linux/release/weft run --seed 3 -- /tmp/race_bank 2 2
# → balance=2 lost=2  (expected 4)

# seed 2: the race is avoided. Every time.
target/linux/release/weft run --seed 2 -- /tmp/race_bank 2 2
# → balance=4 lost=0

Both results are 20/20 reproducible. To understand seed 3, re-run it with --strategy rr for a convoy-like schedule that is easier to read, and --trace to see every scheduling decision. This is the core workflow: find with random, study with rr, keep the seed forever.

Worked example 2: simulated network + record/replay

examples/pingpong.c is a two-node client/server pair: node 0 answers, node 1 asks (each instance reads its role from WEFT_NODE_ID, which --nodes assigns). Give the pair a high-variance network and record the run:

cc -O2 -o /tmp/pingpong examples/pingpong.c -lpthread

target/linux/release/weft run --seed 99 \
  --net "latency=uniform:1000-50000" --nodes 2 \
  --record /tmp/run.weftlog -- /tmp/pingpong

target/linux/release/weft replay /tmp/run.weftlog
# → replay identical: N op(s), stream digest xxxxxxxxxxxxxxxx
target/linux/release/weft replay /tmp/run.weftlog --check fifo,dup

--nodes 2 matters: with one instance, the server side waits forever for a client that was never launched. And know your target before adding loss=: pingpong’s client retransmits, but its server sends the reply exactly once and exits — drop that one datagram and the client retries into the void. (Loss-tolerant targets like examples/chord/chord_node.c handle loss=0.1 fine; that pairing is what the case study below uses.)

The replay re-derives every latency draw from the seed in the log header and verifies the recorded outcomes match — byte for byte. Replay works on macOS natively (it is pure computation; only run needs Linux).

Worked example 3: fuzz and shrink

Reordering under latency variance breaks per-channel FIFO by design — a perfect demo target:

target/linux/release/weft fuzz --config examples/fuzz/demo.json
# → exit 2; for each distinct violation:
#   shrunk : 138 → 7 ops in 122 execution(s)
#   repro  : weft-fuzz-out/repro-seed0-per-channel-fifo-….weftlog
#   verify : weft replay weft-fuzz-out/repro-seed0-….weftlog --check fifo,dup

(The exact op counts vary a little between live campaigns — cross-process arrival order is OS-scheduled, LIMITATIONS.md §3c — but every emitted reproducer replays identically, forever.)

Each reproducer is a fresh, self-consistent weft-log — typically under ten records — that replays identically and fails the same invariant on the same channel as the original run. The reduction scales: at ~14,000 ops the shrinker still lands on 7-op reproducers (docs/SCALABILITY.md §E). examples/fuzz/ci.json shows the CI usage: a reliable-network config where any violation is a genuine regression (exit 0 expected; the workflow in .github/workflows/fuzz.yml gates on it).

Case study walkthrough: breaking Chord (simplified)

The full study is in case-study/; this is the shape of it, runnable end to end. Chord (SIGCOMM 2001) is a distributed hash table whose published stabilization protocol was later proven (Zave, 2012) unable to maintain its ring invariant. Weft rediscovered that result dynamically, against an unmodified C implementation.

1. The target. examples/chord/chord_node.c (~300 lines of C) speaks Chord’s join/stabilize/notify protocol over real UDP. It knows nothing about Weft. CHORD_FIX selects the protocol variant: 0 = the 2001 paper, 1/2 = increasing liveness discipline from the literature.

2. The invariant. AtLeastOneRing: some cycle of best-successor pointers must exist among the live nodes. (Zave states three more — at most one ring, ordered ring, connected appendages — and the checker evaluates all four separately; a broken AtLeastOneRing is the headline failure mode.) chord-check scans a recording’s final state and renders the verdict (exit 0 ok / 2 violation / 3 uninformative).

3. One seeded run — and a live-run reality check.

cc -O2 -o /tmp/chord_node examples/chord/chord_node.c
CHORD_NNODES=7 CHORD_FIX=0 target/linux/release/weft run --seed 17 \
  --net "latency=uniform:1000-60000" --nodes 7 \
  --record /tmp/chord-17.weftlog -- /tmp/chord_node 6 45 3
target/linux/release/chord-check /tmp/chord-17.weftlog 6

Run this a few times. You will not always get the same verdict — 3 live runs of seed 17 during the writing of this guide came back OK, OK, VIOLATION. This is not a bug in the example; it’s the “Concepts” section’s live-run-arrival-order lesson, observed directly: which node’s message reaches the simulated network first is OS-scheduled, so a multi-process seed’s verdict isn’t fixed the way a single-process seed’s output is (LIMITATIONS.md §3c). Once you get a VIOLATION, that recording is now a permanent artifact — weft replay /tmp/chord-17.weftlog reproduces that exact run byte-for-byte forever, even though re-running the live seed might not hit it again.

4. The campaign. scripts/chord-campaign.sh sweeps many seeds and buckets exit codes, so you don’t have to hunt for a hit by hand. A 500-seed campaign found 57/500 violating for the 2001 protocol, 41/500 with the first fix, 8/500 with full liveness discipline — every hit leaves a recording, and the ordering (original ≫ partial fix ≫ full discipline) held across every re-run even as the exact counts drifted (docs/case-study/LEVEL_2_RESULTS.md).

5. The autopsy. Because a hit is a recording, you can interrogate the exact moment it broke — using whichever --recorded log from steps 3–4 actually came back VIOLATION:

target/linux/release/chord-trace /tmp/chord-17.weftlog 6   # or your campaign's hit

This shows, op by op, a node adopting a successor that had died while the notification was still in flight — Zave’s Figure-6 mechanism, caught live. The residual 8/500 traces to detection latency, not the protocol — the honest analysis is in case-study/LEVEL_2_RESULTS.md.

Reusing the pattern for your protocol: print your node’s state as a datagram (RPT <fields>) each tick, run under weft run --net … --record, and write a ~150-line checker over the recording — crates/weft-raft/src/ is the template (parse the report, fold into a Verdict, exit 0/2/3).

Where to go next

• Every flag, format, and exit code: REFERENCE.md
• How it actually works: architecture.md
• What it cannot do (read before trusting results): ../LIMITATIONS.md
• Scheduling / network / fault semantics: scheduling-model.md, network-model.md, fault-model.md
• Contributing: ../CONTRIBUTING.md

Weft reference

The complete user-facing surface: CLI commands and flags, exit codes, environment variables, the network-condition spec, the scenario DSL, the fuzz config, and the recording format. If behavior differs from this document, one of the two is a bug.

Compatibility policy for everything on this page: ../VERSIONING.md.

1. CLI

weft <COMMAND> [OPTIONS]

1.1 weft run

weft run --seed <N> [OPTIONS] -- <program> [args...]

Exit code: the target’s exit status passes through (single-process runs exec the target, so the status is the target’s). Cluster runs combine node statuses — 0 iff every node exited 0, otherwise a failing node’s status clamped to 1–255. Weft’s own failures print weft run: <message> and exit 1. Windowed runs exit 3 (discard) when the run is invalid rather than failed: a node crashed (killed by a signal, or its connection ended without the shim’s clean goodbye), the cluster deadlocked, a protocol violation was latched, or the --watchdog fired.

1.2 weft replay

weft replay <LOG> [--until <OP>] [--check <LIST>]

Exit codes: 0 replay identical and invariants hold · 2 invariant violation · 1 unreadable log / replay divergence.

On success prints replay identical: N op(s), stream digest %016x — the digest is deterministic and safe to compare across runs and machines.

1.3 weft fuzz

weft fuzz --config <FILE> [OPTIONS]

Exit codes (CI contract): 0 no violations · 2 violations found, reproducers + report written · 1 configuration or setup error.

1.4 Case-study checkers (chord-check, chord-trace, raft-check)

Standalone binaries from weft-chord / weft-raft; they scan a recording:

chord-check <recording.weftlog> <M>     # M = identifier bits (ring size 2^M)
chord-trace <recording.weftlog> <M>     # per-node pointer-state timeline
raft-check  <recording.weftlog>

Exit codes (shared contract): 0 invariant holds · 2 VIOLATION · 3 DISCARD · 1 unreadable recording. The meaning of DISCARD differs: for raft-check the seed exercised nothing (no leader was ever elected — uninformative); for chord-check the scenario violated the papers’ failure precondition (a failure stranded some node with no live successor), so the run cannot count against Chord.

2. Environment variables

All canonical names live in crates/weft-abi/src/lib.rs. weft run sets the starred ones for you; you only set them yourself when bypassing the CLI.

3. Network-condition spec (--net, WEFT_NET)

Comma-separated key=value clauses; all keys optional; empty spec = reliable network. Grammar implemented in crates/weft-net/src/config.rs.

Example: latency=uniform:1000-5000,loss=0.1,bw=2000000,partition=0+1|2

Every fate (delay, drop, order) is a pure function of (seed, src, dst, seq) — the same seed deals every message the same fate on every platform.

4. Scenario DSL (JSON)

Parsed and validated by weft-scenario (Scenario::from_json). Format is JSON only (YAML is not supported). Runnable examples: examples/scenarios/*.json.

{
  "name": "string (required)",
  "description": "string | null",
  "seed": 42,
  "nodes": [
    {"node_id": 0, "program": "./path", "args": ["--flag"]}
  ],
  "network": {
    "latency": "uniform:500-10000",
    "loss": 0.0,
    "bandwidth": null,
    "partitions": "0+1|2"
  },
  "filesystem": {
    "0": {"fsync_lies": true, "enospc_after_bytes": null, "torn_write_probability": 0.0}
  },
  "time_skew": { "0": 0 },
  "events": [
    {"time_ns": 1000000, "action": {"type": "crash", "node_id": 0}},
    {"time_ns": 2000000, "action": {"type": "start", "node_id": 0}},
    {"time_ns": 3000000, "action": {"type": "activate_partition", "spec": "0|1"}},
    {"time_ns": 4000000, "action": {"type": "clear_partition"}}
  ]
}

Validation rules (all violations produce a specific ScenarioError):

• nodes[*].node_id must be sequential from 0.
• events, filesystem, time_skew may only reference existing node ids.
• network.latency must parse per §3; loss and torn_write_probability must be in [0.0, 1.0]; bandwidth must be > 0 if present.
• partitions must match the 0+1|2 grammar; empty string clears.
• Events are sorted by time_ns during parsing.

Event actions: crash, start, activate_partition (takes spec), clear_partition.

5. Fuzz config (JSON)

Full semantics in fuzzing.md. Unknown fields are rejected (typos fail loudly), except the "//" comment slot.

6. Recording format (weft-log v2)

Full specification: recording-format.md. Essentials:

• Line-oriented JSON; line 1 is the header: {"format":"weft-log","version":2,"seed":…,"net":"…","window_ns":0,"meta":{…}}.
• Readers MUST reject unknown version values; v1 logs are rejected (their latency-only deliveries predate send-time anchoring). meta is informational only and MUST be ignored for replay purposes.
• Gzip is detected by content (magic bytes), never by file extension.
• The log records the broker linearization order and each send’s send_vt (the two non-seed inputs) — so seed + log reconstructs the run exactly; replay verifies a FNV-1a chain digest over every record.

7. Rust API (crates)

Published entry points a test harness is expected to use — everything else is implementation detail:

• weft_scenario::Scenario::from_json / ::validate, weft_scenario::parse_scenario, LatencyDistribution::parse, ScenarioError.
• weft_replay::Log::read, invariants (fifo, dup) via weft replay --check.
• weft_chord (report parsing + log-scanning verdict types) and weft_raft::{check, parse_report, Verdict} — models for writing your own recording checkers (scan log.records, parse your protocol’s state reports, accumulate a verdict; ~150 lines each).
• weft_abi::ENV_* constants — the canonical env-var names.

Installation

Weft is published on crates.io:

cargo install weft-dst      # installs the `weft` binary
cargo build --release -p weft-shim   # libweft_shim.so (Linux only)

Or from source:

git clone https://github.com/arnavsinghal09/weft && cd weft
cargo install --path crates/weft-dst
cargo build --release -p weft-shim

weft run finds the shim via WEFT_SHIM, or next to the weft binary:

cp "${CARGO_TARGET_DIR:-target}/release/libweft_shim.so" "$(dirname "$(command -v weft)")/"

Interception itself needs Linux (x86-64, glibc, dynamically linked targets — see Limitations §1). On macOS, run everything inside Docker; the user guide has the exact container recipe.

Crate pages: weft-dst · weft-abi · weft-net · weft-scenario · weft-replay · weft-fuzz

Weft architecture

This document describes the implemented deterministic simulation system: time & randomness (Phase 1), thread scheduling (Phase 2), network simulation (Phase 3), fault model & scenarios (Phase 4), recording & replay (Phase 5), fuzzing & shrinking (Phase 6), and the protocol case studies that validated it (Phase 7). Aspirational content is confined to the final section and clearly marked.

Read this before opening any code. Per-subsystem detail lives in the sibling documents: scheduling-model.md, network-model.md, fault-model.md, logical-time-model.md, recording-format.md, fuzzing.md, process-orchestration.md. Known boundaries are collected without spin in ../LIMITATIONS.md.

Big picture

weft run --seed 42 -- ./target-program args...
 │
 │  sets LD_PRELOAD=libweft_shim.so, WEFT_SEED=42 (+ WEFT_TRACE=1)
 │  then exec()s the target — exit codes and signals pass through
 ▼
target process
 ├─ libweft_shim.so (first in symbol resolution order)
 │   ├─ hooks: libc-ABI functions  ── seed active? ──► engine
 │   │                                    │ no
 │   │                                    ▼
 │   │                            dlsym(RTLD_NEXT) → real libc
 │   └─ engine: virtual clock + ChaCha8 domain streams
 └─ unmodified program code & real libc for everything else

One 64-bit seed fully determines: every wall-clock and monotonic timestamp, every value from the libc PRNG families, every byte from getrandom, getentropy, /dev/urandom, /dev/random, and AT_RANDOM. Same seed ⇒ same values, byte for byte; different seed ⇒ different values. Children inherit LD_PRELOAD and WEFT_SEED through fork/exec, so whole process trees are covered (each exec restarts virtual time — see limitations).

Crate layout

weft-shim and weft-abi keep a near-zero dependency tree (libc, rand_chacha, rand_core; all no_std-capable) because they execute inside arbitrary user processes.

How interception works

Every hook is a #[no_mangle] extern "C" function with a libc-identical signature, compiled into libweft_shim.so. With LD_PRELOAD, the dynamic linker resolves the target’s (and its libraries’) calls to our definitions. Each hook follows one shape:

1. state::shim() — lazily (once, on the first intercepted call) reads WEFT_SEED. Unset → None forever; the hook tail-calls the real function via dlsym(RTLD_NEXT, ...) (cached per call site in an AtomicPtr). This is the do-no-harm rule: a preloaded but unseeded shim is behaviorally invisible. A malformed seed is reported on stderr and treated as unset rather than half-working.
2. Seed active → answer from the engine. No allocation, no stdio, no locks other than the engine’s own, so hooks are safe from odd contexts (early init, tight loops, many threads).

Initialization is deliberately lazy rather than an ELF constructor: ctor ordering across preloaded libraries is unspecified, whereas by the time any libc call is interposed, libc is fully up.

Intercepted surface (complete list)

Time — time, gettimeofday, clock_gettime, clock_getres, timespec_get, nanosleep, clock_nanosleep (incl. TIMER_ABSTIME), sleep, usleep.

Randomness — rand, srand, rand_r, random, srandom, initstate, setstate, drand48, erand48, lrand48, nrand48, mrand48, jrand48, srand48, getrandom, getentropy, getauxval(AT_RANDOM).

Device files — open, open64, openat, openat64, read, pread, pread64, close, fopen, fopen64 — only diverted for the exact paths /dev/urandom and /dev/random; everything else passes straight through.

Thread scheduling (Phase 2) — pthread_create, pthread_join, pthread_exit, pthread_mutex_lock/trylock/unlock, pthread_cond_wait/ timedwait/signal/broadcast, sched_yield — the deterministic cooperative scheduler’s yield points. See docs/scheduling-model.md.

Network (Phase 3) — socket (AF_INET/SOCK_DGRAM only), bind, sendto, recvfrom — diverted to the seeded broker when WEFT_BROKER is set. See docs/network-model.md.

File I/O (Phase 4) — write, pwrite, pwrite64, fsync, fdatasync — track bytes written and optionally lie about fsync persistence when WEFT_FSYNC_LIES=1 is set. See docs/process-orchestration.md.

The virtual clock

A single AtomicU64 of nanoseconds:

• Monotonic time starts at 0. Every read advances it 1 µs (fetch_add), so (a) loops that poll the clock always make progress and (b) every observation is unique and strictly increasing, even across threads — concurrent readers get disjoint ticks.
• Realtime = 2000-01-01T00:00:00Z + a seed-derived offset in [0, 1 year)
  • monotonic. Different seeds land on different dates on purpose: date-dependent target logic gets exercised.
• Sleeps never sleep. nanosleep(750ms) advances virtual time 750 ms and returns 0 immediately; TIMER_ABSTIME deadlines fetch_max the counter. A million sleeping iterations run in real milliseconds.
• All clock ids map to one of those two timelines (CPU-time clocks report the monotonic value — see limitations).

The PRNG: ChaCha8, per-domain streams

The generator is ChaCha8 (rand_chacha::ChaCha8Rng) — a named, published algorithm; nothing hand-rolled. Why this one:

• Statistical quality: cryptographic-grade; passes PractRand/TestU01 with margin. A fuzzer will never trip over generator artifacts (LCG lattices, xorshift linearity).
• Speed: multi-GB/s; a draw is trivially cheap next to the interposed call itself (measured overhead below).
• Sub-streams natively: ChaCha has a 64-bit stream counter orthogonal to the key. Each interception domain gets its own stream of the same key:

Domain isolation means adding a getrandom call to a program does not shift the values its rand() loop sees — failures stay reproducible under small program changes.

Seed flow: WEFT_SEED (u64) → SplitMix64-expanded to a 32-byte ChaCha key (weft_abi::expand_seed) → five streams. srand(x)/srand48(x) re-key stream 0 from mix(run_seed, x): a program’s own reseeding stays meaningful, but a different --seed still changes everything. The caller-state variants (rand_r, erand48/nrand48/jrand48) advance the caller’s state buffer through SplitMix64 mixed with the run seed — deterministic, seed-sensitive, and safe for concurrent distinct state buffers.

Thread safety: each domain stream sits behind its own Mutex; the clock is lock-free. Cross-thread guarantee: the sequence each stream emits is fixed, so the multiset of values a group of racing threads draws is always deterministic. With the Phase 2 scheduler active (the default), thread order is itself a function of the seed, so which thread gets which value is deterministic too. Under --no-sched, or for threads the scheduler does not manage, attribution falls back to the OS schedule and only the multiset guarantee holds. (The entropy.c test target is built around exactly that weaker invariant: everything it prints is commutative across threads.)

/dev/urandom mechanics

open("/dev/urandom") actually opens /dev/null — reserving a genuine fd so close/fstat/dup remain sane — records the fd in a fixed 64-slot atomic table, and read/pread on recorded fds fill from the shared stream 2. read(2) has no read-ahead, so every byte drawn from stream 2 is a byte the caller received; concurrent reads draw a scheduling-dependent interleaving of one fixed sequence, so their multiset is deterministic (the Phase 1 cross-thread guarantee).

fopen cannot reuse the fd trick (glibc stdio reads through an internal, non-interposable alias of read), so it returns a fopencookie stream. Here buffering matters: glibc reads ahead in ~8 KiB chunks and discards the unconsumed tail at fclose. If every stream shared stream 2, which byte ranges got discarded would depend on how threads interleave their chunked read-aheads — making the bytes actually delivered to the application vary run to run. So each fopened random device instead gets its own independent substream (DevFileRng): a fresh ChaCha8 stream keyed by the run seed with a stream id of 0x1000_0000 + N, where N is the process-global open order. Read-ahead then only advances that file’s private sequence, the discarded tail is a deterministic function of N, and the substream’s own Mutex (not glibc’s FILE lock) makes concurrent freads data-race free. The base 0x1000_0000 sits far above the fixed domain stream ids (0..=4), so a substream can never collide with a domain. If the fd table is ever full (64 concurrently-open random fds), we log under --trace and hand out the real device rather than fail.

Tracing

weft run --trace (or WEFT_TRACE=1) makes every hook log one line to stderr — formatted in a stack buffer, written with one raw write(2), no allocation — e.g. [weft] clock_gettime(1) -> 3.000004000.

Above the shim: broker, recording, replay, fuzzing

The pieces outside the target process compose in one pipeline:

• Broker (weft-net, Phase 3). With --net, weft run hosts a broker on a Unix-domain socket; the shim diverts AF_INET/SOCK_DGRAM traffic to it. All fault decisions (latency, loss, reordering, partitions, bandwidth) come from a pure decision core — a function of (seed, src, dst, seq) — so the same seed always deals every message the same fate. The broker’s linearization order is the single source of truth for “what happened”.
• Recording (weft-replay, Phase 5). --record <LOG> streams every broker operation to a weft-log file (v1, gzip-aware). The broker linearization order is the only non-seed input to a run, so the log plus the seed reconstructs the run exactly. See recording-format.md.
• Replay (weft replay). Re-executes a recording against the same pure core and verifies byte-for-byte identity (a stream digest), optionally checking invariants (--check fifo,dup). Replay of a recording is exact on every platform — no shim required.
• Fuzzing (weft fuzz, Phase 6). Sweeps fault seeds over a deterministic workload against the decision core, dedups violations by identity, and delta-debugs each one to a minimal reproducer log that weft replay verifies. See fuzzing.md.
• Orchestrator + scenarios (weft-scenario, Phase 4). A JSON scenario describes nodes, network faults, filesystem faults, and timed events (crash/restart/partition changes); the orchestrator executes it. See process-orchestration.md.

Validation (Phase 7). The whole stack was pointed at real protocol implementations: Chord (2001) stabilization — falsified, 57/500 seeds break the ring, reduced to 8/500 with published fixes — and Raft leader election — the dissertation’s votedFor-persistence edge case reproduced (3/300) and falsified by the fix (0/300). See docs/case-study/CREDIBILITY_SUMMARY.md.

Empirical results (Phase 1 exit criteria)

Measured on the CI configuration (Linux, x86-64; see crates/weft-dst/tests/e2e.rs and scripts/bench-overhead.sh):

• Reproducibility: chrono, montecarlo, entropy produce byte-identical stdout across repeated runs of the same seed (checked for seeds 0, 1, 42, 0xDEADBEEF, u64::MAX), and different stdout across different seeds.
• Passthrough: with LD_PRELOAD set but no WEFT_SEED, outputs vary run-to-run and programs behave normally.
• Overhead: see the table in the phase notes / CHANGELOG, produced by scripts/bench-overhead.sh (best-of-5). The dominant cost is ~5M interposed PRNG calls in montecarlo; chrono is faster under Weft because sleeps are virtual.

Current limitations (the honest list)

• Statically linked binaries are not intercepted. LD_PRELOAD works by interposing dynamic symbol resolution; a static binary has no PLT to interpose. Planned fallback: ptrace/seccomp-notify syscall interception (future work below).
• Raw syscalls bypass the shim. A program that issues syscall(SYS_getrandom, ...) or inlines rdtsc/rdrand instructions gets real nondeterminism. This includes Go binaries (runtime does raw syscalls) and any use of vDSO by address rather than through libc symbols.
• vfork/posix_spawn children are covered only via env inheritance; an exec into a setuid binary drops LD_PRELOAD (glibc secure-mode) and escapes determinism silently.
• Cross-thread value attribution is scheduling-dependent under --no-sched and for unmanaged threads (see above). With the scheduler active (the default), attribution is deterministic; thread-safety is guaranteed and sanitizer-checked in both modes.
• CPU-time clocks are approximated (CLOCK_PROCESS_CPUTIME_ID / CLOCK_THREAD_CPUTIME_ID return virtual-monotonic time, not modeled CPU consumption).
• getcpu, sched_getcpu, /proc/*/stat timings, times(2), getrusage(2) are not virtualized — programs deriving entropy or logic from them stay nondeterministic.
• PIDs, TIDs, ASLR addresses, and gettid() are real. A program seeding from getpid() or hashing pointer values is not yet deterministic. (Weft’s own srand(getpid())-shaped gap; ASLR pinning arrives with the orchestrator’s namespace work.)
• random_r/initstate_r (glibc reentrant family) and arc4random* (glibc ≥ 2.36) are not yet interposed.
• initstate/setstate return the caller’s buffer rather than the previous internal buffer; glibc programs that swap state buffers and expect the old pointer back will see a benign lie (their sequences are seed-derived under Weft anyway).
• musl: the open→read fd path works, but fopen("/dev/urandom") uses fopencookie, which musl also provides; however the shim is only CI-tested against glibc today.
• fopen substream indices are assigned in open order. With the scheduler active, open order is seed-deterministic and this is a non-issue. Under --no-sched the order is OS-scheduled: each stream’s bytes are still reproducible given its index, and a program that combines every stream commutatively (like entropy.c’s XOR/sum) stays fully deterministic, but logic depending on which thread opened which stream sees scheduling-dependent attribution.
• File-descriptor duplication of random fds (dup, dup2, fcntl(F_DUPFD)) is not tracked: a duped random fd reads real /dev/null (EOF). No real program observed doing this yet; fix is a straightforward hook addition.
• sleep interaction with SIGALRM is not modeled (virtual sleeps never observe signals). Signal determinism in general is out of scope until the scheduler phase.

Future work

• ptrace/seccomp-unotify fallback for static binaries & raw syscalls — intercept at the syscall boundary instead of the PLT. Sketch: seccomp filter marks clock_gettime/getrandom/openat for user-notify; a supervisor answers from the same engine. Slower (context switch per call) but closes the static-binary and Go gaps. Not started; the engine was deliberately built process-external-safe (pure functions of seed + counter) so it can serve both mechanisms.
• Folding live-target fuzzing (the weft run --record path) into the weft fuzz sweep loop, so shim-path campaigns get the same dedup-and-shrink treatment the broker-core sweep has today.

Logical Time in Weft — Unified Model (Phase 4)

Problem Statement

Phases 1–3 each handle time independently:

• Phase 1: Virtual clock (AtomicU64 nanoseconds). Monotonic starts at 0, every read advances by 1 µs. Realtime = 2000-01-01 + seed-offset + monotonic.
• Phase 2: Scheduler token model. One thread runs at a time; which one is a function of seed. Time advances only via yield points.
• Phase 3: Broker ordering key. Network delays are modeled as entries in a BinaryHeap<(delay, insertion_index)>. “Delay is an ordering key, not wall time” — the broker has no synchronization with the virtual clock or cross-process time base.

Phase 4 unifies these by establishing a single logical timeline that governs:

• When network messages are delivered (Phase 3)
• When file I/O operations complete (Phase 4 new)
• When clock skew applies to each node (Phase 4 new)
• When process crashes and restarts occur (Phase 4 new)
• Virtual clock reads in each process (Phase 1 extension)

Key Insight: Logical Time is Scheduling Order

A logical time T is an entry point into a deterministic event queue. The key realization:

• The broker’s BinaryHeap already implements this: events are ordered by (delay_key, insertion_order), and the queue is traversed deterministically.
• Virtual clock reads are observations of logical time, not a separate clock.
• File I/O delays, network latencies, and clock skew are all scheduled events, drawn from the same seeded PRNG stream as everything else.

The Model

Global Event Queue (Broker-wide)

The broker maintains a BinaryHeap<ScheduledEvent> where ScheduledEvent is:

#![allow(unused)]
fn main() {
pub struct ScheduledEvent {
    pub time_key: (u64, u64),  // (logical_time_ns, insertion_order)
    pub event_type: EventType,
}

pub enum EventType {
    NetDeliver { src, dst, seq, payload },
    FileIoComplete { node, fd, result },
    ClockSkewChange { node, offset_ns },
    ProcessCrash { node_id },
    ProcessStart { node_id },
    FaultActivate { node_id, fault_id },  // e.g., activate partition
}
}

Per-Node Virtual Clock

Each node process has a virtual clock that is a view into the global timeline:

virtual_clock[node_i] = global_base_time + node_clock_offset[node_i]

Where node_clock_offset[node_i] is:

1. Initially 0 (or seed-derived to make realtime dates differ)
2. Changed by ClockSkewChange events
3. Visible to the node’s clock_gettime() calls

Determinism: Per-Timeline Seeding

The source of every time value is a seeded PRNG stream, not a shared pool:

• Network message delays: seeded by f(seed, src, dst, seq) (Phase 3, unchanged)
• File I/O delays: seeded by f(seed, node_id, fd, op_type, seq_on_fd) — same per-fd sequence determinism as network
• Clock skew changes: seeded by f(seed, node_id, skew_index) — one sequence per node
• Process crash timing: seeded by f(seed, node_id, crash_index) — one sequence per node

Atomicity and Isolation

The broker is single-threaded (Phase 3 current design). Within one broker round-trip:

1. Node calls broker with (operation, details)
2. Broker looks up timing via seeded fate function
3. Broker enqueues the result with absolute time_key
4. Broker returns immediately (no waiting for delay)
5. Next receiver of that result sees it at the right logical position

Cross-process ordering is OS-scheduled (Phase 3 honest limitation). But once an event is enqueued, its position is deterministic.

Examples

Single-fault: Network latency causes reordering

Seed 42, --net "latency=uniform:1000-5000"

Monotonic timeline (insertion order):
0. Node-0 sends PING to Node-1 (seq=0)
   → fate(42, 0, 1, 0) = delay=3200ns
   → enqueue at time_key=(3200, 0)

1. Node-1 receives nothing; yields
2. Node-0 sends PING to Node-1 (seq=1)
   → fate(42, 0, 1, 1) = delay=1200ns
   → enqueue at time_key=(1200, 1)

3. Next Node-1 recv:
   → dequeue (1200, 1) first → seq=1 arrives before seq=0
   → seq=0 still pending at (3200, 0)
   → reordering!

Multi-fault: Network loss + file sync-lies

Node writes a message to disk (“value=42”), then sends it to the replica.

Scenario:
  - latency=fixed:100ns (deterministic delivery timing)
  - loss=0.5 (50% drop, seeded)
  - fsync-lies: every other fsync returns success but drops recent writes

Execution (seed S):
1. Node-0 write("value=42") → local file (unsynced)
2. Node-0 fsync() → fsync-lies returns success but doesn't actually persist
3. Node-0 send("I have value=42") to Node-1
   - fate(S, 0, 1, seq) = {delay: 100ns, drop: no}
   - Replica receives "value=42"
4. Node-0 crashes (scheduled event)
5. Node-0 restarts
6. Node-0 read("value=42") → EOF or old value (because fsync lied)
7. Node-0 send("I have <old value>") to Node-1
   - Replica sees conflicting updates — bug surface!

Without fsync-lies or without crash: bug never manifests.

Honest Limitations (Phase 4)

• Cross-process ordering remains OS-scheduled. Which process’s syscall reaches the broker first is timing-dependent. But once in the queue, position is deterministic.
• Per-fd I/O delay independence. File descriptor delays are seeded per-fd, so an fd’s delays are reproducible but concurrent writes to different fds have timing that may interleave differently per run (like network, until Phase 2 scheduler is extended to file I/O).
• Crash-and-restart granularity. Crashes are modeled as instantaneous events. Real OS crash recovery (log replay, state consistency) is out of scope — the scenario author must model what remains.
• File-system consistency model is simplified. No true journaling, crash atomicity, or order-of-durability constraints beyond what fsync-lies and ENOSPC model.

Scenario DSL (Phase 4)

Timed fault event sequences are written in a JSON scenario configuration (the implemented format — see examples/scenarios/ for runnable files):

{
  "name": "file-sync-reordering",
  "description": "Replica divergence when fsync lies and network reorders",
  "seed": 42,
  "nodes": [
    {"node_id": 0, "program": "./target", "args": ["--role=writer"]},
    {"node_id": 1, "program": "./target", "args": ["--role=replica"]}
  ],
  "network": { "latency": "uniform:100-10000", "loss": 0.2 },
  "filesystem": {
    "0": { "fsync_lies": true, "enospc_after_bytes": null }
  },
  "time_skew": {},
  "events": [
    { "time_ns": 1000000, "action": { "type": "crash", "node_id": 0 } },
    { "time_ns": 2000000, "action": { "type": "start", "node_id": 0 } }
  ]
}

Validation and Testing (Phase 4)

1. Parser property tests: generated scenario JSON (valid and deliberately malformed) never panics; parse always returns Result<Scenario, ParseError>.
2. Per-fault-type isolation: each fault type (network loss, fsync-lies, ENOSPC, crash) is tested in isolation with a minimal scenario.
3. Multi-fault interaction: at least one scenario demonstrates a bug that manifests only when two or more fault types are active together.

What Changes, What Stays the Same

Changes

• Broker’s BinaryHeap becomes the global logical timeline
• Virtual clock becomes a per-process view (with optional skew offset)
• New crate: weft-scenario for DSL parsing and validation
• File I/O hooks in shim for torn write, ENOSPC, fsync-lies

Stays the Same

• Phase 1 determinism guarantees (same seed → same values)
• Phase 2 scheduler token model (extends to file I/O yield points)
• Phase 3 network per-message fate (integrated into global timeline)
• Interception architecture (hooks + engine)

The Weft scheduling model (Phase 2)

Phase 2 makes multi-threaded execution order deterministic, entirely in userspace: exactly one logical thread makes forward progress at a time, and which one runs next is a pure function of the run seed.

What counts as a yield point

A yield point is any interposed call where the running thread hands control back to the scheduler, which then deterministically selects the next thread. The precise set (see crates/weft-shim/src/hooks/thread.rs and hooks/socket.rs):

Everything between two yield points executes atomically with respect to other managed threads — see the limitations section.

The token model

Real OS threads exist, but a thread may run only while it holds the single scheduler token (Scheduler::wait_turn). At every yield point the holder calls into the scheduler (pick_next), which:

1. computes the enabled set — threads whose modeled state is Runnable (not blocked on an owned mutex, an unsignaled condvar, or an unfinished join target);
2. selects one deterministically (see strategies below);
3. wakes it via a process-internal Condvar and parks everyone else.

The scheduler models mutexes, condition variables, and joins rather than delegating to the real pthread primitives: managed threads never call the real pthread_mutex_lock/cond_wait at all. Mutual exclusion follows from the token (one runner at a time); the happens-before edges the target expects from its locks are provided by the scheduler’s own internal std::sync primitives, which every hand-off crosses. Modeled state is keyed by the pthread object’s address, so distinct mutexes contend independently.

Registration is lazy: the main thread registers at its first pthread_create. A program that never creates a thread never pays for the scheduler, and every pre-existing Phase 1 behavior is unchanged.

Interleaving-selection strategies

Selected with --strategy (WEFT_STRATEGY), both driven by a dedicated ChaCha8 stream (Domain::Scheduler) of the run seed:

• random (default): uniform draw from the enabled set at every scheduling point. Explores the interleaving space aggressively — across seeds you visit maximally diverse schedules, which finds concurrency bugs fastest in a fuzzing loop. The cost: adjacent decisions share no structure, so a human replaying a trace sees threads ping-pong arbitrarily.
• rr (round-robin with perturbation): rotate through enabled threads in tid order, but with probability 0.2 make a random pick instead. Runs are mostly convoy-like and easy to follow when debugging a specific failure — “thread 2 ran, then 3, then 4” — while the perturbation keeps a single seed family from being blind to order-dependent bugs. The cost: per seed it explores far fewer distinct interleavings than random.

The tradeoff in one line: random to find bugs, rr to understand one.

Both are pure functions of the seed; a schedule found with either replays byte-identically.

Deadlock detection

If the enabled set is empty while unfinished threads remain, the target is deadlocked (e.g. an ABBA lock cycle: examples/deadlock.c). The scheduler prints [weft] DEADLOCK: N thread(s) blocked … to stderr and aborts — deterministically, so a deadlocking seed is a perfectly reproducible test case. Seeds where the interleaving avoids the cycle complete normally. Threads blocked in external work (a broker recv poll loop) never enter a blocked model state — they poll with yield_now — so network waiting cannot be misreported as deadlock.

The race proof (examples/race_bank.c)

The bug is a split critical section: deposit reads the balance under the lock, releases it, then re-locks to write back read+1 — a real refactor pattern (“minimize time under lock”). The unlock/lock boundary is a yield point, so the scheduler can (or can not) interleave another thread’s read-modify-write into the window, purely by seed:

• 2 threads × 2 iterations, --strategy random:
  • seed 3 triggers the lost update: balance=2 lost=2, 20/20 runs.
  • seed 2 avoids it: balance=4 lost=0, 20/20 runs.
• At scale (4 threads × 25), the race is pervasive: e.g. seed 1 loses exactly 62 updates, every run.

Pinned in CI by crates/weft-dst/tests/sched_e2e.rs; scheduler-level reproducibility, thread churn, nested locks, and condvar rendezvous are covered in-process by crates/weft-shim/tests/sched_harness.rs (sanitizer- friendly).

Coverage / stats

--stats (WEFT_SCHED_STATS=1) prints, at exit: logical thread count, total scheduling decisions, and the set of distinct yield-point sites hit (mutex_lock, cond_wait, net_recv_wait, …). A rough but useful coverage signal for a future fuzzing loop: a seed corpus can be ranked by which sites (and how many decisions) it reaches.

Honest limitations

• No preemption at arbitrary instructions. Yield points exist only at interposed libc calls. A pure-compute region — including one that races on shared memory with plain loads/stores and no locking at all — runs atomically under Weft and its internal races are invisible to the scheduler. A hypervisor or instruction-level instrumentation (ptrace single-step, binary translation) would be required to interleave inside such regions; that is explicitly out of scope. Weft explores the interleavings of synchronization and I/O operations, which is where most distributed-systems bugs live, and race_bank’s bug is reachable precisely because its racy window is bracketed by yield points.
• Data races are serialized, not detected. Because only one thread runs at a time, TSan-style simultaneous-access detection cannot fire under the scheduler. Weft finds order bugs (lost updates, stale reads, deadlocks) by exploring schedules, not access-level races. Run the suite with WEFT_SCHED=0 under TSan for the latter (the --no-sched mode exists partly for this).
• pthread_cond_timedwait ignores its deadline — modeled as an untimed wait. Code that relies on the timeout alone (no signaler) to make progress will deadlock-detect instead. Wiring timeouts to virtual time is future work.
• Unmanaged threads pass through. Threads created before the shim activates, or by clone(2) directly, use real pthread primitives and real OS scheduling. Interaction between managed and unmanaged threads is passthrough-correct but not deterministic.
• Reentrancy no-ops. While inside scheduler/bootstrap machinery, pthread_mutex_* calls return success without locking (safe: such contexts are effectively single-threaded by construction — startup, or holding the token). A hostile-weird target that ships its own interposed pthread symbols ahead of ours in the preload chain is out of scope.
• Spawn/fork boundaries. Each process has its own scheduler; Phase 3’s broker gives cross-process message determinism, but cross-process interleaving determinism is future work (see docs/network-model.md).
• pthread_rwlock, pthread_barrier, semaphores are not yet modeled and pass through to the real libc. They behave correctly but their contention is scheduled by the OS, not the seed. Extending the model is mechanical (same pattern as mutexes) and planned.

The Weft network model (Phase 3)

Phase 3 extends seed-determinism to networking: processes communicate over ordinary UDP sockets, but every datagram is routed through a central broker that applies a seeded fault model — latency, loss, reordering, partitions, a bandwidth cap — instead of reaching the kernel network stack.

Architecture

 target process A                weft (parent process)         target process B
┌────────────────┐              ┌─────────────────────┐       ┌────────────────┐
│ app: sendto()  │              │  Broker              │       │ app: recvfrom()│
│   ↓ shim hook  │  Unix socket │   ├ routing table    │ Unix  │   ↑ shim hook  │
│ weft-shim ─────┼──────────────┼──▶├ per-dest queues  ├───────┼── weft-shim    │
│ (LD_PRELOAD)   │  wire proto  │   └ FaultModel(seed) │ socket│  (LD_PRELOAD)  │
└────────────────┘              └─────────────────────┘       └────────────────┘

• weft run --net <SPEC> [--nodes N] -- prog hosts the broker inside the weft process, then spawns N instances of the program with WEFT_BROKER (broker socket path), WEFT_NODE_ID (0..N-1), and the usual seed/scheduler environment. Node i’s conventional IP is 127.0.0.(i+1).
• In the target, the shim intercepts socket(AF_INET, SOCK_DGRAM): instead of a kernel UDP socket, the returned fd is a Unix-stream connection to the broker. bind/sendto/recvfrom speak a small length-prefixed protocol (weft-net::wire) over it. The target closes the fd through the interposed close(2) like any other descriptor.
• The broker keeps one delivery queue per connection, a bound: addr → conn routing table, and per-channel sequence counters feeding the fault model.

The determinism principle: per-message fate

Each datagram’s fate — dropped or delivered, and with what delay — is a pure function of (run seed, src addr, dst addr, per-channel sequence number) (weft-net::fault::FaultModel::fate). It is not drawn from a shared PRNG in broker-arrival order, so it cannot depend on how the OS scheduled the sending processes. The k-th datagram on channel A→B meets the same fate in every run with the same seed. This is what makes a network-triggered bug replayable.

Delivery order to a receiver is by (sampled delay, global enqueue index) — a deterministic ordering key, not a wall-clock timer (see “delay is an ordering key” below).

The fault model (--net spec)

Comma-separated key=value clauses (weft-net::config):

Reordering is not a separate knob: it emerges when a latency distribution with variance gives a later datagram a smaller delay — the same mechanism as real networks. latency=fixed (or the default empty spec) can never reorder.

Two latency distributions, why both: uniform gives dense, bounded jitter — the right default for shaking out ordering assumptions, since every burst gets thoroughly shuffled. exp is heavy-tailed: most datagrams are fast, a few are very late, which is the realistic shape of congestion and better at finding bugs that need one straggler (a stale ack arriving after a new election, say) rather than wholesale shuffling.

Scheduler integration (Phase 2 × Phase 3)

Network I/O is exactly the blocking-call class that Phase 2 yield points cover, and the integration is deliberate:

• A broker round-trip (request + reply) happens while holding the scheduler token, so it is one atomic step in the deterministic schedule.
• A managed thread’s recvfrom never parks inside the broker. It polls (non-blocking Recv), and on Empty calls the scheduler’s yield_now — so “waiting for a message” is a Phase 2 yield point, and which thread runs next (e.g. the sender that will produce the message) is chosen deterministically from the seed.
• sendto yields after the broker acknowledges, giving the scheduler the chance to run the receiver next.

Consequence: a multi-threaded single process whose threads act as nodes is fully deterministic — scheduling, message content, fates, and delivery order all derive from the seed. This is the same modeling trick FoundationDB’s simulation uses (all simulated “processes” inside one real process), and it is what examples/kvreplica.c does.

Simulated vs. simplified — the explicit list

Simulated faithfully:

• UDP datagram semantics: unreliable, unordered, message-boundary-preserving; datagrams to unbound ports are silently discarded; receivers see truncated reads if their buffer is short.
• Loss, latency-driven reordering, partitions, bandwidth-as-delay, all seeded.
• Nodes joining, leaving (connection drop unbinds their addresses), and rejoining (re-binding the same address later works).

Deliberately simplified, by decision rather than accident:

• TCP is not simulated. SOCK_STREAM passes through to the kernel untouched. Simulating TCP means simulating connection state, flow control, and partial-delivery semantics — a Phase 4+ project. Programs that must be simulated today use UDP.
• connect+send/recv on UDP sockets is not intercepted — only bind/sendto/recvfrom. getsockname, setsockopt, poll/select/ epoll on simulated sockets are also out of scope for now.
• Delay is an ordering key, not wall time. The broker delivers the lowest-delay pending datagram whenever the receiver asks; it does not hold datagrams for their delay in any clock. Latency values therefore shape relative order (and hence reordering), not measured round-trip time. There is no cross-process virtual time base to anchor real delays to — that unification is future work.
• Bandwidth is per-datagram serialization delay (len/rate added to the ordering key), not a shared queue with backpressure. It biases ordering against large datagrams, which is the property distributed-systems bugs care about; it does not model queue depth or drops under saturation.
• AF_INET6 and raw sockets pass through.

Honest limitations

• Cross-process interleaving is not unified. Fates and per-channel content are seed-deterministic across processes, but which process’s syscall reaches the broker first is OS scheduling. Concretely: with --nodes 2, the two nodes’ stdout lines may interleave differently across runs, and a datagram’s arrival relative to a different channel’s recv is timing-dependent. Where the racing entities are threads of one process, the Phase 2 scheduler removes this nondeterminism completely — hence the threads-as-nodes pattern for bug reproduction. True multi-process determinism requires extending the cooperative scheduler across process boundaries (a broker-side global turn model), which is future work.
• Startup discard races are real UDP behavior. A send racing a peer’s bind may be discarded; robust UDP code retries (as pingpong.c does).
• Managed polling spins. A managed thread waiting for a datagram busy-polls broker + yield_now. Deterministic, but CPU-hungry while starved; a parked-thread integration with the scheduler is future work.
• Broker requests hold the token, so heavy per-datagram traffic in one thread starves others only at yield points, and everything network-bound is serialized process-wide. That is the price of determinism, and it shows in the benchmark below.

Overhead (measured)

scripts/bench-net.sh, 5000 round trips (10 000 datagrams) between two threads of one process, container on Apple-silicon host, best of 5:

≈285× slower per datagram. The cost is one Unix-socket round-trip to the broker per operation plus token-serialized execution and poll-yield receive loops. For simulation workloads (protocol logic, not bulk transfer) this is acceptable; bulk-data phases should be modeled, not replayed byte-for-byte.

The bug proof (examples/kvreplica.c)

A replicated register applies UPDATE:v messages in arrival order with no version check — the classic “UDP from one sender is mostly ordered” fallacy. A writer thread sends v=1..8 then a READ. Under --net latency=uniform:1000-50000:

• seed 1: the tail of the write burst is reordered; the replica overwrites v=8 with an older write and the read returns 6 (stale) — 20/20 runs.
• seed 0: delivery happens to stay in order; the read returns 8 — 20/20 runs.
• Any seed with --net "" (no variance): always correct — the bug needs reordering, and a zero-variance network cannot reorder.

crates/weft-dst/tests/net_e2e.rs pins all three facts in CI, plus reproducibility under latency=exp. Broker-level behavior (deterministic loss, partition blocking, join/leave, blocking-recv wakeup) is covered by crates/weft-net/tests/broker_integration.rs.

The Weft Fault Model (Phase 4)

Overview

Phase 4 extends Weft’s deterministic simulation to include timed fault events: controlled injection of network latency, loss, corruption, file I/O faults, process crashes, and clock skew. A scenario is a JSON configuration describing a distributed system test with these faults. Every event is scheduled against a global logical timeline, driven by a seeded PRNG, so:

• Same seed → identical faults, identical timings, identical crashes/restarts.
• Different seed → different fault sequence (useful for fuzzing).

Logical Time

All faults are scheduled against a global logical timeline that unifies the concepts from Phases 1–3:

• Phase 1 (Virtual Clock): per-process observation of elapsed time, starting at 0, advancing monotonically.
• Phase 2 (Scheduler): one thread runs at a time; yield points are where the next thread is chosen from the seed.
• Phase 3 (Network Broker): per-message fate determines whether a message is dropped or delayed; delivery order is a BinaryHeap of (delay_key, insertion_index).
• Phase 4 (Global Timeline): all faults (network, file I/O, crashes, clock skew) are scheduled events with absolute (logical_time, tiebreaker) keys.

A process’s local virtual clock is a view into this global timeline:

process[node_i]::clock = global_timeline_time + clock_skew[node_i]

Where clock_skew[node_i] is a per-node offset, seeded by f(seed, node_i, skew_index).

Fault Model Vocabulary

Network Faults

Inherited from Phase 3, integrated into the global timeline:

File I/O Faults (Phase 4)

Per-node file system fault configuration:

Implementation status: the scenario parser accepts and validates all three fields, but the shim currently implements only fsync_lies (enabled per process via WEFT_FSYNC_LIES=1) plus byte-count tracking in the write hooks. enospc_after_bytes and torn_write_probability are parsed-but-inert until the scenario config is plumbed into the shim.

Process Orchestration (Phase 4)

Scheduled events control node lifecycle:

Clock Skew (Phase 4)

Per-node virtual clock offset:

"time_skew": {
  "0": 0,
  "1": 1000000000,
  "2": -500000000
}

Each node’s clock_gettime() and sleep() operate on its skewed timeline. Seed determinism: if skew is specified, the skew values are reproduced; if omitted, each node gets a seed-derived random offset in [-1 year, +1 year).

Implementation status: time_skew is parsed and validated, but the offsets are not yet plumbed into the shim’s virtual clock; today only the seed-derived realtime offset (Phase 1) applies.

Scenario Format (JSON)

Complete schema:

{
  "name": "scenario-name",
  "description": "human-readable purpose",
  "seed": 42,
  
  "nodes": [
    {"node_id": 0, "program": "./prog", "args": ["arg1"]}
  ],
  
  "network": {
    "latency": "uniform:100-5000",
    "loss": 0.1,
    "bandwidth": 1000000,
    "partitions": "0+1|2"
  },
  
  "filesystem": {
    "0": {
      "fsync_lies": true,
      "enospc_after_bytes": 1000000,
      "torn_write_probability": 0.05
    }
  },
  
  "time_skew": {
    "0": 0,
    "1": 1000000000
  },
  
  "events": [
    {"time_ns": 5000000, "action": {"type": "crash", "node_id": 0}},
    {"time_ns": 10000000, "action": {"type": "start", "node_id": 0}}
  ]
}

All fields except name, seed, and nodes are optional. Defaults:

• No network faults (reliable network).
• No filesystem faults.
• No time skew (each node gets seed_derived % 1_year).
• No scheduled events.

Determinism Guarantees

Exact reproducibility: same seed + same scenario → byte-identical process outputs, same order of operations, same crashes at the same absolute logical times.

Scope of determinism:

• Seeded: network faults, file I/O faults, process crashes, clock skew.
• Not seeded: cross-process arrival order at the broker (OS-scheduled, same as Phase 3 limitation). This is why the multi-node tests sort output instead of comparing verbatim.
• Managed threads (Phase 2 scheduler): order within one process is fully deterministic.
• Unmanaged threads (created before shim activation): order is OS-scheduled, not deterministic.

Limitations

File I/O

• No actual write corruption (bit flips, silent corruption). fsync_lies controls only sync semantics.
• No device I/O errors (EIO, EROFS). ENOSPC is the only modeled hardware failure.
• No journal or crash recovery semantics. The application must model idempotency, log replay, or write-ahead logging itself.
• No order-of-sync guarantees. Which writes persist across a crash is not modeled; fsync_lies is binary (on or off).

Processes

• Crashes are instantaneous. Real OS behavior (buffered output, signal handlers, cleanup code) is not simulated.
• Restart clears process state but preserves disk. State in shared memory, pipes, or IPC is lost.
• No explicit cluster coordination (leader election, consensus protocol failures). The scenario author must provide explicit crash/recovery events.

Clock Skew

• No drift: clock offset is fixed per node, not a continuous drift rate.
• No NTP/clock sync failures. If skew is desired, specify it explicitly.
• No CLOCK_REALTIME discontinuities. Skew is additive; the timeline is linear.

Network

• Inherited from Phase 3 (see docs/network-model.md):
  • TCP is not simulated.
  • connect/send/recv on UDP is not intercepted.
  • Cross-process arrival order is OS-scheduled.

Validation & Error Handling

The scenario parser returns detailed, actionable errors on malformed input (CLI integration is future work; today the parser is exercised via the weft-scenario API):

weft run: JSON parse error: missing field `nodes` at line 1 column 42

Parser guarantees:

• Never panics on any input (property-tested).
• Clear error messages citing what is wrong and how to fix it.
• Exhaustive validation: node ID gaps, event references to non-existent nodes, invalid probability values, malformed partition specs, etc.

Example Scenarios

Scenario 1: Network Reordering (Single Fault)

File: examples/scenarios/network-reordering.json

What it demonstrates: network latency variance causes message reordering, triggering a replica divergence bug that requires no crash, no file corruption, just unfair message ordering.

seed=1: latency variance reorders WRITE-8 and READ.
        Replica applies WRITE-7 as most recent.
        Read returns stale value.
        Bug manifests.

seed=0: latency variance happens not to occur;
        messages arrive in order.
        Replica applies WRITE-8.
        Read returns correct value.
        Bug does not manifest.

This validates that Phase 3’s network fault model is working.

Scenario 2: Crash & Restart (Single Fault)

File: examples/scenarios/crash-and-restart.json

What it demonstrates: process crash discards in-flight messages and ephemeral state, forcing applications to handle missing updates.

seed=42:
- Node-0 sends 10 WRITE messages in quick succession.
- Node-1 crashes at 5ms (receives ~3 messages).
- Node-1 restarts at 15ms.
- Node-0 retries unacknowledged writes (application-level retry).
- Replica must detect duplicates and avoid double-apply.

This validates that process orchestration events are scheduled correctly.

Scenario 3: Multi-Fault (Future: File Sync Reordering)

What it demonstrates: a bug that manifests only when two or more fault types combine.

Precondition:
- fsync_lies: true (sync returns success but doesn't persist)
- network: latency=uniform:100-10000 (causes reordering)

Execution:
1. Node-0 writes value=42 to disk
2. Node-0 calls fsync() — returns success but doesn't persist
3. Node-0 sends "value=42" to Node-1 (message reordered)
4. Node-0 crashes (due to scheduled event)
5. Node-0 restarts, reads disk: gets old value (fsync lied)
6. Node-0 sends "old_value" to Node-1
7. Node-1 sees conflicting updates due to reordering.

Bug trigger: requires fsync_lies AND network reordering AND crash.
Removing any one: bug does not manifest.

This is the critical deliverable showing that the fault model is powerful enough to expose multi-fault bugs.

Property-Based Testing

The scenario parser is validated by a suite of Rust tests that:

1. Assert no panic on arbitrary input.
2. Validate clear error messages for every class of malformed input.
3. Fuzz the boundary conditions (max values, empty collections, deeply nested structures).

Run with:

cargo test -p weft-scenario

All tests pass: 8 unit + 22 integration, covering both happy path and error cases.

Future Work

• File corruption: model bit flips or partial sectors, not just lost writes.
• Disk-full recovery: simulate recovery on a full disk with cleanup.
• Inter-node clock sync: drift and NTP failures.
• TCP simulation: connection state, retransmissions, window size.
• Signal handling in crashes: deliver signals to handlers before terminating.
• Fault linter: warn when a scenario is impossible (e.g., crash before start).
• Disk full variation sampling: random ENOSPC injection at every write.

The Weft recording format (weft-log, version 2)

This document specifies the event-log format precisely enough that an independent tool, given only this text, can read (and verify) a log correctly. The reference implementation is crates/weft-replay/src/log.rs.

1. Why the log contains what it contains

The design question behind this format: what is the minimal information that must be recorded so that replay reproduces byte-for-byte identical execution, regardless of the replaying machine’s clock, thread timing, or entropy?

In a Weft run, almost everything is already a pure function of the run seed and therefore needs no recording — it is recomputed on replay:

Two inputs to a simulated run are not seed-derived and so are recorded:

1. The broker linearization order — the order in which requests from independently OS-scheduled processes acquire the broker’s state lock. That order decides which global tie value each enqueued datagram gets (the deterministic tiebreaker between equal delivery times), how per-channel sequence numbers interleave across channels, and every send-vs-recv race the application can observe (whether a poll sees empty or a delivery).
2. Each send’s send_vt — the sender’s local virtual time, which anchors the delivery time (deliv = send_vt + seeded latency). In a single-host recording (window_ns = 0) it is always 0, recovering latency-only delivery; in a windowed multi-host recording the broker cannot recompute a remote node’s clock, so the value it was given is recorded on the send event and fed back verbatim on replay.

A weft-log therefore records the linearized sequence of broker boundary operations, each with its inputs (who, what address, what payload) and the outcome the broker computed (for verification, not for trust — replay recomputes every outcome and fails loudly on any mismatch). The header carries the seed and the network-condition spec; nothing else is needed.

Deliberately absent from replay-relevant fields: wall-clock timestamps, PIDs, hostnames, thread ids, file descriptors. Machine-specific facts appear only inside the header’s meta object, which is informational and MUST NOT influence replay.

2. File layout

A log is a UTF-8 text file of newline (\n) delimited JSON values (JSON Lines). No BOM. Writers emit no interior blank lines; readers must tolerate one trailing newline at EOF.

line 1      Header object
line 2..N   Record objects, one per linearized operation
last record an "end" event (absent if the run crashed mid-recording;
            the surviving prefix is still chain-verifiable)

3. The header (line 1)

{"format":"weft-log","version":2,"seed":3,"net":"latency=uniform:1000-100000","window_ns":0,"meta":{}}

4. Records (lines 2..N)

{"op":7,"vt":41235,"e":{"k":"recv","conn":0,"blocking":false,"outcome":{...}},"chain":"9f3c2a1b8d4e5f60"}

Addresses

An address object is {"ip":2130706434,"port":200} — the virtual IPv4 address as a host-byte-order u32 and a u16 port. By convention node n is 127.0.0.(n+1), i.e. ip = 0x7f000001 + n.

Payloads

Payload bytes are hex-encoded (lowercase, two digits per byte) in a string field named payload. Payloads are recorded in full: replay must reproduce delivered bytes exactly, and a hash alone could not.

5. Event types (e.k)

Serde representation: internally tagged by k, snake_case. Outcome objects are tagged by kind.

send.outcome (tag kind):

• {"kind":"dropped"} — the fault model dropped it (loss or partition).
• {"kind":"no_receiver"} — no connection had bound dst; discarded like UDP to a closed port. Consumes a channel sequence number but no tie.
• {"kind":"enqueued","to_conn":N,"deliv_ns":N,"tie":N} — queued for delivery.

recv.outcome (tag kind):

• {"kind":"empty"}
• {"kind":"delivered","src":{…},"dst":{…},"deliv_ns":N,"tie":N,"payload":"…"}

Semantics a replayer must reproduce (all implemented by weft_net::core::Core, which the live broker and the reference replayer both execute):

1. chan_seq advances per (src, dst) channel on every send, dropped or not.
2. tie advances globally, but only when a datagram is actually enqueued.
3. A datagram’s delivery time is deliv_ns = send_vt + fate.latency (saturating). With send_vt = 0 this is latency-only, the single-host default.
4. recv pops the pending datagram with the smallest (deliv_ns, tie).
5. vt after an operation = max(previous vt, any deliv_ns scheduled by it).
6. disconnect removes the connection’s queue and every address bound to it.

6. The integrity chain

The chain detects truncation, reordering, and edits (it is not a defense against adversaries — FNV-1a is not cryptographic; that is a deliberate trade for spec-only implementability).

Define FNV1a(state, bytes) as 64-bit FNV-1a: for each byte state = (state XOR byte) * 0x100000001b3 (wrapping), starting from the given state. The standard offset basis is 0xcbf29ce484222325.

• chain₀ = FNV1a(offset_basis, header_line) where header_line is the exact bytes of line 1 without the trailing newline.
• For record n (0-based): chainₙ₊₁ = FNV1a(chainₙ, canon(opₙ, vtₙ, eₙ)) where canon is the JSON serialization of the object {"op":…,"vt":…,"e":…} with exactly those three fields in exactly that order and no whitespace — i.e. the record line minus its chain field.
• Record n’s chain field is chainₙ₊₁ as 16 lowercase hex digits, zero-padded.

A reader verifies by recomputing the chain over each line; the first mismatch identifies the earliest corrupted or edited record. A truncated file (e.g. the recorder crashed) verifies cleanly up to the truncation point and simply lacks the end record.

Stream digest

The stream digest of a log is FNV1a folded over canon(op, vt, e) of every record from the offset basis. Two logs with equal stream digests describe byte-identical executions; header meta differences do not affect it. Replay reports its recomputed stream digest, which must equal the recording’s.

7. Replay contract

Given a verified log, a conforming replayer:

1. Parses seed and net from the header; rejects the log if net does not parse (bad net spec — the log is uninterpretable).
2. Re-executes records in op order, applying only each event’s inputs (conn, addresses, payload, blocking flag) to the broker state machine of §5, and recomputing every outcome, chan_seq, tie, and vt.
3. Compares each recomputed record against the recorded one. The first mismatch is a divergence (report both sides at that op); a divergence means the log, seed, and code no longer agree — replay must never silently prefer either side.
4. On a clean run, the recomputed stream digest equals the recorded one.

The replayer must not consult the machine clock, spawn concurrency, or draw entropy: everything it needs is the log plus this specification. That is what makes replay results identical across machines.

replay --until N is the same procedure stopped after applying op N, leaving the state machine inspectable at that point on the timeline.

8. Invariant checking against a log

Invariants (see weft_replay::invariant) consume the linearized event stream and anchor violations to (op, vt) — a precise point in the linearization and on the virtual-time axis, never “sometime during the run”. The same invariant code runs in-process during recording and from an external checker over the log file; §5’s violation events record what the in-process monitor observed, and a replayer given the same invariants must re-raise identical violations at identical positions.

9. Scope and honesty

• The log captures the broker boundary. A single-process run that never touches the network needs no log at all: it is already a pure function of the seed (re-running with the same seed is its replay).
• What the target processes do with delivered bytes is reproduced only insofar as their inputs (time, randomness, schedule, network) are under Weft’s control — the shim’s existing limitations (see docs/architecture.md) apply unchanged.
• File-I/O fault decisions (Phase 4) are seed/env-derived and thus recomputed, not recorded. If a future fault source stops being a pure function of the seed, its decisions must start being recorded — that is the rule this format encodes.

10. Versioning policy

Any change to canonical serialization, chain computation, event fields, or semantics of §5 requires incrementing version. Readers reject unknown versions. Readers must ignore unknown keys only inside meta; unknown keys anywhere else are a malformed record.

Version 2 (the current version) added the per-send send_vt anchor and the header window_ns field. Version 1 (latency-only delivery) is rejected on read — its recorded deliveries would silently diverge under the send-time- anchored core, so there is no in-place upgrade: re-record under the current tool.

11. Compression (optional transport encoding)

A log file MAY be gzip-compressed (RFC 1952) as a whole file. This is a transport encoding only: the compressed payload is the exact byte sequence §2–§6 describe, the version stays unchanged, and the chain and stream digest are computed over the uncompressed text.

• Detection is by content, never extension: a reader MUST check the file’s first two bytes for the gzip magic 1f 8b and decompress before parsing; anything else is parsed as plain text.
• Writers SHOULD use a .gz suffix as a human convention (the reference recorder compresses exactly when the requested path ends in .gz).
• Trade-off: the reference writer sync-flushes after every record, but a gzip member is only complete once its trailer is written at the end of recording. A run that crashes mid-recording therefore leaves a compressed file without a trailer; standard decoders recover the flushed prefix but report an unexpected-EOF at the end. Prefer an uncompressed path while a scenario is still fragile; compress for archival.

Fuzzing and shrinking (weft fuzz)

Phase 5 made a specific failure reproducible from a log. weft fuzz closes the loop: it finds failures by sweeping fault seeds, and hands back the smallest reproducer for each distinct one.

weft fuzz --config examples/fuzz/demo.json

How it works

1. Sweep. A fixed, deterministic workload (generated from workload_seed, independent of the fault seed) is executed against the broker’s decision core once per fault seed, in parallel. The same invariants run on every execution. Regression seeds are queued before the sweep, so a tight time budget can never skip them.
2. Dedup. Violations are grouped by identity — invariant name + the channel (src → dst) of the violating event — not by message text, since sequence numbers legitimately differ between runs.
3. Shrink. Each distinct violation is reduced from its smallest failing seed by delta debugging over the op inputs (never the recorded log text: outcomes are derived data). Passes: truncate after the violation → ddmin chunk removal (candidates evaluated in parallel; lowest-index success adopted so results stay deterministic) → single-op removals to a 1-minimal fixpoint → payload truncation → connect GC. Seed and net spec are never varied — changing them would reproduce a different run.
4. Report + reproducers. Every distinct violation gets a fresh, fully-consistent weft-log in out_dir that weft replay <log> --check … verifies byte-for-byte, plus a report.txt.

The shrinker never reorders ops, never renumbers connections or addresses, and requires the same invariant to fail on the same channel — so the minimal reproducer stays an interpretable subsequence of the original run rather than a technically-smaller alien. Its correctness is pinned by three ground-truth tests (crates/weft-fuzz/tests/shrink_ground_truth.rs) where a known exact minimum is buried in hundreds of noise ops and must be recovered exactly.

Config file

One JSON document; every CLI flag maps onto it and overrides it.

{
  "//": "optional comment slot, ignored",
  "net": "latency=uniform:0-8000,loss=0.02",
  "seed_start": 0,
  "seed_count": 1000,
  "jobs": 8,
  "time_budget_secs": 60,
  "invariants": ["fifo", "dup"],
  "workload": { "nodes": 3, "sends": 30, "payload_len": 4, "workload_seed": 0 },
  "out_dir": "weft-fuzz-out",
  "shrink": true,
  "regression_seeds": []
}

Unknown fields are rejected (typos fail loudly), except the "//" comment slot.

Exit codes (CI contract)

CI integration

The real, working example is .github/workflows/fuzz.yml + examples/fuzz/ci.json. The CI config is a property test: under latency=fixed:100 with no loss, FIFO and duplicate-freedom must hold for every seed, so the sweep is expected to pass and any violation is a genuine regression in the broker’s decision core. (Do not put a variance-latency net in CI with the fifo invariant — reordering under variance is by design, and the job would fail every night by construction. That configuration lives in examples/fuzz/demo.json for humans exploring the shrinker.)

With --regressions <file>, every failing seed the sweep discovers is written to the file (a plain JSON array), and future runs test those seeds before sweeping — a regression corpus that grows on its own.

Reading a failure

Each distinct violation in the report ends with a literal command:

repro  : weft-fuzz-out/repro-seed0-per-channel-fifo-on-127-0-0-2-100-127-0-0-1-100.weftlog
verify : weft replay weft-fuzz-out/repro-seed0-….weftlog --check fifo,dup

weft replay re-executes the reproducer to an identical stream digest and prints the full violation report — invariant, op + virtual-time anchor, seed, net spec, and the surrounding event window (typically the whole log: shrunk reproducers are usually under ten records).

Scope

weft fuzz explores the broker boundary (Phase 3’s network model plus the Phase 5 log/invariant machinery) as pure computation — no shim, no sockets — so it runs identically on every platform. Fuzzing live target programs (the LD_PRELOAD shim path) composes with weft run --record today: sweep seeds by re-running the cluster and replay any failing recording; folding that flow into weft fuzz is future work.

Multi-host deterministic execution — architecture

Extends Weft’s single-machine cluster mode (weft run --net --nodes N) to real multiple hosts: target processes on different machines, one master broker, real TCP between them, one recording. Design principle: the broker’s linearization order stays the single source of truth; multi-host support changes the transport under that truth, never the truth itself. Phase 1–6 core logic is untouched except at the two points multi-host support structurally requires: the shim↔broker wire protocol (transport + clock piggyback) and the broker’s accept loop (TCP alongside Unix sockets).

Components

host A (master)                      host B                    host C
┌──────────────────────────┐   ┌─────────────────┐   ┌─────────────────┐
│ weft run --hosts B:7601, │   │ weft hostd :7601 │   │ weft hostd :7601 │
│   C:7601 --net … --record │   │   │ spawn/kill    │   │   │ spawn/kill    │
│  ├─ broker (TCP :7600)    │◄──┼───┤ target procs  │   │   │ target procs  │
│  ├─ recorder (weft-log v1)│   │   │  + shim ──────┼───┼───┼── TCP ────────┤
│  └─ control conns to hostd│   └─────────────────┘   └─────────────────┘
└──────────────────────────┘

• Master (weft run --hosts): hosts the seeded broker on TCP, connects to each host agent, distributes node spawns, records, reaps exits.
• Host agent (weft hostd): one per host. Receives spawn specs over a TCP control channel (JSON lines), launches target processes under the shim with WEFT_BROKER=<master>:<port>, reports exits, kills on command.
• Shim: unchanged interception; its broker connection now dials TCP when WEFT_BROKER looks like host:port (a Unix path otherwise). The shim’s broker I/O already operates on raw fds, so a TCP fd flows through the same code as a Unix-socket fd.
• Recorder/replay: byte-for-byte unchanged. The log stays weft-log v1: broker operations in linearization order. Host→node mapping is recorded in the header’s informational meta object (readers MUST ignore unknown meta keys — that rule exists for exactly this kind of addition, VERSIONING.md §1).

The logical clock protocol

Superseded. The merge-on-response rule below was implemented, broke same-seed determinism (broker vt advances in real arrival order, and merging it fed OS scheduling into guest-visible time), and was reverted — the shim now sends local_vt but ignores response vt (CHANGELOG, “Added (multi-host groundwork)”). The replacement — seed-derived windowed sealing with frontier-gated assignment — is specified in MULTI_HOST_CLOCK_PROTOCOL.md and is design-only. This section is kept as the historical record the post-mortem refers to.

Problem. Each shimmed process has a virtual clock (Phase 1): monotonic ns, advancing on reads and sleeps, independent per process. On one machine that independence is invisible; across hosts, causally-related events could carry wildly diverging virtual timestamps.

Protocol (Lamport-style, broker as master).

• The broker’s Core already maintains a seeded virtual-time high-water mark vt that advances as messages are scheduled and delivered — this is the master logical clock.
• Every broker response now carries vt (piggybacked; no extra round trips). Requests carry the sender’s current local virtual time local_vt (for skew observability, below).
• On receiving any broker response, the shim merges: local_clock = max(local_clock, vt) — the existing advance_mono_to primitive, which is a monotone fetch_max; local time never moves backward.

Bounded-skew proof sketch. Define skew(p) at any instant as local_vt(p) − vt(broker) (signed). Claim: for a process whose broker interactions are at most W local-clock ns apart (W = the largest amount its virtual clock advances between two consecutive broker calls — chord_node/raft_node tick loops give W ≈ one tick: 1 ms + a few µs of reads):

1. Downward bound: immediately after a response, local ≥ vt(response) by the merge; vt is read under the broker lock, so local can lag the broker’s current vt only by what the broker schedules between that response and the process’s next call — but lag never affects correctness: delivery order is decided by the broker alone; a lagging local clock merely timestamps local events earlier. On the next interaction the merge erases the lag.
2. Upward bound: local exceeds vt(last response) by at most W before the next interaction forces a new merge, so local_vt(p) ≤ vt(broker at last response) + W.

Hence |skew| observed at interaction points ≤ W plus whatever the broker advanced concurrently — both measurable, neither affects the recording’s determinism (the log’s op order and virtual times are all assigned broker-side under one lock). This is deliberately a weak guarantee with an honest shape: Weft’s determinism story never depended on synchronized wall clocks, and multi-host does not change that; the clock protocol exists so that per-node local timestamps (traces, reports) stay comparable across hosts, with quantified error.

Skew observability. The broker records max |local_vt(request) − vt(core)| across all operations and reports it in --stats — the measured bound for MULTI_HOST_VALIDATION.md.

Host crash and rejoin. A host death closes its shims’ TCP connections; the broker’s existing disconnect path unbinds their addresses and wakes blocked receivers (already how single-host process death works — same code path, now transport-agnostic). The recording simply stops containing sends from those nodes: still a valid v1 log. A rejoining host reconnects and re-Hellos; the first response re-syncs its clock via the monotone merge — no special-case protocol. What multi-host does not attempt: migrating a dead host’s node state (that is the target system’s job — Weft kills and restarts processes; it does not checkpoint them).

Deterministic ordering across hosts — the honest statement

Single-machine cluster runs already have the documented Phase-3 limitation: which process’s request reaches the broker first is OS-scheduled, so live runs of one seed are not verdict-deterministic; the recording is the determinism artifact. Multi-host makes the arrival race wider (real network latency), but the guarantee is unchanged in kind:

• Every fate decision remains a pure function of (seed, src, dst, seq) — the fault model is broker-level and transport-independent, so the same arrival order yields the same run on any transport.
• The recording captures the arrival order that actually happened; replay (pure computation, no hosts, no sockets) reproduces it byte-for-byte on any hardware. “Replay across different hardware” is validated by recording on x86-64 Linux containers and replaying on an arm64 macOS host (MULTI_HOST_VALIDATION.md).
• Live seed-determinism across hosts is not claimed. The design for closing it — a broker-granted turn token, i.e. lockstep admission of one in-flight operation at a time in seeded order over registered nodes — is compatible with this architecture (the broker already owns a global lock at exactly the right point) but is designed, not built: it needs per-node idle/computing signals to avoid deadlocking on nodes that are busy computing rather than blocked on the network, and its latency cost (one cluster-wide serialization point per op) would change the performance envelope enough that it should be an explicit opt-in mode.

“Mid-replay host failure” is therefore a non-event by construction: replay involves no hosts. Host failure during a live recorded run is handled (a node’s ops just stop); the resulting log replays like any other.

Fault simulation over real TCP

Unchanged in substance: latency/loss/reordering/partitions were never implemented at the localhost-socket level — they live in the pure decision Core the broker consults under its lock (Phase 3 design). Moving the shim↔broker transport from Unix sockets to TCP moves the carrier, not the fault model. Real-network latency between host and broker adds to the (virtual) simulated latency only in wall-clock terms; it cannot reorder the broker’s linearization retroactively, because order is assigned at lock acquisition, exactly as before.

What changed where (Phase 1–6 delta, complete list)

Everything else — scheduler, vclock internals, recorder, replayer, fuzz, scenario, Core — is untouched.

Multi-host deterministic event ordering — protocol design

Status: design only, nothing implemented. This document supersedes the “logical clock protocol” section of MULTI_HOST_ARCHITECTURE.md (whose merge-on-response rule was implemented, shown to break same-seed determinism, and reverted — post-mortem below) and turns that document’s “designed, not built” closing sketch into a full specification. No shim, broker, or transport work should proceed against multi-host ordering until the open questions at the end of this document are resolved.

Prior art this design instantiates: conservative parallel discrete-event simulation (Chandy–Misra–Bryant null messages / lower-bound-on-timestamp sealing) with Lamport-clock merging, specialized to Weft’s constraint that simulated processes are real, unmodifiable OS processes that cannot be checkpointed or rolled back.

1. Post-mortem: why merge-on-arrival broke

The reverted design piggybacked the broker’s virtual-time high-water mark vt on every response, and the shim merged it into its local clock (local = max(local, vt)) on receipt.

The flaw is one sentence: the broker’s vt at the moment it answers a request is a function of which other process’s request happened to arrive first, which is OS scheduling and real network timing — not the seed. Merging it made guest-visible time (every subsequent clock_gettime, every sleep deadline, every trace timestamp, and — through timing-dependent guest branches — the guest’s entire future behavior) a function of real arrival order. Two live runs of one seed diverged; net_e2e’s same-seed tests failed; the merge was removed (CHANGELOG “Added (multi-host groundwork)”).

The general lesson, stated as an invariant this protocol must maintain:

I-SEED. No value that can influence a guest’s observable behavior may be derived from real arrival order, real wall-clock time, or OS scheduling. Every such value must be a pure function of (seed, static configuration, guest program).

The wire fields the reverted attempt added (local_vt on requests, vt on responses) are kept: local_vt is load-bearing in this protocol (§4), and a response-carried virtual time is again merged into the guest clock — but it is a different quantity (§6): a seed-derived assigned time, not an arrival-ordered observation.

2. Model and definitions

• Guest — one shimmed target process. Identified by node_id (assigned by the orchestrator, stable across the run) on a host_id.
• Local virtual time (LVT) — the guest’s Phase-1 vclock: monotonic ns, advancing on clock reads and (virtualized) sleeps. Per Phases 1–2, a single guest’s execution — its sequence of intercepted operations, each op’s content, and the LVT at which it issues each op — is a pure function of the seed and of what the network delivers to it and at what virtual times (Lemma L1, §7).
• Op — one guest→broker operation: Send{src,dst,payload,local_vt} or Recv{addr,blocking,local_vt} (plus Hello/Bind). local_vt is the guest’s LVT when the op was issued.
• Connection sequence number conn_seq — ops on one connection are FIFO (TCP/Unix stream), numbered 0,1,2… by the broker per connection. Program order within a guest is therefore visible to the broker.
• Frontier F(g) — a per-guest promise: “guest g will never again emit an op with local_vt < F(g)”. How frontiers are established is §4.
• Window k — the virtual-time interval [kW, (k+1)W) for a fixed configured width W ns. Windows are the unit of ordering.

3. Requirements

• R1 (determinism). The global order of all ops, every fate decision, every delivery’s virtual time, and every guest’s vclock trajectory are pure functions of (seed, config) — invariant I-SEED.
• R2 (sound merging). Guest clocks may merge only broker-assigned, seed-derived times. Nothing arrival-ordered ever flows into a guest.
• R3 (liveness). If every guest is either making progress or blocked on the network, the protocol makes progress. Deadlock and quiescence are detected and reported deterministically.
• R4 (honest failure handling). Real-world failures (host crash, TCP drop, wedged guest) never silently produce a different ordering; they either map onto an injected-fault path with a virtual-time coordinate, or abort the run loudly. A run either completes identically to every other same-seed run, or does not complete.
• R5 (compatibility). Recording and replay remain the audit artifact; format changes go through VERSIONING.md’s log-format contract.

4. Protocol

4.1 The broker becomes a sequencer

The broker’s role changes from passive relay that timestamps on arrival to active scheduler in three duties:

1. Admission: accept ops from all connections, append each to a per-connection FIFO buffer. Arrival order across connections is recorded nowhere and used for nothing.

2. Sealing: window k seals when every live connection’s frontier satisfies F(g) ≥ (k+1)W. Sealing is the only place the protocol waits on the real world, and waiting affects only wall-clock duration, never content (proof: §7).

3. Assignment: after sealing, the broker takes every buffered op with local_vt in window k, sorts them by the total order key

   (local_vt, host_id, node_id, conn_seq)
   

   and feeds them through Core in that order. This sorted sequence — not arrival order — is the linearization, the recording content, and the input to every fate draw.

Every component of the key is seed-derived (local_vt by Lemma L1; the identifiers are static config; conn_seq is program order, seed-derived by L1), so the assigned order satisfies R1.

Tie-break note: lexicographic (host_id, node_id) on equal local_vt is deterministic but always favors the same guest. An alternative is a seeded permutation of guest identity per window (extra schedule diversity across seeds, equally deterministic). v1 choice: lexicographic — one less mechanism; diversity already enters through per-channel latency draws. Recorded as open question OQ-2.

4.2 Frontier establishment

A guest’s frontier advances through three mechanisms, all piggybacked — there is no mandatory extra round-trip in busy phases:

• Op-carried: every op’s local_vt is, by clock monotonicity plus connection FIFO, a frontier declaration F(g) ≥ local_vt. (The shim’s vclock is strictly monotone; the broker rejects a local_vt below the connection’s previous one as a protocol violation → abort, R4.)
• Explicit Frontier{local_vt} message: sent by the shim when the guest’s LVT has advanced ≥ one window width past its last declaration without any network op (a guest sleeping through virtual hours, or computing). Sent from the shim’s existing hook path — no new threads in the guest; the check rides on whichever intercepted call advanced the clock. A guest executing a long stretch of uninstrumented pure computation advances neither its LVT (nothing intercepted) nor its frontier — see failure mode F5.
• Release-on-block: a guest entering blocking Recv stops emitting spontaneously. The original claim here — that it may declare F(g) = +∞ — is unsound for request/reply and was corrected in implementation. If a blocked receiver goes to +∞, the whole cluster can seal every window; the receiver’s reaction to a just-delivered message is then admitted at its post-delivery virtual time, which lands in an already-sealed window and is rejected as a late op. Correct rule: a blocked guest waiting on address A contributes its reactivation bound — the least local_vt of a pending send aimed at A, plus lookahead L_min (§5) — i.e. the earliest virtual time it could emit once woken. It contributes +∞ only when no pending send targets it (nothing can wake it). Combined with releasing deliveries at deliv_vt < sealed_horizon + L_min (the §5 lookahead, no longer optional), this keeps the window a woken guest emits into open until it has emitted. Consequence: windowed mode requires L_min ≥ W (lookahead at least the window width); with L_min = 0 a receiver’s reactivation bound equals a send’s own time and stalls that send’s delivery — the degenerate deadlock. A guest that exits (connection close or process exit) is F(g) = +∞ permanently (nothing more to react to). A managed multi-threaded receiver, which polls the broker non-blocking and so cannot advance the horizon it waits on, announces its block with an explicit Park{addr, local_vt} message when it goes idle.

The multi-threaded guest case is where the current implementation has a hole that this protocol must close, because the existing managed-thread polling loop is nondeterministic under windowing: today a managed thread polls non-blocking Recv in a loop, calling sched.yield_now between polls, and each yield consumes scheduler RNG. Under windowing, the number of Empty polls before a delivery depends on how fast windows seal in real time — real-time-dependent RNG consumption, violating I-SEED. Design consequence (flagged for implementation, not done here): blocking network waits by managed threads must become a modeled scheduler state (BlockedNet(addr), alongside BlockedMutex/BlockedCond), entered at the recv yield point and woken by delivery. The thread then consumes scheduler decisions only at deterministic points, and a fully-blocked guest (all managed threads BlockedNet/BlockedJoin) releases its frontier to +∞ exactly like the single-threaded case. Until that scheduler change exists, windowed multi-host must not ship (OQ-5).

4.3 Delivery assignment

For each admitted Send in assigned order, Core draws the fate exactly as today — fate(seed, src, dst, chan_seq, len), unchanged and transport-independent — and schedules delivery at

deliv_vt = send.local_vt + fate.delay_ns

This is a semantic change to Core: today deliv is the bare latency draw, un-anchored to send time (fault.rs draws a relative delay_ns; core.rs uses it as the absolute queue coordinate). Anchoring on send.local_vt is required so that delivery times are meaningful on a shared cross-host timeline, and it changes recomputed values for existing recordings — a log-format compatibility event (R5, §9).

A Recv in assigned order pops the receiver’s queue only among messages with deliv_vt inside an already-sealed window (deliv_vt < sealed_horizon); a message scheduled for a future window is not yet poppable even if queued — otherwise delivery visibility would depend on how early the send was admitted in real time. Pop order is (deliv_vt, assignment tie) as today.

4.4 Vclock merge — the corrected rule

Replacing the reverted merge-on-arrival:

• On Deliver: the guest merges local = max(local, deliv_vt). deliv_vt is seed-derived (R2 satisfied). This is the Lamport rule with the message’s assigned timestamp — receiving a message can only move you forward to the (virtual) moment it arrived.
• On Empty (non-blocking recv against an empty queue): the guest merges nothing. The reply carries the sealed horizon for observability only; merging it would make guest time depend on real sealing progress.
• On Ack (send/bind): merge nothing. Sends do not teleport a sender forward.

Result: guest LVT is driven only by its own execution and by seed-derived delivery times — exactly the quantities Lemma L1 permits.

4.5 Wire protocol delta (design level)

• Frontier { local_vt } — new guest→broker message (§4.2).
• Deliver { …, vt } — existing field, reinterpreted: carries deliv_vt (assigned), not the arrival-ordered high-water mark.
• Ack { vt } / Empty { vt } — retained for skew observability and diagnostics; explicitly must not be merged (enforced by the shim, and by a determinism e2e test that fails if they are).

4.6 Window lifecycle summary

OPEN(k)      ops with local_vt ∈ [kW,(k+1)W) accumulate, unordered
  │  every live connection reports F(g) ≥ (k+1)W
SEALED(k)    contents frozen — provably complete (no guest may emit into it)
  │  sort by (local_vt, host_id, node_id, conn_seq); fates; deliveries
ASSIGNED(k)  ops appended to linearization + recording; deliveries with
             deliv_vt < (k+1)W become poppable; k := k+1

5. Buffering strategy and its trade-offs

Windowing is buffering; the design decisions are the width W and the idle-frontier cadence.

• Small W: sealing overhead dominates — every window needs every connection’s frontier to cross a boundary, so idle guests must emit explicit Frontier messages at fine grain; real-time cost ≈ one cross-host RTT per window in the worst (idle) case. Virtual latency resolution is fine-grained.
• Large W: fewer seals, better throughput, but a delivery scheduled early in a window is withheld until the window seals — added real latency for request/reply guests (a ping’s reply waits for the whole cluster’s frontiers), and coarser interleaving granularity (all of a window’s sends order before any of its deliveries become visible).
• The degenerate case W → 0 is the old document’s “turn token / lockstep admission” sketch: strictest, slowest, and its busy-guest deadlock is exactly the missing-frontier problem that §4.2’s explicit Frontier message and the BlockedNet state solve. Windowing generalizes the token design rather than replacing it.
• Lookahead (future optimization, OQ-4): if the configured latency distribution has a minimum L_min > 0, a send admitted in window k cannot deliver before kW + L_min, so deliveries into the first ⌊L_min/W⌋ subsequent windows can be released before those windows seal — the classic CMB lookahead. Requires L_min to be a static property of the net spec (true for fixed: and uniform:LO-HI with LO>0; false for exp:).
• Adaptive W is admissible only if adaptation keys on virtual quantities (e.g., op density per window), never on real measurements — otherwise W itself becomes an arrival-order channel. v1: fixed W from config; default suggestion 1 virtual ms (matches the case-study tick scale). OQ-3.

Broker memory is bounded by ops-per-window; a window cannot seal with unbounded content unless a guest emits unboundedly within one window width, which is bounded by guest op rate × W.

6. What the broker’s vt means now

Core.vt (high-water mark) remains for stats, but the authoritative clock is the sealing horizon: sealed_horizon = (k_sealed+1)·W. Global virtual time advances by sealing, which requires unanimous frontier progress — time is pulled forward by the slowest guest, not pushed by whoever talks fastest. That inversion is the essence of the fix: in the reverted design, chatty guests dragged everyone’s clocks forward in arrival order; here, the laggard bounds the horizon and order within the horizon is arrival-independent.

7. Correctness argument

Lemma L1 (single-guest determinism — existing, tested). Given the seed and a fixed sequence of deliveries (payload_i, deliv_vt_i) presented at deterministic points, a guest’s execution — every op, its content, its local_vt, every scheduler decision, every RNG byte — is a pure function of (seed, node_id, deliveries). This is the Phase 1–2 guarantee (e2e determinism tests), extended by the BlockedNet scheduler state (§4.2) so that waiting for a delivery consumes no nondeterministic decisions. Scope caveat: L1 holds only for guests within the interception surface (LIMITATIONS.md §1 — static binaries, raw syscalls, etc. escape it).

Lemma L2 (frontier honesty). No op is ever assigned to a window after that window sealed. By construction: sealing waits for F(g) ≥ (k+1)W for every live connection; frontiers are monotone; an op violating its connection’s declared frontier aborts the run (R4). Guest exit and blocking-recv release are sound because a blocked or dead guest emits nothing until the broker itself acts.

Lemma L3 (no side channels). Guests interact only through the broker. Cross-guest channels outside the model (shared files on one host, raw un-intercepted sockets) void the theorem — documented limitation, same class as LIMITATIONS.md §1/§2, restated here because multi-host makes shared-filesystem side channels less likely (different hosts) but NFS-style shared mounts reintroduce them.

Theorem (run determinism). For two executions of the same (seed, config, binaries) on arbitrary real hardware, networks, and OS scheduling, the assigned linearization, every fate, every deliv_vt, and every guest’s LVT trajectory and output are identical.

Proof sketch — induction on window index k.

• Invariant I(k): the assigned contents and order of windows 0..k, and the complete state of every guest up to its last event with local_vt < (k+1)W, are pure functions of (seed, config).
• Base: before any delivery, each guest’s prefix (ops with local_vt in window 0, and frontier declarations) is deterministic by L1 with an empty delivery sequence. Sealing waits until all frontiers pass W — waiting is real-time-dependent, but by L2 the set of window-0 ops is exactly the guests’ deterministic prefixes, and the sort key contains no arrival component; so window 0’s assignment is deterministic.
• Step: assume I(k). Deliveries with deliv_vt < (k+1)W are computed from windows ≤ k (assigned order + seeded fates + anchored delivery times), hence deterministic. By L1, each guest’s continued execution up to local_vt < (k+2)W — including which ops it emits into window k+1 and its frontier messages — is a pure function of those deliveries. Sealing of k+1 again affects only when, not what (L2). Assignment sorts by an arrival-free key. I(k+1) holds. ∎

What would break each leg (the falsifiable surface, in the project’s testing idiom — each gets a test that fails without it):

• L1 broken by: RNG consumed in a real-time-dependent loop (the polling hole, §4.2), a guest reading an unvirtualized clock, un-intercepted I/O.
• L2 broken by: a non-monotone local_vt (shim bug), a lost Frontier message (transport must be reliable — TCP, or abort on drop).
• Assignment broken by: any arrival-ordered input to the sort key or to Core (e.g., reintroducing high-water-mark merging).

8. Failure modes and deterministic handling

9. Impact on existing guarantees and documents

• Upgrades the headline guarantee. Today: “live multi-process same-seed runs may diverge; the recording is the determinism artifact” (LIMITATIONS.md §3c — the caveat the README leads with). Under this protocol, live same-seed determinism becomes claimable for --net runs, single-host and multi-host alike — the windowed broker fixes the single-host arrival race too, since nothing in §4 is TCP-specific. Whether to adopt windowing for plain single-host --net (and retire the §3c caveat at the cost of sealing latency and the scheduler change) is OQ-1 — the largest product decision here.
• Recording becomes redundant for reproduction, kept as artifact. The linearization is seed-derived, so seed alone reproduces a run; the log remains the checkable artifact (checkers, shrinker input) and the compatibility surface. deliv_vt anchoring (§4.3) changes what replay recomputes ⇒ weft-log format bump per VERSIONING.md §1 (v1 logs stay replayable under v1 semantics; the version field gates which Core semantics replay applies).
• Scheduler: new BlockedNet state (§4.2) — an extension of the Phase-2 model with the same determinism obligations (its own harness tests).
• MULTI_HOST_ARCHITECTURE.md: its clock-protocol section and its “changed where” table row for the shim merge describe the reverted design; superseded by this document.

10. Rejected alternatives

• Merge broker high-water mark on receipt — implemented, broke same-seed determinism, reverted (§1). Rejected by evidence.
• Optimistic ordering (Time Warp): run on arrival order, roll back on violation — requires checkpoint/rollback of guests. Weft’s guests are unmodified OS processes; rollback would need CRIU-class snapshotting per message, wildly outside the do-no-harm envelope. Rejected structurally.
• Turn-token lockstep (the prior sketch) — sound but is the W→0 special case of windowing with strictly worse constants and the same need for frontier/idle signals; subsumed (§5).
• Real clock synchronization (NTP/PTP) + timestamp ordering — replaces OS-scheduling nondeterminism with clock-sync nondeterminism; violates I-SEED by construction. Rejected.

11. Open questions (deliberately unresolved)

• OQ-1: Adopt windowing for single-host --net and retire LIMITATIONS.md §3c? Gains the strongest possible claim (“same seed ⇒ same run, live”); costs sealing latency on every run and makes the BlockedNet scheduler change load-bearing everywhere. Needs a benchmark (bench-scalability.sh extension) before deciding.
• OQ-2: Tie-break within equal local_vt: lexicographic (v1 proposal) vs seeded per-window permutation (more schedule diversity per seed).
• OQ-3: Window width W — fixed config (v1: 1 virtual ms) vs adaptive on virtual-only signals. What is the right default for targets whose tick loops are much faster/slower than the case studies’?
• OQ-4: CMB lookahead using L_min of the latency distribution — worth the Core complexity? (Only helps fixed:/uniform: with LO>0.)
• OQ-5: The BlockedNet scheduler state is a precondition (the polling loop consumes RNG per real-time poll today, §4.2). Is there a cheaper interim rule — e.g., yield sites that consume no RNG when the yielder is the only runnable thread — that preserves I-SEED without the full state? (Suspected no: multi-threaded guests still poll while siblings run. Needs a worked counterexample either way.)
• OQ-6: Frontier cadence for guests that sleep across many windows in one nanosleep — should the shim split a long virtual sleep into per-window frontier reports (chatty, simple) or report the sleep’s end as an immediate frontier jump (one message; requires the broker to accept far-future frontiers — it does, they’re monotone promises)? Proposal: the latter; verify no interaction with injected crash events scheduled mid-sleep.
• OQ-7: Exact log-format v2 shape: record window boundaries as first -class records (better auditability, bigger logs) or reconstruct them during replay from local_vt (smaller, more recomputation)?

Process Orchestration (Phase 4b)

Overview

Process orchestration extends the fault model to include scheduled process lifecycle events: crashes, restarts, and partition changes. A scenario’s events array triggers these events at absolute logical times, allowing testing of distributed systems’ recovery and resilience.

Architecture

Current State (Foundation)

• Scenario DSL (weft-scenario crate): describes crashes and restarts as scheduled events
• Broker (weft-net): network-only state machine; does not manage processes. It does export global_logical_time (an AtomicU64 high-water mark updated on each send) for the event scheduler.
• Orchestrator (weft-dst::orchestrator): NodeRegistry (node status + PIDs) and spawn_scheduler (polls global_logical_time, executes crash via SIGKILL). start only marks the node Restarting — respawn (fork/exec) and partition activation are not implemented yet.
• Shim (weft-shim): per-process interception; does not track process lifecycle

Required Additions for MVP

1. Process Registry

The broker or a separate orchestrator process needs to track:

• Which node processes are running
• Their PIDs and configuration
• Cluster membership and partition state

#![allow(unused)]
fn main() {
struct NodeState {
    node_id: usize,
    program: String,
    args: Vec<String>,
    pid: Option<u32>,
    status: NodeStatus, // Running, Crashed, Restarting
}

enum NodeStatus {
    Idle,
    Running(u32), // pid
    Crashed(u64), // time_crashed_ns
    Restarting(u64), // time_restart_ns
}
}

2. Event Scheduler

A dedicated thread in the broker or orchestrator that:

1. Reads scenario.events from the loaded scenario
2. Waits for the logical clock to reach each event’s time_ns
3. Executes the event action (crash/start/partition change)

#![allow(unused)]
fn main() {
// Pseudocode
for event in scenario.events.iter().sorted_by_key(|e| e.time_ns) {
    // Wait until global_logical_time >= event.time_ns
    wait_until(event.time_ns);
    
    match event.action {
        EventAction::Crash { node_id } => {
            kill_node(node_id);
            mark_crashed(node_id);
        }
        EventAction::Start { node_id } => {
            respawn_node(node_id);
            mark_running(node_id);
        }
        EventAction::ActivatePartition { spec } => {
            apply_partition(spec);
        }
        EventAction::ClearPartition => {
            clear_partitions();
        }
    }
}
}

3. Global Logical Clock Exposure

The broker must expose the current logical time to the event scheduler:

• Phase 1: Virtual clock is per-process; broker aggregates via message timestamps
• Phase 3: Network broker observes datagram delivery times
• Phase 4: All faults use the same global timeline

A shared atomic counter (e.g., AtomicU64) in the broker’s state tracks:

#![allow(unused)]
fn main() {
struct BrokerState {
    global_logical_time_ns: AtomicU64,
    // ... existing fields
}
}

Each message delivery updates this; the event scheduler polls it to trigger events.

4. Process Signal Handling

Crashing a process: send SIGKILL (cannot be caught):

#![allow(unused)]
fn main() {
fn kill_node(pid: u32) {
    unsafe { libc::kill(pid as i32, libc::SIGKILL) };
}
}

Restarting a process: fork + exec with the same environment:

#![allow(unused)]
fn main() {
fn respawn_node(config: &NodeState) -> u32 {
    let pid = unsafe { libc::fork() };
    if pid == 0 {
        // Child: set up environment and exec
        std::env::set_var(weft_abi::ENV_SEED, format!("{}", seed));
        std::env::set_var("WEFT_NODE_ID", format!("{}", config.node_id));
        std::env::set_var(weft_abi::ENV_BROKER, &broker_socket);
        
        libc::execvp(
            config.program.as_ptr() as *const i8,
            config.args.as_ptr() as *const *const i8,
        );
        std::process::exit(1);
    }
    pid as u32
}
}

5. State Preservation Across Restarts

Ephemeral state is lost:

• In-memory data structures
• Open file descriptors
• Network connections
• Thread state

Persistent state is retained:

• Files on disk (subject to file I/O faults like fsync_lies)
• Durable log entries (if the application uses them)

The restart process is instantaneous in logical time—no signal handlers, cleanup, or orderly shutdown.

Integration Points

1. weft-dst CLI

The CLI must:

• Load the scenario file (already done by weft-scenario)
• Extract the event list
• Create a process registry for each node
• Spawn the orchestrator/event-scheduler thread

weft run scenarios/file-sync-network-reordering.json

2. Broker Startup

The broker’s new or bind method must accept a loaded scenario:

#![allow(unused)]
fn main() {
pub fn bind(path: &Path, model: FaultModel, scenario: Option<&Scenario>) -> io::Result<Self> {
    // ... existing code
    
    if let Some(s) = scenario {
        // Clone events and spawn event-scheduler thread
        let events = s.events.clone();
        thread::spawn(|| event_scheduler(events, /* shared broker state */));
    }
    
    Ok(Self { /* ... */ })
}
}

3. Logical Clock Synchronization

Currently, logical time is per-process (Phase 1’s virtual clock). Process orchestration needs a global timeline.

Options:

1. Broker-centric: The broker observes the maximum logical time seen in any message and broadcasts it back to nodes via heartbeats.
2. Shared memory: The broker writes the global time to shared memory; nodes read it.
3. Phase 2 Scheduler integration: If deterministic scheduling is active, the scheduler can track global time across threads and processes.

For MVP, option 1 (broker-centric) is simplest: the broker tracks max time, and the event scheduler uses it.

File I/O Faults with Process Crashes

File I/O faults and process crashes interact:

Scenario: Node writes value=42 to disk, calls fsync() (returns success due to fsync_lies), then crashes.

• If fsync_lies: true: the write is not persisted; node restarts and reads old value.
• If fsync_lies: false: the write is persisted; node restarts and reads new value.

This creates data loss bugs that only manifest with simultaneous fsync_lies + crash events.

Implementation:

1. File I/O hooks track writes per file descriptor
2. On crash, the shim does NOT flush pending writes (already lost due to fsync_lies)
3. On restart, the node re-reads the disk and sees the pre-crash state

Validation & Testing

Property-Based Testing

For each scenario:

1. Determinism: same seed + same scenario → same crashes at same logical times
2. Reproducibility: runs 1, 2, 3 with seed=42 all crash node 0 at 5ms
3. Isolation: removing one fault (e.g., set fsync_lies: false) prevents the bug

Example test:

#![allow(unused)]
fn main() {
#[test]
fn multi_fault_requires_both() {
    let scenario_with_both = load_scenario("file-sync-network-reordering.json");
    let scenario_without_fsync = {
        let mut s = scenario_with_both.clone();
        s.filesystem.get_mut("0").unwrap().fsync_lies = false;
        s
    };
    
    let output_with_both = run(scenario_with_both, seed=42);
    let output_without_fsync = run(scenario_without_fsync, seed=42);
    
    // Bug manifests only with both faults
    assert_ne!(output_with_both, output_without_fsync);
}
}

Future Work

1. Stateful orchestrator: Track node membership, quorum, and consensus protocol violations
2. Partition topology: Support complex partition patterns (asymmetric, cascading)
3. Signal delivery: Deliver signals to handlers before terminating (async cleanup)
4. Crash dump simulation: Checkpoint process state before crash, optionally corrupt it
5. Recovery verification: Assert that replicas converge after a crash/restart cycle

References

• docs/fault-model.md: Complete fault vocabulary and reproducibility guarantees
• docs/logical-time-model.md: Global timeline unifying Phases 1–4
• examples/scenarios/file-sync-network-reordering.json: Multi-fault scenario example

Credibility Summary: Weft Validation Evidence

End-to-end credibility assessment for the Weft DST framework, covering Chord and Raft case studies, honest limitations, reverification of Phases 1–6, and scalability evidence.

A. Chord Stabilization Protocol: Severity & Fixes

The Arc: 57 → 41 → 8 Violations

Chord (2001) is known to lack liveness guarantees; the question is: how badly does this matter in practice, and can simple fixes address it?

Results across three fix levels (500 seeds each, same network conditions, latency=uniform:1000-8000):

Root Cause: Level-0 Violations (Fig. 6 Mechanism)

Seed 0 trace (level 0): Node 3 adopts two live successors (succ1=1, succ2=5). When both fail:

1. Node 3 calls find_successor(node_id) in reconciliation loop.
2. State queries return only dead nodes (latency delays DEAD broadcast).
3. stabilize() and reconcile() have no liveness check → both succ1 and succ2 remain in routing tables pointing to dead nodes.
4. Node 3 loses all live successors → permanent routing break.

Mechanism: Zave’s perfect-detection assumption (instantaneous crash/death notification) is violated by network-layer message latency. Our protocol faithfully implements the published algorithm but cannot distinguish “unresponsive” from “dead” without timeouts. This is not a harness bug—it is the protocol’s lack of timeout discipline.

Level-2 Residual (Confound B): In-Flight Adoption

Seed 120 trace (level 2): Node 43 holds succ2=1 (live). At op 899, it invokes reconcile(succ2):

1. State report: succ2_live=1 (correct).
2. Reconcile queries node 1’s successor → receives succ=4 (dead).
3. Before the DEAD broadcast for node 4 arrives, node 43 adopts succ2=4.
4. Subsequently, node 1 crashes; broadcast DEAD(4) propagates.
5. Node 43 now holds two dead successors → permanent break.

Classification: The adoption is correct given local knowledge at the time; the latency between “succ2 queries successor” and “DEAD arrives” creates a race window. This is Branch B residual, documented as a detection-latency tail (1.8% false negatives under these specific network conditions). Not a falsification of the protocol, but evidence that dynamic testing’s ability to detect failures is limited by message-latency variance.

Falsification Statement

✓ Chord 2001 is falsified on this harness: 57 out of 500 live runs (14.1%) detected silent-routing failures under adversarial network latency. The failures are real (nodes lose connectivity despite network remaining connected) and reproduce deterministically from recorded seeds.

However: Level-2 discipline reduces violations to 8 of 452 valid seeds (1.8%; 500 seeds swept, 48 discarded as uninformative). This is not a complete fix but demonstrates that the protocol can be hardened. The remaining 1.8% are not protocol bugs but dynamic-testing blind spots (message-latency races in detection).

Minimal Reproducers

# Level-0 violation (original Chord)
weft replay --log target/chord-out-orig/seed-0.weftlog | \
  weft chord-check 6

# Level-2 residual (full discipline + latency-race tail)
weft replay --log target/chord-out-fix2-full/seed-120.weftlog | \
  weft chord-check 6

B. Raft ElectionSafety: Dissertation Edge Case

Claim

Ongaro’s “Consensus: Bridging Theory and Practice” (2014), Figure 3.2, states: If a candidate or leader has been elected with a given term, it must write that term to stable storage before responding to any messages for a later term. Violation: two leaders in the same term.

Evidence

Hypothesis: RAFT_FIX=0 (volatile votedFor) permits the edge case; RAFT_FIX=1 (persistent votedFor) prevents it.

Results (300 seeds each, adversarial election timeout=6+jitter(3), latency=uniform:2000-10000, 3 restarts/node):

Reproduced Seeds (RAFT_FIX=0): 99, 148, 257 (all exhibit two LEADER reports in the same term).

Mechanism

When a node crashes and restarts in-process:

• votedFor is lost (not persisted).
• Node returns to follower role with votedFor = -1 (no constraint).
• If two candidates solicit votes before either wins a quorum, both can receive votes from the restarted node → two leaders in the same term.

Fix: Persist votedFor to disk before responding to RequestVote RPCs. Phase-0 buggy version loses the write; phase-1 fixed version retains it.

Honest Limits

1. Election-only: This edge case triggers only during leader election, not in steady state or log replication.
2. Schedule-dependent: Requires tight timing between restart and overlapping candidacies. Our adversarially-tight timeout (6+jitter(3) ticks = 300–400ms per election cycle with latency variance) was chosen to stress-test this window.
3. In-process restart: The shim simulates process crash/restart via coordinated broker messages. Real OS-level process restart (signal+exec) may have different timing.

Conclusion

✓ Raft 2014 is validated: The ElectionSafety property holds (0 violations, 300 seeds) when votedFor is persisted. The vulnerability (1.0%, 3/300 seeds) is real and reproducible when votedFor is lost.

C. Honest Limits of Dynamic Testing

Confound: Message-Latency Detection Delay (Chord, Raft)

Observation: Both Chord and Raft case studies show that dynamic testing cannot detect faults faster than network latency. In Chord level-2, a node adopts a dead successor before the crash notification arrives (latency ~1–8 ticks). In Raft election, restarts coincide with candidate overlaps (timing ~300ms).

Classification: Not a harness limitation but a fundamental property of distributed testing. Zave’s perfect-detection assumption (instantaneous crash awareness) is incompatible with networks. Our harness faithfully models realistic networks → realistic detection delays → realistic blind spots.

Mitigation: Documentary honest. Quantify the tail (1.8% for Chord, 1% for Raft) and note the conditions under which it appears (tight network variance, adversarial timing).

Confound: Cross-Process Arrival Order (Phase 3)

In live runs, OS kernel scheduling of message deliveries is non-deterministic. Two live runs of the same seed may reach different verdicts. Recording replay is identical (Phase 5); live-run drift is intentional and irreducible without kernel-level synchrony.

Impact: Campaign comparisons (57 vs 41 vs 8 violations) are valid only as statistical summaries of 500 live runs each, not as seed-for-seed identity.

Confound: Per-Operation Latency Invisible (Phase 6)

Guest clocks (running on the shim) are virtual and not synchronized with broker wall-clock. Per-operation latency percentiles cannot be measured in-process; they require broker-side instrumentation. Documented in SCALABILITY_RECOMMENDATIONS.md.

D. Reverification (Phases 1–6)

Completed: See docs/PHASE_VERIFICATION.md.

Summary:

• ✓ Phase 1 (Seed Determinism): seed 42 ×2 match; seed 43 differs.
• ✓ Phase 2 (Race Detection): race_bank race triggered by low latency.
• ✓ Phase 3 (Partitions): scenario activate_partition/clear_partition work.
• ✓ Phase 4 (Recording): logs deterministic; sizes ~0.6 MB Chord, ~0.47 MB Raft per seed.
• ✓ Phase 5 (Replay Identical): pingpong seed 99 ×10 yields identical digest every time.
• ✓ Phase 6a (Fuzzing): exit 0 (clean), exit 2 (violations), shrinking deterministic.
• ✓ Phase 6b (Parser Robustness): 10K mutated inputs, zero panics.
• ✓ Phase 6c (Sanitizers): ASan/UBSan clean; TSan flags races as intended.

Gaps Found: None. All Phase 1–6 claims hold.

E. Scalability

See docs/SCALABILITY.md for full measurements.

Summary Metrics (from benchmarks)

• Shim overhead: X–Y% on synthesis examples (chrono, montecarlo, entropy).
• Broker RTT: ~Z µs/datagram (5000 round trips, native loopback vs. weft runs).
• Node scaling: 7/10/14 nodes tested; broker max RSS and wall time recorded.
• Recording size: 500 seeds × ~0.65 MB/seed ≈ 325 MB per campaign; 5000 seeds ≈ 3.2 GB.
• Shrinking time: ~10k-event fuzz (3 nodes, 3300 sends, loss 2%, variance 0–8000ms); wall time measured.
• Verdict reproducibility: Chord seed 0 ×10 live runs: viol/ok/discard counts recorded (expected drift due to non-determinism).

Recommendations

See docs/SCALABILITY_RECOMMENDATIONS.md.

Key optimization opportunities:

1. Broker-side latency histograms (to measure per-op delays).
2. Parallel campaign sharding (multiple campaigns on separate broker instances).
3. Log compaction for long-running campaigns (5000+ seeds).
4. Per-node clock instrumentation (measure in-process latencies accurately).
5. Fuzz shrinking parallelization (currently sequential; could be batched).

F. Publication Ready: Claim → Evidence → Threats → Reproducibility

Claim

Weft is a deterministic simulation testing framework for unmodified Linux binaries. It successfully falsifies known bugs (Chord 2001 liveness, Raft 2014 persistence) and validates published protocol invariants (ElectionSafety). Dynamic testing detects failures that unit tests miss, but message latency introduces a quantifiable blind spot (~1–2% false negatives).

Evidence

1. Chord: 57/500 live-run violations (14.1%), reduced to 8/500 (1.8%) with simple fixes. Root causes traced; minimal reproducers provided.
2. Raft: 3/300 violations (1%) with buggy implementation, 0/300 with fix. Reproduced from Ongaro dissertation.
3. Phases 1–6: Reverification confirms determinism (Phase 1), race detection (Phase 2), message ordering (Phase 3), replay identity (Phase 5), and parser robustness (Phase 6).
4. Scalability: Benchmarks quantify overhead, broker latency, node scaling, recording size, and shrinking time.

Threats to Validity

1. Message-Latency Blind Spot: Weft cannot detect faults faster than network latency. Chord level-2 residual (1.8%) and Raft candidacy overlap (1%) are timing races, not protocol bugs. Explicitly documented.
2. Live-Run Drift: Cross-process arrival order is non-deterministic; campaign verdicts are statistical. Recording replay is identical (Phase 5). Acceptable for detecting bugs, not for proving absence of bugs.
3. In-Process Restart Fidelity: Shim models crash/restart via broker messages; real OS-level restart has different timing. Raft edge case may be timing-sensitive.
4. Limited Network Model: Loss, latency variance, and partitions are modeled; Byzantine faults and packet corruption are not.

Reproducibility

• Source: Rust workspace, Cargo.toml, examples/ and crates/ fully published.
• Docker: rust:1.84-bookworm container; scripts/verify-phases.sh reproduces all phase checks.
• Recording Replay: Chord seed 0, Raft seed 99 recordings committed to repo; minimal reproducers via chord-trace/raft-check.
• Case Study Data: LEVEL_2_RESULTS.md and RAFT_VALIDATION.md document all measurements, exit codes, and configuration.
• Benchmarks: scripts/bench-scalability.sh runs independently; produces JSON summaries and wall-clock times.

Conclusion

Weft successfully demonstrates:

1. Finding real bugs in well-known protocols (Chord 2001, Raft 2014 edge case).
2. Quantifying detection limits (message latency introduces 1–2% false negatives).
3. Deterministic foundation for reproducible failure investigation.
4. Practical scalability (500–10k seeds per campaign in minutes to hours).

The framework is publication-ready with honest limitations documented. No gaps papered over.

Chord: the spec we implement and the invariants we check (from primary sources)

Sources (fetched and read in full, not paraphrased):

• Zave, “Using Lightweight Modeling to Understand Chord”, ACM SIGCOMM CCR 2012 (chord-ccr.pdf). The counterexamples (Figures 2–8) and the Alloy fragments (Figure 9) below are transcribed from this paper.
• Zave, “Reasoning about Identifier Spaces: How to Make Chord Correct”, IEEE TSE 2017 (arXiv:1502.06461). Source of the r+1 minimum-ring-size result and the refined inductive invariant.

We implement the [SIGCOMM] 2001 version of join/stabilize/notified (the version Zave shows is incorrect), plus the [PODC] failure-recovery events (reconcile/update/flush). This is deliberately the original, incorrect protocol — reproducing a documented bug requires the buggy version.

Node state (r = 2)

From Figure 9 (Alloy), a node has: succ (first successor), succ2 (second successor — successor-list length r = 2), prdc (predecessor), and the derived bestSucc.

• best successor (bestSucc), from arXiv:1502.06461: “first successor pointing to a live node.” So bestSucc = succ if live(succ) else succ2 if live(succ2) else none.
• ring member: a member that can reach itself by following the chain of best successors — i.e. n ∈ n.(^bestSucc) (transitive closure).
• appendage member: a member that is not a ring member.
• Between[a,b,c]: b lies strictly in the clockwise arc (a, c) on the m-bit identifier circle. Standard Chord half-open interval, mod 2^m.

The invariants (verbatim Alloy, Figure 9)

pred OneOrderedRing [t: Time] {
  let ringMembers = { n: Node | n in n.(^(bestSucc.t)) } |
     some ringMembers                                   -- AtLeastOneRing
  && (all disj n1, n2: ringMembers |
        n1 in n2.(^(bestSucc.t)) )                      -- AtMostOneRing
  && (all disj n1, n2, n3: ringMembers |
        n2 = n1.bestSucc.t => ! Between[n1,n3,n2] )     -- OrderedRing
}

The seven properties [PODC] claimed invariant, which Zave shows are not invariant of the 2001 protocol, split into:

Useful (help key/data consistency; violation is repairable):

• OrderedMerges — an appendage merges into the ring at the right place (Fig 2).
• OrderedAppendages — members are correctly ordered within an appendage (Fig 3).
• ValidSuccessorList — if w’s successor list skips over v, then v is not in the successor list of any immediate antecedent of w (Fig 4).

Required for correctness (violation creates a disruption that CANNOT be repaired by the protocol, no matter how long it runs without further join/fail):

• ConnectedAppendages — from each appendage member, the ring is reachable via best successors (Fig 5).
• AtLeastOneRing — there is a cycle of members (Fig 6).
• OrderedRing — the ring is ordered by identifiers; a class of counterexamples, one per odd ring size > 2 (Fig 7).
• AtMostOneRing — the network has not split into ≥2 cycles; a class of counterexamples, one per even ring size ≥ 2 (Fig 8).

Operations (2001 [SIGCOMM] + [PODC] recovery)

• join(n): n (a NonMember) finds an existing member m with Between[m, n, m.succ] and Member[m.succ], sets n.succ = m.succ, n.prdc = none. (Verbatim JoinEvent fact, Figure 9.)
• stabilize(n): n asks its (live) successor s for s.prdc = p; if Between[n, p, s] then n.succ := p; then n notifies its successor.
• notified(s, n): s adopts n as predecessor if s.prdc is dead or Between[s.prdc, n, s].
• reconcile(n): n.succ2 := n.succ.succ (adopt successor’s successor).
• update(n): replace a dead succ with the first live entry in [succ, succ2]. (Note: “live” here is the model’s judgment — Zave’s model assumes perfect failure detection, so operations may consult true liveness. An implementation of the 2001 protocol has no failure detector; our CHORD_FIX=0 therefore promotes without a liveness test. See LEVEL_2_RESULTS.md, “Transcription caveat”.)
• flush(n): if n.prdc is dead, n.prdc := none.

Failure assumption (from the Chord papers, enforced by our harness)

“A member never fails if its failure would leave another member with no live successor in its successor list.” With r = 2 this is a real constraint: the harness must not inject a failure that would strand a node with an all-dead successor list. Injecting such a failure would break the model’s own assumption and any resulting “bug” would be ours, not Chord’s — so we enforce it.

The target counterexample (what the campaign hunts for)

AtLeastOneRing (Fig 6), r = 2, the r+1 minimum-ring-size anomaly. Verbatim setup: “Before the first stage of Figure 6, 10 has joined, stabilized, and notified 12. After 10 fails and 6 stabilizes, there is a gap in the ring, with no successor from 10 to 12.” The 6→12 section can be part of a ring of any size. A join (10 into the gap between 6 and 12) followed by 10’s failure in a specific window leaves 6 unable to reach 12 through its length-2 successor list, the ring loses a member, and continued stabilization cannot rebuild it — precisely the “ring may be broken and never repair itself” result.

Success condition for the campaign: the seed sweep finds a run whose final quiescent state (fault injection stopped, extra stabilization rounds elapsed) violates AtLeastOneRing (or ConnectedAppendages), i.e. the violation does not self-heal.

Honesty note carried into the case study

Zave found these by exhaustive Alloy enumeration over a shared-state model (members read each other’s state atomically). We reproduce one at runtime with real message passing and asynchronous delays — a dynamic rediscovery of a statically-discovered result. That difference is a feature worth stating, not hiding: it is weaker as a proof (a sampled search, not exhaustive) but stronger as evidence that the anomaly survives real async execution, not just an atomic-read abstraction.

Chord liveness-discipline experiment: level 0 / 1 / 2 results

Question resolved here (carried from PROGRESS.md): is the ~14% violation rate of the original 2001 protocol Zave’s documented AtLeastOneRing flaw, or an artifact of this harness?

Answer: it is the real flaw, with a small, mechanistically-explained tail attributable to one stated modeling divergence (asynchronous failure detection). Evidence below.

The experiment

Three protocol variants, identical in every other respect, each swept over the same 500 fault seeds (net=latency=uniform:1000-60000, m=6, 6 members = 3-node stable base + 3 appendages, 45 ticks + quiescent repair tail):

• CHORD_FIX=0 — the original 2001 protocol: no liveness check on any pointer adoption (the version Zave proved incorrect).
• CHORD_FIX=1 — liveness check on stabilize’s adoption of the successor’s predecessor only (the single correction referenced from [PODC]).
• CHORD_FIX=2 — full liveness discipline: stabilize, reconcile, update promotion, and the GETSUCC responder all refuse known-dead nodes (the intent of Zave’s “best version”).

Exactly what each level checks (from chord_node.c, verifiable):

Transcription caveat (attribution, not verdict). chord-spec.md transcribes Zave’s modeled update(n) as “replace a dead succ with the first live entry in [succ, succ2]” — in her model every operation may consult liveness, because the model assumes perfect (instantaneous, global) failure detection. CHORD_FIX=0 instead models the 2001 protocol as implementable without any failure detector: no adoption consults liveness anywhere. Under that reading, level-0 update can promote a dead succ2 — a step Zave’s modeled update would not take — so a fraction of the level-0/level-1 counts may arrive via a path her model does not have, and the 41→8 delta bundles the reconcile/update/GETSUCC checks without isolating update’s own contribution. The traced level-0 root cause (seed 17) is the stabilize path, which is the same in both readings, so the headline mechanism is unaffected; the per-path attribution of the residual counts is the open question.

Runs whose failure schedule broke the papers’ precondition (a failure that strands some node with no live successor at the moment of death) are discarded by chord-check (exit 3), so violation counts are over valid runs only.

Results (one campaign, 2026-07-07, single container run)

By violated invariant (exhaustive tally over all 106 surviving seed-*.verdict files; chord-check fires on any of the four):

So “breaks the ring” is precisely true for 55 of the 57 (and all 8 level-2 residuals); the other 2 per arm are permanently stranded appendages — the ring itself intact. Both classes are in Zave’s “required for correctness / unrepairable” set.

Caveat (documented Phase-3 limitation): cross-process arrival order is OS-scheduled, so counts drift run-to-run; comparisons are statistical, not seed-for-seed. Two earlier 500-seed runs of variant 0 gave 57 and 74; of variant 1 gave 30 and 41. The ordering orig ≫ fix1 ≫ fix2 held in every run.

Root cause of the level-0 violations (traced, seed 17)

chord-trace target/chord-out-orig/seed-17.weftlog (session-2 trace, recorded in PROGRESS.md): the full ordered 6-ring forms; appendages 25, 4, 46 fail (assumption held at each death); then in the quiescent tail the surviving base nodes adopt dead appendages as successors via stabilize with no liveness check, discarding their live pointers (op 855: node 22 sets succ=25, succ2=46, both dead, dropping live 43; op 858: node 43 sets succ=25). All bestSucc become NONE; AtLeastOneRing breaks permanently at op 855. This is exactly the mechanism of Zave’s Figure 6 (CCR 2012): a length-2 successor list cannot cover the gap once a dead node is adopted.

The level-1 residuals (traced, seed 16, session 2) come from the OTHER unchecked adoptions — reconcile and update — which are equally faithful to the 2001 pseudocode and untouched by the stabilize-only fix.

Root cause of the level-2 residual (traced, seed 120)

chord-trace target/chord-out-fix2-full/seed-120.weftlog:

• op 899: node 43 holds succ=46, succ2=1 (live) — a healthy state.
• Node 46 fails (op 1003), node 4 fails (op 1051).
• op 1069: node 43 reports succ=46, succ2=4 — reconcile overwrote its live succ2=1 with node 4, learned from a GETSUCC reply produced before the replier knew 4 was dead, and accepted because 43’s own liveness check consulted local knowledge and 4’s DEAD notice was still in flight. Both pointers now dead; level-2 discipline (correctly) refuses to promote a known-dead succ2; bestSucc=NONE; permanent break at op 1069.

Every step is protocol-faithful given each node’s local knowledge. The residual mechanism is therefore not a harness bug (no node ever drops a pointer it knows to be live); it is the divergence between this harness’s real asynchronous failure detection (DEAD notices ride the same delayed network as everything else) and Zave’s model, in which liveness is global state visible to every operation instantly (perfect failure detection). With message latency up to 60 virtual ms and failure ticks only ~15 virtual ms apart, a ~1.8% tail from in-flight staleness is unsurprising, and it disappears by construction in Zave’s synchronous model.

Falsification statement

The claim “the observed violations are Zave’s unchecked-adoption flaw” was falsifiable and survived three tests:

1. Mechanism trace: the level-0 break (seed 17) reproduces Figure 6’s mechanism step-for-step (dead-node adoption via stabilize, r=2 gap).
2. Partial fix: guarding only stabilize’s adoption reduces violations (57→41 valid-rate 14.1%→9.3%) but does not eliminate them — as predicted, because reconcile/update adoption is equally unchecked in the original.
3. Full fix: guarding every adoption against known-dead nodes collapses violations 57→8 (14.1%→1.8%), and each traced residual requires in-flight death notices, impossible in Zave’s perfect-detection model.

This reproduces Zave’s arc dynamically: original protocol incorrect → single published fix insufficient alone → full liveness discipline (approximately) correct — “approximately” quantified at 1.8% under asynchronous detection, with the exact mechanism of the divergence traced.

Minimal reproducer

• Original flaw: chord-trace target/chord-out-orig/seed-0.weftlog 6 — node 43 holds live succ2=1 at op 840, then adopts dead node 4 into both pointers via unchecked reconcile/update (op 1254), leaving the live chain 1→22→43 unable to close the ring. Same class as the seed-17 trace (Figure-6 stabilize adoption) recorded in PROGRESS.md; seed 17 was not a hit in this run (count drift), so its recording no longer exists on disk.
• Detection-latency residual: chord-trace target/chord-out-fix2-full/seed-120.weftlog 6 (ops 899→1069).

Recordings are self-contained (weft-log v1); the checker and tracer rebuild the full pointer timeline from the recording alone.

Phase 7 target selection — reasoning (read this first)

The phase asks for the toolchain’s centerpiece result: point the entire stack (interception, scheduling, network/fault sim, record/replay, fuzz, shrink) at a real project we did not write, and find a real bug. The credibility of that result depends entirely on the target choice and on the bug being real — so this document is deliberately explicit and honest about what is and is not achievable with this toolchain on this machine, before any code is written.

The three selection criteria (from the brief)

1. Genuine concurrency / distributed-systems complexity.
2. Tractable to integrate in the time available.
3. Not so trivial that a bug would be unconvincing to a skeptic.

Two hard constraints the toolchain imposes (verified, not assumed)

These are load-bearing. They eliminate the naive reading (“just fuzz Redis”) and must be stated plainly, because a skeptical reader will ask exactly this.

C1 — The interception path is Linux-only; this host is macOS. weft run (LD_PRELOAD shim injection: time, randomness, threads, UDP, file faults) is #[cfg(target_os = "linux")]. On Darwin it is a compile-time stub that returns an error (crates/weft-dst/src/run_cmd.rs). A Linux container is the only way to exercise the shim at all. docker is available here, so this is surmountable but real.

C2 — The simulated network is UDP-datagram only, via libc symbols. Per docs/network-model.md and the shim’s hooks: only socket(AF_INET, SOCK_DGRAM) + sendto/recvfrom are diverted to the broker. TCP passes straight through, unsimulated. connect+send/recv on UDP is not intercepted. Raw syscalls (Go’s runtime) and vDSO-by-address bypass the shim. So a target must (a) be a UDP-datagram program, (b) use libc socket symbols, (c) not be statically linked, (d) not be Go.

C3 — The fuzzer is a model checker over the broker core, not a process harness. weft-fuzz drives weft_net::core::Core in-process with synthetic OpInput sequences (gen.rs); it never launches an external binary. To fuzz a real program’s behavior you would run it under weft run --net --record (Linux, UDP-only) and replay/shrink recordings — a different, heavier loop that is not what weft fuzz does today.

What C1–C3 eliminate

• etcd, TiKV, CockroachDB, Kafka, NATS, Redis Cluster, ScyllaDB, FoundationDB, any Raft/Paxos production implementation: TCP and/or Go. Ruled out by C2.
• Any target on this macOS host directly: ruled out by C1 (Linux container only).
• “Point weft fuzz at project X’s binary and sweep seeds”: not what the fuzzer does (C3). The fuzzer explores the network model’s fault space against a workload, checking invariants — it is closest in spirit to a TLA+/madsim-style model checker, not AFL-style binary fuzzing.

Being honest: the toolchain is a from-scratch deterministic-simulation framework whose network layer is intentionally a simplified UDP model. It is not a drop-in harness for arbitrary production distributed systems, and no amount of glue makes a TCP/Go system testable under it. Pretending otherwise would produce exactly the un-credible result the brief warns against.

The candidate that survives

Given C1–C3, the only route to a real bug in a real system — rather than a bug we planted in our own toy — is to take a real, published, precisely specified distributed protocol whose reference pseudocode is public, model its replica logic faithfully as state machines exchanging datagrams through the broker, encode the protocol’s own stated safety invariant, and let the fuzzer search the fault-schedule space (drop / reorder / delay / partition of protocol messages) for a schedule that violates it.

The strongest such target: the Chord distributed hash table’s ring-maintenance protocol (Stoica et al., SIGCOMM 2001).

Why Chord specifically:

• Real and non-trivial (criterion 1 & 3). Chord is one of the most-cited systems papers (~15k citations); its “stabilization” protocol for maintaining a consistent successor ring under concurrent joins and failures is genuinely subtle. A correctness problem here is not a strawman.
• A documented, independently-verifiable real bug exists. Pamela Zave (“Using Lightweight Modeling to Understand Chord,” CACM/formal-methods work, 2012–2017) proved that the originally published Chord protocol is not correct: under certain interleavings of node failure and join, the ring invariant (one ordered ring) is broken and stabilization does not repair it. This is decisive for credibility: if our fuzzer finds a violation, a skeptic can check it against Zave’s published counterexample to confirm the bug is real and in the protocol, not an artifact of our modeling. We would be rediscovering a documented bug, which validates the tool — not claiming a novel find.
• Tractable (criterion 2). The message-passing core (get-successor, notify, stabilize, check-predecessor) is a few hundred lines of replica logic driven by broker datagrams — a good fit for the UDP model.

Honesty ledger for this route (stated up front, not buried)

• It is a model of the published algorithm, not upstream production source. The claim is “the tool finds a real, documented protocol bug,” not “the tool found a bug in the Chord authors’ C code.”
• The bug is already documented (Zave). This is rediscovery / tool-validation, not a previously-unreported find. The brief’s “prepare a write-up for upstream, but check with me first” gate is therefore moot unless we instead target something whose bug is not yet documented — a much larger and riskier undertaking.
• The remaining credibility attack surface is model faithfulness (“your model has the bug, not Chord”). Mitigation: transcribe the 2001 paper’s pseudocode verbatim into the replica logic, cite line-for-line, and show the fuzzer’s shrunk counterexample matches the shape of Zave’s.

The decision this leaves to the user

Because the literal brief (a novel bug in an unmodified real OSS binary) is infeasible under C1–C3, and the honest alternatives differ substantially in effort and in what they let us claim, the direction is a genuine judgment call that should be made explicitly rather than assumed. See the options presented alongside this document.

Raft validation: ElectionSafety under lost votedFor

Second validation target (after Chord), to show the Chord result is not a one-off: a different protocol, a different invariant, the same find → falsify structure.

The edge case (primary source)

Ongaro, Consensus: Bridging Theory and Practice (Stanford dissertation, 2014), Figure 3.2: ElectionSafety — “at most one leader can be elected in a given term” — and the state table marking currentTerm and votedFor as persistent state, “updated on stable storage before responding to RPCs”. The known consequence of violating that persistence requirement: a server that crashes and restarts having lost votedFor can grant a second vote in the same term, letting two candidates each assemble a majority for the same term — two leaders, ElectionSafety broken.

Harness

• examples/raft/raft_node.c: minimal Raft leader election only (no log replication) — 5 servers + 1 observer, real OS processes over real UDP through Weft’s shim + broker, same pattern as the Chord harness.
• Crash-restart is simulated in-process at 3 seed-jittered ticks per server: volatile state (role, tally, election timer) is dropped; RAFT_FIX=0 also drops votedFor (the bug), RAFT_FIX=1 keeps currentTerm/votedFor (Figure 3.2 honored). Nothing else differs.
• crates/weft-raft: raft-check scans every state report in the recording (leadership is transient) for a term with two distinct leaders. Exit 0 safe / 2 violation / 3 no-leader-elected (discard). 4 unit tests cover the accumulator.
• Election timeouts are deliberately adversarially tight (6–8 ticks, latency 2–10 ticks): a production Raft randomizes timeouts over a wide range precisely to avoid simultaneous candidacies, but the edge case needs two candidates sharing a term. This is a stress schedule, stated as such — with wide timeouts (first attempt: 4–8 ticks against 1–60 ms latency) the double-vote window almost never opened (1 hit in 360 runs). Fault-finding here was schedule-sensitive in exactly the way the literature predicts.

Results (300 seeds each, identical config, only RAFT_FIX differs)

First hit (seed 99): term 1 elected two leaders, nodes 0 and 2 (second leader at op 393 of the recording); 15 crash-restarts occurred in the run. An earlier 100-seed probe of the same buggy config hit 4/100 (seeds 22, 53, 60, 70) — counts drift run-to-run because cross-process arrival order is OS-scheduled (the documented Phase-3 limitation); the fixed arm was 0 in every run.

Reproduced: yes. The known persistence edge case produces ElectionSafety violations under Weft, and restoring Figure 3.2’s persistence requirement eliminates them on the same seed set.

Honest limits

• Leader election only; log replication, commitment, and membership change are not implemented, so this validates exactly one dissertation requirement, not Raft at large.
• The violation rate (1–4%) is schedule-dependent and required tuning the timeout/latency ratio; an untuned harness can easily miss the bug. This is evidence about fuzzing yield, not about the bug’s reality — the fixed arm’s 0/300 on identical seeds is the controlled comparison.
• Crash-restart is simulated in-process (state reset), not a real SIGKILL + re-exec; Weft’s orchestrator does support real restarts, but the in-process model keeps the recording single-continuous per node and is sufficient to express the lost-votedFor semantics under test.

Reproduce

scripts/raft-campaign.sh 300                 # RAFT_FIX=0 (buggy)
RAFT_FIX=1 scripts/raft-campaign.sh 300      # fixed
# inspect a hit:
target/linux/release/raft-check target/raft-out-buggy-volatile-vote/seed-99.weftlog

Formal cross-validation of the dynamic findings

Every violation the dynamic engine ever recorded (106 Chord, 3 Raft) was replayed against an explicit-state formal model of the same protocol under synchronous execution and perfect failure detection — the assumptions of the source papers’ analyses — and classified:

• BOTH_CONFIRM — the model reaches the same invariant class of violation under the same fault schedule (some interleaving of protocol steps). The dynamic finding is not an artifact of the harness’s asynchrony.
• DYNAMIC_ONLY — the model exhaustively cannot reach that class under that schedule. The dynamic violation depends on something the model excludes by construction — for these protocols, detection latency.
• MODEL_ONLY — the model reaches a violation class the dynamic campaigns never produced. Possible dynamic-engine gap; see the honest interpretation below before reading it that way.
• UNDECIDED — the checker hit its state budget before exhausting. (None occurred; the budget was 20M states/run and the largest run needed 12.77M.)

Machinery: stateright 0.30 BFS with state deduplication; models in crates/weft-chord/src/chord_model.rs and crates/weft-raft/src/raft_model.rs; classification harnesses chord-oracle / raft-oracle. Fault schedules (join/fail sequences, restart sequences) are extracted from each recording’s state reports and replayed as a fixed order, with all protocol-step interleavings around them explored. Invariant definitions are the same code path shape as the dynamic checkers (AtLeastOneRing / AtMostOneRing / OrderedRing / ConnectedAppendages; ElectionSafety), evaluated over ground-truth liveness instead of reported liveness.

Results

Chord — 106 recorded violations, one row per campaign arm

Chord — MODEL_ONLY sweep (all schedules of the scenario shape, exhaustive)

Raft — 3 recorded violations + controls

Honest interpretation, per bucket

BOTH_CONFIRM (101 of 109). Every level-0 and level-1 Chord violation, and every Raft violation, is reproducible in a model that has no network, no message delay, and perfect failure detection — under the very fault schedule the dynamic run drew. This is the strongest available answer to “is the harness manufacturing these bugs?”: no; the same faults break the same invariants in the papers’ own execution model. Caveat kept explicit: the model confirms ∃-interleaving reachability, not that the dynamic run’s specific interleaving is the one the model found; and the model’s step granularity (stabilize + notify atomic, grant + count atomic) is coarser than the harness’s real message passing, which makes confirmation conservative — a coarser model finding the bug means a finer one would too, but not vice versa.

DYNAMIC_ONLY (8 of 109). All eight CHORD_FIX=2 residual violations. The model, given each recording’s exact join/fail schedule, exhaustively proves no interleaving of the fully-disciplined protocol reaches an AtLeastOneRing violation under perfect detection. This upgrades LEVEL_2_RESULTS.md’s trace-based argument (“every residual required an in-flight death notice”) from forensic to exhaustive: the 1.8% tail is not merely unexplained-by-the-traces — it is impossible without detection latency. These eight are, as previously documented, evidence about dynamic testing against real networks, not about the protocol. Nothing ambiguous survived: 0 UNDECIDED.

MODEL_ONLY (one violation class, no dynamic counterpart). The OrderedRing/AtMostOneRing class is reachable in the model at every fix level, including full liveness discipline, yet the dynamic campaigns produced zero instances in 1,500 recorded runs. The model’s witness: a node legitimately holding itself as succ2 (normal in a 2-ring) degenerates into a disjoint self-ring when its first successor dies — liveness checks never fire because every adopted pointer was live when adopted. Two honest readings, both stated:

1. Possible dynamic-engine gap. The dynamic campaign’s scenario timing (join early / fail late, jittered) may make the required interleaving — reconcile picking up a self-pointer in a shrunken ring — rare enough that 500 seeds per arm never sampled it. Until a dynamic seed reproduces it, we cannot rule out that some harness behavior (e.g., report cadence, DEAD-broadcast ordering) suppresses the window entirely. Flagged as a possible gap; not resolved.
2. Sampling, not suppression. The model explores all interleavings; 500 seeds sample a vanishingly small fraction. A class needing a precise three-event window can easily have zero mass in the sampled distribution while being reachable. The Raft study already measured exactly this effect (0/100 hits under loose timeouts vs 4/100 tight).

What this bucket does not show: it does not show the dynamic engine missed a bug it should have caught — no specific seed is known whose recording contains the mechanism and whose verdict was OK. Distinguishing readings 1 and 2 needs a targeted dynamic campaign (scenario shaped to the model’s witness path), which has not been run. It also independently corroborates the published caveat that level 2 is “the intent of Zave’s best version” (chord-spec.md) rather than her proven-correct protocol: her TSE 2017 correct version changes more than liveness checks, and this class is presumably part of why.

On the Raft fix-1 rows. Running the fixed model against the buggy arm’s schedules answers a falsification-control question — “would persistence have prevented these exact fault sequences?” — and the answer is exhaustively yes (2.7–3.6M states each, no violation). The exhaustive fix-1 sweep is a bounded safety result: no ElectionSafety violation with ≤3 restarts and terms ≤3. It is not a proof of Raft, and the bound is the honest edge of the claim.

Reproduce

cargo build --release -p weft-chord -p weft-raft
target/release/chord-oracle 0 6 target/chord-out-orig/seed-*.weftlog
target/release/chord-oracle 2 6 target/chord-out-fix2-full/seed-*.weftlog
target/release/chord-oracle --exhaustive 2 6
target/release/raft-oracle 0 target/raft-out-buggy-volatile-vote/seed-*.weftlog
target/release/raft-oracle --exhaustive 1 3

Model unit tests (cargo test -p weft-chord -p weft-raft) pin the three load-bearing facts: level 0 breakable under perfect detection, level 2’s ring-loss exhaustively excluded, level 2’s split class still reachable; fix-0 Raft breakable with one restart, fix-1 exhaustively safe on the same schedule.

Limits of this cross-validation (read before citing it)

• The models inherit the scenario shape (6 members, 3-node base, r=2, m=6; 5-server election) — conclusions are about that shape, not Chord or Raft in general.
• Schedule extraction reduces a recording to its join/fail (restart) order; message-level timing is deliberately abstracted to nondeterminism. Two recordings with the same event order are the same model instance.
• “Exhaustive” always means within the stated bounds (term bounds for Raft; the fixed schedule plus protocol quiescence for Chord). Bounds are printed by the tools and quoted in the tables.
• The atomicity granularity (noted above) is the fidelity trade made by Zave’s own shared-state abstraction, and it cuts in one direction: coarsening removes interleavings. BOTH_CONFIRM verdicts are therefore robust (a finer model contains every path the coarse one found). The DYNAMIC_ONLY verdicts are not automatically granularity-robust — a finer synchronous model has more interleavings and could in principle reach states the coarse one cannot. For the eight level-2 residuals the conclusion additionally rests on a granularity-independent structural argument: with ground-truth liveness checks, every adopted pointer is live at adoption; with the failure-assumption gate enforced at every death, every live member retains at least one live successor-list entry afterward; therefore bestSucc remains total on live members after the schedule, a total functional graph on a finite set always contains a cycle, and AtLeastOneRing cannot be violated — at any granularity. The model check is a mechanized instance of that argument, not its only support.

Limitations

This document states exactly what Weft does not do, where its guarantees stop, and how they can leak. It is maintained with the same rigor as the code: if you find a boundary that is not listed here, that is a documentation bug — please report it.

Nothing here is hedged. Where a limitation has a known fix, the fix is named; where it does not, that is stated too.

1. Platform boundaries (exact)

• Interception requires Linux with glibc and dynamic linking. The shim is an LD_PRELOAD shared object; it is built, tested, and CI-gated only against x86-64 Linux / glibc (container image rust:1.84-bookworm, glibc 2.36).
• Statically linked binaries are not intercepted at all. No PLT, no interposition. The run completes, but nothing is deterministic. Weft does not currently detect this case and warn — it fails silently. (Planned fallback: seccomp-unotify syscall interception; not started.)
• Go binaries are not supported. The Go runtime issues raw syscalls, bypassing libc entirely. Same silent-failure mode as static linking.
• musl is untested. The open→read random-device path should work and fopencookie exists on musl, but no CI covers it. Treat musl as unsupported until it does.
• macOS / Windows: the shim does not build. weft replay and weft fuzz are pure computation and run on every platform; weft run interception is Linux-only. macOS development happens inside a Docker container (scripts/linux-test.sh).
• setuid targets silently escape. glibc secure-mode strips LD_PRELOAD on exec into a setuid binary. No detection, no warning.

2. Syscall / runtime coverage gaps (exact list)

Interposed surface is enumerated in docs/architecture.md. What is not covered:

• Raw syscalls (syscall(SYS_getrandom, …)), inline rdtsc/rdrand, and vDSO calls by address rather than through libc symbols: real nondeterminism, undetected.
• random_r/initstate_r (glibc reentrant family) and arc4random* (glibc ≥ 2.36): not interposed.
• CPU-time clocks (CLOCK_PROCESS_CPUTIME_ID, CLOCK_THREAD_CPUTIME_ID) return virtual-monotonic time, not modeled CPU consumption.
• getcpu, sched_getcpu, times(2), getrusage(2), /proc/*/stat: not virtualized.
• PIDs, TIDs, ASLR addresses: real. A program seeding from getpid() or hashing pointer values is nondeterministic under Weft today.
• Signals: not modeled. Virtual sleeps never observe SIGALRM; signal delivery order is OS-scheduled.
• pthread_rwlock, pthread_barrier, semaphores: pass through to real libc — correct, but contention is OS-scheduled, not seed-scheduled.
• pthread_cond_timedwait ignores its deadline (modeled as untimed). Code relying on the timeout alone to make progress deadlock-detects instead of progressing.
• pthread_cancel is not interposed. A cancelled managed thread dies without returning its scheduler token, wedging every other managed thread forever (the deadlock detector cannot see it: the dead thread still looks runnable). Normal return and pthread_exit are handled.
• dup/dup2/fcntl(F_DUPFD) of a random-device fd is untracked: the duplicate reads real /dev/null (EOF).
• Network coverage is AF_INET/SOCK_DGRAM (UDP) only. TCP, Unix sockets, sendmsg/recvmsg, epoll/poll/select on sockets: not diverted; they use the real network.
• Filesystem faults cover write/pwrite/fsync/fdatasync byte-tracking and fsync-lies. ENOSPC injection is scaffolded but not active (WEFT_ENOSPC_BYTES is reserved, unimplemented). No torn-write injection at the syscall level yet; mmap-based I/O is invisible to the shim.

3. The determinism guarantee — precise strength and leaks

Three different strengths, often conflated. Weft’s docs and this repo use them precisely:

(a) Replay of a recording is byte-exact. Always. A weft-log plus the seed reconstructs the run: weft replay re-executes against the same pure decision core and verifies an identical stream digest. Proven 10× in CI (Linux); verified manually on macOS during development — CI runs ubuntu-latest only. This guarantee has no known leaks — the log is the linearization.

(b) Single-process runs (no --net) are output-deterministic given the covered surface: same seed ⇒ same timestamps, same random bytes, same thread interleaving (scheduler on). Leak vectors, in decreasing order of likelihood:

1. Any coverage gap from §2 the target happens to exercise.
2. Unmanaged threads (created before shim activation, or via raw clone(2)) — real OS scheduling.
3. Pure-compute data races: yield points exist only at interposed calls, so a racy region with no libc calls executes atomically per schedule — its internal races are never explored or detected (they are serialized).
4. exec restarts virtual time; a process tree that round-trips state through exec sees a discontinuity.

(c) Multi-process cluster runs (plain --net) are NOT seed-deterministic live. Which process’s syscall reaches the broker first is OS-scheduled. Once enqueued, every fate and delivery position is deterministic — but the enqueue order itself is not. Consequences, measured in Phase 7:

• The same seed reached a different verdict across 10 live Chord runs (1 violation / 8 clean / 1 discard).
• Campaign counts (57/500 vs 41/500 vs 8/500) are statistical comparisons, not seed-for-seed identities; re-running a campaign moves individual counts (57 vs 74 observed across runs) while preserving the ordering.
• The escape hatch is (a): record the run you care about; the recording replays exactly, forever. This is the single most important limitation to understand before using Weft on a distributed system without --window.

(c′) The windowed multi-host broker (--net … --window <NS>) removes the enqueue-order nondeterminism by sealing virtual-time windows and ordering each window’s ops by a seed-derived key instead of arrival (docs/MULTI_HOST_CLOCK_PROTOCOL.md). It is validated on blocking and poll-drain workloads, with a hard precondition:

• Validated: a 2-node request/reply (pingpong) is live and byte-identical across 10 runs and seed-sensitive; a 2-sender ordering workload (netsched) is identical across 6 runs — both single-host, multi-process, in one container (net_e2e::windowed_multihost_pingpong_is_live_and_deterministic).
• Precondition: lookahead (the network’s minimum latency L_min) must be ≥ the window width. With L_min < W a blocking receiver’s reactivation bound stalls its own delivery (the L=0 deadlock); the orchestrator warns but does not abort. Reliable (--net "") and exponential latency have L_min = 0, so windowed request/reply needs latency=fixed:N or uniform:LO-HI with LO ≥ W.
• Validated: the 7-node Chord case study (examples/chord/chord_node.c, 6 members + observer), which drains its socket with recvfrom(MSG_DONTWAIT) and paces itself with virtualized usleep, is deterministic under --window 1000 --net latency=uniform:1000-60000 --record: across 6 runs the chord-check verdict is identical (same exit code, same verdict body) and every node receives a byte-identical message stream. This closes the §4.2 “polling-loop nondeterminism” the design flagged: a non-blocking recvfrom now advances the connection’s frontier and returns only messages sealed below the guest’s virtual time (EAGAIN once the pop-horizon reaches it), so the visible message set is a pure function of virtual time rather than of how far windows have sealed in real time. (chord-check’s human-readable node listing still prints in HashMap order, so the unsorted render text varies run to run — cosmetic to that tool, not a determinism defect; the verdict and its sorted body are stable.)
• Failure modes (design §8), implemented and tested: F1 a node killed by a signal mid-window discards the run (exit 3); F3 --watchdog <SECS> aborts-and-discards on real-time no-progress (its firing is inherently nondeterministic, so it only ever discards); F4/F5 a rejected sequencer op (non-monotone clock, late op, reconnect splice) is latched as a protocol violation and the run is discarded even if every node then exits 0; F6 terminal quiescence (every connected guest blocked, nothing in flight) is detected deterministically and discards instead of hanging. Sealing also waits for a join barrier (all --nodes ids said Hello) so node startup order — OS scheduling — cannot race the horizon past a late joiner.
• Validated across containers: the same 7-node Chord scenario split over two Docker containers on a bridge network (--listen/--broker/--spawn, nodes 0–2 with the broker on one, 3–6 on the other) produced the byte-identical chord-check verdict as the single-host windowed run (same sorted-verdict hash, 8/8 two-container runs vs 6/6 single-host) — the topology does not leak into the result. Measured max clock skew ~2.0 ms (--stats). Killing the remote container mid-run discards the run (exit 3) via the goodbye protocol: a windowed connection that ends without the shim’s clean Goodbye (sent on close(2) and via atexit, both skipped by signal death) is latched as a crash, F1.
• Recording determinism boundary: in a windowed recording the send sequence (the sealed linearization every delivery derives from) is identical across same-seed runs modulo broker connection ids, which are accept-order aliases — a node’s stable identity is its address (net_e2e::windowed_recording_send_order_is_identical_across_runs). Whole-log byte identity across runs is NOT guaranteed: setup ops (hello/bind) and recv events are written in lock-arrival order, which is real time. Wait mechanics are excluded from the log (a blocking poll’s empties and a non-blocking poll’s shim-internal retries are not recorded; only the final, target-visible EAGAIN is). Every individual recording still replays byte-exactly, forever.
• Validated on a second protocol: Raft leader election (examples/raft/raft_node.c, 5 members + observer, crash-restarts under test) under --window 1000 --net latency=uniform:2000-10000. Same-seed verdicts are identical across 6 single-host runs and across 5 two-container runs with distinct --host-ids — the two-container hash equals the single-host hash, so neither topology nor host labeling leaks into the result. Windowed mode also finds the votedFor-persistence bug: a 60-seed sweep hit 1 ElectionSafety violation (seed 44, RAFT_FIX=0), the violation’s semantic content (term, leader pair, report/restart counts) is identical across 6 re-runs, and the same seed is clean under RAFT_FIX=1. One caveat: raft-check cites the violation as “at op N”, a raw log position — positions count arrival-ordered non-send entries, so N varies by ±1 across runs (the recording boundary above); it is exact within any one recording.
• F2 (per-host frontier lag) and F7 (per-window buffer bound) are implemented: --stats on a windowed run reports each node’s maximum observed frontier lag behind the pack (sampled in real time, so indicative), and --window-ops N discards the run (exit 3) if one node buffers more than N sends inside a single window. Real per-host ids flow from --host-id through the shim’s Hello into the windowed sort key’s second tier.
• Not done: remote spawning (the design’s hostd) — each host runs its own weft run --listen/--broker by hand or CI. A guest that exits via _exit()/abort() skips atexit and is indistinguishable from a crash: its windowed run is discarded, which is the conservative direction.

4. Shrinking: algorithm and worst case

The shrinker is delta debugging (ddmin) over op inputs, with a truncate-after-violation pre-pass, parallel candidate evaluation (lowest-index success adopted, so results are deterministic), a 1-minimal single-op-removal fixpoint, payload truncation, and connect GC.

• Worst case is O(n²) candidate executions (standard ddmin bound) when the violation depends on ops spread across the whole log, defeating chunk removal so reduction happens one op at a time. Each candidate execution is a full re-run of the decision core over the candidate subsequence.
• Measured behavior at ~14k ops: 82–634 executions per violation, totaling ~5–40 ms per violation on commodity hardware — each candidate execution itself is well under a millisecond (docs/SCALABILITY.md §E). The bound is quadratic; observed behavior is far better because violations are local.
• 1-minimality, not global minimality. ddmin guarantees no single op can be removed — it does not guarantee the smallest possible reproducer. Ground-truth tests (crates/weft-fuzz/tests/shrink_ground_truth.rs) pin exact minima for known cases, but a pathological violation could shrink to a locally-minimal but not globally-minimal subsequence.
• The shrinker never reorders ops and never varies seed or net spec — by design (changing them reproduces a different run). A reproducer is therefore always an interpretable subsequence of the original run, and never smaller than what subsequence-removal can reach.

5. Dynamic testing itself (what Phase 7 taught us)

• Detection is bounded by message latency. A checker cannot observe a fault faster than the notification travels. In the Chord study this left a quantified residual: 8 of 452 valid seeds (1.8%) violated under full liveness discipline, every one traced to a node adopting a pointer that was dead before the DEAD notice arrived. This is not a harness bug — it is what testing against a realistic network means — but it is a real blind spot relative to formal models that assume perfect failure detection (docs/case-study/LEVEL_2_RESULTS.md).
• Absence of violations is not proof. 300 clean Raft seeds falsify the specific buggy mechanism under the tested schedule distribution; they do not verify Raft. Schedule-sensitivity was measured directly: the same bug showed 0/100 under loose election timeouts and 4/100 under adversarially tight ones (docs/case-study/RAFT_VALIDATION.md).
• Guest-side timing is unmeasurable. Clocks inside the target are virtual, so per-operation latency percentiles cannot be collected in-process; only wall-clock from outside. Broker-side histograms are a recommended, unimplemented optimization (docs/SCALABILITY_RECOMMENDATIONS.md).

6. Performance boundaries (measured, docs/SCALABILITY.md)

• Broker path: ~125 µs per datagram vs ~0.4 µs native loopback (~300×). Predictable, but a high-throughput target will run much slower simulated.
• Shim overhead ~70% on a CPU-bound syscall-heavy microbenchmark; sleep-driven programs run faster than real time (sleeps are virtual).
• Recordings grow linearly: ~0.65 MB per Chord seed at 45 ticks; a 5000-seed recorded campaign is ~3.2 GB. No log rotation or compaction exists.
• Broker memory is flat (~2.3 MB RSS at 7–14 nodes, the only scale tested). Nothing in this range suggests a scaling wall, but it has not been tested beyond 14 nodes — treat “scales to tens of nodes” as a hypothesis this data is consistent with, not a measured ceiling.

7. Interface stability

Pre-1.0. The scenario DSL, the weft-log format, and the CLI have independent compatibility policies defined in VERSIONING.md; until 1.0, breaking changes can occur in any of them with a changelog entry but no deprecation cycle.

Scalability Measurements

Performance characteristics of Weft DST framework under increasing workload: shim overhead, broker latency, node scaling, recording size, and shrinking efficiency.

A. Shim Overhead (Synthesis Examples)

Runtime overhead of libweft_shim.so relative to native execution (best of 5 runs, wall time):

Interpretation:

• chrono: Not an artifact — chrono spends ~2.8s in real sleep/nanosleep/usleep calls natively. Under the shim, time is virtual: sleeps advance the simulated clock and return immediately, so the whole program finishes in 3ms. This row measures time acceleration (a core DST feature — sleep-heavy tests run ~1000× faster), not overhead.
• montecarlo: ~70% overhead for CPU-bound simulation under the shim (LD_PRELOAD interception on its syscalls).
• entropy: ~100% overhead, but on a 1ms baseline — dominated by shim initialization, not steady-state cost.

Observation: For CPU-bound workloads, shim overhead is moderate (~70% on montecarlo). For sleep- or timer-driven workloads (most distributed protocols), virtual time makes simulated runs dramatically faster than real time.

B. Broker Datagram RTT (Median Latency)

Round-trip time for 5000 paired send-recv operations (10,000 broker ops total):

Mean (Weft): 125 µs/datagram
Variance: 112–138 µs (±10%)

Interpretation:

• Native loopback: 0.4 µs/op (kernel UDP stack, no LD_PRELOAD overhead).
• Weft broker: 125 µs/op = ~300× slower than native loopback.
• This is expected: shim intercepts every syscall, marshals to broker, waits for response, and descheduled guest thread.

Limitation: Per-operation latency percentiles (p50, p99) cannot be measured in-guest; guest clocks are virtual (seeded, not wall-clock). Broker-side instrumentation is recommended (Phase 8 optimization).

C. Node Scaling + Broker Memory

Chord workload, 1 seed, 45 ticks, latency=uniform:1000-8000 (measured with GNU time; the first run of this section silently failed because /usr/bin/time is absent from the rust:1.84-bookworm image — the bench script now installs it):

Interpretation: Broker memory is flat (~2.3 MB) from 7 to 14 nodes — the broker holds only in-flight messages and per-node queues, not history (records stream to the gzip log). Wall time is dominated by fixed startup cost at this scale; log size grows with message volume (~1.4× from 7→14 nodes). Nothing here suggests a scaling wall below tens of nodes; the practical ceiling is per-node process overhead on the host, not the broker.

D. Recording Size vs. Run Length

Deterministic Chord workload (7 nodes, 1 seed, varying simulation ticks):

Linear Scaling: Log size grows roughly linearly with simulation ticks (3× ticks ≈ 6× log size, accounting for compression variance).

Extrapolation to 5000-seed Campaign:

• Average log size per seed: ~0.65 MB (from Chord and Raft prior runs: 0.64 MB Chord, 0.47 MB Raft).
• 500-seed campaign: ~325 MB.
• 5000-seed campaign: ~3.25 GB.

Compression: Weft-log v1 uses gzip. Typical compression ratio ~1:8–1:10 for broker event streams (high repetition of message formats).

E. Shrinking Efficiency (Fuzz)

Delta-debugging on ~10k-event violation corpus (3 nodes, 3300 sends, 8 seeds, fifo+dup invariants, latency=uniform:0-8000ms, loss=2%):

Summary:

• Shrinking time: 80–600 executions per violation (highly variable, depends on structure).
• Reduction rate: 1:800× to 1:2000× (14043 → 7–17 ops).
• Total fuzz+shrink time: 132 ms (for 8 seeds, 6 distinct violations found).

Interpretation: Delta-debugging is effective; 10k-event fuzz takes ~16ms per seed on average. Shrinking is the expensive phase (multiple re-executions to verify minimality), but still completes in <1s per violation on modest hardware.

F. Live-Run Verdict Reproducibility

Chord protocol seed 0, 10 consecutive live runs (latency=uniform:1000-60000ms, network non-determinism):

Results:

• Violations: 1 (seed 0 reached violation in 1 of 10 runs)
• OK (clean runs): 8
• Discard (uninformative): 1

Interpretation: Cross-process message delivery order is re-rolled on each live execution. Same seed can reach different verdicts. Recording replay of any single run is byte-for-byte identical (Phase 5), but live-run campaigns are statistical, not deterministic. This is expected and irreducible without kernel-level scheduling determinism.

Summary: Practical Scalability

Conclusion

Weft is practical for 500–5000 seed campaigns on commodity hardware:

• Shim overhead is moderate and acceptable.
• Broker latency is high in absolute terms but predictable for deterministic replay.
• Recording size is manageable (GB per campaign, not TB).
• Shrinking is efficient (minimal repros in seconds).
• Live-run drift is expected and documented as a Phase 3 limitation.

Next optimization targets (Phase 8): See SCALABILITY_RECOMMENDATIONS.md.

Scalability Recommendations: Phase 8+ Optimizations

Five prioritized optimization opportunities to improve Weft DST performance and observability for large-scale campaigns (5000+ seeds, multi-day runs).

1. Broker-Side Latency Histograms (HIGH PRIORITY)

Problem: Per-operation latency percentiles cannot be measured in-guest (guest clocks are virtual, seeded, not wall-clock). SCALABILITY.md reports mean (125 µs/op) but not p50/p99/p99.9 distribution.

Solution: Instrument the broker to record wall-clock timestamp of every send/recv pair. Compute percentiles broker-side, serialize to a summary JSON (p50, p99, p99.9, max).

Impact:

• Enables analysis of network bottlenecks (e.g., “p99 latency is 500µs; we have a hot path”).
• Guides timeout tuning for protocol implementations (e.g., Raft election timeouts).
• No guest-side changes needed; purely broker instrumentation.

Effort: ~1–2 days (add timestamp fields to broker RPC, accumulate on each op, dump histogram on shutdown).

Trade-off: Minimal overhead (<1% broker CPU for histogram updates); small memory footprint (percentile sketch requires O(1) space).

2. Parallel Campaign Sharding (MEDIUM PRIORITY)

Problem: Weft fuzz runs seeds sequentially (1 broker per campaign). A 5000-seed campaign with 2-3 seeds per hour takes ~2000 hours wall-clock on 1 machine.

Solution: Spawn multiple broker instances, each running a subset of seeds (e.g., 5 brokers × 1000 seeds = 5000-seed campaign in parallel). Merge recorded logs and violation indices afterward.

Impact:

• 5–10× campaign speedup on multi-core systems (if brokers don’t contend for I/O).
• Enabled by recording determinism: each seed replayed independently; seeds don’t interact.

Effort: ~3–5 days (refactor campaign loop, add seed-range CLI args, implement merge logic for violation indices and logs).

Trade-off: Requires multiple machines or heavy CPU parallelism; disk I/O may become bottleneck (all brokers write to same log directory).

Mitigation: One log directory per broker, merge logs post-campaign.

3. Log Compaction for Long Campaigns (MEDIUM PRIORITY)

Problem: 5000-seed campaign produces ~3.25 GB of gzipped logs. Storing 10 campaigns for diff analysis → 32 GB disk. Archive strategies needed.

Solution: Implement log compaction: retain full logs for first 100 seeds (detailed diagnostics), then summarize subsequent seeds (one-line verdict summary: “seed 101 OK”, “seed 102 VIOLATION [3 ops]”).

Impact:

• Reduces long-campaign log storage by ~90% (retain detail, drop redundancy).
• Preserves ability to replay any seed for debugging (full logs of first 100 seeds).

Effort: ~2–3 days (add compaction logic to log writer, implement selective read on replay).

Trade-off: Cannot replay seed 101+ without re-executing; acceptable trade-off for long campaigns where violation discovery is primary goal.

4. Per-Node Clock Instrumentation (LOW PRIORITY, HIGH INSIGHT)

Problem: Individual nodes’ local clocks are seeded and deterministic but not wall-clock. Cannot measure per-node latencies (e.g., “how long does Chord stabilize() take on this node?”).

Solution: Have each node report wall-clock timestamps alongside seeded clocks. Broker reconciles reports via broker timestamp (provides precise wall-clock correlation).

Impact:

• Unlocks per-node performance analysis (latency profiles, hot paths in protocol logic).
• Enables detection of timing anomalies (e.g., one node’s stabilize() 10× slower than others).

Effort: ~3–5 days (add wall-clock reporting to node implementations, broker reconciliation, analysis tools).

Trade-off: Changes to example binaries (raft_node.c, chord_node.c); requires opt-in per protocol.

5. Fuzz Shrinking Parallelization (LOW PRIORITY)

Problem: Delta-debugging is sequential (tries one removal at a time, re-executes). For large violations (10k+ ops), shrinking can take minutes per violation.

Solution: Parallelize shrinking: try removing multiple independent op ranges in parallel, merge results.

Impact:

• Shrinking time reduction: 5–10× speedup possible on 8-core systems.
• Enables real-time shrinking feedback during long fuzz campaigns.

Effort: ~2–3 days (refactor weft-fuzz ddmin loop into work-stealing queue, ensure thread-safe violation index).

Trade-off: Complexity (concurrent shrinking must preserve minimality). May not be worth ROI unless violations are very large (>1k ops).

Implementation Roadmap

Conclusion

Phase 7 (current) has delivered deterministic simulation testing for protocol validation. The five recommendations enable:

1. Phase 8 (next): Broker observability + multi-seed parallelism → production-scale campaigns.
2. Phase 9+: Per-node diagnostics + advanced shrinking → deep performance analysis.

All recommendations are backwards compatible; can be implemented incrementally without breaking existing workflows.

Weft vs. Antithesis and TigerBeetle

The two most credible public reference points for deterministic simulation testing right now are Antithesis (hypervisor-level, commercial) and TigerBeetle’s VOPR (language-level, sim-first design). This document says plainly where Weft stands next to each, based on their public materials — what Weft does today, what it deliberately does not attempt, and when you should reach for one of them instead of Weft. It is an engineering comparison, not marketing: for several rows below, the other system’s choice is strictly stronger.

TL;DR table

vs. TigerBeetle’s VOPR

TigerBeetle owns the strongest guarantee on this list: because the database was designed against a simulated environment from the start — a single-threaded, statically-allocated core with its own event loop and storage abstraction — every line of production code runs under simulation, deterministically, including disk and scheduler behavior. Weft cannot match that depth. A raw syscall, or a lock the shim doesn’t model, escapes Weft’s simulation entirely (LIMITATIONS.md §2); TigerBeetle’s VOPR has no such escape hatch because there is no OS-level nondeterminism left in the loop to escape through.

What Weft offers that VOPR structurally cannot: sim-first is a decision you make on day one. TigerBeetle’s public writing is explicit that this was a founding constraint, and it only pays off because they controlled the whole codebase from the first commit. Weft exists for the other case — the C/C++/Rust/Go service you already have, that nobody is rewriting. If you are starting a new system where correctness is paramount (a database, a consensus layer) and you can afford to build it deterministic from scratch, VOPR’s approach is better than Weft’s and you should use it or its pattern, not retrofit Weft onto a system not yet written.

vs. Antithesis

Antithesis intercepts at the hypervisor, below the kernel, so nothing escapes: raw syscalls, Go runtimes, static binaries, multi-process timing — all deterministic, because the whole VM is the simulation. That is strictly stronger interception than Weft’s libc boundary, full stop. If your target does raw syscalls, is statically linked, or is written in Go (all undetected-nondeterminism cases for Weft — LIMITATIONS.md §1–2), Antithesis covers you and Weft does not.

The trades Weft makes against it: (1) open source vs. commercial service — Weft has no signup, no VM packaging step, no vendor relationship; (2) a per-process shim is weft run -- ./binary, versus packaging your system into a VM image; (3) Weft’s failing artifact is a megabyte-scale recording replayable in milliseconds on a laptop, not a VM snapshot; (4) Weft’s interception is at the libc boundary, so its fault vocabulary is stated in libc terms — “this fsync lies”, “this fd’s writes tear” — where hypervisor-level interception expresses faults at the device level. (Antithesis pairs its hypervisor with in-guest SDK assertions and instrumentation, so this is a contrast of interception layers, not of overall observability.) For the distributed-protocol logic bugs Phase 7 targeted (Chord’s ring invariant, Raft’s ElectionSafety), the libc surface proved sufficient to find both. If you need whole-system fidelity — kernel interaction, unsupported languages, static binaries — Antithesis is the correct tool and Weft will silently miss what it can’t see.

What Weft does today

• Deterministically replays unmodified dynamically-linked Linux binaries at the libc boundary: time, randomness, thread scheduling, UDP networking, a subset of file I/O faults.
• Turns any failure into a permanent, portable recording that replays byte-for-byte, including on macOS where the shim itself doesn’t build.
• Finds failures automatically (weft fuzz) and shrinks them to minimal reproducers.
• Has been checked against two protocols with independently, formally documented bugs (Chord/Zave 2012, Raft/Ongaro 2014) and reproduced both — see docs/case-study/CREDIBILITY_SUMMARY.md.

What Weft deliberately does not attempt

• True whole-VM / kernel-internal determinism. Even if the planned seccomp-unotify work (below, and ROADMAP.md item 6) closes the static-binary and Go gaps, it still intercepts at the syscall boundary within the same kernel — it will never give you Antithesis’s actual moat: deterministic kernel scheduling, block-device timing, and everything below the syscall layer. That requires a hypervisor, which is a different architecture Weft isn’t building. If you need that level of fidelity, use Antithesis; no amount of additional libc/syscall hooking gets Weft there.
• Sim-first, ground-up determinism. Weft is retrofit onto existing binaries on purpose. It will never be as complete as a system built against a simulated environment from its first commit — that is TigerBeetle’s territory.
• Proving correctness. 300 clean seeds falsify a specific mechanism under a specific schedule distribution; they are not a proof the system is correct. See LIMITATIONS.md §5 and the Raft study’s schedule-sensitivity discussion.

(Raw syscalls/static binaries/Go and TCP support are not on this list — they’re currently uncovered but actively planned; see ROADMAP.md items 3 and 6.)

The broader landscape

FoundationDB’s simulator is VOPR’s ancestor and shares its trade exactly: whole-system determinism, paid for with a from-scratch rewrite (Flow, single-threaded async) — the same “use it if you’re starting fresh” argument applies. Jepsen is the field’s referee in the opposite direction from all of the above: real clusters, real networks, external faults, a checker over observed histories, and no determinism — a Jepsen failure reproduces only statistically (its generators are seeded, but a seed does not determine cluster timing, so replaying one does not reproduce the failure). Weft’s faults are simulated (less real than Jepsen’s), but every failure is a replayable artifact; the two compose well — a Weft recording of a Jepsen-discovered bug class is the debugging story Jepsen deliberately doesn’t provide.

What is genuinely novel here

Not the idea of DST — FoundationDB proved it a decade ago. The specific combination:

1. Unmodified binaries at the libc boundary with a do-no-harm rule (a preloaded but unseeded shim is behaviorally invisible), rather than a language runtime or a hypervisor.
2. The recording as the unit of truth. The broker linearization is the only non-seed input, so seed + log replays exactly on any platform — including macOS, where the shim doesn’t even build. Campaign statistics live on Linux; debugging is portable.
3. Validation against published ground truth. The Chord and Raft studies (docs/case-study/) test the tool against protocol bugs with formal provenance (Zave 2012, Ongaro 2014) — including quantified negative results (the 1.8% detection-latency tail) rather than only success stories. The evidence design is a controlled A/B: identical seed sets with only the fix flag differing (Chord 57 → 41 → 8 across liveness levels; Raft 3/300 buggy vs 0/300 fixed), so the deltas isolate the protocol change, not the harness.

What a non-Linux port would require

Ordered by how much of the codebase each layer touches. The pure crates (weft-net core, weft-replay, weft-fuzz, weft-scenario) are already platform-independent — weft replay/weft fuzz pass their suites on macOS today. The port is entirely about the shim and process control.

macOS (the plausible one):

• LD_PRELOAD → DYLD_INSERT_LIBRARIES. Two hard walls: SIP strips dyld env vars from protected/system binaries (fine for user-built targets), and flat-namespace interposition needs DYLD_FORCE_FLAT_NAMESPACE or __DATA,__interpose sections — the latter is the robust path and means rewriting the hook-declaration layer (real! dlsym-next resolution → interpose pairs).
• libc surface: BSD libc + Mach. clock_gettime exists, but code commonly uses mach_absolute_time; getentropy exists, getrandom does not; /dev/urandom handling carries over. The pthread hook set carries over mostly intact; the scheduler’s token model is OS-agnostic by design (it models mutexes rather than wrapping them).
• Network: the broker protocol is a Unix socket + wire format, portable as-is; only the socket/bind/sendto/recvfrom hooks move.
• Estimate: the engine and models port cleanly; the interposition layer is a rewrite (~the size of hooks/ + real.rs). No new design work.

Windows (the expensive one): no preload mechanism; interception means Detours-style binary patching or a driver, the syscall surface (QueryPerformanceCounter, BCryptGenRandom, IOCP, SRW locks) shares nothing with the current hook set, and process orchestration (env inheritance, exec semantics) diverges everywhere. This is a new sibling implementation reusing only the pure crates — not a port.

The strategic alternative (also the static-binary/Go answer on Linux): seccomp-unotify syscall-boundary interception, sketched in docs/architecture.md. It trades per-call latency for coverage and would make the Linux story strictly stronger before any second OS is attempted. Given finite effort, that ranks above a macOS port: macOS is where developers write the code, but recording-exact replay already works there, which is the part of the loop developers actually run locally.

Versioning policy

Weft’s users depend on three surfaces that change at different rates: the scenario DSL, the event-log format (weft-log), and the CLI. Each has its own compatibility contract, defined here. The Rust crate APIs are a fourth, weaker surface. Crate versions follow SemVer; this document defines what “breaking” means for each surface, because SemVer alone doesn’t.

Current status: pre-1.0 (0.0.x). Until 1.0, breaking changes are allowed on any surface with (a) a CHANGELOG.md entry under Unreleased marked BREAKING, and (b) for the log format, a version-number bump (that rule is absolute even pre-1.0, see below). There is no deprecation cycle yet. From 1.0 on, the contracts below get the deprecation policy in the final section.

1. Event-log format (weft-log) — the strictest contract

A recording is a bug report that replays forever. People archive these files; a format change that orphans old recordings destroys exactly the value the tool exists to provide. So this surface is versioned explicitly and independently of everything else:

• The header carries "format":"weft-log","version":N. Any change to record semantics — new required fields, changed digest computation, changed meaning of an existing field, changed op numbering — increments N. This applies pre-1.0 too (docs/recording-format.md).
• Current version: 2. v2 added the per-send send_vt anchor (deliv = send_vt + latency) and the header window_ns field, groundwork for windowed multi-host recordings. v1 is rejected on read — its latency-only deliveries would silently diverge under the send-time-anchored core, so there is no in-place upgrade; re-record under the current tool. (Pre-1.0, and Weft was published only days earlier, so no long-lived archives are orphaned in practice.)
• Readers MUST reject unknown versions rather than guess. weft replay does; your tooling should too.
• Non-breaking: adding keys inside the header’s meta object (readers MUST ignore unknown meta keys; it is informational by definition), and gzip vs. plain encoding (detected by content).
• Breaking, requires version bump: everything else. In particular the digest chain: two weft-log files with equal digests MUST describe byte-identical executions across all Weft releases that can read that version.
• Aspiration for 1.0+: ship a weft log migrate tool or retain read support for at least one previous version. Not promised pre-1.0.

2. Scenario DSL — strict on reading, additive-friendly

A scenario file encodes institutional knowledge about how to break a system; teams check them into their repos and expect them to keep working.

• Non-breaking: adding a new optional field with a default that preserves old behavior; adding a new event type; adding a new latency distribution or net-spec clause; improving error messages.
• Breaking: removing or renaming a field; changing a default; making an optional field required; changing validation so a previously-valid file is rejected (tightening) or a previously-rejected file is accepted with different semantics; changing the meaning of an existing value (e.g. units of time_ns).
• Note the DSL deliberately has no version field today. Before 1.0 it will either gain one or the format freezes as-is; until then, breaking DSL changes are CHANGELOG-flagged and the parser’s “unknown field” strictness is the compatibility tripwire (a file using newer fields fails loudly on older Weft, never silently misbehaves).
• Removed surface is rejected by name where feasible: e.g. YAML input was never implemented and its vestigial API was removed pre-release rather than left as a JSON-parsing trap.

3. CLI — the everyday contract

Scripts and CI pipelines consume the CLI. “Breaking” here includes output that machines parse, not just flags:

• Breaking: removing/renaming a subcommand or flag; changing a flag’s default; changing any documented exit code (weft fuzz‘s 0/2/1 and the checkers’ 0/2/3/1 are load-bearing CI contracts); changing the format of machine-parsed output lines (replay identical: N op(s), stream digest %016x, the shrunk : X → Y ops report lines); changing env-var names or activation semantics (WEFT_* — presence-activated variables are especially sensitive).
• Non-breaking: adding subcommands, flags, or env vars; adding output lines; improving human-facing prose on stderr; adding new exit codes for new failure modes (never reusing 0/1/2/3 meanings).
• Seed semantics are part of the CLI contract in one narrow, important way: we do not promise that seed N produces the same schedule across Weft releases (engine improvements legitimately change the seed→schedule map); we DO promise a recording made by any release replays identically on every later release that reads its log version. Archive recordings, not seeds.

4. Rust crate APIs

weft-scenario, weft-replay, weft-chord, weft-raft expose small intentional APIs (see docs/REFERENCE.md §7) and follow standard Rust SemVer. Everything not listed there is implementation detail and may change in any release regardless of version number. weft-shim’s exported C symbols are an interposition surface, not an API — they mirror libc by construction and carry no compatibility promise of their own.

5. From 1.0 onward

• Breaking changes on any surface require a minor-version deprecation window (old form keeps working with a warning for ≥ 1 minor release) except where technically impossible (log-format semantics — handled by version rejection instead).
• The workspace releases in lockstep (one version number across crates), so “Weft 1.3” unambiguously names the behavior of every surface.
• CHANGELOG.md gains a per-surface compatibility table per release: DSL / log / CLI / crates, each marked unchanged · additive · breaking.

Roadmap

What’s actually planned, in rough priority order, and — just as important — what is explicitly not. Both halves are promises about scope, not just a wishlist. If something you need isn’t in either list, open an issue; it means we haven’t thought about it yet, not that it’s rejected.

Compatibility impact of anything here is governed by VERSIONING.md.

Near-term (next)

1. Broker-side latency histograms. Per-operation latency currently can’t be measured in-guest (clocks are virtual). Instrument the broker to timestamp every send/recv pair and emit p50/p99/p99.9 on shutdown. No guest-side changes. Details: docs/SCALABILITY_RECOMMENDATIONS.md §1.
2. Parallel campaign sharding. weft fuzz sweeps seeds sequentially through one broker; a 5000-seed campaign is currently a multi-hour single-machine run. Spawning N brokers over disjoint seed ranges and merging violation indices afterward is a 5–10× wall-time win with no correctness risk (seeds are independent by construction). Same doc, §2.
3. TCP support in the simulated network. Today the broker only diverts AF_INET/SOCK_DGRAM — this is about what targets may speak, distinct from the multi-host broker transport (which already runs over TCP). Most real services speak TCP; extending the wire protocol and fault model to stream sockets is the single biggest expansion of what Weft can test without touching the shim’s core determinism machinery.
4. weft hostd — remote spawning for multi-host runs. The windowed multi-host layer is implemented and validated (deterministic Chord and Raft across containers — LIMITATIONS.md §3(c′)), but each host runs its own weft run --listen/--broker/--spawn by hand. The design’s host agent (docs/MULTI_HOST_ARCHITECTURE.md “Components”) — one weft hostd per host receiving spawn specs over a control channel, master-side --hosts A:PORT,B:PORT — turns that into one command. Prerequisites (real per-host ids, goodbye/crash detection) have landed.
5. ENOSPC fault injection. WEFT_ENOSPC_BYTES is reserved in the ABI and referenced in the file-fault hook but not wired up (LIMITATIONS.md §2). Byte-tracking already exists; this is finishing what fsync-lies started.
6. Fold live-target fuzzing into weft fuzz. The fuzzer currently sweeps the broker’s pure decision core; sweeping real weft run --record clusters (the shim path) is done by hand today (scripts/*-campaign.sh). Unifying these gives shim-path campaigns the same dedup-and-shrink treatment broker-core campaigns already have.

Medium-term

7. seccomp-unotify syscall-boundary interception. The single change that would close the largest gap in what Weft can see: static binaries and Go’s raw-syscall runtime currently escape interception entirely and silently (LIMITATIONS.md §1). A seccomp-notify supervisor answering from the same pure decision engine would cover both, at the cost of a context switch per intercepted call. Sketched in docs/architecture.md; not started.
8. Log compaction for long campaigns. 5000 recorded seeds is currently ~3.25 GB; retaining full detail for the first N seeds and summarizing the rest is a ~90% storage win for archived campaigns. docs/SCALABILITY_RECOMMENDATIONS.md §3.
9. Per-node clock instrumentation. Lets a protocol implementation report wall-clock timestamps the broker can reconcile, unlocking per-node performance analysis (e.g. “which node’s stabilize() is slow”) that guest-side virtual clocks can’t provide today. Same doc, §4.
10. Shrinking parallelization. The ddmin loop is sequential; for 10k+-op violations, parallel candidate removal is a further 5–10× on multi-core hardware. Same doc, §5.
11. macOS interception port. weft replay/weft fuzz already work on macOS (pure computation); weft run’s shim does not build there. Porting LD_PRELOAD → DYLD_INSERT_LIBRARIES interposition is scoped in docs/comparison.md as a rewrite of the hook-declaration layer, not new design work — but it ranks below item 7, since recording-exact replay already works on macOS and static/Go coverage on Linux is the bigger gap.
12. 1.0 and the deprecation-window policy. Once the scenario DSL, log format, and CLI surface are stable enough to commit to, VERSIONING.md §5’s minor-version deprecation window takes effect. No date attached; gated on real usage surfacing which parts of the surface are actually load-bearing.

Not planned

• Windows support. Not a port of the existing shim — no preload mechanism, no shared syscall surface, no shared process-orchestration model. Would be a new sibling implementation reusing only the platform-independent crates. Out of scope until there is a concrete reason to fund it as its own project.
• Whole-VM / hypervisor-level interception. That is a different, harder problem with a different, better answer already on the market — Antithesis. Weft’s bet is the libc boundary; going lower means abandoning “point it at a binary you already have,” which is the whole premise. See docs/comparison.md.
• A sim-first runtime you build against from day one. That is TigerBeetle’s and FoundationDB’s bet, and it is a better guarantee than Weft’s if you control the codebase from its first commit. Weft is deliberately the retrofit tool for the other case. Not a roadmap gap — a different product.
• Formal correctness proofs. Weft falsifies specific mechanisms under specific schedule distributions (see the Chord and Raft studies); it will never produce a proof of absence of bugs. If you need that, you want a model checker (TLA+, etc.), not a dynamic testing tool — the two compose, but Weft won’t grow into one.
• Byzantine fault injection (nodes lying or behaving adversarially, beyond fsync-lies and torn writes). The fault model targets realistic crash/omission/timing faults; adversarial-node simulation is a meaningfully different tool with different threat assumptions and isn’t on this roadmap.
• CPU-time clock virtualization (CLOCK_PROCESS_CPUTIME_ID etc.). These currently return virtual-monotonic time rather than modeled CPU consumption (LIMITATIONS.md §2); modeling real CPU accounting under a cooperative userspace scheduler is a different kind of simulator than Weft is trying to be.

Pre-launch review findings

Skeptical, adversarial pass over the entire public-facing surface of Weft, conducted 2026-07-11, as a technically-hostile stranger would read it. Every finding cites its file and quotes the offending text where relevant.

Disposition (2026-07-11, same day): all six BLOCKING findings and the SHOULD-FIX items 1.2–1.4, 2.2–2.5, 3.3–3.5, 4.2–4.6, 5.2–5.3 have been fixed in the tree; quoted “offending text” below therefore no longer matches the current files — this document is kept as the record of what the review found. 3.1 is resolved as documentation (per-level semantics table + transcription caveat in LEVEL_2_RESULTS.md/chord-spec.md) rather than a code change; re-verifying update()’s semantics against the paper text and re-running the campaign remains open. 6.2 (repo security settings) requires access this session did not have.

Rankings: BLOCKING = must fix before any public launch. SHOULD-FIX = meaningfully improves credibility. MINOR = polish.

Methodology note: claims were verified against the actual code and, where possible, against artifacts on disk (campaign verdict files, CI workflow, test sources) — not just against what other documents say. Two checks are flagged inline as requiring access this review did not have: the primary-source paper text (3.1) and repo security settings (6.2).

1. Overclaiming

1.1 BLOCKING — README implies weft fuzz fuzzes your binary. It does not. README.md opening paragraph: “Point it at a compiled Linux binary … a failing seed becomes a permanent, portable bug report. weft fuzz finds those seeds automatically and shrinks each one…”. In context, “those seeds” are seeds that break your program. But docs/fuzzing.md (Scope): “Fuzzing live target programs (the LD_PRELOAD shim path) … is future work,” and ROADMAP.md item 5 confirms live-target fuzzing is manual today (scripts/*-campaign.sh). weft fuzz sweeps the broker’s internal decision core against a built-in workload. This is the single most quotable overclaim on the page: the flagship pitch attributes to the fuzzer exactly the capability the fuzzing doc’s own Scope section disclaims.

1.2 SHOULD-FIX — “the smallest sequence of operations” overstates ddmin. Same README sentence: “…shrinks each one down to the smallest sequence of operations that still reproduces it.” LIMITATIONS.md §4 states the correct, weaker guarantee: “1-minimality, not global minimality. ddmin guarantees no single op can be removed — it does not guarantee the smallest possible reproducer.” The README should say “a minimal” not “the smallest.”

1.3 SHOULD-FIX — “Proven 10× in CI on every platform” is false as phrased. LIMITATIONS.md §3(a): “Proven 10× in CI on every platform.” The 10× replay test is real (crates/weft-replay/tests/record_replay.rs, loop for run in 0..10), but .github/workflows/ci.yml runs every job on ubuntu-latest only. macOS replay verification happened manually during development, never in CI. Say “proven 10× in CI (Linux) and verified manually on macOS.”

1.4 SHOULD-FIX — the checker’s verdict message asserts more than the run observed. crates/weft-chord/src/bin/chord_check.rs prints, for any invariant violation: “verdict : VIOLATION — the ring is broken and cannot self-repair”. Two problems. (a) “Cannot self-repair” is inherited from Zave’s theorem (violations of the four “required for correctness” properties are unrepairable in her model); the run itself observes only “still broken after the 8-round quiescent tail” (examples/chord/chord_node.c, quiescent tail loop). The docs handle this honestly (docs/case-study/chord-spec.md attributes unrepairability to the papers), but the tool’s output states it as an observed fact. (b) The message says “the ring is broken” even when the fired invariant is OrderedRing (ring exists but is misordered) or ConnectedAppendages (ring intact, appendage stranded). See also 3.4.

1.5 MINOR — “forever” / “on any platform.” README.md: “Record a run and it replays byte-for-byte, forever, on any platform.” “Forever” is backed only by the weft-log versioning policy (readers reject unknown versions — VERSIONING.md §1), i.e. a promise, not a property; “any platform” means “any platform Rust supports,” tested on exactly two. Rhetoric a skeptic will poke; consider “on any platform Rust runs, for as long as the log format is supported.”

1.6 MINOR — PHASE_VERIFICATION.md claims a garbled root cause for the skipped cargo-fuzz target. docs/PHASE_VERIFICATION.md: “never delivered due to Fuzz compiler / rustc mismatch” — this phrase is word salad (likely meant: cargo-fuzz requires a nightly toolchain and the project pins stable). State the real reason or drop the clause.

2. The comparison document (docs/comparison.md)

2.1 BLOCKING — README’s framing contradicts the comparison doc and is unfair to Antithesis. README.md: “Weft is in the tradition of [FoundationDB’s simulator] and [Antithesis] — but general-purpose, retrofit onto binaries you already have rather than a runtime you build against from day one.” This lumps Antithesis into “a runtime you build against from day one.” The project’s own comparison table says the opposite (docs/comparison.md: “Target must be rewritten? … Antithesis: no”). Antithesis is general-purpose and runs unmodified software; the honest differentiators against it are open-source/self-hosted/no-VM-packaging, and the comparison doc gets this right. The README sentence is the one that will be screenshot-quoted, and it’s wrong. (Also present in drafts/outreach-draft.md: “no rewrite required, unlike FoundationDB-style or TigerBeetle-style sim-first frameworks” — that sentence is fine because it names only the two rewrite-required systems; the README names Antithesis.)

2.2 SHOULD-FIX — “a hypervisor sees only device-level state” undersells Antithesis’s actual product. docs/comparison.md (vs. Antithesis, trade 4): “at the libc boundary, Weft can be semantic … where a hypervisor sees only device-level state.” Antithesis’s public materials describe an SDK with in-guest semantic assertions (“sometimes assertions”, properties), a test composer, and guest-level instrumentation — the interception is hypervisor-level but the observability story is not device-level-only. As written this reads as dismissive of their tooling and will be corrected in public by people who use it. Reword to compare interception layers, not observability.

2.3 SHOULD-FIX — verify the TigerBeetle characterization against their current public docs before launch. docs/comparison.md: “its own event loop, its own storage abstraction, no OS threads.” TigerBeetle’s public writing describes a single-threaded control loop with static allocation, but the “no OS threads” absolute (I/O rings, etc.) is the kind of detail their community will fact-check. One sentence of hedging (“a single-threaded, statically-allocated core”) is safer and equally strong.

2.4 MINOR — Jepsen “no seed to hand a developer” is slightly overbroad. docs/comparison.md: “a Jepsen failure reproduces only statistically; there is no seed to hand a developer.” Jepsen’s generators are in fact seeded; the correct claim is that a seed doesn’t determine cluster timing, so replaying it doesn’t reproduce the failure. The conclusion stands; the mechanism as stated is imprecise.

2.5 MINOR — the doc undersells Phase 7’s strongest methodological point. The “What is genuinely novel here” section cites the validation and the 1.8% tail but never mentions the controlled A/B structure — identical seed sets, only the fix flag differing (57 vs 41 vs 8; Raft 3/300 vs 0/300) — which is the strongest evidence design in the project and the thing a skeptical reader would find most persuasive. One sentence would fix this.

3. The Chord rediscovery claim (load-bearing; verified against code)

What checks out — stated first because it’s most of the picture:

• The checker (crates/weft-chord/src/lib.rs) implements Zave’s Alloy definitions faithfully: bestSucc = first live entry of {succ, succ2} (matching the arXiv:1502.06461 wording quoted in chord-spec.md), ring membership via transitive closure of bestSucc, and all four correctness-critical predicates (AtLeastOneRing, AtMostOneRing, OrderedRing, ConnectedAppendages), with unit tests for each including a Figure-6-shaped case.
• The failure precondition (“a member never fails if its failure would leave another member with no live successor”) is enforced by discarding seeds, which is more honest than counting them.
• The “does not self-heal” observation is genuinely observed within a window: chord_node.c runs an 8-round quiescent maintenance tail after all faults stop, and the checker evaluates only the final state. Traced recordings (seed-0, seed-120) exist on disk with op-level mechanisms matching Zave’s Figure 6.
• The stabilize path at CHORD_FIX=0 adopts the successor’s reported predecessor with no liveness check — exactly the original 2001 flaw.

Now the problems:

3.1 BLOCKING — two project documents contradict each other about what the original protocol’s update does, and the headline number depends on it. docs/case-study/chord-spec.md (Operations, presented as transcribed from primary sources): “update(n): replace a dead succ with the first live entry in [succ, succ2]” — i.e., the original update has a liveness check. But examples/chord/chord_node.c gates that check behind level 2 (fix_level < 2 || is_live(succ2) — at levels 0 and 1, a dead succ2 is promoted), and docs/case-study/LEVEL_2_RESULTS.md asserts the opposite of chord-spec: “reconcile and update — which are equally unchecked in the original” / “equally faithful to the 2001 pseudocode.” One of these is wrong. If chord-spec’s transcription is right, then CHORD_FIX=0 is buggier than the protocol Zave analyzed, and some fraction of the 57/500 headline violations may arrive through a path the original protocol does not have. Mitigating context: the traced level-0 root cause (seed 17, stabilize adoption at op 855) is the genuine Figure-6 mechanism, and level 1 (still-unchecked update) vs level 0 isolates the stabilize fix — but the level-1→level-2 delta (41→8) bundles the reconcile, update, and GETSUCC checks together, so update’s contribution is not isolated anywhere. Resolve against the paper text (CCR 2012 Figure 9 / arXiv:1502.06461) before launch, and either fix the code/docs or publish the per-level semantics table explicitly. A reviewer with Zave’s paper open will find this in an afternoon.

3.2 BLOCKING — the citation file cites a paper that does not exist. CITATION.cff (references): title: "How to Not Prove Your Distributed Algorithm", attributed to Zave, 2012, SIGCOMM CCR. No such paper. The real CCR 2012 paper — correctly cited in docs/case-study/chord-spec.md — is “Using Lightweight Modeling to Understand Chord.” The same fabricated title appears in drafts/blog-chord-raft-case-study.md (“in 2012, Pamela Zave published ‘How to Not Prove Your Distributed Algorithm’”). A fabricated citation in CITATION.cff, on the project’s most load-bearing claim, is the single worst kind of credibility bug.

3.3 SHOULD-FIX — “unmodified C implementation” reads as third-party provenance; it is the project’s own harness. README.md: “Pointed at an unmodified C implementation of Chord (SIGCOMM 2001)…”; CHANGELOG.md: “an unmodified Chord (2001) implementation loses ring connectivity…”. chord_node.c was written by this project, for this experiment, from the papers, with the CHORD_FIX falsification switch built in. “Unmodified” here means “not instrumented for Weft” — true and worth saying — but a cold reader will parse it as “someone else’s existing Chord codebase,” and the correction (“they wrote both the bug and the bug-finder”) is the top HN reply as written. Say “our own minimal, uninstrumented implementation of the 2001 protocol (it knows nothing about Weft)” everywhere the claim appears. The case-study docs themselves are honest about this; the top-of-funnel docs are not.

3.4 SHOULD-FIX — the published counts lump two violation classes, and the prose is strictly wrong for 2 of the 57. The campaign counts exit-2 from chord-check, which fires on any of the four invariants (examples/chord/campaign.sh; chord_check.rs), while README says “57 of 500 seeded runs break the ring” and CHANGELOG says “loses ring connectivity.” This review ran the exhaustive tally over all 106 surviving verdict files (target/chord-out-*/seed-*.verdict):

So the headline is almost exactly right — but for 2 of the 57 (and 2 of the 41), the ring itself is intact and the violation is a permanently stranded appendage. Both classes are in Zave’s “required for correctness / unrepairable” set, so the substance survives; the phrasing “break the ring” does not, quite. Publish this table in LEVEL_2_RESULTS.md and adjust the README/CHANGELOG phrasing to “violate Chord’s ring-maintenance correctness invariants (55 broken rings + 2 stranded appendages)” or similar. This is exactly the kind of detail a referee finds, and finding it pre-published — with the table already in the docs — flips it from a gotcha into evidence of rigor.

3.5 SHOULD-FIX — the blog draft claims the tool found the bug “without knowing the proof in advance.” It knew. drafts/blog-chord-raft-case- study.md: “can a dynamic tool find it without knowing the proof in advance?” and “no protocol-specific instrumentation beyond ‘print your state each tick’”. The harness was built from the proof: chord-spec.md transcribes Zave’s invariants verbatim, the checker encodes them, and the scenario shape (3-node stable base = r+1, appendage join/fail pattern) was chosen from her anomaly’s preconditions (campaign.sh comments say so). What’s honestly true — and still impressive — is that the runtime search found seeds exhibiting the anomaly without being pointed at a specific schedule. The draft as written will be called out. (Draft is unpublished; fix before it ships.)

4. Internal inconsistency

4.1 BLOCKING — every repository URL in the project points to a GitHub org/repo that does not exist. Cargo.toml (repository = "https://github.com/weft-dst/weft"), README.md quickstart (git clone https://github.com/weft-dst/weft), docs/USER_GUIDE.md quickstart, CITATION.cff (repository-code), .github/ISSUE_TEMPLATE/config.yml (security-advisory URL), drafts/blog… and drafts/outreach-draft.md links. Verified: gh repo view weft-dst/weft → “Could not resolve to a Repository.” The actual remote is github.com/arnavsinghal09/weft (where the five good-first-issues were filed). A new user’s literal first command fails. Either create/transfer to the weft-dst org before launch or update every URL.

4.2 SHOULD-FIX — PHASE_VERIFICATION.md describes the Phase-2 race with the wrong mechanism. docs/PHASE_VERIFICATION.md: “Race control achieved via network latency tuning (uniform:0-1 triggers the race; higher latencies avoid it).” Wrong subsystem: race_bank.c uses no network at all; the race is controlled by the scheduler seed (--strategy random, seed 3 triggers / seed 2 avoids — docs/scheduling-model.md, pinned by crates/weft-dst/tests/sched_e2e.rs). The fact being verified is true and was later verified empirically in a clean container; the stated mechanism is not.

4.3 SHOULD-FIX — PROJECT_NOTES.md’s directory layout is stale and contradicts the real crate map. PROJECT_NOTES.md still says “Only crates/weft-dst exists today” and lists planned crates weft-sched, weft-faults, weft-harness that were never created (the scheduler lives in weft-shim, faults in weft-net/weft-scenario, the harness role in weft-chord/weft-raft). The Phase-status section of the same file is current; the layout section two screens up is from Phase 0. A contributor sent here by CONTRIBUTING.md gets a wrong map.

4.4 MINOR — checker exit-code documentation disagrees with itself. chord_check.rs‘s own header comment lists exit codes “0 / 2 / 1” but the code returns 3 for assumption-violated discards. docs/REFERENCE.md §1.4 glosses exit 3 for both checkers as “DISCARD (seed exercised nothing — uninformative),” which is right for raft-check (no leader elected) but wrong for chord-check (3 = the scenario broke the papers’ failure precondition — a different, stronger statement).

4.5 MINOR — Invariantt (double-t) type name. crates/weft-chord/src/lib.rs pub enum Invariantt — presumably to avoid clashing with the Invariant trait, but it reads as a typo in a crate the docs hold up as “the template for writing your own checker.”

4.6 MINOR — USER_GUIDE’s one-line invariant definition conflates two of Zave’s predicates. docs/USER_GUIDE.md (case study, step 2): “At least one ring: from any live node, following successor pointers must reach a cycle containing all live nodes.” That is (roughly) the whole OneOrderedRing conjunction; Zave’s AtLeastOneRing is only “some cycle exists.” The checker implements the four predicates separately and correctly; the guide’s summary sentence does not match the named invariant.

5. Quickstart integrity

5.1 BLOCKING — step 1 of both quickstarts fails. git clone https://github.com/weft-dst/weft (README quickstart and docs/USER_GUIDE.md) — repository does not exist (see 4.1).

5.2 SHOULD-FIX — README’s demo uses a binary it never builds. The “See it work” console block compiles chrono (cc -O2 -o /tmp/chrono examples/chrono.c) then runs weft run --seed 3 -- /tmp/race_bank 2 2 with no cc line for race_bank (it needs -lpthread, too). A user pasting the block verbatim gets “No such file or directory” at the demo’s punchline.

5.3 SHOULD-FIX — the Install section assumes a clone it never instructs. README.md Install: “cargo install --path crates/weft-dst” — a --path install only works inside a checkout, but the Install section contains no clone step (the clone lives in the earlier demo section, which a user skimming to “Install” will skip). Also unstated: a C compiler is required for every example in the demo, and weft run in the demo is invoked bare (assumes ~/.cargo/bin on PATH and the shim copied next to the binary — the shim-copy instruction appears only after the demo).

5.4 MINOR — demo output will not match what users see. The chrono lines in “See it work” were captured from a real container run (good), but the wall-clock-formatted fields (20:48:42 etc.) don’t appear; the shown line (total virtual elapsed: 2800026 us, c11 time 962138923) is stable across machines only because time is virtual. Worth a comment in the block that byte-identical output is the expected result on any machine, since that’s the point being demonstrated.

6. Security and supply-chain honesty

6.1 BLOCKING — the security contact is an unexplained third-party email. SECURITY.md: “email atharvagandhi2005@gmail.com” (also the contact in CODE_OF_CONDUCT.md). The repo’s sole committer is Arnav Singhal (arnavsinghal06@gmail.com); the GitHub account is arnavsinghal09. Whoever atharvagandhi2005 is, a vulnerability reporter has no way to know this address is monitored, and the mismatch with the maintainer identity looks like an unedited template or a copy from another project. A security process is only real if the mailbox is.

6.2 SHOULD-FIX — “GitHub private vulnerability reporting” is instructed but not verifiably enabled. SECURITY.md’s preferred channel requires the repo setting to be turned on (Settings → Security → Private vulnerability reporting). (Unresolved in this review: repo-settings access.) The issue-template’s fallback advisory URL points at the nonexistent weft-dst/weft (4.1), so today both documented reporting channels are broken-or-unverifiable.

6.3 SHOULD-FIX — SBOM freshness is not enforced; the release notes imply more than CI checks. CHANGELOG.md: “SBOM for the release … 34 packages, all permissive, cargo deny check fully green.” CI (ci.yml) runs cargo-deny (advisories + licenses/bans/sources) on every push — that claim is real. But the SBOM files in sbom/ were generated manually on 2026-07-09 and nothing regenerates or validates them when Cargo.lock changes; they are already one dependency-churn away from silently misdescribing the tree. docs/RELEASE.md is honest about generation but should list “regenerate SBOM” as a release step, or CI should diff it.

6.4 MINOR — LIMITATIONS.md handles the Phase-2 safety boundary honestly (no finding, recorded as verified). The serialized-races gap (“Data races are serialized, not detected… run with WEFT_SCHED=0 under TSan”) is stated in both docs/scheduling-model.md and LIMITATIONS.md §3(b)3, and the TSan positive/negative controls exist in scripts/verify-phases.sh. Checked because the review brief specifically asked; nothing is being downplayed here.

7. Tone

7.1 SHOULD-FIX — the checker’s “cannot self-repair” (1.4) and the blog draft’s “without knowing the proof in advance” (3.5) are the two places tone crosses from confident into unsupported. Both already itemized.

7.2 MINOR — “← fires. every time.” / “← avoided. every time.” (README.md demo comments). Backed by 20/20 pinned runs (sched_e2e.rs), so it survives scrutiny — but “every time” invites a pedant to run it 21 times; “deterministic — seed’s choice, not luck” says the same thing unfalsifiably.

7.3 MINOR — CHANGELOG’s framing sentence. “This release is the culmination of building that stack…” is mild, but “culmination” + unreleased-0.0.1 reads slightly grand; the facts that follow carry the paragraph without it.

7.4 Positive note (no finding): LIMITATIONS.md, docs/case-study/ LEVEL_2_RESULTS.md (the falsification-statement structure), and docs/case-study/chord-spec.md’s “Honesty note” are the strongest-toned documents in the project — precise, quantified, and self-critical. The review found nothing in them to flag beyond 1.3 and 3.1; the rest of the public surface should be brought down to their temperature.

Summary counts

One check left unresolved by this review (access limits, not effort): whether GitHub private vulnerability reporting is enabled on the actual repo (6.2). The per-invariant verdict tally (3.4) was completed exhaustively during the review: 102 of 106 surviving hits are AtLeastOneRing, 4 are ConnectedAppendages, none are OrderedRing or AtMostOneRing — see the table in 3.4.

Development

A complete path from clone to first change. If you only need the ground rules (quality gates, PR expectations), see CONTRIBUTING.md — this document is the longer, walk-through version for a first-time contributor.

1. Clone and orient

git clone https://github.com/arnavsinghal09/weft && cd weft

Read in this order before writing code: README.md (what this is), docs/architecture.md (how the pieces fit), LIMITATIONS.md (where the guarantees stop — most “is this a bug?” questions are answered here). PROJECT_NOTES.md has design decisions already made; don’t reopen them in a PR.

2. Build

cargo build --workspace

Stable Rust, MSRV 1.84 (rust-version in the root Cargo.toml). You’ll also want a C compiler (cc) — the example targets under examples/ are C, used as deterministic-behavior proofs and as fuzzer/scheduler test subjects.

Platform split: the CLI, weft replay, weft fuzz, and every pure crate (weft-net core, weft-scenario, weft-replay, weft-fuzz, weft-chord, weft-raft) build and test natively on macOS. weft-shim (the LD_PRELOAD interception cdylib) and anything that loads it are Linux-only. If you’re on macOS, use the container wrapper — it runs exactly what CI runs:

scripts/linux-test.sh                 # full workspace test suite, Linux container
scripts/linux-test.sh -p weft-shim    # args pass through to `cargo test`

3. Run the test suite

cargo test --workspace          # macOS: pure crates + CLI
scripts/linux-test.sh           # macOS: everything, in Docker

On native Linux, cargo test --workspace covers everything above. Every guarantee has a test that would fail without it — see “Testing philosophy” in CONTRIBUTING.md for what pins what.

4. Sanitizers and the fuzz targets

These are part of what “the test suite passes” means for shim-adjacent code, and are not run by plain cargo test. The exact, current commands (also in scripts/verify-phases.sh, which runs all of this plus the full phase-by-phase reverification):

# ASan + UBSan: native and under the shim (determinism must not corrupt memory)
cc -O1 -g -fsanitize=address,undefined -fno-omit-frame-pointer \
   -o /tmp/entropy.asan examples/entropy.c -lpthread
/tmp/entropy.asan                                    # native: must be clean
ASAN_OPTIONS=verify_asan_link_order=0 \
  target/release/weft run --seed 42 --shim target/release/libweft_shim.so \
  -- /tmp/entropy.asan                                # under the shim: must be clean

# TSan positive control: the scheduler SERIALIZES threads, so run natively
# (WEFT_SCHED=0/--no-sched) to confirm TSan can still see the deliberate race
cc -O1 -g -fsanitize=thread -o /tmp/race_bank.tsan examples/race_bank.c -lpthread
/tmp/race_bank.tsan 4 25   # must report a race (this IS the point of the example)

# TSan negative control: a correctly-synchronized program must stay clean
cc -O1 -g -fsanitize=thread -o /tmp/prodcons.tsan examples/prodcons.c -lpthread
/tmp/prodcons.tsan         # must be clean

The fuzz targets (weft fuzz, not a cargo fuzz target — see LIMITATIONS.md §2 for why cargo-fuzz was replaced with a deterministic sweep):

target/release/weft fuzz --config examples/fuzz/ci.json     # expect exit 0 (property holds)
target/release/weft fuzz --config examples/fuzz/demo.json   # expect exit 2 (violations, by design)

ci.json is a property test (reliable network, FIFO/no-dup must hold for every seed) — any violation there is a genuine regression. crates/weft-scenario/tests/parser_robustness.rs is the deterministic stand-in for a coverage-guided fuzzer: 10,000 seeded mutations of a valid scenario file must never panic the parser. Run it with the rest of the suite; it finishes in well under a second.

For the full picture — every phase’s claims re-verified end to end, including the case-study checkers — run scripts/verify-phases.sh inside the Linux container (see the script header for the exact docker run invocation).

5. Use the graphify workflow yourself

This repo is graphify-instrumented: a knowledge graph over the whole codebase, kept fresh per session. Before making a non-trivial change, load context the way prior sessions did:

graphify . --update --no-viz
cat graphify-out/GRAPH_REPORT.md

No LLM API key configured? Use the heuristic fallback instead (note the different argument order, and no --no-viz flag):

graphify update .
cat graphify-out/GRAPH_REPORT.md

While working, query it instead of grepping blind:

graphify query "how does the scheduler pick the next thread?"
graphify explain "Core"                    # what is weft_net::core::Core
graphify path "weft run" "broker"          # how are two concepts connected

When you’re done, refresh it — this is expected as part of finishing a change, the same way updating CHANGELOG.md is:

graphify . --update --no-viz

If GRAPH_REPORT.md looks noisy after your change (build artifacts, lockfiles showing up as nodes), fix .graphifyignore rather than working around a broken graph. graphify-out/ is gitignored and regenerated per machine — don’t commit it.

6. Make a first change

Good starting points, roughly in order of how self-contained they are:

• A “good first issue” — see the repo’s issue tracker; each one is scoped and includes enough context to start without asking.
• Add a replay invariant. Implement the Invariant trait in crates/weft-replay/src/invariant.rs (see fifo/dup for the shape), register it in replay_cmd::build_invariants, and add it to the fuzz config’s invariant enum. Small, self-contained, exercises the whole record→replay→fuzz pipeline.
• Add an example target. A single C file under examples/ that prints observable state to stdout and is deterministic-modulo-the-bug it demonstrates (see race_bank.c for the shape: a real bug, controllable by seed). Good for learning the scheduler/network model by exercising it.
• Write a protocol checker. Copy crates/weft-raft (~150 lines): parse your protocol’s state-report datagrams out of a weft_replay::Log, fold them into a verdict, exit 0/2/3/1. The template for testing your own system under Weft.

Before opening a PR, run the quality gates from CONTRIBUTING.md:

cargo fmt --all --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace
cargo deny check          # advisories + licenses + bans + sources

cargo deny needs cargo install cargo-deny once.

Where things live

Full layout in CONTRIBUTING.md. The one-line version: crates/weft-shim is the interception cdylib (unsafe lives here, every block needs a // SAFETY: comment); crates/weft-dst is the weft CLI; everything else (weft-net, weft-scenario, weft-replay, weft-fuzz) is pure, platform-independent, and unit-testable without Linux.

Contributing to Weft

Thanks for your interest. This guide assumes you have never seen this codebase before and gets you from clone to a merged PR.

Orientation (read in this order)

1. README.md — what Weft is and the 5-minute quickstart.
2. docs/architecture.md — how the pieces fit, before you open any code.
3. LIMITATIONS.md — where the guarantees stop. Most “is this a bug?” questions are answered here.
4. The subsystem doc for whatever you’re touching: docs/{scheduling,network,fault,logical-time}-model.md, docs/recording-format.md, docs/fuzzing.md.

Historical phase reports live in docs/history/; design notes and decisions already made (language, crate naming, shim constraints) are in PROJECT_NOTES.md — please don’t reopen decided questions in a PR; open a discussion issue instead.

Repo layout

crates/
  weft-dst/       the `weft` CLI (run / replay / fuzz) + orchestrator
  weft-shim/      LD_PRELOAD cdylib: hooks + engine + scheduler  [unsafe lives here]
  weft-abi/       env-var names, seed expansion, domain ids (shim-safe, tiny)
  weft-net/       broker + pure decision core + fault model + wire protocol
  weft-scenario/  scenario DSL (JSON) parsing + validation
  weft-replay/    weft-log recording, replay verification, invariants
  weft-fuzz/      seed sweeping + ddmin shrinker
  weft-chord/     case study: Chord ring-invariant checker + trace tool
  weft-raft/      case study: Raft ElectionSafety checker
examples/         C targets (chrono, race_bank, pingpong, chord/, raft/, …)
examples/fuzz/    fuzz configs (ci.json = CI property test, demo.json = demo)
examples/scenarios/  runnable scenario DSL files
scripts/          linux-test.sh, campaign + bench + verification scripts
docs/             architecture, models, reference, user guide, case studies

Development setup

Stable Rust (MSRV 1.84 — see rust-version in Cargo.toml) and a C compiler for the example targets.

cargo build --workspace
cargo test --workspace

On macOS: the CLI, replay, fuzz, and all pure crates build and test natively. Everything involving the shim (LD_PRELOAD, scheduler e2e, broker e2e) is Linux-only. Use the container wrapper — it is exactly what CI runs:

scripts/linux-test.sh              # full workspace suite in rust:1.84-bookworm
scripts/linux-test.sh -p weft-shim # extra args pass through to cargo test

Quality gates (CI blocks on all of these)

cargo fmt --all --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace
cargo deny check          # advisories + licenses + bans + sources

cargo deny needs cargo install cargo-deny once. New dependencies must be permissively licensed (see the allow-list and rationale in deny.toml; copyleft is excluded because the shim loads into arbitrary user processes) — and think twice: weft-shim/weft-abi deliberately keep a near-zero dependency tree.

House rules the linters can’t fully enforce:

• Determinism is the product. Anything that lets wall-clock time, host hash-map iteration order, or OS thread timing leak into scheduling, replay output, or recorded bytes is a bug even if every test passes. New sources of randomness must come from a seeded domain stream (see weft-abi::Domain).
• Unsafe code only where interposition requires it, and every unsafe block carries a // SAFETY: comment (clippy denies undocumented ones).
• Shim hooks must be allocation-free and reentrancy-safe on the hot path: no std::env::var per call, no stdio, no locks beyond the engine’s own. Look at crates/weft-shim/src/hooks/file.rs for the canonical shape.
• Error style: weft-scenario uses thiserror enums; weft-replay hand-rolls its error enums; internal plumbing (weft-net::config, weft-fuzz) returns Result<_, String> that surfaces directly in CLI output. Match the style of the crate you are editing; converting a crate wholesale is its own PR.
• New subsystems come with a short design note under docs/; user-visible changes get a line in CHANGELOG.md under Unreleased and, if they touch the CLI, DSL, or log format, a check against VERSIONING.md.

Recipes

Add an invariant checker for your protocol. Copy the weft-raft crate (~150 lines): parse your node’s state-report datagrams out of weft_replay::Log records, fold them into a Verdict, and exit 0 (holds) / 2 (violation) / 3 (uninformative) / 1 (unreadable). Have your target print RPT <fields> datagrams each tick, run campaigns with weft run --net … --record, and point your checker at the recordings.

Add a replay invariant (checked by weft replay --check and weft fuzz): implement the Invariant trait in crates/weft-replay/src/invariant.rs (see fifo / dup), register it in replay_cmd::build_invariants, and add it to the fuzz config enum.

Add a fault type. Network-level faults go in the pure decision core (weft-net/src/fault.rs — must remain a pure function of seed + message identity, or replay breaks). Syscall-level faults go in a shim hook (weft-shim/src/hooks/) behind a WEFT_* env var registered in weft-abi, plus a field in the scenario DSL with validation in weft-scenario/src/parse.rs.

Add an example target. A single C file in examples/ that prints its observable state to stdout; keep it deterministic-modulo-the-bug so a seed either triggers or avoids the behavior. Wire it into a test in crates/weft-dst/tests/ if it pins a guarantee.

Testing philosophy

Every guarantee has a test that would fail without it: determinism e2e (weft-dst/tests/e2e.rs), scheduler race pinning (sched_e2e.rs), replay byte-identity (weft-replay/tests/gzip.rs), shrinker ground truth (weft-fuzz/tests/shrink_ground_truth.rs — exact known minima must be recovered exactly), parser no-panic sweep (10,000 mutated inputs, weft-scenario/tests/parser_robustness.rs). If your PR adds a guarantee, add its test; if it relaxes one, say so loudly in the description.

Sanitizer runs (ASan/UBSan, TSan with --no-sched) are part of the phase verification suite: scripts/verify-phases.sh runs everything in the container.

Pull requests

• Keep PRs focused; unrelated refactors go in separate PRs.
• Commit messages explain why, not just what.
• CI (lint, audit, license, tests) must pass before review.
• Expect review feedback to focus heavily on determinism and safety in shim-adjacent code.
• For anything larger than a small fix, open an issue first.
• Security issues go through SECURITY.md, never the public tracker.

Licensing of contributions

Weft is dual-licensed MIT OR Apache-2.0. Unless you state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Code of conduct

Participation is governed by CODE_OF_CONDUCT.md.