Search papers, labs, and topics across Lattice.
This study investigates the ability of large language models to generate formal specifications using both a rarely seen formal language and a mainstream language, JavaScript, within the context of SysMoBench. By employing a controlled comparison across four advanced models and three distinct systems, the research reveals that the fidelity of specifications is primarily governed by the specification contract rather than the language used. Notably, while executable JavaScript can achieve fidelity comparable to TLA+, understanding complex protocols remains a significant challenge that no contract shape or language can fully address.
Executable JavaScript can match the fidelity of formal specifications, but understanding complex protocols remains a critical hurdle for large language models.
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.
