finixpos: production payment-alignment case study (task, corpora, reference models, 7-model study) - #4
Open
jdubray wants to merge 54 commits into
Open
finixpos: production payment-alignment case study (task, corpora, reference models, 7-model study)#4jdubray wants to merge 54 commits into
jdubray wants to merge 54 commits into
Conversation
Phase-4 builds its per-invariant cfg by appending the expert invariant to the model's phase-2 base cfg (forwarded via --config-file). If that base cfg carries the model's own INVARIANT/PROPERTY/CONSTRAINT/ACTION_CONSTRAINT/ POSTCONDITION sections, the expert check is contaminated: TLC can halt on the model's assertion before the expert one gets a clean verdict (false FAIL), or a model CONSTRAINT/ACTION_CONSTRAINT shrinks the state space so a violating path is never reached (false PASS). This affects every model whose phase-2 cfg flows into phase 3, not just BYO methods that emit a cfg. Strip those sections from the base cfg before composing the per-invariant cfg sent to TLC. The keyword set follows TLC's ModelConfig and includes the singular and plural forms. Classification is comment-aware (handles \* and (* *) comments, including multi-line) and treats a keyword line as a section header only when it is not an assignment, so a constant whose name collides with a keyword is not dropped. Comments inside a dropped section are dropped with it, and CRLF is normalized. Add regression tests: unit coverage for the keyword and comment forms, the keyword-as-constant case, and the safety/liveness composition paths, plus TLC-gated behavioral tests that show the verdict actually changes for INVARIANT (plain and comment-prefixed) and CONSTRAINT contamination.
* ci: run pytest on push and PR Add a GitHub Actions workflow that installs the package, sets up Java, fetches tla2tools.jar (pinned to the same version as scripts/setup_tools.py), and runs the test suite. The TLA+ tests, including the TLC-gated behavioral ones, run in CI rather than skipping. Scoped to tests/test_languages for now. tests/test_models is left out: test_model_connection.py makes live provider API calls that need secrets, and test_litellm_adapter.py has pre-existing failures unrelated to this workflow. * ci: add python matrix, concurrency cancel, and pyproject cache key * ci: narrow matrix to 3.10/3.11 and set requires-python >=3.10 (mcp needs 3.10) --------- Co-authored-by: Qian-Cheng-nju <Qian-Cheng-nju@users.noreply.github.com>
Co-authored-by: Qian-Cheng-nju <Qian-Cheng-nju@users.noreply.github.com>
JavaScript + SAM pattern (sam.js.org) via @cognitive-fab/sam-pattern and @cognitive-fab/sam-fsm: the bench's first non-formal-language backend, and the first to use the direct Phase 3 transition-validation path. - tla_eval/languages/js_sam.py: LanguageBackend subclass; shells out to a Node helper (tools/js-sam/cli.mjs, JSON-in/JSON-out) like Alloy/PAT. Phase 2/4 use the sam-pattern bundled behavior explorer (depthMax 6, bench-wide constant). Agent translators remap to a direct API call, matching Alloy/PAT precedent. - tools/js-sam: helper CLI (ping/validate/check/transitions/invariants); captures sam-pattern acceptor throws (async-wrapped) and treats gated 'unexpected action' rejections as legal model behavior. - Direct Phase 3 path: new language-neutral NDJSON trace loader (trace_loader.py) + implementation of the stubbed direct branch in transition_validation.py per add_new_spec_language.md 3.3. - spin task: js-sam prompts (Rocket Launcher in-context example, mandatory module contract) and 3 starter invariant templates. - scripts/run_benchmark.py: TLA+ tool gate now applies only when the TLA+ backend is selected; other languages use backend.check_available(). - Tests: 29 new (backend integration via real Node, trace loader, direct-path evaluator) plus known-good/known-bad spec fixtures and synthetic traces. docs/js_sam_backend_spec.md records the design and the implementation map. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
From-scratch explainer for reviewers new to the integration: what SysMoBench is, what the JS-SAM backend adds, the module contract, the reference and adversarial fixtures, every test that was run and what it demonstrates, and the honest list of what is not yet demonstrated (no live LLM runs, real spin traces not in the repo). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
claude-sonnet-4-20250514 generated a JS-SAM spin spec from the Asterinas source and passed Phase 1 (first attempt, no correction loop), Phase 2 (clean depth-6 exploration), and Phase 4 (3/3 expert invariants via the live translation path). Phase 3 remains blocked on captured traces. The run surfaced a config bug: the claude entry requested max_tokens 200000, which the Anthropic API rejects for claude-sonnet-4 (output cap 64000). Lowered with a dated probe note; this entry also backs the Alloy/PAT invariant-translator remaps. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
_run_helper assumed a POSIX host: it called os.getuid()/os.getgid() (absent on Windows) and mounted the helper and spec at their host paths, which are invalid container destinations for Windows C:\ paths. Decouple host paths from fixed in-container mount points (/opt/js-sam, /work), normalize -v sources to forward slashes, rewrite specPath to the container path, and pick a non-root --user via a hasattr(os, "getuid") guard (host uid:gid on POSIX, fixed 1000:1000 on Windows). Behavior is unchanged on Linux/macOS; the JS-SAM backend now runs on a Windows host against Docker Desktop. Verified by the existing container integration tests plus a real Phase 1/2 sandbox run.
claude-sonnet-4-20250514 retired 2026-06-15, so the `claude` entry
returned not_found. Repoint it to claude-opus-4-8.
Opus 4.7+, Fable 5, and Mythos 5 removed temperature/top_p/top_k and
return a 400 if any are sent. Dropping them from models.yaml is not
enough — the adapter falls back to GenerationConfig defaults and sent
temperature unconditionally, and litellm's drop_params does not yet
cover these newer models. Add _should_omit_sampling_params() (mirroring
_should_omit_top_p) and guard both temperature and top_p with it.
Verified end to end: get_configured_model("claude").generate_direct(...)
succeeds, and a full spin/JS-SAM run passes Phases 1, 2, and 4.
_display_evaluation_results prints ✓/✗ status glyphs, which raise UnicodeEncodeError on consoles whose default encoding can't represent them (e.g. Windows cp1252) — the evaluation succeeds, then the final summary print crashes. Reconfigure sys.stdout/sys.stderr to UTF-8 at startup; a no-op where they already speak it.
"States explored" was hardcoded to 0 for any backend that isn't TLA+: runtime_check only parsed it from TLC output, and the invariant evaluator never set the top-level field at all (so even TLA+ Phase 4 showed 0). The JS-SAM helper already returns stepsExplored — it just wasn't threaded through. Add states_explored to ModelCheckOutcome and populate it from the JS-SAM check response; seed runtime_check's states from the backend outcome (TLA+ still overrides via its own parse); and set the invariant evaluator's top-level states_explored to the sum across cases. Also fix the JS-SAM Phase-4 metadata key (steps_explored -> states_explored) so the evaluator actually reads it. Verified on spin/JS-SAM: Phase 2 reports 326592 steps (depthMax 6), Phase 4 reports 979776 (326592 x 3 invariants).
Adds the trace-capture harness for the spin task so JS-SAM Phase 3
(transition validation) runs against real Asterinas spinlock behavior
rather than being blocked on missing traces.
- scripts/harness/spin/run.sh: clone Asterinas v0.16.0 (LF), apply the
reference instrumentation + the 2-thread ktest patch, build+run under
QEMU-TCG on an ext4 docker volume, parse serial JSON into NDJSON.
- scripts/harness/spin/build_and_test.sh: in-container build+run.
- scripts/harness/spin/parse_traces.py: folds kernel events
(TryAcquireBlocking/AcquireSuccess/AcquireFail/Release) into
(pre, post) windows keyed on the objective {lockHeld, lockHolder}
state; JS-SAM's projection rule ignores model-internal bookkeeping.
- data/patches/spin_2thread_ktest.patch: adds test_spin_2thread, a
2-actor contention scenario (try_lock avoids single-CPU deadlock);
the reference ktests are single-actor.
- data/sys_traces/spin/spin_2thread.ndjson: the captured 8-window trace
set (force-added; traces are normally generated, not checked in).
The v0.16.0 pin (patch doesn't apply to main), LF normalization of the
clone and patches, and the ext4 build volume (host FS lacks fallocate)
are what make this Linux-oriented flow run under Docker Desktop on
Windows. Verified: Phase 3 scores 87.5% (7/8) on the Opus 4.8 spin model.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Documents the first four-phase JS-SAM run on the spin task (Opus 4.8): method, the Phase 3 kernel trace-capture pipeline, results (Phase 3 87.5%, with the try_lock-from-free modeling discrepancy), the cross-platform fixes, limitations, and reproduction steps. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Broadens Phase-3 coverage from 8 to 28 windows. test_spin_seq exercises alternating holders, try_lock successes, and repeated failed contention (still single-CPU-safe). build_and_test.sh now takes the ktest name as an argument and run.sh loops over both scenarios into per-scenario NDJSON. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Generalizes the agent-based invariant translator so backends other than TLA+ can use it instead of remapping to a single direct LLM call (maintainer Open Question 4). - New evaluation/semantics/agent_translation.py: language-neutral core (CLI selection, workspace setup, subprocess exec, output read). Caller supplies the workspace files, agent instructions, and output parser. - TLA+ AgentInvariantTranslator now delegates to it (behavior preserved; its _select_agent_cli/_execute_agent_cli move into the shared module). - JS-SAM translate_invariants: translator=claude-code/codex now drives the agent CLI (JS predicates against the generated spec, reusing the existing JSON parser); "claude"/explicit model still uses the direct call. End-to-end agent runs require the claude-code/codex CLI. - Tests mock the CLI boundary: shared-core success/missing-output/failure /codex paths, JS-SAM agent routing, and TLA+ delegation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds sonnet (Sonnet 4.6) and haiku (Haiku 4.5) model entries and records the three-model comparison across all four phases on the 28-window trace corpus. Transition validation (Phase 3) is the discriminating metric: Opus 89.3% > Sonnet 50.0% > Haiku 21.4%, while all three pass phases 1/2/4 — the clearest evidence that JS-SAM's signal is in reproducing real system behavior. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fable 5 (Anthropic's most capable model) scores only 50.0% (14/28) on Phase 3 — below Opus 4.8 (89.3%) and tied with Sonnet — despite passing phases 1/2/4. Cause is systematic: its model no-ops every ReleaseLock (0/11), leaving the lock held after release. Demonstrates that general capability rankings do not automatically transfer to formal-modeling accuracy, and that transition validation catches whole-action defects the other phases miss. Fable 5 model entry sends no sampling params or thinking config (both removed on that model; adapter's _should_omit_sampling_params covers it). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Feeds each model its own failing Phase-3 transitions (real pre/action/ post vs what its model produced) and asks it to fix the spec, then re-scores. One round, same 28-window corpus. Result — self-correction tracks capability, more sharply than one-shot: Opus 4.8 89.3% -> 100% (full repair) Fable 5 50.0% -> 100% (fully fixes its ReleaseLock defect, 0->100%) Sonnet 4.6 50.0% -> 60.7% (fixes AcquireLock; ReleaseLock still 0%) Haiku 4.5 21.4% -> 21.4% (no improvement) Fable's baseline defect turns out to be a recoverable slip, not a capability ceiling. Adds scripts/experiments/repair_phase3.py (driver) and docs/js_sam_repair_experiment.md (write-up + caveats). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Phase-3 repair driver was placed under scripts/experiments/, which is gitignored, so the prior commit shipped the write-up without the script it references. Move it to scripts/repair_phase3.py and fix the doc reference. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Head-to-head on spin (same 4 models). Both languages: 4/4 pass syntax (P1). They diverge at model-checkability (P2): JS-SAM 4/4, TLA+ 1/4. Attributed precisely: - Opus & Sonnet: unbounded `CHOOSE v : v \notin Threads` for "no owner" — SANY accepts, TLC rejects. A TLA+ semantic trap absent in JS (native null). Caught 2/4 models incl. the strongest. - Haiku: harness config generation fell back -> no usable .cfg (0 states) — a config surface JS-SAM's self-contained module avoids entirely. - Fable: clean (574 states, 7 invariants). Direct evidence for the JS-SAM hypothesis, with honest caveats (the TLA+ gap mixes a real pitfall with a config-gen shortfall; single task; direct translator; Phase 3 not compared). Also fixes scripts/setup_tools.py: shutil.move ran inside the open NamedTemporaryFile block, truncating tla2tools.jar / CommunityModules on Windows (broken zips -> ClassNotFoundException: tla2sany.SANY). Flush and close before moving, and verify the byte count against Content-Length. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…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
…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
4 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.
What this adds
The finixpos task and study: a SysMoBench case study on a production restaurant POS ↔ PAX A920 Pro ↔ Finix payment state-alignment protocol, written in SAM semantics. This branch is the artifact set referenced by the companion arXiv article ("Artifacts and reference models at https://github.com/jdubray/SysMoBench-1").
Task + corpora
tla_eval/tasks/finixpos/— task.yaml, pinned 7-variable observable-state contract, prompts for three arms (JS-SAM / leannext()/ constrained TLA+), verbatim source packet with provenance (EXTRACTION.md).data/sys_traces/finixpos*— four real-execution trace corpora (75/101-window pre-fix, 24-scenario post-fix v1/v2), generated by an instrumented copy of the production workflow against the repo's own terminal emulator + failure-injection proxy (data/patches/finixpos_trace.patch).trace_loader.pyextended to the harness's{pre, action, data, post}event form (+ test).Reference models + correctness deliverable
reference/FinixPOS*.tla): base + environment, crash/staleness/two-attempt/refund extensions, patched-semantics variants; annotated counterexamples for every confirmed gap; mutation + positive controls (CONTROLS.md).reference/sandbox_repro/) — including the demonstrated code/emulator-vs-real-rails 422-shape divergence.CONTAMINATION.md,EXTENDED_FAILURE_MODEL.md,corpus_coverage.md.Study
scripts/finixpos_tv.py(mechanical three-arm replay),finixpos_phase3_study.py(resumable, prompt-cached), rescore/analysis/post-fix scripts.output/finixpos_*).next()contract is best-or-tied and never unscoreable for all seven models across two vendors; TLA+ deficits are dominated by checkability + the guard idiom; semantic error is language-independent. The cross-vendor replication is of ordering and taxonomy, not level.docs/finixpos_study_results.md(design:docs/finixpos_study_plan.md).Not included
The article itself (published independently on arXiv) and the production-code fix patches (maintained in the POS repo).
.gitignoreupdated accordingly.Validation
make testadditions: trace-loader event-form test passes (one pre-existing unrelated failure on clean tree, documented in results doc).🤖 Generated with Claude Code
https://claude.ai/code/session_011bXyeoAhL6iz3CibTtU2Qv