Specula: Scaling formal specifications for autonomous model checking of system code

• URL: http://arxiv.org/abs/2607.25333v2
• Date: Mon, 03 Aug 2026 09:00:50 GMT
• Title: Specula: Scaling formal specifications for autonomous model checking of system code
• Abstract summary: Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code.<n>Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications.
• Score: 8.484545401876316
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.

Related papers

• SpecCoder: Specification-Aware Code Generation with Curriculum Dual-Task Reinforcement Learning [30.588079618949447]
  SpecCoder is a specification-aware two-stage training framework for code generation.<n>It first employs specification-guided SFT to train GRPs to derive structured specification analyses and generate code conditioned on them.<n>It then introduces curriculum dual-taskO, which jointly optimize specification-guided generation and discrimination to encourage stronger correspondence between specifications and code behavior.
  arXiv  Detail & Related papers  (2026-09-05T11:52:54Z)
• KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base [9.796586560498026]
  We propose KBSpec, which augments large language models (LLMs) with dual-source knowledge of formal specification language corpora.<n>Results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches.
  arXiv  Detail & Related papers  (2026-06-19T11:37:00Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol.<n>CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions.<n>We observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate.
  arXiv  Detail & Related papers  (2026-04-14T04:31:45Z)
• MASEval: Extending Multi-Agent Evaluation from Models to Systems [77.09381093359598]
  MASEval is a framework-agnostic library that treats the entire system as the unit of analysis.<n>It allows researchers to explore all components of agentic systems, opening new avenues for principled system design.
  arXiv  Detail & Related papers  (2026-03-09T18:46:17Z)
• Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC [6.536447932095715]
  This paper introduces SYSSPEC, a framework for developing generative file systems.<n>Instead of imprecise prompts, SYSSPEC employs a multi-part specification that accurately describes a file system's functionality.<n>To manage evolution, we develop a DAG-structured patch that operates on the specification itself.
  arXiv  Detail & Related papers  (2025-12-15T07:15:01Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems [12.181911851729614]
  We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems.<n>We focus on concurrent and distributed systems, which are keystones of today's critical computing infrastructures.
  arXiv  Detail & Related papers  (2025-09-27T05:24:54Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
  We use TLA+ to model fine-grained behaviors of ZooKeeper and the TLC model checker to verify its correctness properties. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space.
  arXiv  Detail & Related papers  (2024-09-22T02:59:56Z)
• TurboSpec: Closed-loop Speculation Control System for Optimizing LLM Serving Goodput [37.56866491624234]
  Large Language Model (LLM) serving systems batch concurrent user requests to achieve efficient serving.<n>We present TurboSpec, a speculation control system that automatically profiles the execution environment.<n>We demonstrate its effectiveness across diverse workloads and hardware configurations.
  arXiv  Detail & Related papers  (2024-06-20T07:43:33Z)
• InfiBench: Evaluating the Question-Answering Capabilities of Code Large Language Models [56.723509505549536]
  InfiBench is the first large-scale freeform question-answering (QA) benchmark for code to our knowledge. It comprises 234 carefully selected high-quality Stack Overflow questions that span across 15 programming languages. We conduct a systematic evaluation for over 100 latest code LLMs on InfiBench, leading to a series of novel and insightful findings.
  arXiv  Detail & Related papers  (2024-03-11T02:06:30Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  Continual Learning (CL) is an important aspect that remains underexplored in the code domain. We introduce a benchmark called CodeTask-CL that covers a wide range of tasks, including code generation, translation, summarization, and refinement. We find that effective methods like Prompt Pooling (PP) suffer from catastrophic forgetting due to the unstable training of the prompt selection mechanism.
  arXiv  Detail & Related papers  (2023-07-05T16:58:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.