1 Introduction↩︎

Formal specifications are among the most effective tools for establishing the correctness of concurrent and distributed systems [1], and among the least used: writing them demands rare expertise and sustained effort. LLMs raise an obvious question, namely whether they can write specifications for us, and a harder one: how would we know if they got it right? A generated specification can be syntactically flawless, explore cleanly under a model checker, satisfy plausible invariants, and still describe a system that does not exist. The SysMoBench benchmark [2] confronts this directly. Its authors observed that when asked to model Etcd’s Raft implementation, a frontier LLM produced, in effect, the specification from the appendix of the Raft paper, a “textbook” model with little connection to the implementation at hand [3]. SysMoBench therefore grades specifications in four phases of increasing demand: (1) syntax, (2) runtime model checking, (3) transition validation, which replays \((\mathit{pre}, \mathit{action}, \mathit{post})\) windows captured from real executions against the generated model, and (4) invariant verification.

SysMoBench was built for TLA⁺ [4], and has since grown a pluggable backend interface with Alloy [5] and PAT/CSP# [6] backends. All three are formal languages, and all three are rare in LLM training corpora relative to mainstream programming languages. This asymmetry motivates the extension we present here.

1.0.0.1 The JS-SAM hypothesis.

SAM [7], [8] is a software-engineering pattern whose semantics are explicitly derived from TLA⁺: actions compute proposals from inputs, a model accepts or rejects proposals as the sole locus of mutation, and state is a pure function of the model. A SAM specification is an ordinary executable JavaScript module. JavaScript is plausibly the single most abundant programming language in LLM training data. The hypothesis, then:

Can an LLM produce a correct specification of a real system more readily in a pattern hosted by a language it has seen constantly in training (JavaScript), than in formal languages it has rarely seen, while preserving the TLA⁺-style discipline that makes the artifact checkable?

Either answer is informative. If JS-SAM scores diverge upward, host-language familiarity dominates and formal syntax is a bottleneck; if scores match or fall, the hard part is modeling, not notation.

1.0.0.2 Contributions.

This paper reports the first end-to-end results from the JS-SAM backend, all on the SysMoBench spin task (the Asterinas OS spinlock [9]):

1. A non-formal-language backend for SysMoBench (§3): the JS-SAM module contract, a sandboxed execution helper, and, a first for the benchmark, a direct Phase-3 replay path requiring no coding-agent orchestration, because SAM’s step relation is \(\mathit{model.present}(\mathit{action}(\mathit{data}))\).

2. A reproducible kernel trace-capture methodology (§4): instrumenting the real Asterinas spinlock, driving a two-thread contention scenario in a single-CPU kernel test without deadlock, and folding low-level kernel events into model-independent \((\mathit{pre}, \mathit{action}, \mathit{post})\) windows, producing the 28-window corpus used throughout.

3. A four-model comparison (§5) showing that Phases 1, 2, and 4 have no discriminating power on this task while Phase 3 spreads the models from 0% to 86.4% on state-changing windows (21.4% to 89.3% headline, against an identity base rate of 21.4%), and that general model capability does not predict modeling accuracy: the most capable model tested produced a specification that no-ops every lock release.

4. A repair-loop experiment (§6) demonstrating that self-correction from precise trace feedback is a distinct capability axis from one-shot accuracy: capable models repair fully (verified by a held-out generalization audit as fixes, not memorization), the weakest not at all, with mid-tier outcomes unstable at \(N{=}1\).

5. A JS-SAM-vs-TLA⁺ evaluability comparison (§7): 4/4 JS-SAM specifications reach end-to-end evaluability versus 1/4 for TLA⁺, reported strictly per cause (a known TLC idiom trap twice, a harness fault once) and shown to vanish under a one-line prompt guardrail: a default-prompt robustness observation, not a language-capability finding.

6. A controlled cross-language conformance study (§8): a pre-registered, paired design realized as a full \(3{\times}2\) factorial in (contract, prompt) (\(N{=}5\) generations per cell), pinning both languages to the same observable-state contract and replaying the same trace corpus mechanically in both. The completed factorial attributes the conformance gap to the SAM contract’s machinery, not to the JavaScript language, not to formality, and not (as an incomplete design had suggested) primarily to prompt prescriptiveness: the bare-next contract reaches 100% for every model without the semantics block, while the semantics block within SAM moves only two of four models. This yields a concrete design change for the backend, validated by 40/40 bare-next specifications passing every phase across two tasks (§8.4).

7. A consensus-class boundary study (§9): the bare-next contract carried to Etcd Raft, a 97-window corpus captured through the implementation’s own trace instrumentation, validated by a hand-written reference specification at 100%, where 0 of 20 one-shot bare-next specifications pass every phase. The failure analysis separates what the contract still buys (transcription, evaluability) from what it cannot (semantic derivation, and a specification-vs-program distinction the strongest model reasons its way past), and a one-round repair experiment stratifies the four models into convergent, slowly convergent, regressing, and plateaued.

8. An ecological check on the deployed TLA⁺ path (§7.3): the benchmark’s agent-mediated Phase 3, run on the Experiment-3 specifications, confirming the harness-vs-model attribution of the evaluability gap and exposing a scoring-semantics difference between the deployed and controlled oracles.

In light of the results, we regard the trace-capture methodology (2), the controlled-comparison methodology (6), and the contract-shape finding as the primary contributions; the JS-SAM backend (1) is the vehicle that surfaced them, and its own results argue for the bare-next revision of its contract.

1.0.0.3 Scope of claims.

Four boundaries govern everything that follows, and we state them before the results rather than after. (i) Checkable, not verifiable. What this paper demonstrates is that executable JavaScript specifications can be checked: bounded safety exploration over reachable states, and conformance replay against finite execution traces. It does not demonstrate verification in the sense TLA⁺ enables: no liveness or temporal-logic properties, no fairness, no unbounded state spaces, no mechanical proof (§10). (ii) Task scale. The controlled factorial concerns one system, the spinlock, a 28-window corpus, with the bare-next-contract validation extending to a second task (a distributed lock service, 60 windows) and to a third at consensus scale (Etcd Raft, 97 windows; §9). The Raft study tests only the bare-next contract: the factorial’s SAM and TLA⁺ arms remain spinlock-only, so the contract-vs-prompt ordering is still conditional on the small tasks. (iii) Controlled and ecological, reported separately. The cross-language comparison uses a direct, mechanical TLC replay; the benchmark’s deployed agent-mediated TLA⁺ Phase 3 was run on the same specifications (§7.3) and confirms the per-cause attribution, but the two paths score different window sets under different oracles and their numbers are not interchangeable (§10). The comparison is to TLC specifically, not the wider TLA⁺ toolchain. (iv) Limited statistical resolution. Experiments 1–3 are single-generation; the factorial runs \(N{=}5\) per cell, where the exact permutation test’s smallest attainable \(p\) is \(2/252\approx0.0079\): effect sizes, not \(p\)-values, are the primary quantities throughout. We present the study as a case study whose value lies in the precision of the failure attribution and the reproducibility of the pipeline, not as a settled verdict on the hypothesis (§12).

2 Background↩︎

2.1 SysMoBench↩︎

SysMoBench [2] pairs eleven real systems (concurrent synchronization primitives and distributed protocols, from the Asterinas spinlock to Etcd Raft) with instrumentation harnesses and expert-written invariants. Given the system’s source, an LLM generates a specification, which is scored in four automated phases:

Phase 1, Syntax.

Does the specification parse and structurally validate? (For TLA⁺: the SANY analyzer.)

Phase 2, Runtime model checking.

Does bounded state-space exploration terminate without errors, deadlocks, or nondeterminism? (For TLA⁺: TLC [10].)

Phase 3, Transition validation (conformance).

Execution traces from the real system are cut into windows \((\mathit{pre}, \mathit{action}, \mathit{post})\); each window passes if the generated model, started at \(\mathit{pre}\) and applying \(\mathit{action}\), produces \(\mathit{post}\). The output is a per-action scorecard.

Phase 4, Invariant verification.

Expert invariants (e.g., mutual exclusion) are translated into the specification’s language and checked.

The benchmark’s central published finding is that frontier LLMs cluster near 100% on syntax but average roughly 46% on conformance and 41% on invariants [3]: models write valid TLA⁺ fluently yet describe the textbook protocol rather than the implementation. Phase 3 exists precisely to distinguish “writing TLA⁺” from “modeling this system.”

2.2 The SAM pattern↩︎

SAM (State-Action-Model) [7], [8] factors a program’s temporal behavior the way TLA⁺ factors a specification. An action is a pure function from inputs to a proposal; the model alone decides whether to accept a proposal and mutate itself (the analogue of a TLA⁺ next-state relation, with acceptors playing the role of guards); state is a pure function of the model. A step of the system is \(\mathit{model.present}(\mathit{action}(\mathit{data}))\). The pattern is implemented by the sam-pattern library [11], which also provides a bounded explorer (checker) over the model’s reachable states; in the JS-SAM backend, this checker is what executes Phases 2 and 4.

Two properties make SAM suitable as a specification substrate. First, the semantic alignment with TLA⁺ means the benchmark’s phases map onto it without distortion: bounded exploration is Phase 2, replaying a trace window is literally one SAM step, and invariants are predicates over \(\mathit{getState}()\). Second, the artifact is an executable JavaScript module: there is no separate tool chain between the specification and its own evaluation.

3 The JS-SAM backend↩︎

SysMoBench backends implement a LanguageBackend interface and register themselves; the CLI and the four evaluators resolve them by name with no further plumbing. The JS-SAM backend consists of a Python adapter and a small Node.js helper (tools/js-sam/cli.mjs) with four subcommands (validate, check, transitions, invariants), one per phase.

3.0.0.1 Module contract.

The generation prompt instructs the model to emit a single CommonJS module:

module.exports = {
  instance,       // SAM instance (synchronous steps)
  init,           // () => void : reset to the initial state
  actions,        // { AcquireLock: (data)=>void, ReleaseLock: (data)=>void }
  getState,       // () => plain JSON-serializable snapshot
  setState,       // (snapshot) => void : force a state (Phase 3 replay)
  checkerIntents, // action descriptors + input domains (Phases 2 & 4)
};

actions must cover exactly the task’s target actions; getState must return a plain object (this is what trace states are diffed against); setState exists solely so Phase 3 can replay a window without searching for a path to its pre-state; and the module must be deterministic and I/O-free. checkerIntents declares each action’s finite input domain (for spin, every \(\{\mathit{thread}, \mathit{callType}\}\) combination), playing the role of a TLA⁺ constants block. Notably, there is no separate configuration artifact: the module is self-contained, a fact that becomes material in §7.

3.0.0.2 Sandboxing.

Model-generated JavaScript is untrusted. Every helper invocation runs in a throwaway node:20-slim Docker container with no network, a read-only root filesystem, a non-root user, and CPU/memory/PID caps. The container is the trust boundary.

3.0.0.3 The direct Phase-3 path.

For TLA⁺, SysMoBench’s transition validation drives TLC through a coding-agent workflow that constructs a checking module per window. JS-SAM needs none of that: the evaluator loads the module, and for each window executes setState(pre); actions[name](data); and diffs getState() against post under the benchmark’s projection rule (only keys present in the trace’s post-state must match, so model-internal bookkeeping is ignored). This “direct path” is the first non-agent Phase-3 implementation in the benchmark, and it follows from SAM’s semantics: a window is a SAM step.

3.0.0.4 Cross-platform engineering.

Making the pipeline run on a Windows host (in addition to Linux/macOS) required fixing several host assumptions in the harness (POSIX-only os.getuid() calls, host-path container mounts invalid for C:\ paths, and console encoding), plus threading the helper’s stepsExplored metric through a field previously hardcoded to zero for non-TLA⁺ backends. We also generalized the benchmark’s agent-based invariant translator (previously TLA⁺-only) into a shared, language-neutral component that JS-SAM can use, although all experiments below use the direct translator for parity across languages. These changes are upstreamed as pull requests.

4 Capturing ground truth: kernel traces for Phase 3↩︎

Phase 3 is the only phase requiring data external to the model, and SysMoBench does not ship trace corpora: traces are generated on demand by instrumenting the real system. Additionally, the maintainers’ own spin captures use three threads while the JS-SAM prompt models two, so the backend required its own corpus at the granularity it models. This section documents the pipeline; it is the experimental setup’s main methodological contribution and is fully reproducible from a single script.

4.1 Pipeline↩︎

1. Pin a compatible revision. The reference instrumentation patch applies cleanly at Asterinas v0.16.0 (matching the toolchain in the asterinas/asterinas:0.16.0 image), not at main.

2. Instrument. Apply the benchmark’s reference patch, which adds a trace module to the kernel’s spinlock emitting one serial JSON event per lock operation, plus a new two-thread kernel test (below).

3. Build and run. Inside the container: build the initramfs and run the instrumented kernel test under QEMU (software emulation), collecting the event stream from the serial port.

4. Parse. Fold the event stream into \((\mathit{pre}, \mathit{action}, \mathit{post})\) NDJSON windows.

4.2 A two-thread contention scenario without deadlock↩︎

The reference spinlock kernel tests are single-actor: every operation is attributed to one thread, so contention, the behavior that makes a lock interesting, never appears in the trace. But a blocking lock() from a second actor in a single-CPU kernel test would spin forever. The scenario therefore expresses the second actor’s contention through non-blocking try_lock calls that fail without blocking:

actor0.lock()      -> TryAcquireBlocking(0), AcquireSuccess(0)  // 0 holds
actor1.try_lock()  -> AcquireFail(1)          // contention, no deadlock
actor0.release()   -> Release(0)
actor1.lock()      -> TryAcquireBlocking(1), AcquireSuccess(1)  // 1 holds
actor0.try_lock()  -> AcquireFail(0)          // contention
actor1.release()   -> Release(1)
actor0.try_lock()  -> AcquireSuccess(0)       // try from free succeeds
actor0.release()   -> Release(0)

A second, longer scenario (more alternation of the holder, more failed and successful try_lock attempts, and same-thread reacquisition) extends the corpus from 8 windows to 28 windows (17 AcquireLock, 11 ReleaseLock), the corpus used in all experiments below.

4.3 Model-independent state windows↩︎

The kernel emits low-level events (TryAcquireBlocking, AcquireSuccess, AcquireFail, Release). The parser folds these into windows keyed on the objective spinlock state, \(\{\mathit{lockHeld}, \mathit{lockHolder}\}\), the real observable ownership, and relies on the projection rule to ignore any model’s internal bookkeeping (thread status, call type). A failed acquire under contention produces a window whose post-state ownership is unchanged; a successful acquire records the new holder together with whether it arrived via the blocking (lock) or non-blocking (try) path. Keying the corpus on observable state keeps the ground-truth oracle independent of any model under test.

5 Experiment 1: four models, four phases↩︎

5.1 Setup↩︎

Four Claude models spanning the capability range (Haiku 4.5, Sonnet 4.6, Opus 4.8, and Fable 5, Anthropic’s most capable model at the time of writing) each generated one JS-SAM specification for spin. These are the models’ production names, not pseudonyms; the exact API identifiers are claude-haiku-4-5, claude-sonnet-4-6, claude-opus-4-8, and claude-fable-5 (accessed May–July 2026), pinned in the repository’s config/models.yaml. Each model generated via a single prompt (direct_call), and the same artifact was scored in all four phases. Phase 2 and 4 exploration ran through the sam-pattern library’s bounded checker at the task’s default depth bound of 6; Phase 3 used the 28-window corpus; Phase 4 checked three expert invariants (MutualExclusion, LockStatusConsistency, NoDeadlock) translated via the direct API path.

5.2 Results↩︎

Two results stand out.

5.2.0.1 Only the reality check discriminates.

Every model passes Phase 1, Phase 2, and Phase 4. On this task those three phases have zero discriminating power. The checker reports an identical 326,592 “states explored” per model, but that number is not evidence of structurally equivalent state spaces: it is the checker’s step count, that is, safety-callback invocations over the intent-permutation tree, \((d{+}1)\cdot 6^{d} = 7\cdot 6^{6}\), a pure function of the contract-pinned intent domain and depth bound, identical for any conforming spec and therefore model-independent. Counting distinct semantic states (unique model snapshots) instead separates the specs: 7 for Opus, Fable, and Sonnet, but 1 for Haiku, whose intent actions drop their arguments so every proposal is rejected, so its exploration never leaves the initial state. Haiku’s Phase-2 pass is thus vacuous (no crash, deterministic, and serializable hold trivially for a spec that cannot move), and its Phase-4 invariants are satisfied over that single state. Phase 2 verifies checkability, not semantic adequacy; the distinct-state count, now reported by the checker, is the semantic signal. Phase 3 spreads the models across a \(4\times\) range, and, restricted to comparisons it can make, orders Opus above the mid tier above Haiku. A base-rate audit sharpens the spread: 6 of the 28 windows (all contention acquires) have post \(=\) pre, so the identity function scores 21.4% overall and 35.3% on acquires. Haiku’s column is exactly that base rate: its “Acquire 6/17” is precisely the six freebies, and it passes zero windows requiring a state change, so conditional on the 22 change windows the spread is not 21.4–89.3% but 0–86.4% (Opus 19/22, Fable and Sonnet 8/22, Haiku 0/22). Every arm of every model collects all six freebies; the conditional-on-change rate is the discriminating metric and accompanies headline rates hereafter. This independently reproduces, in a non-formal language, the central SysMoBench finding for TLA⁺: internal consistency is cheap; conformance with the real system is where specifications fail [3].

5.2.0.2 General capability does not predict modeling accuracy.

The most striking column is Fable 5, the most capable model tested, scoring 50%, below Opus 4.8 and tied with mid-tier Sonnet. The cause is specific and systematic, not noise: Fable’s specification handles acquisition competently (14/17) but no-ops every single release (0/11). After any ReleaseLock, its model leaves the lock held:

ReleaseLock  expected {lockHeld: false, lockHolder: null}
             got      {lockHeld: true,  lockHolder: 0}

The release logic reads correctly in isolation (it guards on the holder, then clears the state) but on replay the release never takes effect: a categorical, whole-action modeling defect. Crucially, this specification passed syntax, completed the full bounded exploration (7 distinct states) without violation, and satisfied all three invariants, including mutual exclusion. (Its release does fire when reached from the initial state, where its auxiliary threadStatus guard holds; the defect is that replay pins only the observable pre-state, leaving the guard unsatisfiable, so exploration from init cannot expose it.) Only replay against the real kernel’s transitions caught it.

The recurring failure among the passing acquisitions is also precise: all three 14/17 models fail exactly the three try_lock-from-free windows, the non-blocking acquire that should succeed on a free lock. Blocking acquisition (abundant in training data and in textbook treatments) is modeled correctly by every model except Haiku; the less common non-blocking path is where they slip. This echoes, at micro scale, SysMoBench’s “textbook modeling” diagnosis: models reproduce the familiar template and miss the implementation-specific path.

6 Experiment 2: repair from trace feedback↩︎

6.1 Setup↩︎

If a model is shown exactly which transitions its specification got wrong (the pre-state, the action and its data, the real system’s post-state, and what the model produced instead), can it fix the specification? For each model we ran one repair round: score the original specification on Phase 3; build a repair prompt containing the full original module plus every failing window; ask the model to rewrite the module; confirm the result still passes Phase 1; re-score Phase 3 on the same 28-window corpus.

6.2 Results↩︎

6.2.0.1 Self-correction separates the models, but the middle tier is noise.

In the run of Table 2, Opus and Fable repair to a perfect 28/28 in a single round, Sonnet repairs partially (it fixes the try_lock acquisition defect but not its release path), and Haiku does not improve at all: superficially a clean three-tier gradient (full / partial / none). A replication run (part of the generalization audit below, with artifacts saved) revised this: Sonnet also repaired to 28/28. The boundary that is stable across both runs is two-tier: Opus, Fable, and (unstably) Sonnet can exploit transition-level feedback; Haiku cannot; and single-round repair outcomes for mid-tier models are sampling-dependent at \(N{=}1\).

6.2.0.2 The Fable reversal.

Fable’s baseline looked no better than Sonnet’s, and its failure mode, a whole action silently broken, looked worse. Yet under repair, Fable fully recovers: its release defect was a recoverable slip, not a capability ceiling. One-shot specification accuracy and repair-from-feedback are different axes of capability, and a benchmark that measures only the former will misrank models for any workflow that includes a correction loop, which realistic agentic formal-modeling workflows do [3].

6.2.0.3 Generalization audit: the repairs are fixes, not memorization.

Repaired specifications were originally re-checked only on Phases 1 and 3, on the same 28 windows quoted in the repair prompt, leaving open that a repair might memorize the failing windows (branch on the pre-state, return the expected post), which would make this an experiment about prompt-following rather than modeling. An audit re-ran the repair loop with artifacts saved and scored each baseline and repaired specification on the seen corpus, on held-out windows, and on Phases 2 and 4. The 28 seen windows collapse to 8 distinct (pre-state, action, data) combinations; the held-out set is the 10 combinations of the observable domain the corpus never shows (acquire on a held lock, release by a non-holder, release of a free lock). All repaired specifications pass all held-out windows, reach the same 7 distinct semantic states as a correct specification under bounded exploration (Haiku’s unrepaired specification remains at 1), and hold all invariants. Direct inspection found no memorization (no state-equality tables or window literals); the successful repairs are the same root-cause fix, moving the release ownership check from the auxiliary threadStatus guard (unsatisfiable under a pinned observable pre-state) to the authoritative lockHeld/lockHolder, with Sonnet’s repair documenting the diagnosis in a comment. One structural honesty note: because the kernel instrumentation emits acquire events at acquisition success, every held-out combination is an observable no-op, so held-out scoring alone refutes only memorizers with unsafe defaults; the inspection and Phase-2/4 evidence carry the conclusion, and a state-changing held-out set (as locksvc affords) is the right vehicle for a stronger version of this audit.

6.2.0.4 What this does and does not measure.

The repair prompt contains the failing windows themselves, so the experiment measures “can the model exploit precise, correct feedback,” not blind improvement. That is the intended question (it is exactly the signal available inside an agentic repair loop) but it is not a from-scratch re-test. A multi-round follow-up (scripts/repair_multiround.py) answers the convergence question: Haiku does not converge (three rounds of full-failure feedback leave it at 6/28 with its exploration still confined to one state, 6\(\to\)​6\(\to\)​6, with every round’s spec saved and audited), while Sonnet full-repairs in round one again (its second full repair in three runs, further evidence the original “partial” tier was a sampling artifact).

7 Experiment 3: JS-SAM versus TLA⁺↩︎

7.1 Setup↩︎

The head-to-head the backend exists to inform: the same four models, the same spin task, one direct_call generation per model per language, scored on Phase 1 (syntax: SANY vs.module validation), Phase 2 (model checking: TLC vs.bounded exploration), and Phase 4 (invariant verification, direct translator for both languages). Phase 3 is deliberately not compared: JS-SAM’s Phase 3 is a self-contained direct replay while TLA⁺’s is a heavyweight coding-agent path, that is, different mechanisms rather than a fair one-to-one. Phase 4 is compared as pass/fail because the two languages ship different invariant-template counts for spin (seven for TLA⁺, three for JS-SAM), and the JS-SAM three are safety-only, a qualitative weakness examined in §12: as implemented, JS-SAM Phase 4 could not have failed the never-releasing defect of §5 in principle.

7.2 Results↩︎

Table 3 summarizes the per-phase outcome and Table 4 the per-model TLA⁺ detail.

7.2.0.1 Syntax is not where the languages differ.

Every model writes syntactically valid specifications in both languages, consistent with SysMoBench’s finding that frontier models have essentially saturated TLA⁺ syntax [3]. The divergence is at Phase 2: whether the specification is actually checkable. All four JS-SAM modules run; one of four TLA⁺ specifications does. Each TLA⁺ failure is attributable to a specific structural cause.

7.2.0.2 Cause 1: a TLA⁺ semantic pitfall JavaScript does not have.

Opus and Sonnet both modeled “no lock owner” as NULL == CHOOSE v : v \notin Threads. SANY accepts this (syntax passes) but TLC cannot enumerate a CHOOSE whose bound variable ranges over an unbounded domain (CHOOSE itself is deterministic), so model checking fails. The idiom is natural, looks correct, and is a well-known TLC trap, though the indictment is of LLM TLA⁺ fluency rather than of the language: no experienced TLA⁺ author models absence this way, and agentic workflows already write around it in practice [12]. JavaScript has a native null, so the corresponding JS-SAM specifications express the same concept with no trap available to fall into. This structural hazard caught two of four models, including the model with the best JS-SAM conformance score (Opus). It is a clean instance of the hypothesis’s mechanism: the failure is not “the model cannot model a spinlock” (its JavaScript model of the same system scored 89.3% against real traces) but “the formal language exposes a semantic surface on which competent models slip.”

7.2.0.3 Cause 2: a configuration surface JS-SAM does not have.

TLA⁺ model checking requires a separate .cfg artifact (constants, init/next, invariants) that the harness must generate to match the specification; for Haiku, that generation fell back and produced no usable configuration (zero states explored). A JS-SAM module is self-contained and executable: there is no second artifact to generate, so this entire failure mode is structurally absent. We flag the attribution honestly: the CHOOSE failures belong to the models; the Haiku failure belongs to the harness. But the asymmetry itself is structural: one language’s evaluability depends on a fragile secondary artifact and the other’s does not.

7.2.0.4 Net.

On this task, models reach an end-to-end evaluable specification far more readily in JS-SAM (4/4 through Phase 4) than in TLA⁺ (1/4). Read narrowly, this is evidence for the hypothesis in its practical form: host-language familiarity plus a self-contained executable artifact lowers the barrier to a usable specification. It does not, by itself, show that JS-SAM specifications are more faithful; it shows they are far more often checkable at all, which is the precondition for faithfulness to be measured. And given the per-cause attribution above and the guardrail result of §8, we treat the 4/4-vs-1/4 figure throughout this paper as a within-experiment observation about default-prompt robustness, not a conclusion about the languages, and as a lower bound on TLA⁺: a one-line prompt guardrail removes the gap entirely (§8), and deployed agentic workflows already write around the CHOOSE idiom [12]. One asymmetry in this experiment must be named at the point of claim rather than in the limitations: the 1/4 figure is a one-shot number for a language whose failures we have just argued are trivially repairable, whereas the JS-SAM side receives a repair round in Experiment 2. Symmetry, together with Erik Meijer’s suggestion in review that a fair comparison must steer and repair the larger-surface-area language on the same terms [13], demands the same for TLA⁺: one repair round per failing specification (the model’s own specification, its configuration, and TLC’s verbatim error output, nothing else) repairs both. Sonnet’s rewrite adopts the string sentinel the guardrail prescribes (NULL == "NULL"; TLC passes, 111 distinct states); Opus keeps the CHOOSE but bounds it over a singleton set (TLC passes, 159 distinct states); both preserve the action structure. Carried through the invariant pipeline, both repaired specifications hold all seven expert invariants (7/7 each, matching the one TLA⁺ specification that passed unrepaired), after resolving one further harness artifact the rescore itself exposed: the pipeline appends each translated invariant under its template name, so a specification that defines its own MutualExclusion, as Sonnet’s repair does, draws a duplicate-definition parse error that scores as an invariant failure. Per this paper’s per-cause discipline we report that as a benchmark defect, not a specification one. The 1/4 figure is thus bounded from two directions: a one-line guardrail prevents the failure, and one round of TLC feedback repairs it fully, consistent with the repair-axis findings of Experiments 2 and 5, and further evidence that the evaluability gap is shallow. Experiment 4 (§8) measures faithfulness directly, under a design built to make the two languages comparable, and resolves it in an unexpected place.

7.3 The deployed agent-mediated path↩︎

It is worth asking what the benchmark’s as-deployed TLA⁺ Phase 3 (a coding agent that instruments the system, captures traces, cuts windows, and drives TLC per window) makes of these same four specifications. We ran it: each Experiment-3 specification through the deployed launcher, with a fresh QEMU kernel capture per run and the scope pinned to the two target actions (Table 5).

Three observations follow, each modest but worth stating precisely.

First, the per-cause attribution of Experiment 3 survives the ecological test. The harness configuration fault does not exist on the deployed path (the agent writes its own configurations and checking modules), so Haiku’s specification becomes evaluable, confirming that failure belonged to our harness. The CHOOSE idiom persists: the agent reproduced the failure against the pristine specification and its own original configuration, and correctly concluded that no checking-side workaround exists, since the sentinel is a derived operator rather than a rebindable constant. Deployed evaluability is therefore 2/4, against 1/4 controlled; the deployed path is the more forgiving instrument, and what remains is exactly the model-written idiom.

Second, the two paths do not measure the same thing. The deployed agent excluded the six contention no-op windows as out of scope (documented exclusions, with precedent in the benchmark’s reference materials), where the controlled oracle requires them as identity transitions. Deployed and controlled pass rates are computed over different window sets and should not be compared numerically.

Third, and most consequential for interpreting agent-mediated scores, the deployed oracle is interpretive. Haiku’s specification models AcquireLock as request initiation (idle to trying, ownership unchanged) rather than as acquisition success. The agent read the specification, cut its windows on the corresponding trace events, and scored it 19/19, a perfect score on the specification’s own reading of the action names, for the same model whose JS-SAM specification scored the identity base rate against the pinned-schema oracle. Neither score is wrong; they answer different questions. The pinned oracle asks “does the specification reproduce the agreed observable semantics”; the agent asks “is the specification consistent with the traces under its own vocabulary.” The gap between those questions is invisible until one runs both instruments on the same artifact, which is the practical argument for keeping a controlled conformance mode alongside the deployed one (§10).

8 Experiment 4: cross-language conformance under a controlled contract↩︎

Experiment 3 could not compare Phase 3 across languages because the two backends implement it by incomparable mechanisms: JS-SAM runs a mechanical replay, while TLA⁺ runs a coding-agent path, necessary because a free-form TLA⁺ specification invents its own variable names, so mapping trace states onto spec states requires interpretation. A naive comparison would measure the replay machinery, not the specifications. This experiment removes that asymmetry with a pre-registered, paired design; the full methodology note, written to be socialized with the benchmark maintainers, is included in the artifact repository.

8.1 Design↩︎

8.1.0.1 Equalize the observable-state contract.

The degree of freedom that forces TLA⁺ onto the agent path, namely free choice of variables, is one the JS-SAM prompt already removes by pinning getState()’s shape. We remove it symmetrically: a constrained TLA⁺ prompt mandates VARIABLES lockHeld, lockHolder (the trace schema), action operators AcquireLock(thread, callType) / ReleaseLock(thread), and a TLC-safe sentinel (NONE == "none", not CHOOSE). Both languages then answer the identical question, namely express this system over this observable state, and trace states map onto spec states with no interpretation.

8.1.0.2 A direct TLC replay path (no agent), functional on both sides.

With the contract fixed, TLA⁺ transition validation becomes mechanical, mirroring JS-SAM’s setState \(\to\) action \(\to\) diff: for each window, a synthesized module pins the pre-state in its initial predicate and takes exactly one step of the window’s action. Mere reachability of the traced post-state would be too weak a criterion: a TLA⁺ action is a relation, and an over-permissive action can reach the correct post-state while also admitting wrong ones, passing an existential check that the functional JS replay (one next state, compared exactly) would fail. The replay therefore enforces the same functional relation on both languages: it enumerates the action’s one-step image from the pinned pre-state and requires that the image be exactly the traced post-state (branching factor 1; over-permissiveness fails the window). The check was validated in three directions: a contract-following specification passes 28/28 (positive control); the same specification with ReleaseLock mutated to a no-op fails exactly the 11 release windows (negative control); and a deliberately permissive specification (holder set to any thread on acquire) passes 28/28 existentially but only 11/28 functionally, with branching factor 2 (permissive control), demonstrating that the functional check is strictly stronger and necessary. An audit of all 20 generated TLA⁺ specifications found every one deterministic: existential and functional scores coincide on every window, and the maximum branching factor is 1. The TLA⁺ results below are therefore earned under a relation as strict as the JS one, not inflated by existential slack.

Two commitments of this oracle must be named, because they are modeling-paradigm choices rather than neutral ground. First, requiring every trace event to map onto a named, total, successor-producing action is the bare-next/JS paradigm by construction. Idiomatic TLA⁺ specifies enabling conditions and relies on stuttering (\([\mathit{Next}]_{\mathit{vars}}\) always admits \(\mathit{vars}' = \mathit{vars}\)): a failed acquisition is naturally a disabled action plus a stutter, which this oracle scores as unscoreable rather than as a legitimate no-op, penalizing enabling-condition specifications independent of their correctness. Wherever the cross-language comparison is drawn, we therefore report the conditional (paradigm-fair) score alongside the unconditional one, and we flag a stutter-aware oracle (a \(post = pre\) window satisfiable by a stuttering step) as the fairer instrument for such specifications. Second, the functional branching-factor-1 requirement encodes a determinism assumption that holds here only because the trace scenarios are deterministic by construction; for genuinely concurrent systems a relational next-state is fidelity, not over-permissiveness, and the oracle must weaken to set-conformance (traced post-state in the one-step image, with tightness reported separately) before this methodology reaches Raft-class protocols.

8.1.0.3 Four arms, because the prompt and the contract are both confounds.

An initial two-arm run (deployed JS-SAM prompt vs.constrained TLA⁺) produced what looked like a decisive TLA⁺ reversal. But the constrained TLA⁺ prompt states the exact single-step observable semantics (free \(\to\) acquire; held \(\to\) unchanged; holder \(\to\) release), which the deployed JS-SAM prompt does not: a difference in prompt content, not in language. And even with prompts equalized, the two substrates still differ in a second way: the SAM contract obliges an executable module with proposal/acceptor wiring and auxiliary state, while the TLA⁺ specification is a bare two-variable relation. We therefore ran four arms initially: JS(deployed), the shipped JS-SAM prompt; JS(constrained), the deployed prompt plus the identical semantics block used by the TLA⁺ arm; plain-JS, the same constrained semantics, but the specification is a bare next(state, action, model) transition function (argument names follow SAM usage) over only \(\{\mathit{lockHeld}, \mathit{lockHolder}\}\): JavaScript, yet structurally isomorphic to the TLA⁺ relation, with no SAM library and no auxiliary state; and TLA(constrained). JS(constrained) vs.TLA(constrained) varies language and contract together; plain-JS vs.TLA(constrained) varies only the language; JS(constrained) vs.plain-JS varies only the contract.

8.1.0.4 Completing the factorial: the missing bare-next-without-semantics cell.

These arms form an incomplete \(2{\times}2\) in (contract, prompt): the bare-next arm always carried the semantics block, so “contract minimality buys transcription fidelity” was established only conditional on spec-level semantics in the prompt, and any prompt-vs-contract effect ordering rested on the incomplete design. We added the missing cell, plain-JS(no-semantics): the identical bare-next contract (module shape, two observable keys, action names, data schema, and a description of the replay mechanism) with the entire single-step semantics block removed, so the model must derive the transition semantics from the Rust source alone. A mirrored TLA⁺ derivation arm (the constrained TLA⁺ contract, semantics block likewise removed) was added alongside it, completing the \(3{\times}2\) of Table 6; its result, the study’s only cross-language split, is analyzed in the findings below, with the full audit trail preserved in §12.

8.1.0.5 Replication, pairing, and checkability.

\(N{=}5\) generations per model per arm (80 in total), all scored per-window on the same 28-window kernel corpus. A pooled per-window McNemar test would be pseudo-replicated here: generations collapse to 1–2 unique behavioral fingerprints per (model, arm), so pooling \(5\times28\) windows counts the same underlying defect up to five times and inflates any \(\chi^2\). The analysis of record is therefore at the generation level: we report per-arm uniqueness counts and an exact two-sided permutation test with the generation as the unit (statistic: difference in mean per-generation pass rate; all \(\binom{10}{5}=252\) relabelings; the smallest attainable \(p\) is \(2/252\approx0.0079\), so starred results sit at the test’s floor). Because the generations collapse to so few distinct behaviors, we present \(\Delta\) as the primary quantity and read the permutation \(p\)-values as descriptive rather than as hypothesis tests: the effect sizes are large and uniform; the inferential machinery around them is at its resolution floor. The pre-registered checkability policy (conditional vs.unconditional scoring) proved moot in the constrained arms: zero windows were unscoreable in any constrained or plain-JS generation. (It becomes load-bearing in the derivation arms below.)

8.2 Results↩︎

8.3 Findings↩︎

8.3.0.1 Prompt prescriptiveness is a large, real confound that the completed factorial nonetheless demotes from the headline.

Adding the same semantics block to the JavaScript prompt, changing nothing else, moved Fable from 57.9% to 95.7% and Sonnet from 50.0% to a perfect 100%. The two-arm run alone would suggest a decisive language reversal, read as “most of that effect was the prompt.” The completed factorial shows that reading is an artifact of examining only the SAM column: at the generation level the within-SAM prompt effect is large for exactly those two models (Fable \(\Delta{=}.379\), \(p{=}.024\); Sonnet \(\Delta{=}.500\), \(p{=}.0079\)) and absent for Opus (\(\Delta{=}.079\), \(p{=}1\)) or Haiku (\(\Delta{=}.121\), \(p{=}1\)), whereas the contract effect without any semantics block (SAM vs.bare-next, both promptless) is large and uniform for all four models (\(\Delta{=}.186/.421/.500/.714\), each at the permutation floor). Prompt prescriptiveness remains a result in its own right, a first-class experimental variable large enough to masquerade as a language effect, but on this task it is the model-dependent factor, and the contract is the uniform one.

8.3.0.2 The missing cell: the bare-next contract needs no semantics block.

The bare-next-without-semantics arm reaches 100% for every generation of every model, including Haiku, at 28.6% under the SAM contract with the same absent semantics. All 20 generations are textually distinct (5/5 unique per model, saved with the study artifacts) yet behaviorally identical and correct: given a bare next() target, every model derives the observable single-step semantics from the kernel source alone. This settles the conditionality the incomplete design left open: contract minimality buys transcription fidelity unconditionally on spec-level semantics in the prompt. Two honesty notes travel with this. First, with both bare-next cells and TLA⁺ at 100%, effect ordering at the top is not identifiable: the within-bare-next prompt effect and any prompt\(\times\)contract interaction have no headroom to appear (a ceiling effect); what is identifiable is that contract \(\geq\) prompt for every model, strictly greater for Opus and Haiku, and that the bare-next contract suffices without semantics while the semantics block within SAM does not (three of four models below 100%). Second, the 100% ceiling itself is a property of this task’s tiny observable relation; the locksvc replication (§8.4) shows the bare-next result generalizing to a richer state, but the factorial has not yet been re-run there.

8.3.0.3 The derivation arms split the languages, and the split is the oracle’s paradigm, not the language.

With the semantics block removed from both minimal contracts, bare-next JS reaches 100% for every model while TLA⁺ falls to 78.6–100% (\(\Delta{=}.214\) for Opus and Sonnet, at the permutation floor; Table 6). The mechanism contains no wrong post-states: every TLA⁺ shortfall window is unscoreable, because unguided models write the idiomatic guarded action (enabled only when the lock is free), and under this oracle a disabled action on a pinned contention pre-state has no successor. The bare-next contract’s totality forbids that idiom structurally; TLA⁺ permits it; and the semantics block’s “held \(\Rightarrow\) unchanged” clause is precisely what converts the guard into a no-op branch. Scored conditionally (the paradigm-fair reading, per the oracle commitments stated in the design), the guard-idiom specifications are 100% correct on every window they can replay, and the languages tie here too. “Contract first, prompt second” therefore refines to: the prompt matters exactly where the contract under-constrains, and the unconditional split is a fact about the oracle’s paradigm, reported as headline only because the benchmark’s deployed scoring is unconditional.

8.3.0.4 A real, one-directional residual survives the prompt control.

With identical semantics in both prompts, TLA⁺ reaches 100% conformance for every model and every generation, while constrained JS-SAM does so only for Sonnet. At the generation level the residual is large for Opus and Haiku (both at the permutation floor, \(p{=}.0079\), read descriptively), vanishes for Sonnet, and for Fable does not replicate (\(\Delta{=}.043\), \(p{=}.44\)): the pooled McNemar had starred Fable’s deficit, and that specific claim was pseudo-replication, now withdrawn. The residual is largest for the weakest model (Haiku: 40.7% vs.%), and the direction is uniform: descriptively, no JS-SAM specification ever passed a window that its TLA⁺ counterpart failed, in any arm. (When one arm is at 100% this is partly structural, as §12 notes, but the direction is uniform in the deployed arm as well, where the gap sits at the permutation floor for all four models.)

8.3.0.5 The plain-JS arm locates the residual: it is the contract, not the language.

The fourth arm ties TLA⁺ at 100% for every model and every generation, with identical per-window outcomes in every paired generation-set (\(\Delta{=}0\); no test needed). Haiku is the cleanest single datum: the weakest model, which reaches only 40.7% through SAM’s machinery, expresses the identical semantics perfectly as a bare transition function, in the same language. Three attributions fall out. It is not the language: same JavaScript, different shape, 100%. It is not formality: TLA⁺ and plain-JS share the same shape, a minimal declarative single-step transition over exactly the observable state, and both sit at 100%; what the three-arm data suggested was “formal directness” is really minimal declarative shape. It is the SAM contract’s defect surface: proposal/acceptor wiring, intent firing, and the mandatory auxiliary state (threadStatus, callType), precisely where Experiment 1’s try_lock-from-free and release bugs lived. Every moving part the contract obliges is transcription surface, and the tax falls hardest on the weakest model (Haiku pays 59 points; Sonnet pays nothing).

8.3.0.6 Verdict against the pre-registered outcomes.

Not the strong “JS-SAM wins” (the direction is reversed), and not a tie at the backend level, but at the language level a tie is exactly what the controlled comparison shows: JavaScript expresses the transition relation as reliably as TLA⁺ once the specification shape is matched. The pre-registered outcome list did not anticipate this resolution. For transparency, the plain-JS arm was designed after the three-arm results were known, though it was scored blind, by the same mechanical replay, on the same corpus.

8.3.0.7 Design implication for JS-SAM.

The Phase-3 fidelity gap is the cost of the SAM specification contract, not a language limit, and the two can be decoupled. The backend can offer a bare-next specification shape (next(state, action, model), the JavaScript analogue of the TLA⁺ relation), or score conformance against a plain transition core over only the observable variables, dropping the mandatory auxiliary state from the replay contract. SAM’s ceremony is not gratuitous (the instance, intents, and value domains are exactly what feed the Phase-2/4 bounded explorer) but it should be paid where it buys something: explorable structure for model checking, not conformance replay. A prototype confirms the decoupling is practical: a \(\sim\)​40-line generic breadth-first explorer over {init, next} runs the entire pipeline in the same locked-down sandbox, so the SAM machinery is not required by any phase. Two points keep this precise. First, the SAM checker itself was never the execution problem: it ran Phases 2 and 4 for every JS-SAM arm in this paper (the full depth-6 intent exploration each time) without failing on any specification it was given; the tax is on the authoring side, namely the instance, intents, acceptors, and auxiliary state the model must hand-write to make a specification checker-consumable. (“Ran without failing” is itself a bounded claim: the metric audit in §5 shows the checker also ran to completion on a specification whose exploration never leaves its initial state, so a clean Phase-2 run certifies checkability, not adequacy.) Second, nothing is lost at this scale by the replacement: the SAM checker and the generic explorer are both bounded safety explorers (reachable states, invariants, deadlock), equivalent in checking power on these state spaces. The hybrid path keeps the library checker unchanged (the model writes only the pure next, the harness generates the scaffolding the checker consumes), relocating the checker from the specification contract to the tooling, which is where TLC has always lived on the TLA⁺ side: no one asks the model to write TLC. A follow-up study closes the loop with model-generated specifications: each of the four models generated five bare-next specifications (\(N{=}5\), 20 in total, each saved and evaluated as a single artifact across all phases), and 20 of 20 pass every phase (loadable, Phase-2 clean, Phase-3 28/28, all three Phase-4 invariants holding). Two caveats travel with this result: spin’s observable state is tiny (three reachable states), so the bare-next explorer’s adequacy must be re-validated on richer tasks; and the 20 generations collapse to roughly nine unique solutions (the models converge on the same correct next), which is expected for so small a system but limits the effective sample. Both caveats are resolved by a second task (§8.4).

8.3.0.8 Checkability, revisited.

Zero unscoreable generations in the constrained TLA⁺ arm confirms Experiment 3’s attribution: the earlier “1/4 model-checkable” was entirely the unbounded-CHOOSE trap plus the configuration surface, both of which the pinned contract and direct replay remove. The checkability gap is real but shallow, a matter of guardrails, not capability.

8.3.0.9 A free variance check on Experiment 1.

The JS(deployed) arm replicates Experiment 1’s setting at \(N{=}5\). The single-generation scores (89.3, 50.0, 50.0, 21.4) sit near the five-run means (81.4, 57.9, 50.0, 28.6), and the model ordering is preserved (with Fable’s mean now slightly above Sonnet’s). Experiment 1’s qualitative conclusions survive replication; its exact figures move by up to \(\sim\)​8 points, which is the error bar readers should apply to any single-generation number in this paper.

8.4 Generalizing the bare-next result: a second task↩︎

The bare-next-contract demonstration carried two caveats: a three-state observable space, and 20 generations collapsing to \(\sim\)​9 unique solutions. To resolve both, we built a second full bare-next task around locksvc, SysMoBench’s distributed lock service, generated by PGo (a compiler from Modular PlusCal, MPCal, to Go), chosen over the ring-buffer candidate because it runs as an ordinary Go test with no kernel build, demonstrating in passing that the trace-capture methodology of §4 is not kernel-specific. The harness runs PGo’s trace-recorder test five times and folds the raw MPCal events into observable windows over \(\{\mathit{holder}, \mathit{waiters}\}\), a lock holder plus the set of waiting clients, yielding a 60-window corpus (15 per action), self-consistent across runs. The set representation is itself a correction found by the base-rate audit: a first version modeled waiters as a FIFO in client-send order and required grants to go to the head, but the real server grants in arrival order, which the network reorders relative to send order (one capture logged sends \(1,3,2\) while the server queued \(\langle 3,2,1\rangle\), the exact reordering the upstream specification’s NoPriorityInversion comment warns about); the send-ordered fold silently converted ten real grants and releases into no-op windows. Arrival order is not a function of the client-side single steps, so at this projection the waiting clients form a set and a grant may go to any waiter of a free lock; the corpus was re-folded (15 no-change windows remain, all legitimately the CriticalSection no-ops, identity base rate 25%) and the study regenerated from scratch. The fold also repairs a real trace artifact: PGo’s empty vector clocks allow a CriticalSection event to be logged before its own Grant; the harness reorders each grant before its critical section, which is causally sound (the critical section cannot be entered without the grant). The replay and drivers were generalized to be task-agnostic: per-task action domains and invariants, and the projection rule in place of spin-specific keys.

The result replicates in full on the corrected corpus: 20 of 20 freshly generated bare-next specifications pass every phase (5/5 per model, including the bounded progress checks), over a 20-state observable space with a genuine waiting set, and with 14/20 unique solution texts (4/4/4/2 per model), that is, materially different correct implementations, all conforming, 45/45 on the state-changing windows. Both caveats are thereby resolved: the clean sweep is not an artifact of a trivial state space, and the models do not converge on a single memorized solution. Across the two tasks, 40/40 model-generated bare-next specifications pass every phase. We are explicit about what this number is and is not: it is evidence that the bare-next contract is viable at this scale (a spinlock’s 3 observable states and a lock service’s 20) and a hypothesis-generating result about contract minimality in general, not a settled conclusion. Both tasks saturate, which demonstrates robustness of the contract on tasks this size while saying nothing about tasks where a bare transition relation stops being sufficient; the decisive test is a consensus-class protocol with non-trivial state (Raft with logs, terms, and votes). That test is Experiment 5, and §9 reports where the streak ends.

9 Experiment 5: derivation at depth on a consensus-class task↩︎

The bare-next-contract result carried one conditionality that the first two tasks could not discharge: both have observable relations a competent reader can largely anticipate from the action names. A consensus protocol does not. This experiment carries the bare-next contract, unchanged in shape, to SysMoBench’s etcd task, the Raft implementation of etcd-io/raft, and the very system whose “textbook” mismodeling motivated the benchmark [3].

9.1 Task and corpus↩︎

Upstream etcd-io/raft ships its own trace instrumentation behind a build tag, a TraceLogger interface whose events carry each node’s term, vote, commit index, log size, and role, added by the maintainers for their own TLA⁺ validation work. Our harness therefore only supplies a sink (one JSON line per event) and determinism: five scenarios drive a three-node cluster through the library’s RawNode interface with hand-delivered messages, no goroutines, and no randomness. The scenarios are an election; replicated proposals; heartbeat rounds; a stale-log campaign rejected by a quorum (the candidate steps down, and the incumbent re-establishes itself at a higher term through the append reject/retry protocol); and a higher-term re-election observed by all nodes. Delivery orders vary across scenarios. A fold projects the event stream onto a whole-cluster observable state,

yielding 97 windows over the five canonical actions (ElectionTimeout 8, HandleVoteRequest 16, ClientProposal 8, HandleAppendEntries 57, HandleHeartbeat 8). The corpus is validated the way the earlier ones were: zero self-consistency violations, byte-identical regeneration, and a hand-written reference bare-next specification that replays 97/97 and explores cleanly, the positive control that distinguishes “the models failed” from “the fold is wrong.” Two projection approximations are documented with the harness (per-entry log terms are not observable, so vote up-to-dateness reduces to an index comparison; both are exact on these corpora by construction), and both matter below.

9.2 One-shot results↩︎

Each of the four models generated five bare-next specifications from the contract-pinned derivation prompt (state shape, action names, data schemas; no semantics block; the transition semantics must come from raft.go), scored across all phases: Phase 2/4 by the generic bounded explorer (depth 8; roughly \(1.3\times10^{5}\) distinct states, four orders of magnitude beyond the spinlock’s three), Phase 3 by the same mechanical replay as every bare-next study above (Table 8).

The 40/40 streak ends here, and it ends informatively. What the contract bought on the small tasks it still buys: every specification is a loadable, explorable, replayable artifact, and nothing fails for the mechanical reasons the SAM contract induced on the spinlock. What breaks is what no contract shape carries.

9.2.0.1 The dominant failure is the vote rule, for every model.

HandleVoteRequest accounts for essentially all conformance shortfall in three models (and two windows of the fourth); Haiku additionally mishandles append/log-match cases. The most-failed windows (12–14 of the 20 specifications each) are the votes where the subtleties interact: a re-election at term 3 following a rejected stale campaign, and the second election at term 2. A representative failure: a follower at \(\{\mathit{term}{=}2, \mathit{vote}{=}\textit{self}\}\) receives a vote request at term 3 from a candidate with an up-to-date log; the trace post is \(\{\mathit{term}{=}3, \mathit{vote}{=}\textit{candidate}\}\) (step down, reset, grant); a failing specification produces \(\{\mathit{term}{=}3, \mathit{vote}{=}\textrm{`0'}\}\), that is, it bumps the term and wrongly denies the vote. The projection is implicated in a precise way: with per-entry log terms unobservable, the textbook two-field up-to-dateness comparison is inexpressible, and a correct specification must recognize that the faithful reduction at this projection is the index comparison. This is the benchmark’s “textbook modeling” failure reproduced at protocol scale: the models write the Raft paper’s rule where the implementation-faithful reduction is required.

9.2.0.2 The strongest model’s failure is a specification-vs-program distinction.

Four of Fable’s five specifications reach 97/97 conformance and then fail the CommitWithinLog invariant under exploration. The defect is instructive enough to quote: its heartbeat handler updates the commit index unclamped, with a comment stating (correctly) that a Raft leader never advertises a commit index past the follower’s log. That reasoning is sound for the closed protocol, in which only a conforming leader generates messages. The bounded explorer, however, draws action payloads from the declared input domains (an open-world semantics under which a heartbeat may carry any commit value), reaches a state with \(\mathit{commit} > \mathit{log}\), and reports the violation. (The reference specification clamps, which is also what the implementation’s own commitTo enforces at runtime.) Both readings of this failure deserve stating: under the benchmark’s deployed scoring the specification fails Phase 4, full stop; read closed-world, the model made a defensible protocol argument that happens to be the wrong argument for a specification, whose obligations extend to inputs the protocol forbids. The contract never states which world next() must be total over. That is the same category of paradigm commitment as the totality-vs-enabling-conditions choice in the Phase-3 oracle (§8), now surfacing in Phase 4, and it should be made explicit in the contract rather than left for the strongest model to reason past.

9.2.0.3 The phases re-differentiate at scale.

On the spinlock, Phases 1, 2, and 4 had no discriminating power and we reported that as a finding about task scale. Raft confirms the other half of the prediction: bounded exploration now catches a real defect (the unclamped commit) that the trace corpus provably cannot (no captured trace contains a protocol-forbidden message), while trace replay catches the vote-rule errors that exploration alone would rate internally consistent. At consensus scale the two external checks are complementary rather than redundant, which is the regime the benchmark was designed for.

9.3 One round of repair↩︎

Experiment 2’s question transfers directly: shown exactly what failed, can the models fix it? Each failing specification received one repair round, consisting of its own module, every failing window with the pinned pre-state, the real post-state, and the module’s actual output, and any invariant violation with the predicate source and a violating reachable state, nothing else, and the rewrite was re-scored across all phases (Table 9).

One round takes the suite from 0/20 to 6/20, all in the top two tiers, and the spinlock’s two-tier repair picture (capable models repair fully, the weakest not at all) stratifies into four regimes.

Fable converges: every specification reaches 97/97, and in four of five cells the invariant counterexample was sufficient for it to add the clamp it had reasoned away, without disturbing conformance. Opus converges more slowly: two full passes, the remainder within two windows. Haiku’s plateau is structural rather than stochastic: five independently generated specifications all repair to exactly 93/97, failing the identical four hard vote windows; shown its own wrong outputs on precisely those windows, it cannot derive the rule, consistent with its non-convergence across three rounds on the spinlock.

Sonnet’s behavior is the finding we did not anticipate. In three of five cells the rewrite fixes the quoted windows and destroys a large fraction of previously correct behavior (95/97 to 59/97 in the worst case), including the one invariant-failing cell, which fixed the invariant and collapsed conformance in the same rewrite. Nothing comparable was visible on the spinlock, where a specification is small enough that a rewrite is effectively a regeneration. At protocol scale, preserving what already works emerges as its own capability axis, distinct from both one-shot accuracy and defect repair, and a repair loop that re-scores only the defects it fed back would report Sonnet’s rewrites as successes. Full per-window re-scoring after repair is not an optional nicety; it is what makes the regression visible at all.

9.4 What the boundary is↩︎

Stated carefully: contract minimality buys transcription fidelity, not semantic derivation. The bare-next contract’s 100% held exactly as long as the observable relation could be derived without deep reading of the implementation; at Raft the bottleneck moves to understanding (the vote rule under the projection, the clamp a specification owes to inputs the protocol forbids) and no contract shape reaches it. Three qualifications keep this within its evidence. The Raft study tests the bare-next contract only; whether the SAM and TLA⁺ arms would fare better or worse here is untested (we would predict neither rescues the vote rule, since the failure is language-independent modeling, but that is a prediction, not a result). The corpus, like every corpus in this paper, is a deterministic, protocol-easy slice: no crashes, no partitions beyond one staged stale campaign, no reordering beyond the scheduled variations. And the repair experiment is one round at \(N{=}5\); the regression finding in particular deserves replication before it hardens into a claim about Sonnet rather than about this run.

10 Scope of the cross-language comparison↩︎

Before discussing the results, we consolidate in one place, rather than scattered through the experiments, what the JS-SAM-vs-TLA⁺ comparison does and does not establish. Readers should carry this section’s qualifications into every cross-language claim in this paper.

10.1 Four asymmetries↩︎

1. Controlled and ecological are different instruments. All cross-language conformance numbers come from the direct, mechanical TLC replay built for Experiment 4, not from the benchmark’s deployed, agent-mediated TLA⁺ Phase 3. The controlled path is what makes the languages comparable at all (an agent in the loop would confound spec quality with agent capability). The deployed path (§7.3) confirms the per-cause attribution (the harness fault vanishes, the CHOOSE idiom persists) but it scores a different window set (contention no-ops excluded rather than required) under an interpretive oracle (the specification’s own reading of its action names). Its numbers and the controlled numbers answer different questions and must not be compared cell-to-cell.

2. The oracles are not the same oracle. The conformance oracle requires every action to be total (a successor for every pinned pre-state), the bare-next/JS paradigm by construction. Idiomatic TLA⁺ writes enabling conditions and stutters; this oracle scores a disabled action as unscoreable, penalizing the idiom independent of correctness. Every unconditional cross-language number therefore embeds a paradigm choice; the conditional (paradigm-fair) scores, reported alongside throughout, are the like-for-like reading, and under them the derivation-mode split disappears entirely.

3. The CHOOSE trap is a guardrail matter, not a capability gap. The unbounded-CHOOSE failures of Experiment 3 are a known TLC anti-pattern that no experienced TLA⁺ author writes, that agentic workflows already guard against [12], and that a one-line prompt guardrail eliminated in our own runs. The “evaluability gap” is a default-prompt robustness observation.

4. One failure was ours, not the language’s. Haiku’s TLA⁺ Phase-2 failure was a harness fault (config generation produced no usable .cfg). It is reported per-cause everywhere, and the 4/4-vs-1/4 figure must not be read as purely a language effect.

Net: what the comparison establishes is that under a matched minimal contract and an identical mechanical oracle, JavaScript and TLA⁺ express this system’s transition relation equally well, and that the observed gaps are attributable to contract shape, prompt content, an avoidable idiom, and one harness fault. What it does not establish is any claim about TLA⁺ in the hands of a guarded agentic workflow, or about the cross-language question on tasks richer than the two the factorial studied (the Raft study of §9 has no TLA⁺ arm). The TLA⁺ figures in this paper are lower bounds.

10.2 What JS-SAM cannot do↩︎

The comparison in this paper is to TLC’s bounded explicit-state checking, because that is the phase SysMoBench automates. TLA⁺ the ecosystem is a strictly larger proposition, and none of the following has any analogue in the JS-SAM backend, with either the SAM checker or the bare-next explorer:

• Liveness and temporal logic. Neither explorer checks any LTL/CTL property. The bare-next explorer’s bounded progress checks are EF-reachability within a depth bound, a bounded-horizon safety-shaped property, not liveness: they cannot express “every acquisition eventually succeeds.”

• Fairness. There is no notion of weak or strong fairness over actions; behaviors in which an enabled action is ignored forever are outside the framework’s vocabulary.

• Unbounded verification. Exploration is bounded by depth over finite intent domains. There are no refinement mappings, no inductive invariance proofs, no symbolic checking of parameterized or unbounded state spaces (cf.Apalache [14]), and no mechanical theorem proving (cf.TLAPS [15]).

• Compositional reasoning. TLA⁺ supports reasoning about a system as a composition of specifications; a JS-SAM module is a single closed transition system.

A JS-SAM specification is thus a checkable artifact (bounded safety exploration plus conformance replay against finite traces), and the phrase “specification language” in this paper’s title should be read under that qualifier. On the tasks studied, the checkable subset happened to be the only part of the pipeline with discriminating power (Phase 3), and safety-only Phase 4 provably could not catch the headline bug (§12); that is a fact about these tasks and this benchmark’s phases, not a demonstration that the missing capabilities are dispensable. For systems whose correctness burden lies in liveness under fairness, which includes every consensus protocol, TLA⁺’s verification capabilities have no substitute here.

10.3 What SAM offers that the bare-next contract does not↩︎

The contract-tax finding is easily over-read as “SAM was a mistake.” The factorial supports a narrower statement: SAM’s machinery is transcription surface for conformance replay, where it buys nothing, and that is a claim about where scaffolding should be paid, not about its value. What the SAM contract provides that a bare next() does not: explicit intent signatures with finite input domains (the analogue of a TLA⁺ constants block, and exactly what makes Phases 2 and 4 executable without a hand-written harness); a single locus of mutation with acceptor guards, which is the natural shape for modeling interactive and reactive systems where proposals can be rejected; and an explorable structure the bounded checker consumes directly. The design implication drawn in §8 is accordingly a relocation, not a removal: the model writes the pure transition core; the harness generates the SAM scaffolding the checker needs, which is where TLC’s apparatus has always lived on the TLA⁺ side.

11 Discussion↩︎

11.0.0.1 “Looks right” is not “is right,” in any language.

The experiments repeatedly produced specifications that passed every internal-consistency check while being wrong about the real system, most vividly Fable’s never-releasing spinlock, which preserved mutual exclusion because it was broken, and its Raft heartbeat handler, which omitted a safety clamp on a correct protocol argument. External ground truth is what catches both (trace replay in the first case, open-world exploration in the second), and which check catches what turns out to depend on task scale (§9). This replicates SysMoBench’s core claim [2], [3] in a new language substrate, which strengthens it: the phenomenon is about LLM modeling, not about TLA⁺.

11.0.0.2 The familiar path is modeled; the unfamiliar path is not.

For the three stronger models, every Experiment-1 failure lands on a less-common code path: the non-blocking try_lock-from-free acquisition (all three) and release bookkeeping (two of the three). Blocking acquisition, the version of a spinlock every textbook presents, was modeled correctly by all but the smallest model. This is the “textbook template” failure mode of [3] reproduced at the granularity of individual actions within a 100-line system.

11.0.0.3 Repair belongs in the evaluation loop, scored on the whole specification, not the fed-back defects.

The repair experiments suggest that single-shot leaderboard scores understate some models (Fable, on both tasks) and overstate the ceiling of others (Haiku, on both). Since practical formal-modeling deployments will be agentic loops with exactly this kind of counterexample feedback, benchmarks arguably should report both axes. The Raft repair round (§9.3) adds a methodological requirement: Sonnet’s rewrites fix the quoted defects while breaking previously correct behavior, so a repair loop that re-checks only its own feedback would score regressions as successes. Repair must be re-scored on the full corpus and all phases. The repair drivers we contribute make both measurements cheap for any bare-next or JS-SAM task.

11.0.0.4 The hypothesis, after Experiment 4: a split verdict, sharply located.

The practical form of the hypothesis survives: host-language familiarity plus a self-contained executable artifact gets models to an evaluable specification far more often (4/4 vs./4), and evaluability is the precondition for everything else. The strong form, that familiarity yields more faithful models, resolves to a tie once like is compared with like: JavaScript in the shape of the TLA⁺ relation matches TLA⁺ at 100% for every model. (The one cross-language split, in the derivation arms, favors bare-next JS and traces to the bare-next contract’s totality against TLA⁺’s guard idiom, not to the language; scored conditionally, the tie holds there too; §12.) What the three-arm data made look like a language effect was the specification contract: every layer of machinery between the semantics and the artifact (proposals, acceptors, auxiliary state) is surface on which transcription slips, and the tax falls hardest on the weakest models. Neither training-data abundance nor formality is the operative variable on this task; contract minimality is. The largest single-model effect in the study is a prompt effect (Sonnet 50%\(\to\)​100%), but the completed factorial shows the prompt moves only two of four models within the SAM contract while the contract switch moves all four to ceiling with no semantics at all: contract, then prompt, then language is the order of what mattered here. Experiment 5 then bounds the finding from above: at consensus scale the contract still delivers evaluable artifacts and flawless transcription, and the residual failures are modeling (misderived vote rules, a clamp reasoned away) which no contract shape, in any language, was ever going to supply. The hypothesis’s own either-way framing (§1) lands on its second branch: the hard part is modeling, not notation.

11.0.0.5 A benchmark everyone passes measures nothing, and the next task up de-saturates it.

There is a symmetry in the bare-next-contract results that deserves stating plainly. On the two small tasks, the bare-next contract saturates the benchmark: every model, Haiku included, scores 100%, and the informative reading is that under a minimal contract, specifying a system of that size is a solved problem for current frontier models. What saturation exposes is what should be measured next (derivation at depth, scale, and temporal properties), and this study runs the first two: at Raft scale the same contract yields 0/20, Phase 3 and Phase 4 discriminate on complementary defects, and the models separate into four repair regimes. The benchmark’s frontier moved exactly where the saturation analysis said it would. The temporal-property axis remains open (§10.2).

12 Limitations and threats to validity↩︎

We state these plainly; the study is a case study and should be read as one.

• The controlled cross-language comparison concerns one system. Experiments 1–4 all concern the spinlock, the easiest class of SysMoBench task; the bare-next-contract validation now spans three tasks (§8.4, §9), but the factorial controlled comparison itself (the SAM and TLA⁺ arms) has not been repeated beyond it, so the contract-vs-prompt ordering remains a small-task result. The Raft study confirmed one specific prediction (the phases re-differentiate at scale [3]) and bounded another (the bare-next contract’s ceiling); it does not license extrapolating the factorial’s ordering to consensus scale.

• Experiments 1–3 are single-generation. Each cell in Tables 1–4 is one sample. Experiment 4’s \(N{=}5\) deployed-JS arm retroactively bounds the damage (ordering preserved, individual scores moving by up to \(\sim\)​8 points) but the repair-loop and checkability experiments have not been replicated and should be read with that error bar.

• Trace coverage is the quiet weakness of every conformance number here (audited: scripts/trace_coverage_audit.py). The spin corpus is 28 windows from two hand-authored deterministic scenarios, covering 8 of the 18 observable (pre-state, action, data) combinations; contention is expressed only via try_lock (2 combos), and the corpus contains zero windows of a blocking lock() observed while the lock is held. The instrumentation emits the acquire event at acquisition success, where the pre-state is free, so the spin phase (the behavior the primitive is named for) is invisible in this two-variable projection by construction: a woken blocking waiter is indistinguishable from an uncontended acquire. The locksvc corpus is one fixed terminating workload (three one-shot clients; exactly 12 windows per run by protocol completion, hence the exactly-15-per-action count) sampled under five schedules, genuinely distinct (5/5 different action sequences, four different grant orders, including the network reordering that exposed the fold bug), but with no re-requests, no deeper contention, and no failure paths. The vector-clock reorder’s causal premise is verified per event at corpus build, not assumed: every CriticalSection step reads GrantMsg from its mailbox (message-passing happens-before), and the builder refuses traces where that check fails. Net: every 100% in this paper means conformance to a two-variable projection of an easy, deterministic slice of each system’s behavior, faithful to real executions, far from exhausting them, and the conclusion carries this qualifier explicitly.

• The TLA⁺ comparison mixes causes. The 1/4-vs-4/4 result bundles a genuine model-attributable pitfall (unbounded CHOOSE, 2/4) with a harness shortfall (config generation, 1/4). We report the attribution per model (Table 4); the headline number should not be read as purely a language effect. The repair asymmetry here, raised in review by Erik Meijer [13], is closed in full: one round of TLC-feedback repair fixes both CHOOSE failures, and the repaired specifications hold all seven invariants through the pipeline (§7).

• The derivation-level comparison splits the languages for the first time. Experiment 4 as first designed measured transcription, not derivation: it had no TLA⁺-without-semantics arm to pair against the bare-next one. That arm (tld: the constrained TLA⁺ contract with the semantics block removed, mirroring the bare-next derivation arm) completes the design. In derivation mode the bare-next JS contract beats TLA⁺ for Opus and Sonnet (\(\Delta{=}.214\), \(p{=}.0079\) each; 100% vs.%), directionally for Haiku (87.1%, \(p{=}.17\)), and ties for Fable (100%). The mechanism is precise and is not wrong post-states: every TLA⁺ shortfall window is unscoreable. Without instruction, most models write the classic TLA⁺ idiom in which AcquireLock is guarded on the lock being free, so a failed attempt is a disabled action rather than an observable no-op step, and the pinned contention windows have no successor. The bare-next contract’s totality (next() must return a state) structurally forbids this; TLA⁺’s idiom permits it, and the semantics block’s “held \(\Rightarrow\) unchanged” sentence turns out to be what fixes it (\(\texttt{tld}\) vs.\(\texttt{tla}\): \(p{=}.0079\) for both affected models). Under the pre-registered conditional scoring the guard-idiom specs are 100% correct on every window they can replay, so the shortfall is replay-contract incompatibility, not incorrect modeling, and both numbers are reported, with the unconditional as headline. “Contract first, prompt second” thus refines to: the prompt matters exactly where the contract under-constrains.

• The plain-JS arm resolves the substrate asymmetry, but was added post hoc and answers a narrower question. The three-arm design left “executable machinery admits bugs a two-variable relation cannot” as an open alternative; the fourth arm was designed to test exactly that, after the three-arm results were known (its data were then collected by the same blind mechanical replay). Its conclusion has since been extended rather than bounded: a generic {init, next} explorer replaces the SAM scaffolding for Phases 2 and 4 (at equivalent bounded-safety checking power on these state spaces), and 20/20 model-generated bare-next specifications pass every phase on spin, but that demonstration inherits spin’s three-state observable space and a converged solution set (\(\sim\)​9 unique among 20), so the finding needed a second task. The locksvc study (§8.4) supplies it (a 20-state space, 14/20 unique solution texts, 20/20 passing), generalizing the contract-tax removal across tasks of this scale, though not yet to large distributed protocols.

• \(b{=}0\) is partly structural, and the effective sample is small. When the TLA⁺ arm passes every window it fails none, so a JS-only pass is impossible by construction; any paired comparison reduces to whether the JS-SAM failure count is significant. Moreover the generations collapse to 1–2 unique behavioral fingerprints per (model, arm): a pooled window-level McNemar would count the same defect up to five times, so the analysis of record is the generation-level permutation test of Table 7. At the strictest unit (the unique solution, \(n{=}1\)–\(2\) per cell) no significance test is meaningful; the per-solution effect sizes stand on their own.

• The direct TLC replay is the controlled condition, not the deployed one. The benchmark ships an agent-mediated TLA⁺ Phase 3; pinning spec variables to the trace schema trades realism for comparability. Whether a “pinned-schema” Phase-3 mode should exist as a first-class controlled condition alongside the agent path is a methodological question we are putting to the maintainers.

• Phase 4 for JS-SAM is safety-only and could not fail the headline bug in principle. This is stronger than a template-count difference (seven TLA⁺ templates vs.three JS-SAM). The three JS-SAM invariants are all safety properties over reachable states, and a never-releasing lock satisfies every one of them because it is broken: mutual exclusion holds trivially when the lock never changes hands, status consistency holds for a permanently locked holder, and the shipped NoDeadlock (“some thread is not trying”) is satisfied by the stuck holder itself being locked. We verified this empirically: a release-is-a-no-op mutant of the known-good specification passes Phase 4 with the identical 3/3 verdict as the correct one. The properties that would discriminate (every waiter eventually acquires, every hold is eventually released) are liveness, and neither the SAM checker nor the bare-next explorer checks any temporal property (the JS-SAM template library states the exclusion explicitly). 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 specification; only trace replay catches it. As mitigation the bare-next explorer now supports bounded progress checks (EF-reachability: from every reachable state satisfying a premise, a goal state must be reachable within the bound, not liveness: no fairness, bounded horizon). These fail the never-releasing mutant (ReleaseProgress) and would fail the inert Haiku specification (AcquireProgress) that safety-only Phase 4 passed vacuously; all 40 saved model-generated bare-next specifications pass them on both tasks.

• Model family. All four models are from one vendor. The benchmark’s configuration already includes other vendors’ models; the comparison should be broadened before generalizing. A further reproducibility caution: several of the exact model versions used here may not be externally accessible; the saved specifications and raw per-window data, not the model identifiers, are the reproducible objects.

• Missing arms, with status. Several acknowledged-but-load-bearing gaps remain; their current state: the derivation arms (no semantics block, both languages) are run (the one gap that, once filled, changed a conclusion); multi-round repair is run on spin (Haiku does not converge; §6) and single-round on etcd (§9.3); the as-deployed agent-mediated TLA⁺ Phase 3 is run (§7.3) and validates the attribution but, as an interpretive oracle over a different window set, does not substitute for the controlled comparison; other vendors remain blocked on credentials (the registry entries exist in config/models.yaml; only Anthropic keys are available in this environment); and the factorials on locksvc and etcd remain open (the bare-next arms exist; the SAM and TLA⁺ arms need per-task prompts and TLC replay modules). Each is inventoried with run instructions in REPLICATION.md.

• The Raft study’s own limits. The corpus is five deterministic scenarios with no crashes, no partitions beyond one staged stale campaign, and no unscheduled reordering; the projection omits per-entry log terms, with two documented approximations that are exact on these corpora by construction (§9); richer corpora could separate specifications these cannot. The repair round is one round at \(N{=}5\): the four-regime stratification, and Sonnet’s regression in particular, should be read as this run’s result pending replication. And the open-world reading of the CommitWithinLog failures is a scoring commitment: we report deployed (open-world) numbers as headline and the closed-world reading alongside, mirroring the conditional-scoring convention of Experiment 4. Two cells initially recorded as unloadable were traced to a transient sandbox failure under machine load and re-scored clean; the raw results file preserves the note.

• Author positionality, and the case for independent replication. The first author is the author of the SAM pattern. The evaluation pipeline is automated and the corpus is model-independent, which limits (but does not eliminate) the room for favorable design choices; and the study’s sharpest negative finding, the contract-tax attribution, cuts against the SAM contract as deployed, which we take as evidence the pipeline is not tilted toward it. But the deeper issue is that the load-bearing materials on both sides of every comparison are experimenter-authored: the trace scenarios, the semantics block, the derivation prompts, and the repair prompt. No amount of automation neutralizes that. The repository therefore ships a replication guide (REPLICATION.md) that reruns every analysis from committed raw data without API access, regenerates every experiment from pinned prompts and models, and inventories each experimenter-authored material as an independent variable to audit or vary. We consider an independent replication by researchers unaffiliated with SAM (ideally the SysMoBench maintainers) a prerequisite for treating the cross-language conclusions as more than a well-documented single-author case study.

13 Related work↩︎

13.0.0.1 Benchmarking LLM formal modeling.

SysMoBench [2], [3] is the direct foundation of this work: it contributes the four-phase methodology, the eleven-system task suite, and the finding that conformance, not syntax, is where LLM specifications fail. Our contribution is orthogonal: holding the benchmark fixed and varying the specification language, including the first non-formal one. The Specula agent [12] shows that agentic workflows can saturate current SysMoBench tasks in TLA⁺; our repair experiment probes the smallest unit of such a workflow (one counterexample round) across models.

13.0.0.2 The wider LLM\(\times\)formal-methods field.

A relevance-ranked sweep of the 2022–2026 literature (40 works; the map ships with the artifacts) places this study in a thin slice of a fast-moving field. The center of gravity is autoformalization and theorem proving (Lean/Isabelle proof generation and repair [16]–[18]), followed by loop-invariant and precondition generation for deductive verification [19]. Specification-focused work concentrates on natural-language-to-temporal-logic translation [20] and declarative-specification repair [21]; benchmarks are proliferating (e.g., OSVBench for OS-verification specification generation [22]) but grade against reference specifications, proof success, or human judgment rather than execution-trace ground truth. Against that corpus, this study’s two distinctive commitments, conformance to traces captured from the running system as the discriminating oracle and a controlled contract\(\times\)prompt\(\times\)language factorial, are both minority positions. The closest contemporaneous works, an NL-to-TLA⁺ correctness evaluation and counterexample-driven TLA⁺ repair [23], [24], each parallel a single axis of the design here (one-shot generation; repair); the repair-as-separate-axis finding of Experiment 2 matches an emerging pattern across proof repair [18] and specification repair [21].

13.0.0.3 Trace conformance for specifications.

Validating specifications against implementation traces has industrial precedent: MongoDB’s eXtreme modeling checked TLA⁺ models against driver traces [25], and trace validation is the standard answer to “does the spec match the code” [2]. SysMoBench’s transition-window formulation, which we adopt unchanged, makes conformance per-action and per-window rather than whole-trace.

13.0.0.4 Formal methods practice.

TLA⁺ [4] with TLC [10], Alloy [5], and CSP-based PAT [6] are the benchmark’s formal backends; industrial deployments (e.g., [1]) motivate the whole enterprise. SAM [7], [8] occupies an unusual position: an engineering pattern with TLA⁺-derived semantics, here repurposed as a specification language precisely because it sits at the intersection of “formally disciplined” and “abundant in training data.”

13.0.0.5 Executable specifications are not new.

The formal-methods community has long built specification languages that are executable while remaining formally checkable, and this paper’s contribution must be located against that lineage rather than presented as discovering executability. Event-B with Rodin supports executable formal modeling under refinement [26]; Dafny is an imperative language with specifications and automated verification built in [27]; Frama-C/ACSL attaches checkable contracts to executable C [28]; refinement/liquid types make specifications part of an executable program’s type structure [29]; and within the TLA⁺ family itself, PlusCal [30] and Quint [31] deliberately trade notation toward the programmer. The TLA⁺ ecosystem likewise extends well past TLC, the only tool compared here: TLAPS provides mechanical proof [15] and Apalache symbolic model checking [14] (§10.2). What is new in this study is not executable specification but its LLM-generation angle under a trace-grounded oracle: whether frontier models produce more faithful specifications in an executable mainstream language than in a formal one, measured by conformance to traces of the running system, and the finding that the specification contract, not the language, dominated that outcome.

14 Conclusion and future work↩︎

We extended SysMoBench with JS-SAM, its first non-formal specification backend, built the kernel trace-capture pipeline needed to give it a real conformance phase, and ran five experiments across three tasks: the Asterinas spinlock, a distributed lock service, and Etcd Raft. The results make five points with unusual precision for a case study. On the small tasks, transition validation against real traces is the only phase that discriminated among four frontier models (0–86.4% on state-changing windows, with all other phases unanimous and the weakest model sitting exactly at the corpus’s identity base rate). One round of trace-feedback repair reveals a self-correction axis that one-shot scores conceal: capable models repair fully and verifiably (a held-out audit found root-cause fixes, not memorized windows), the weakest not at all, and at protocol scale that axis stratifies further into convergence, slow convergence, regression, and plateau. The same models that reach an evaluable specification in JavaScript 4/4 times manage it in TLA⁺ 1/4 times, for two identified causes, one of them a harness fault, both later removed entirely by a one-line prompt guardrail, both confirmed per-cause by a run of the benchmark’s deployed agent-mediated path, and both CHOOSE failures repaired by one round of TLC-feedback repair: a default-prompt robustness gap, not a language-capability one. Under a pre-registered, paired comparison completed to a full \(3{\times}2\) factorial in (contract, prompt), the faithfulness question resolves in an unexpected place: the conformance gap is attributable to the SAM contract’s machinery, not to JavaScript, not to formality, and not primarily to prompt prescriptiveness. Plain JavaScript in the shape of the TLA⁺ relation ties TLA⁺ at 100% for every model, with or without spec-level semantics in the prompt. And the winning contract, carried to a consensus protocol, finds its boundary: 0 of 20 one-shot specifications pass every phase, for reasons that are modeling rather than transcription, with one repair round recovering 6 of the 20.

The hypothesis that motivated the backend is neither confirmed nor dead; it is answered more usefully than either. Stated plainly, on the tasks tested the completed study ranks what governed LLM specification quality: contract shape first, prompt second, language nowhere, a ranking established on the spinlock factorial and not yet replicated on a richer task. Familiarity buys checkability; contract minimality buys transcription fidelity, and, Experiment 5 shows, only that: on the spinlock every model derives the observable semantics unaided when the target is a bare transition function, but at consensus scale the bottleneck moves to semantic derivation itself (the vote rule under the projection, the clamp a specification owes to inputs the protocol forbids) and no contract shape reaches it. The prompt is the model-dependent factor: four lines of semantics moved Sonnet 50%\(\to\)​100% and Fable 57.9%\(\to\)​95.7% within the SAM contract, but moved Opus and Haiku insignificantly, and at the bare-next contract it had nothing left to move (a ceiling at which effect ordering among the perfect cells is, we note, not identifiable). Every layer of ceremony between the semantics and the artifact cost conformance; the language itself, once shape was matched, contributed nothing measurable (the derivation-mode split between bare-next JS and TLA⁺ traces to contract totality, not language: scored conditionally, the guard-idiom TLA⁺ specifications are perfect on every scoreable window). On the practical question, whether JavaScript can replace TLA⁺, the evidence splits cleanly. For LLM-generated conformance modeling at this scale: yes, interchangeable on fidelity on what we measured, which is conformance to a two-variable observable projection of deterministic, easy slices of each system’s behavior (§12); neither language has been tested on uncovered combinations, projection-invisible behavior such as the blocking spin, richer workloads, or adversarial interleavings. Within that measured slice the tie is exact, and JavaScript carries fewer operational failure modes (no CHOOSE trap, no configuration artifact). For verification: no. Liveness, fairness, temporal-logic properties, large-state and unbounded checking, and mechanical proof (TLC’s temporal checking, Apalache, TLAPS) have no equivalent in either bounded safety explorer used here (the SAM library’s checker or its 40-line generic replacement), and remain TLA⁺’s distinctive value (§10.2). The demonstrated role for executable JavaScript is as a checkable artifact for bounded model checking and trace-conformance validation, complementing, not replacing, TLA⁺’s verification capabilities. The search this motivates is therefore not for a better specification language but for a better specification contract: {init, next} over observable keys, in whatever language the model writes well, with richer machinery generated by the harness rather than transcribed by the model. Two questions that the small-task results left open, derivation at depth and scale, are answered here for the bare-next contract, and the answer reshapes the agenda: derivation at depth is where one-shot generation fails and where feedback loops earn their keep. What remains genuinely open is the cross-language question at that depth (whether TLA⁺ one-shot generation fares any better on Raft, which we predict it does not, since the failures are modeling, but it is a prediction), the temporal properties no bounded safety explorer checks, and corpora adversarial enough to separate specifications these deterministic slices cannot.

The experiments that follow are concrete: (1) promoting the bare-next specification shape from demonstration to backend, and, following Experiment 5, making the open-world totality obligation explicit in the contract: a specification’s next() answers for the declared domain, not only for protocol-reachable inputs; (2) the cross-language factorials on locksvc and etcd (the bare-next arms exist; the SAM and TLA⁺ arms are scoped in the replication guide), the test of whether “language nowhere” survives depth; (3) a prompt-prescriptiveness dose–response study, treating the semantics block as the manipulated variable rather than a nuisance; (4) multi-round repair on etcd, to establish whether Opus converges, whether Sonnet’s regression is systematic, and where Fable’s fifth cell lands; (5) hardening the benchmark surfaces this study kept tripping on, the configuration generator and the invariant pipeline’s name-collision behavior (§7), both now attributed per-cause; and (6) replication beyond one model family. We are contributing the backend, harnesses, drivers, corpora, and the controlled-comparison methodology upstream so these can be run, and challenged, by the community. One such test has since been reported [32]: a study of production software, the payment workflow of an operational point-of-sale system that keeps the register, payment terminal, and payment processor in agreement, runs the same JS-SAM-vs-TLA⁺ comparison and finds the contract-structure ordering replicating across seven models from two vendors.

Acknowledgments↩︎

We thank the SysMoBench / Specula maintainers for the benchmark, the integration guidance that shaped the JS-SAM backend’s scope, and the reference instrumentation for the Asterinas spinlock.

Reproducibility↩︎

All artifacts are public: the JS-SAM backend (tla_eval/languages/js_sam.py, tools/js-sam/), the trace harness (scripts/harness/spin/), the captured corpus (data/sys_traces/spin/), the repair driver (scripts/repair_phase3.py), the Experiment-4 apparatus (the constrained and plain-JS prompts, the direct TLC replay and its functional-check audit (scripts/tla_direct_tv.py, the 20 audited specifications in output/tla_specs/, output/tla_functional_audit.json, the permissive control in tools/tla/), the paired factorial driver with raw per-window data (scripts/tla_phase3_study.py, output/tla_phase3_study.json), the generation-level analysis of record and the repair-generalization audit (scripts/tla_phase3_analysis.py, scripts/repair_generalization.py), the trace-coverage audit (scripts/trace_coverage_audit.py), the pre-registered design and results (docs/js_sam_tla_phase3_.md)), the bare-next-contract prototype and full-pipeline studies (tools/plain-js/, scripts/plain_js_tv.py, scripts/lean_full_pipeline_study.py, the 40 saved generations in output/lean_specs*/, docs/js_sam_lean_contract.md), the locksvc harness and corpus (scripts/harness/locksvc/, data/sys_traces/locksvc/), the etcd harness, corpus, reference specification, and study artifacts (scripts/harness/etcd/, data/sys_traces/etcd/ with pinned provenance, output/lean_specs_etcd/, output/lean_full_pipeline_etcd.json, output/lean_etcd_repair.json, scripts/repair_lean_etcd.py), the deployed agent-path runs (scripts/launch_tv_eval.sh; per-spec reports in output/agent_tv_reports/), the TLA⁺ repair round (scripts/repair_tla_spin.py, repaired specifications and TLC output in output/tla_repair/), the methodology note (paper/methodology.md), the literature map (paper/literature_map.md), and the experiment write-ups (docs/js_sam_.md). All of the above reside on a single branch, js-sam-tla-phase3, of the SysMoBench fork at https://github.com/jdubray/SysMoBench-1; the JS-SAM backend itself is additionally merged upstream into https://github.com/specula-org/SysMoBench (PR #17), with the cross-platform and spin trace-harness changes proposed in PR #21. Requirements: Docker, Node \(\geq\) 20, Python 3, and (for the TLA⁺ arm) Java with tla2tools. A single script reproduces the kernel capture: scripts/harness/spin/run.sh. A replication guide (REPLICATION.md, repository root) re-derives every analysis from committed raw data without API access, regenerates every experiment from pinned prompts and models, and inventories the experimenter-authored materials as independent variables to audit or vary.

References↩︎