JS-SAM vs TLA+: fair Phase-3 study + lean-contract prototype - #3
Open
jdubray wants to merge 31 commits into
Open
JS-SAM vs TLA+: fair Phase-3 study + lean-contract prototype#3jdubray wants to merge 31 commits into
jdubray wants to merge 31 commits into
Conversation
…kers) Removes the agent confound from the JS-SAM-vs-TLA+ Phase-3 comparison by equalizing the observable-state contract and replaying transitions mechanically in TLC. - tasks/spin/prompts/direct_call_constrained.txt: constrains the TLA+ spec to VARIABLES lockHeld, lockHolder + AcquireLock(thread,callType) / ReleaseLock(thread), matching the trace schema, with a TLC-safe NONE == "none" (no unbounded CHOOSE — the trap that broke free-form TLA+). - scripts/tla_direct_tv.py: direct TLC trace-validation. Per window, a TV module pins the pre-state, takes one action step, and asserts the post-state unreachable (INVARIANT NoPost); a violation => window passes. Classifies pass/fail/unscoreable and reports conditional (over scoreable) and unconditional (unscoreable=fail) numbers. - docs/js_sam_tla_phase3_plan.md: pre-registered design + interpretations. Validated: constrained Opus scores 28/28 (100%); breaking ReleaseLock to a no-op fails all 11 release windows (60.7%) — the replay discriminates. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Runs the three-arm paired study (deployed-JS, constrained-JS, constrained-
TLA), N=5 per model, 28-window corpus, scored per-window.
Key result (docs/js_sam_tla_phase3_results.md): most of the raw TLA+ ≫
JS-SAM reversal was PROMPT PRESCRIPTIVENESS — adding the single-step
semantics to the JS prompt closed most of the gap (Fable 58->96%, Sonnet
50->100%). A real, one-directional residual survives: with identical
semantics, TLA+(constrained) hits 100% for every model/generation while
JS(constrained) does not for 3/4 (Opus 89%, Fable 96%, Haiku 41%; Sonnet
ties at 100%); b=0 in every McNemar (JS never beats TLA on any window).
Reads as a partial "formal directness forces precision" effect that strong
models close. Checkability fully solved by the constraint (0 unscoreable).
Adds the constrained JS-SAM prompt (deployed + the same semantics block),
adds {source_code} to the constrained TLA prompt for fairness, and the
paired driver with per-model McNemar. Raw per-window data checked in.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…cript
Adds a fourth arm: a bare next(state, action, data) -> {lockHeld, lockHolder}
pure function (no SAM library, two keys) — structurally isomorphic to the
TLA+ relation — run in the same locked-down Docker sandbox.
Result (docs/js_sam_tla_phase3_results.md): plain-JS ties TLA+ at 100% for
every model and generation (McNemar b=0 c=0 for all four). Haiku goes
40.7% (SAM) -> 100% (plain-JS). So the JS-SAM Phase-3 gap is the SAM
pattern's wiring (proposals/acceptors/intent + mandatory auxiliary state),
NOT JavaScript and NOT "formal vs informal": the dividing line is a minimal
declarative transition shape (TLA+ relation == plain next()), which SAM-JS
lacks. Design implication: a leaner JS-SAM spec contract recovers fidelity.
Adds tools/plain-js/tv.mjs (sandboxed runner), scripts/plain_js_tv.py,
the plain-JS prompt, and the pjs arm + plainJS-vs-TLA McNemar in the driver.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Follows from the plain-JS finding (the Phase-3 gap is SAM's machinery, not
JavaScript). Prototypes a lean spec contract — a pure next(state, action,
data) over the two observable keys, the JS analogue of the TLA+ relation —
and shows it supports all of Phases 2/3/4 without the SAM library:
- tools/plain-js/explore.mjs: generic bounded explorer over {init, next}
(Phase 2 runtime: crashes/determinism/serializable; Phase 4: invariants).
- tools/plain-js/reference_spin.js: reference lean spec.
- scripts/plain_js_tv.py: adds plain_js_explore(); generalizes the sandbox runner.
- scripts/lean_demo.py: runs Phases 2/3/4 on a lean spec in the sandbox.
Reference spec: Phase 2 PASS (3 states), Phase 4 3/3, Phase 3 28/28.
- docs/js_sam_lean_contract.md: design, evidence, integration options
(lean backend / hybrid SAM-scaffolding / status-quo), tradeoffs.
Note: paper/methodology.md updated locally to the four-arm design (gitignored).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Reverses the earlier decision to gitignore paper/. The methodology note and manuscript cite the raw per-window results in output/tla_phase3_study.json (all four arms, N=5, committed at a347471) and the lean-contract prototype; tracking them together keeps the paper reproducible from the repo alone. - paper/methodology.md — four-arm design + §7 result summary - paper/js_sam_sysmobench.tex/.pdf — manuscript - .gitignore: track paper source, ignore only LaTeX build byproducts Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Merges the two half-results into one coherent claim. The prototype validated Phases 2/4 on a reference spec; the paired study validated Phase 3 on model-generated specs but discarded the spec text. This regenerates N lean specs per model, SAVES each, and runs Phases 2/3/4 on the same saved spec. Result: 20/20 model-generated lean specs pass every phase (5/5 each for Opus 4.8, Fable 5, Sonnet 4.6, Haiku 4.5) — loadable, Phase 2 clean (3 states), Phase 3 28/28, Phase 4 3/3. - scripts/lean_full_pipeline_study.py: generate -> save -> all-phase eval, resumable. - output/lean_specs/<model>_<gen>.js: the 20 saved generations (the artifacts the claim rests on). - output/lean_full_pipeline.json: per-spec per-phase raw results. - docs/js_sam_lean_contract.md: path 1 upgraded from plausible to demonstrated; adds the N=5x4-model table. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The spin lean result carried two caveats: a tiny observable state (3 reachable
states, two scalars) and heavy solution convergence. A structurally different
second task settles both. locksvc is PGo's centralized lock service; its
observable state is {holder, waiters} — a lock holder plus a FIFO wait queue
(an unbounded list) — with four actions and FCFS grant semantics.
Trace capture (real Go execution, distsys trace recorder):
- scripts/harness/locksvc/run.sh already existed; parse_traces.py fixed for
Windows UTF-8; build_windows.py (new) folds PGo events into {holder, waiters}
observable (pre,action,post) windows, repairing empty-vclock ordering
artifacts (a CriticalSection logged before its own Grant) causally.
- data/sys_traces/locksvc/: 60 windows across 5 runs (15 per action).
Study (task-agnostic now):
- scripts/lean_task_config.py: per-task action domain + invariants + reference.
- lean_demo.py / lean_full_pipeline_study.py take --task.
- tools/plain-js/tv.mjs generalized to the projection rule (compare every key
in the trace post-state; extra model keys ignored) — was hardcoded to spin.
- tools/plain-js/reference_locksvc.js + plain-js prompt.
Result: 20/20 model-generated lean specs pass every phase on locksvc (5/5 each
for Opus 4.8, Fable 5, Sonnet 4.6, Haiku 4.5). Bounded exploration reaches 31
states (vs spin's 3); solutions de-converge to 11 distinct specs of 20 (spin:
9/20), 36-48 lines with per-model clustering. Artifacts:
output/lean_specs_locksvc/, output/lean_full_pipeline_locksvc.json.
docs/js_sam_lean_contract.md: second-task section + caveats updated.
(paper/ tex edits left to the author; PDF rebuild needs pdflatex, absent here.)
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…symmetry review
Review: the JS and TLA+ Phase-3 replays did not check the same relation, and the
asymmetry favored TLA+. JS is functional (next(pre) must equal post); the TLC
replay was existential (post merely reachable). An over-permissive TLA+ action
passes existentially while admitting wrong post-states; the no-op negative
control only proved failure on unreachable posts, not on permissive specs.
Fix + evidence:
- tla_direct_tv.py: add branching_factor() + functional_replay_window() +
--functional. A window passes only if the action's one-step image from the
pinned pre is exactly {post} (branching factor 1) — as strict as next(pre)==post.
- tools/tla/permissive_spin.tla (negative control): holder := any thread on
acquire. Passes the EXISTENTIAL replay 28/28 (100%) but the functional check
flags 17 windows over-permissive (bf=2) -> 39.3%. tools/tla/reference_spin.tla
passes both (28/28, bf=1). (Fully mixed int/string permissiveness is caught as
unscoreable — TLC throws comparing "none" to an int thread id.)
- tla_functional_audit.py: regenerate + SAVE 20 constrained TLA+ specs (5x4
models) and re-score under the functional check. Result: existential =
functional = 140/140 per model, 0 over-permissive windows, max bf = 1. Every
generated spec is deterministic — the TLA+ 100% is earned under the strict
relation, not an existential artifact.
- tla_phase3_study.py: score_tla now uses the functional check (over_permissive
counts as fail), so the paired comparison applies one relation to both languages.
- output/tla_specs/*.tla + tla_functional_audit.json: the audited artifacts.
- docs/js_sam_tla_phase3_results.md: "Replay-check symmetry" section.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Review: the identical 326,592 "states" across all four models was a red flag — the metric counts explored action-sequences, not states, making Phase 2's number model-independent and the paper's "structurally equivalent state spaces" claim wrong. Audit confirmed, and worse: steps = (d+1)*|intents|^d = 7*6^6 = 326,592 — safety-callback invocations over the intent-permutation tree, a pure function of the contract-pinned intent domain and depthMax (verified empirically at depths 1/2/3: 12/108/864). Identical for ANY conforming spec by construction. Counting distinct semantic states (unique model snapshots) separates them: Opus/Fable/Sonnet 7, Haiku 1 — Haiku's intent actions drop their arguments so every proposal is rejected; its exploration never leaves init. Haiku's Phase-2 PASS (and vacuously its Phase-4 3/3) certified a spec that cannot move. Two Claude generations also differ (June spec: 5; July spec: 7) at identical steps. Nuance on the review's premise: Fable's spec DOES release in exploration (7 states) — its Phase-3 Release 0% is the pinned-observable-state replay hitting its auxiliary threadStatus guard, not an unreachable release. Fixes (TDD: fixture + failing tests first): - tools/js-sam/cli.mjs: explore() tracks a seen-set of serialized snapshots -> distinctStates, surfaced by check + invariants; determinism digest includes it. - js_sam.py: states_explored = distinctStates (semantic); the combinatorial step count stays available as steps_explored/raw_output. - runtime_check.py parse_tlc_output: states_explored = TLC "distinct states found" (was "states generated", a work counter with duplicate visits). Fable's TLA spec: 574 generated / 159 distinct. - tests: spin-neverrelease.js fixture (release no-op) + regression asserting identical steps but differing distinct states; TLC parsing unit tests; repaired test_missing_traces_reported_cleanly (its premise — spin traces not checked in — went stale when the corpus was committed). Docs/paper: comparison tables now show distinct states (7/7/7/1; 159 for the TLA arm); "structurally equivalent state spaces" retracted and replaced by the audit; the three incommensurable counts (326,592 steps / 574 generated / 3 observable) reconciled explicitly in docs/js_sam_vs_tla_comparison.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
…ers revised Review: repaired specs were only re-checked on Phase 1 + Phase 3, on the same 28 windows quoted in the repair prompt; nothing prevented memorizing the failing windows, making "Fable repairs to 100%" possibly a prompt-following result, and Experiment 2's "three tiers" unverified as modeling. scripts/repair_generalization.py re-runs the repair loop with artifacts SAVED (output/repair_specs/) and scores every baseline and repaired spec on: P3-seen (28 windows = 8 distinct combos), P3-heldout (the 10 combos of the observable domain the corpus never shows), P2 (distinct-semantic-state metric), and P4 (three observable invariants). Results: - Opus/Fable/Sonnet repaired: 28/28 seen, 10/10 held-out, 7 distinct states, 3/3 invariants. Haiku: unchanged (6/28, 1 state — still inert). - No memorization: zero state-equality tables/window literals in any repaired spec. Fable's and Sonnet's repairs are the same root-cause semantic fix — release ownership moved from the auxiliary threadStatus guard (unsatisfiable under a pinned observable pre-state) to authoritative lockHeld/lockHolder; Sonnet's repair documents the diagnosis in a comment. - Honest structural limit, stated in script+doc+paper: the kernel emits acquire events at acquisition success, so every held-out combo is an observable no-op — held-out alone refutes only unsafe-default memorizers; inspection and P2/P4 carry the conclusion. A state-changing held-out set (locksvc) is flagged as the stronger follow-up vehicle. - Replication surprise: Sonnet repaired to 28/28 here vs 60.7% originally. The "three clean tiers (full/partial/none)" claim is revised everywhere (doc + paper abstract/intro/section): stable boundary is repairers vs Haiku; mid-tier single-round outcomes are sampling-dependent at N=1. The original "Sonnet cannot fix its release path" contrast is retracted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
…eanalysis Review: pooling windows across 5 generations treats 140 outcomes as independent when generations collapse to a handful of unique solutions — the same bug counted five times, chi-square inflated (c=59, c=83). Correct unit is the unique solution or the generation; report uniqueness for every arm. Audit confirms, worse than estimated: behavioral fingerprints (per-window outcome vectors) collapse to 1-2 unique per (model, arm) for ALL 16 cells — e.g. Haiku's c=83 was one bug counted four times plus one partial. scripts/tla_phase3_analysis.py (new) reanalyzes the committed raw JSON: 1. Uniqueness for EVERY arm (fingerprints; plus text-level uniqueness of the saved regenerated sets as corroboration: pjs 9/20, locksvc 11/20, tla 10/20 unique texts, each collapsing to one behavior per arm). 2. Exact generation-level permutation test (unit=generation, diff in mean pass rate, all C(10,5)=252 relabelings, two-sided; floor p=2/252≈0.0079). 3. Unique-solution view (n=1-2/cell: effect sizes only, no tests). Results at the defensible unit: - deployed-JS vs TLA: significant for ALL four models (p=.0079, at floor) — the contract-tax effect is not a pooling artifact. - constrained-JS vs TLA: significant for Opus and Haiku only. FABLE'S STARRED DEFICIT IS WITHDRAWN (chi2=4.2* pooled -> p=0.44 at generation level). - plain-JS vs TLA: identical in every generation (delta=0; no test needed). All pooled chi-square values retracted in docs + paper + methodology note; tla_phase3_study.py now prints b/c as descriptive only and points to the analysis script; the plan doc records the post-hoc analysis revision; the paper's McNemar table is replaced by uniqueness + permutation results and the "significant for Opus, Fable, and Haiku" finding corrected. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
…ss checks
Review: Phase 4 cannot catch the paper's own headline bug — a never-releasing
lock satisfies mutual exclusion BECAUSE it is broken; the three JS-SAM
invariants are safety-only and demonstrably too weak; the interesting lock
properties are liveness, and neither the SAM checker nor the lean explorer
checks any temporal property. Not a "template count" caveat: Phase 4 as
implemented could not fail Fable's spec in principle.
Verified, precisely:
- The shipped NoDeadlock is "some thread is not 'trying'" — satisfied by the
stuck HOLDER being 'locked'. Empirical demo: a release-is-a-no-op mutant of
the known-good spec gets the IDENTICAL 3/3 Phase-4 verdict as the correct
spec. Pinned as a characterization test
(test_safety_only_phase4_passes_a_never_releasing_lock) that fails loudly if
Phase 4 ever gains the capability.
- Fable's defect is doubly invisible: it manifests only under a pinned
observable pre-state, so even a liveness-capable from-init checker would
pass its spec — only trace replay catches it. Both layers stated.
- The TLA+ template set declares two liveness properties (PROPERTY-routed), so
the P4 gap is qualitative, not just numeric — noted.
Mitigation (TDD): the lean explorer gains bounded PROGRESS checks —
EF-reachability over the explored graph ("from every reachable state
satisfying `from`, a `goal` state is reachable within the bound"). Explicitly
NOT liveness (no fairness, bounded horizon) and labeled as such everywhere.
- tools/plain-js/explore.mjs: state graph + progressViolations.
- lean_task_config.py: Acquire/Release progress for spin; Grant/Release for
locksvc (state-changing — also strengthens future held-out replay).
- Results: never-releasing lean mutant fails ReleaseProgress (safety P4
passes it); the inert-spec class fails AcquireProgress; reference specs and
ALL 40 saved model-generated lean specs pass on both tasks — the
strengthened Phase 4 hardens, not overturns, the 20/20 results.
Docs/paper: "template count differs" limitation replaced by the precise
in-principle statement + empirical demo + mitigation in
docs/js_sam_vs_tla_comparison.md, docs/js_sam_lean_contract.md, and the
paper's Experiment-3 setup + limitations.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
… unconditionally Review: the 2x2 in (contract, prompt) had an empty cell — the lean arm always carried the semantics block, so "contract minimality buys transcription fidelity" was conditional on spec-level semantics in the prompt, and the prompt>contract>language ranking rested on an incomplete design with ceiling effects. Added the missing cell (pjd): the identical lean contract with the entire single-step semantics block removed — the model derives the transition semantics from the Rust source alone (tla_eval/tasks/spin/prompts/plain-js/direct_call_nosemantics.txt). Result: lean-without-semantics = 100% for EVERY generation of EVERY model — including Haiku, at 28.6% under SAM with the same absent semantics. 20/20 generations, 5/5 unique spec texts per model (saved: output/study_specs/), all behaviorally identical and correct. The suspected conditionality is refuted: the contract effect holds without prompt semantics. Completed factorial contrasts (generation-level exact permutation): - contract effect, no semantics (js vs pjd): significant for ALL FOUR models (delta .186/.421/.500/.714, each p=.0079, the floor). - prompt effect within SAM (js vs jsc): significant for only Fable (.379, p=.024) and Sonnet (.500, p=.0079); Opus and Haiku p=1.0. - prompt effect within lean (pjd vs pjs): delta=0 — unidentifiable at ceiling. This INVERTS the earlier headline: "prompt explains most of the reversal" was an artifact of examining only the SAM column. Revised everywhere to: contract first (uniform), prompt second (model-dependent), language nowhere. Ceiling honesty stated: ordering among the 100% cells and any prompt x contract interaction are not identifiable at the top; identifiable claims are contract >= prompt per model and lean-sufficiency without semantics vs SAM-insufficiency with it. - tla_phase3_study.py: pjd arm; saves spec text for every new cell. - tla_phase3_analysis.py: 5 arms, four factorial contrasts + 2x2 table. - results doc: completed-2x2 section; finding 4 revised. - paper: abstract, intro bullet, missing-cell paragraph, tab:crosslang column, findings rewrite, discussion + conclusion ranking corrected (contract, then prompt, then language), derivation open-question updated. - methodology note aligned. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
…he base rate Review: of the 17 acquire windows, contention windows have post = pre — a no-op acquire passes them free; report no-change counts and per-class rates. Verified: 6 of 28 windows (all contention acquires) are no-change => identity base rate 21.4% overall, 6/17 = 35.3% on acquires. Experiment 1's Haiku row is EXACTLY that base rate: Acquire 6/17 is precisely the six freebies, Release 0/11, zero state-changing windows passed. Conditional on the 22 change windows the Experiment-1 spread is 0% (Haiku) / 36.4% (Fable, Sonnet) / 86.4% (Opus) — not 21.4–89.3%. - tla_phase3_analysis.py section 0: corpus composition, identity base rate, per-(model, arm) change/no-change split, freebie share of passes. Study arms: every arm passes all 6 freebies; Haiku SAM+none is 9.1% conditional-on-change (75% of its headline passes were freebies), SAM+sem 24.5% (52.6%). Lean/TLA cells unaffected (100% everywhere). - docs/js_sam_model_comparison.md: base-rate section; finding restated on the conditional metric (0–86.4%). Replication note: re-scoring saved Haiku specs shows a ±2-window sensitivity in sequential replay (async-error attribution timing); either value sits at/near the base rate. - docs/js_sam_tla_phase3_results.md: conditional-on-change table for all five arms; correction largest where scores are lowest; no factorial conclusion flips. - paper: abstract, intro bullet, Experiment-1 finding + tab:models caption, conclusion — spreads restated as 0–86.4% on state-changing windows with the base rate named. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
…order unobservable) Found by the point-7 base-rate audit: 10 of the 60 locksvc windows were no-op grants/releases — grants to a non-HEAD client under the fold's FCFS assumption. Root cause: the fold ordered `waiters` by client-SEND order, but the real server grants in ARRIVAL order, which the network reorders (one capture logged sends 1,3,2 while the server queued <<3,2,1>> — exactly the reordering upstream locksvc.tla's NoPriorityInversion comment warns about). The old fold silently converted real state changes into no-op windows — wrong ground truth. Arrival order is not a function of the client-side single steps the trace exposes, so at this projection waiters is a SET (canonically sorted array): grant valid for any waiter of a free lock; FCFS is unobservable here. - build_windows.py: set-semantics fold + documentation of the bug. - reference_locksvc.js + plain-js prompt: set semantics. - Corpus re-folded: 60 windows, 15 no-change (all legitimately the CS no-ops; identity base rate 25%), zero bogus no-op grants. - Study invalidated and REGENERATED from scratch (old specs implemented head-grant FCFS): 20/20 fresh lean specs pass every phase again — including the bounded progress checks — over a 20-state space, 14/20 unique texts (4/4/4/2 per model), 45/45 on state-changing windows. - docs/js_sam_lean_contract.md + paper locksvc section: correction documented in-line; 31-state/11-20 numbers replaced. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
… fidelity" Review: two hand-authored deterministic scenarios; no blocking-waiter wakeup (the actual spin); locksvc's exactly-15-per-action suggests a deterministic schedule; the vector-clock repair reorders ground truth per an asserted assumption; and the conclusion's "interchangeable on fidelity" doesn't carry the qualifier the Limitations admit. Audited (scripts/trace_coverage_audit.py), with each sub-claim resolved: - spin: confirmed — 2 deterministic ktest scenarios; 8/18 observable combos covered; contention is try-only (2 combos); ZERO blocking-lock-on-held windows. Sharper than the review: the instrumentation emits acquire at acquisition SUCCESS (pre=free), so the spin phase is invisible in this projection BY CONSTRUCTION — a woken blocking waiter is indistinguishable from an uncontended acquire. - locksvc: half-confirmed — the exactly-15/action is protocol completion (one fixed terminating workload: 3 one-shot clients = 12 windows/run), not schedule determinism: the 5 runs are 5/5 distinct action sequences with 4 distinct grant orders (including the network reordering that exposed the fold bug). No re-requests, no deeper contention, no failure paths. - reorder premise: now DEMONSTRATED, not asserted — every CriticalSection event reads GrantMsg=3 from its mailbox (message-passing happens-before), verified per event; build_windows gains validate_cs_consumed_grant() and refuses traces where the premise fails. Docs/paper: "Trace coverage" section in the results doc; the paper's 28-window limitation bullet replaced with the full audit; the conclusion's "yes, interchangeably on fidelity" now reads "interchangeable on fidelity ON WHAT WE MEASURED — a two-variable projection of deterministic, easy slices — untested on uncovered combos, projection-invisible behavior, richer workloads, or adversarial interleavings." Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
Review: derivation (both languages), as-deployed agent path, multi-round repair, other vendors, locksvc factorial — acknowledged but load-bearing; plus independent replication given experimenter-authored materials on both sides. RUN — TLA+ derivation arm (tld: constrained TLA contract, semantics block removed, mirroring the lean derivation arm). The factorial is now a full 3x2 (contract SAM/lean/TLA x prompt none/sem), and derivation splits the languages for the first time: - lean+none beats TLA+none for Opus and Sonnet (100% vs 78.6%, delta=.214, p=.0079 each), directionally for Haiku (87.1%, p=.17), tie for Fable. - Mechanism precise, and NOT wrong posts: every TLA shortfall window is unscoreable. Without instruction, Opus/Sonnet (5/5 gens) and Haiku (3/5) write the classic TLA idiom — AcquireLock GUARDED on the lock being free — making a failed attempt a disabled action, not an observable no-op step; pinned contention windows then have no successor (TLC deadlock). Fable writes no-op-tolerant actions unprompted. - Readings: the lean contract's TOTALITY (next() must return) structurally forbids the partial-action idiom; the semantics block was doing real, previously invisible work for TLA+ specifically (tld vs tla p=.0079 for the affected models); under pre-registered conditional scoring the guard-idiom specs are 100% on scoreable windows — both numbers reported. "Contract first, prompt second" refines to: the prompt matters exactly where the contract under-constrains. RUN — multi-round repair (scripts/repair_multiround.py): Haiku does NOT converge — 6/28 -> 6/28 -> 6/28 across three rounds of full-failure feedback, exploration still 1-state; every round's spec saved and audited (held-out + P2). Sonnet full-repairs in round 1 again (2nd full repair in 3 runs — more evidence the original "partial" tier was sampling noise). NOT RUN, with stated reasons: as-deployed agent path (reintroduces the confound the direct replay removed); other vendors (registry entries exist, credentials don't — user-level unblock); locksvc factorial (lean arms done; SAM/TLA arms need locksvc prompts + a locksvc TLC replay module). REPLICATION.md: rerun every analysis from committed raw data with no API access; regenerate every experiment from pinned prompts/models; inventory of every experimenter-authored material (scenarios, semantics block, derivation prompts, repair prompt, invariant sets, projections) as an independent variable to audit or vary. Paper's positionality bullet now names the experimenter-authored-materials problem and calls independent replication (ideally by the SysMoBench maintainers) a prerequisite for treating the cross-language conclusions as more than a single-author case study. Missing-arms inventory bullet added with per-arm status. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
Camera copy incorporating the full nine-point review response: functional (branching-factor) Phase-3 replay with permissive negative control; Phase-2 distinct-state metric audit (vacuous-pass finding); repair generalization audit (held-out + inspection) and multi-round repair; generation-level statistics replacing the pseudo-replicated pooled McNemar; safety-only Phase-4 precision + bounded progress checks; the completed 3x2 contract-by-prompt factorial including both derivation arms (lean totality vs TLA+ guard idiom); corpus base-rate analysis; trace-coverage audit with the qualifier carried into the conclusion; locksvc corpus correction; missing-arms inventory, replication guide, and the positionality/independent- replication statement. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PX1erummaoUTV7NKhQAdr5
Owner
Author
Review response complete — all nine points addressed, paper finalizedFinal camera copy:
Every claim's raw artifacts are committed (per-window JSON, all generated specs, audit results, trace corpora). Analyses re-run without API access via 🤖 Generated with Claude Code |
…ask, corpora, reference models)
New SysMoBench task extracted from a production restaurant POS (baanbaan
Merchant/v2): pinned 7-variable observable-state contract, 9-action dispatch
alphabet, prompts for the SAM / lean-JS / constrained-TLA+ arms, verbatim
source packet with provenance (EXTRACTION.md).
- Real-execution trace corpora (emulator + chaos proxy): v1 75 windows /
17 scenarios, v2 101 windows (3 windows per acceptor-rewrite rule),
post-fix corpora for patch validation; instrumentation diff in
data/patches/finixpos_trace.patch.
- Hand-written reference models: FinixPOS.tla + environment (TLC-checked),
crash/staleness/two-attempt/refund extensions, patched-semantics variants
(FinixPOSFixed*, FixedV2), annotated counterexamples for every confirmed
gap, sandbox reproduction evidence (real Finix 422 shape), CONTROLS.md
(positive + mutation controls), CONTAMINATION.md, EXTENDED_FAILURE_MODEL.md.
- trace_loader: accept the harness's {pre, action, data, post} event form
(+ test).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv
- Drivers: finixpos_tv.py (mechanical replay, all three arms; validated by positive + mutation controls), finixpos_phase3_study.py (two-phase generate-then-score with Anthropic prompt caching), v2 rescore, post-fix study (best-model+arm revalidation), final analysis (permutation tests, uniqueness counts). - Results of record: 7 models (Fable 5, Opus 4.8, Sonnet 4.6, Haiku 4.5, mistral-large-2512, devstral-2512, labs-leanstral-1-5) x SAM / lean / TLA+ x N=5, scored on both corpora; all 105 + 10 generated specs and per-window statuses committed for the audit trail. - Headline: lean next() contract best-or-tied and never unscoreable for all seven models across two vendors; TLA+ deficits dominated by checkability and the guard idiom; SAM ceremony kills specs in model-specific ways; semantic error is language-independent. Replication is of ordering and taxonomy, not level - only Claude frontier models reached deployment-grade reliability. - config: mistral-large / devstral / leanstral model entries. - docs: study plan (pre-registered design) and full results incl. the correctness deliverable (7 confirmed gaps + review-response revisions, patch v1/v2 validation, accepted-operational-risk scoping). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv
…logy) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv
…prompt
Ground Phase 3 for the etcd task. Upstream etcd-io/raft (pinned 26647d5)
ships complete trace instrumentation behind the with_tla build tag; the
harness adds only an NDJSON TraceLogger sink and five deterministic
3-node RawNode scenarios (election, proposals, heartbeats, stale-campaign
vote rejection, higher-term re-election), then folds the event streams
into whole-cluster observable windows {nodes: {id: {role, term, vote,
commit, log}}}.
Corpus: 97 windows across the five canonical target actions, zero
self-consistency violations, byte-identical regeneration, provenance
pinned per run. A hand-written reference lean spec replays 97/97 through
the benchmark's own sandboxed path (positive control); two projection
approximations (index-only vote up-to-dateness, heartbeat commit clamp)
are documented in the README and exact on these corpora by construction.
The plain-js prompt is the lean derivation form: contract pinned (state
shape, action/data schemas, {init, next} module), no semantics block —
transition semantics must be derived from raft.go.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…round repair Study (scripts/lean_full_pipeline_study.py --task etcd --n 5): all 20 specs load and explore cleanly (~130k distinct states at depth 8), none passes every phase one-shot. Fable reaches 97/97 conformance on 4/5 generations but violates CommitWithinLog under open-world exploration (unclamped heartbeat commit); the other models fall short on Phase 3, dominated by HandleVoteRequest (step-down/vote-reset/up-to-dateness). Per-window failure detail in output/lean_etcd_p3_failures.json. Repair round (scripts/repair_lean_etcd.py): each failing spec gets its own module, every failing window with expected vs actual, and invariant counterexamples; one rewrite; full re-score. Result: fable 4/5 all-pass, claude 2/5, sonnet 0/5 (3/5 cells regress below baseline), haiku 0/5 (all cells plateau at 93/97 on the same four vote windows). tv.mjs now returns the module's produced state on failed windows to support the feedback loop (backward-compatible). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Paper sources are working drafts, not benchmark artifacts; keep them out of the repository. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Paper sources are working drafts, not benchmark artifacts; keep them out of the repository. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01K5kaEQ4WBnGb4SL8FdXJK8
… semantics) The strict-profile breaking change (frozen pre-state, next-draft writes, mandatory unchanged() framing) does not affect this helper or generated specs, which run in default mode: full pytest suite 23/23 green against 2.1.2 in Docker. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UfSbyWEBtEwBsxB2CuSYYv
Add an `opus5` model entry (claude-opus-5) and extend the sampling-omit list to the Claude 5 family. `claude-sonnet-5` had only ever been patched in the sysmobench-etcd worktree, so the main repo would have 400'd on it. Smoke test (spin / TLA+ / direct_call, N=5), written up in docs/opus5_smoke_test_results.md: P1 5/5. P2 first shot 1/5 -- four specs die on `NULL == CHOOSE v : v \notin Threads`, an unbounded CHOOSE that SANY accepts and TLC refuses, so they explore 0 states. One repair round takes P2 to 5/5 with zero regressions. P4 is 35/35. The deficit is idiom selection, not modeling ability. Single-shot P2 understates it by 5x; the repair round is where the signal is. Three harness bugs, two of which corrupt scores independent of model quality: 1. Phase 4 appends `<Name> == ...` to the generated module, colliding with the spec's own operator when the model names its invariants after the expert templates. SANY rejects the module and the invariant is scored FAIL without TLC running. Perfect correlation across 5 runs x 7 invariants. scripts/rescore_p4_name_collision.py re-scores mechanically; all 8 collided invariants then pass. 2. extract_tla in repair_tla_spin.py takes the FIRST ```tla fence, so a reply that quotes the offending line before emitting the rewrite loses its module. repair_tla_spin.py is committed AS IT RAN, unfixed, so the recorded Experiment-3 numbers stay reproducible -- but those numbers were produced with this extractor and any parse-failure repair there should be re-checked. The corrected extractor lives in repair_tla_spin_opus5.py. 3. transition_validation is unusable on Windows: transition_validation.py passes Windows paths to bash, which eats the backslashes (exit 127). Phase 3 never ran, so whether these specs replay real traces is still open. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HkfxRoMS4KxrSyxLB5PpmY
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #2 (
js-sam-experiments). Makes the JS-SAM-vs-TLA+ Phase-3 comparison fair, runs a paired N=5 study across four arms, and prototypes the fix the results point to.What this establishes
The deployed JS-SAM Phase-3 gap vs TLA+ is the SAM pattern's machinery, not JavaScript. A bare
next(state, action, data)over the two observable keys ties TLA+ at 100% for every model.plain-JS vs TLA+: McNemar b=0, c=0, χ²=0 for all four models. The residual is contract ceremony, not the language or the modeling approach.
Methodological controls (why the headline is defensible)
(pre, action, post)window directly (scripts/tla_direct_tv.pyfor TLA+ via a tiny TLC replay module; sandboxednext()for JS), no agent translator in the loop.next(state,action,data), two keys, no SAM library) is structurally isomorphic to the TLA+ relation. It ties TLA+, isolating the gap to SAM's wiring.Raw data travels with the claims
output/tla_phase3_study.json— all four arms × 5 runs × per-windowstatuses(80 cells). The post-hoc plain-JS arm is reproducible from this file, not just the summary table.Lean-contract prototype
The results point to a leaner spec shape.
docs/js_sam_lean_contract.mdproposes it; the prototype shows a pure{init, next}contract runs the entire benchmark pipeline without the SAM library:tools/plain-js/explore.mjs— generic bounded explorer (Phase 2 runtime + Phase 4 invariants) over{init, next}tools/plain-js/tv.mjs+scripts/plain_js_tv.py— Phase 3 replayscripts/lean_demo.pyon the reference spec: Phase 2 PASS (3 states) · Phase 4 3/3 · Phase 3 28/28Caveat kept honest in the doc: clean 100% is on tiny
spinstate; re-run onringbuffer/locksvcbefore generalizing.Paper
paper/(methodology note + manuscript) is now tracked alongside the data it cites.Commits
68aace8constrained prompt + direct TLC replay (fair-Phase-3 blockers)f069835paired N=5 study drivera347471plain-JS arm + raw study JSON5cf432flean{init, next}prototype0d5a8dctrack paper/ with the data🤖 Generated with Claude Code