ACM SIGOPS: Can LLMs Model Real-World Systems in TLA+? — SysMoBench Reveals Critical Gap Between Textbook and Implementation

ACM SIGOPS / Hacker News·medium signalXBlueskyLinkedInCopy link

ACM SIGOPS published research from the Specula team introducing SysMoBench, an automated benchmark testing LLMs on formal specification of 11 real-world concurrent and distributed systems in TLA+. Key finding: LLMs produce structurally correct TLA+ modules but write textbook protocol formalizations rather than modeling actual implementations — they know what Raft looks like but don't know how Etcd splits actions across steps. The team's specialized agent Specula achieves full conformance on tasks where frontier models fail.