09 local verification; date 2026-09-19; Go1.27.0 darwin/arm64 Verified boundary: finite in-memory protocol trajectories only; no real crash, storage sync, network or model checking. Parent independently executed from examples/distributed-systems: GOCACHE=/private/tmp/ds-go-cache go run ./paxos09 : exit0 go vet ./paxos09 : exit0, no diagnostics (parent tool observation). go run -race ./paxos09 : exit0, raw output below. FIRST ATTEMPT (child): go run examples/distributed-systems/paxos09/main.go; exit1, stdlib discovery error. Later source directories existed and parent run succeeded; no demonstrated root cause. examples/distributed-systems/paxos09/main.go:5:2: package errors is not in std (/opt/homebrew/Cellar/go/1.27.0/libexec/src/errors) examples/distributed-systems/paxos09/main.go:6:2: package flag is not in std (/opt/homebrew/Cellar/go/1.27.0/libexec/src/flag) examples/distributed-systems/paxos09/main.go:7:2: package fmt is not in std (/opt/homebrew/Cellar/go/1.27.0/libexec/src/fmt) examples/distributed-systems/paxos09/main.go:8:2: package os is not in std (/opt/homebrew/Cellar/go/1.27.0/libexec/src/os) examples/distributed-systems/paxos09/main.go:9:2: package sort is not in std (/opt/homebrew/Cellar/go/1.27.0/libexec/src/sort) package command-line-arguments: cannot find package PARENT NORMAL RUN FULL OUTPUT GUARDS prepare n=2 to=A ok=true promise=2 accepted={0 }/false prepare n=2 to=B ok=true promise=2 accepted={0 }/false issue n=2 value=X reports=2 wrongMin=false accept n=2 value=X to=A ok=true promise=2 accept n=2 value=X to=C ok=true promise=2 accept n=1 value=X to=C ok=false promise=2 PASS guards: distinct identities, matching ballots, quorum gates, accept raises promise SCENARIO max mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 prepare n=3 to=A ok=true promise=3 accepted={1 X}/true prepare n=3 to=C ok=true promise=3 accepted={2 Y}/true issue n=3 value=Y reports=2 wrongMin=false accept n=3 value=Y to=A ok=true promise=3 accept n=3 value=Y to=C ok=true promise=3 accept n=2 value=Y to=B ok=true promise=2 accept n=1 value=X to=B ok=false promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false history n=3 value=Y voters=[A C] chosen=true learned=true SAFETY violation=false SCENARIO max mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 prepare n=3 to=A ok=true promise=3 accepted={1 X}/true prepare n=3 to=C ok=true promise=3 accepted={2 Y}/true issue n=3 value=X reports=2 wrongMin=true accept n=3 value=X to=A ok=true promise=3 accept n=3 value=X to=C ok=true promise=3 accept n=2 value=Y to=B ok=true promise=2 accept n=1 value=X to=B ok=false promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false history n=3 value=X voters=[A C] chosen=true learned=true SAFETY violation=true SCENARIO promise mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 modeled-recovery node=B mutation=none promise=2 accepted={0 }/false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=false promise=2 accept n=2 value=Y to=B ok=true promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false SAFETY violation=false SCENARIO promise mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 modeled-recovery node=B mutation=promise promise=0 accepted={0 }/false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 accept n=2 value=Y to=B ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=Y voters=[B C] chosen=true learned=false SAFETY violation=true SCENARIO accepted mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 modeled-recovery node=B mutation=none promise=1 accepted={1 X}/true prepare n=2 to=B ok=true promise=2 accepted={1 X}/true prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=X reports=2 wrongMin=false accept n=2 value=X to=B ok=true promise=2 accept n=2 value=X to=C ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=X voters=[B C] chosen=true learned=true SAFETY violation=false SCENARIO accepted mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 modeled-recovery node=B mutation=accepted promise=1 accepted={0 }/false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=B ok=true promise=2 accept n=2 value=Y to=C ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=Y voters=[B C] chosen=true learned=true SAFETY violation=true PASS all: 3 normal histories safe; 3 mutations expose historical quorum conflicts PARENT RACE RUN FULL OUTPUT GUARDS prepare n=2 to=A ok=true promise=2 accepted={0 }/false prepare n=2 to=B ok=true promise=2 accepted={0 }/false issue n=2 value=X reports=2 wrongMin=false accept n=2 value=X to=A ok=true promise=2 accept n=2 value=X to=C ok=true promise=2 accept n=1 value=X to=C ok=false promise=2 PASS guards: distinct identities, matching ballots, quorum gates, accept raises promise SCENARIO max mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 prepare n=3 to=A ok=true promise=3 accepted={1 X}/true prepare n=3 to=C ok=true promise=3 accepted={2 Y}/true issue n=3 value=Y reports=2 wrongMin=false accept n=3 value=Y to=A ok=true promise=3 accept n=3 value=Y to=C ok=true promise=3 accept n=2 value=Y to=B ok=true promise=2 accept n=1 value=X to=B ok=false promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false history n=3 value=Y voters=[A C] chosen=true learned=true SAFETY violation=false SCENARIO max mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 prepare n=3 to=A ok=true promise=3 accepted={1 X}/true prepare n=3 to=C ok=true promise=3 accepted={2 Y}/true issue n=3 value=X reports=2 wrongMin=true accept n=3 value=X to=A ok=true promise=3 accept n=3 value=X to=C ok=true promise=3 accept n=2 value=Y to=B ok=true promise=2 accept n=1 value=X to=B ok=false promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false history n=3 value=X voters=[A C] chosen=true learned=true SAFETY violation=true SCENARIO promise mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 modeled-recovery node=B mutation=none promise=2 accepted={0 }/false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=false promise=2 accept n=2 value=Y to=B ok=true promise=2 history n=1 value=X voters=[A] chosen=false learned=false history n=2 value=Y voters=[B C] chosen=true learned=false SAFETY violation=false SCENARIO promise mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=C ok=true promise=2 modeled-recovery node=B mutation=promise promise=0 accepted={0 }/false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 accept n=2 value=Y to=B ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=Y voters=[B C] chosen=true learned=false SAFETY violation=true SCENARIO accepted mutate=false prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 modeled-recovery node=B mutation=none promise=1 accepted={1 X}/true prepare n=2 to=B ok=true promise=2 accepted={1 X}/true prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=X reports=2 wrongMin=false accept n=2 value=X to=B ok=true promise=2 accept n=2 value=X to=C ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=X voters=[B C] chosen=true learned=true SAFETY violation=false SCENARIO accepted mutate=true prepare n=1 to=A ok=true promise=1 accepted={0 }/false prepare n=1 to=B ok=true promise=1 accepted={0 }/false issue n=1 value=X reports=2 wrongMin=false accept n=1 value=X to=A ok=true promise=1 accept n=1 value=X to=B ok=true promise=1 modeled-recovery node=B mutation=accepted promise=1 accepted={0 }/false prepare n=2 to=B ok=true promise=2 accepted={0 }/false prepare n=2 to=C ok=true promise=2 accepted={0 }/false issue n=2 value=Y reports=2 wrongMin=false accept n=2 value=Y to=B ok=true promise=2 accept n=2 value=Y to=C ok=true promise=2 history n=1 value=X voters=[A B] chosen=true learned=false history n=2 value=Y voters=[B C] chosen=true learned=true SAFETY violation=true PASS all: 3 normal histories safe; 3 mutations expose historical quorum conflicts CLI HELP: GOCACHE=/private/tmp/ds-go-cache go run examples/distributed-systems/paxos09/main.go -h; exit0 Usage of paxos09: -mutate inject the named scenario's defect; detected conflict exits 1 -scenario string all, max, promise, or accepted (default "all") CLI BAD POSITIONAL: same command plus unexpected; wrapper exit1, process killed before expected exit2 observed. UNVERIFIED behavior. signal: killed CLI STANDALONE MUTANT: same command plus -scenario max -mutate; wrapper exit1, killed before intended diagnostic observed. UNVERIFIED standalone branch; default all did execute the same max mutant successfully. signal: killed Style gates: blog-editor read; temporary draft checked with anti-ai-tone tech (0 errors, 0 warnings), followed by anti-persona-fabrication manual/lexical pass (0 matches), then published source write. Build/browser/link rendering and commit remain parent integration responsibilities; no deploy or push performed.