Can large language models write faithful formal specifications of real systems, and does it matter whether they write in a formal language they have seen rarely or in a mainstream language abundant in their training data? We study this on SysMoBench, which grades a generated specification in four phases, the decisive one replaying execution traces captured from the running system. We add JS-SAM, its first non-formal backend, in which a specification is executable JavaScript written in the SAM pattern, a pattern whose semantics mirror TLA+, and run a controlled comparison that separates three variables an ordinary head-to-head entangles: the language, the specification contract (the shape the model must fill), and the prompt. The study spans four frontier models and three systems (an operating-system spinlock, a distributed lock service, and the Etcd Raft consensus implementation), with counterexample-driven repair. Three findings emerge. First, conformance against the real system is the only phase that discriminates among models; internal consistency is inexpensive to satisfy, and a specification that looks right is not thereby right. Second, once the comparison is drawn like for like, the specification contract, not the language, governs fidelity: JavaScript in the shape of the TLA+ transition relation is as faithful as TLA+. Third, a minimal contract carries transcription but not semantic derivation: at consensus scale the difficulty becomes understanding the protocol, which no contract shape and no language supplies. We frame executable JavaScript as a checkable specification substrate that complements, rather than replaces, the verification TLA+ provides, and present the study as a case study.
Formal verification is seldom applied to production software, because writing and maintaining a model has historically cost more than it returns. A companion study [1] extended SysMoBench [4] with a lower-cost alternative: specifications are graded against traces captured from the running system. It found that when large language models write the specifications, reliability is governed by the structure of the specification contract, not the language. This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system, which must keep the register, payment terminal, and payment processor in agreement. We report three results. First, the core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model. The audit found seven failure-handling gaps, nearly all with a common root cause; three were reproduced as real executions, and a patch closing them was re-checked with all failure gates enabled, after which a follow-up patch closed a defect the re-check itself exposed. Systematic extensions of the failure model (crash-restart, stale reads, two attempts) each found the windows they were designed to probe. Second, a single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable against the live API. The emulator-based audit could not detect it, because code and emulator share the same misreading: a correlated-oracle failure. Third, the companion study's central finding replicates across seven models from two vendors: contract structure, not language, governs what LLMs specify reliably. The replication concerns the ordering of contracts and the failure taxonomy, not the absolute level: only the strongest models reached the corpus ceiling, and the harder task restores discriminating power the benchmark had lost.