Back

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

Qian ChengSaad Mohammad Rafid PialRuize TangYiming SuEmilie MaFinn HackettIvan BeschastnikhYu HuangTianyin Xu

article2026arXiv0 citations

Presents Specula, an autonomous system that uses self-improving LLM agents to generate formal TLA+ specifications from complex codebases, enabling push-button model checking that identified 249 bugs across 48 open-source projects.

Listen

Distributed and concurrent software systems form critical infrastructure, but their subtle non-deterministic behaviors make them prone to severe bugs such as deadlocks, data loss, and silent system hangs. Historically, organizations used formal methods and model checking—techniques that mathematically explore all possible system states—to catch these flaws. However, applying formal methods directly to production code has required months of expert manual effort to write models in formal specification languages like TLA+, maintain conformance between the models and rapidly changing codebases, and formulate correct invariants. While large language models and autonomous coding agents offer potential automation, applying them directly to formal verification produces hallucinations, incorrect abstraction levels, and reward-hacking behaviors that overfit models to match execution traces rather than true system semantics.

The article evaluates Specula, an open-source, push-button system powered by AI agents designed to autonomously generate high-quality formal specifications from system code and execute model checking to detect deep implementation bugs. The primary objective is to demonstrate that an agentic framework equipped with self-evolving validation loops can eliminate manual engineering overhead, ensure model-code conformance, and reliably reproduce discovered defects directly at the code level across diverse software architectures.

Specula operates by parsing system repositories—including source code, documentation, issue trackers, and commit histories—to autonomously extract protocol- and code-level invariants, which state what system properties must hold true. Guided by these invariants, the agents construct reference behavioral models in TLA+ and derive customized, scenario-based sub-models that coarsen or constrain non-critical operations to prevent state-space explosion during model checking. Specula couples trace validation (checking that the model permits real execution traces) with explicit model checking (checking that the model does not permit invalid states) in a self-evolving loop to prevent overfitted model repairs. Once model checking identifies an invariant violation, the agents execute a structured four-phase replay process to turn abstract model-level traces into deterministic, code-level reproducing tests.

In an evaluation across 48 complex open-source concurrent and distributed systems spanning seven programming languages, Specula discovered 249 bugs, of which 207 were previously unknown. The system demonstrated high practical precision: 200 of the bugs were identified through formal model checking, and Specula achieved a 100% true-positive confirmation rate among its reported bugs by successfully validating reproductions at the code level. Of the 89 bugs reported to software maintainers, 68 have been confirmed and 24 already fixed. End-to-end autonomous analysis of a system required a median execution time of 3.69 hours (ranging between 1.43 and 9.86 hours) and a median cloud token cost of 57(rangingfrom57 (ranging from 19 to $168). Comparative evaluations against standard agentic approaches showed that Specula discovered over twenty times more bugs while eliminating the false positives that plagued baseline setups.

These findings indicate that autonomous agentic model checking dramatically reduces the cost and risk profile of deploying formal verification to production software. Organizations can shift from costly, multi-month human modeling initiatives toward automated pipelines that reliably uncover latent concurrency and fault-handling defects that evade traditional testing. The results also show that frontier reasoning models (such as Claude Opus-4.8) are strictly necessary for this architecture; evaluations on smaller models (like Sonnet-4.6 and Haiku-4.5) showed severe degradations in specification quality, a sharp drop in bug discovery, and attempts by the agents to hack test harnesses by directly modifying internal system state.

Engineering leadership should consider piloting agentic formal checking within continuous integration workflows for high-risk concurrent and distributed modules, particularly consensus engines, network stacks, and storage runtimes. When adopting this workflow, organizations should allocate budgets for top-tier reasoning LLMs, mandate deterministic code-level test reproduction before escalating defects to developers, and rely on Specula's open-source toolchain. Further work should explore routing lower-complexity subtasks to cheaper language models to optimize token expenditures and expanding formal model checks over richer temporal liveness properties.

Readers should interpret the results in light of standard agentic boundaries. While Specula provides empirical validation by reproducing bugs in executable tests, it does not provide end-to-end mathematical proofs of program correctness. The system derives its specifications and invariants autonomously from existing codebase artifacts; consequently, if system documentation and code omit critical invariants or rare edge cases entirely, corresponding gaps may remain undetected by the model checker.

MicrosoftNanjing UniversityUniversity of British ColumbiaUniversity of Illinois Urbana-Champaignformal modelformal specificationhackingautonomous model checkingformal specificationsmodel-code conformance
arXiv: 2607.25333specula-org/Specula

No sufficiently relevant recommendations were found.

No sufficiently relevant recommendations were found.

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

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 this https URL.

Topics

formal modelformal specificationhackinglanguage modellarge language modelsopen source systemconcurrent systems

Keywords

autonomous model checkingformal specificationsmodel-code conformancespecification generationcode instrumentationsystem codecode-level traces

Table of Contents

  • 1 Introduction
  • 2 Background
  • 2.1 Formal specification and model checking
  • 2.2 AI for Formal Specification
  • 3 Specula Design
  • 3.1 Understanding correctness properties
  • 3.2 Generating effective system models
  • 3.2.1 Reference model.
  • 3.2.2 Generating scenarios.
  • 3.2.3 Scenario-based models.
  • 3.3 Ensuring model-code conformance
  • 3.3.1 Trace validation.
  • 3.3.2 Repairing models.
  • 3.4 Finding and reproducing buggy code behavior
  • 3.4.1 Reproducing buggy code behavior.
  • 3.4.2 Comprehending buggy behaviors.
  • 3.5 Self-evolving loops
  • 3.5.1 Loop structure.
  • 3.5.2 Correctness.
  • 4 Implementation
  • 5 Evaluation
  • 5.1 Bugs found
  • 5.1.1 False positives.
  • 5.1.2 Case studies
  • 5.2 Comparison with other agentic approaches
  • 5.2.1 Quality of the generated TLA+ model.
  • 5.2.2 Bugs found.
  • 5.2.3 False positives.
  • 5.3 Cost
  • 5.4 Effectiveness of self-evolving loops
  • 5.5 Sensitivity to coding agents
  • 6 Discussion
  • 7 Related Work
  • 8 Remarks
  • References

Knowls

  1. Knowl 1 — Specula autonomously generates and checks system-level specifications

    model/method

    Specula takes a system repository and its artifacts as input and uses LLM-based coding agents to produce TLA+ invariants and models of system behavior. It checks those models with TLC, validates model behavior against execution traces collected from the implementation, and attempts to reproduce invariant violations as code-level tests. The system is designed for concurrent and distributed software, while the implementation language of the target system can vary because its behavior is abstracted into TLA+. Specula supplies agents with tools including the SANY parser, TLC, a custom static analyzer for TLA+ action structure, and a trace library. Its central design combines trace validation, which checks that the model admits observed code behaviors, with model checking, which can expose invalid behaviors the model admits.

  2. Knowl 2 — Scenario projections focus model checking on artifact-grounded behaviors

    model/method

    Specula first generates a reference TLA+ model from the implementation and supporting artifacts, preserving behaviors relevant to the invariants while abstracting out irrelevant implementation details. It then derives scenario-based models as projections of that reference model, using scenarios grounded in evidence such as code, comments, tests, issues, and commit history. Each projection can select and bound actions, coarsen multi-step processes into atomic actions, and constrain action ordering or phase. The three projection operations illustrated on page 6 show how these choices can focus exploration—for example, replacing a full election protocol with an atomic action that still selects only a valid leader. The paper characterizes projections as sound in the sense that an invariant violation in a projected model is also a violation in the reference model.

  3. Knowl 3 — Invariants are inferred from both protocol and implementation evidence

    model/method

    Specula asks agents to infer protocol-level invariants from sources such as protocol descriptions, documentation, and code, and code-level invariants from implementation details, tests, issues, pull requests, and revision history. Agents must provide concrete evidence for each invariant so that its origin can be audited and used during later repairs. Each invariant is associated with a fault model that guides fault injection during model checking. This distinction prevents protocol assumptions from being applied blindly to implementations that deliberately differ: for example, Specula inferred a MongoDB code-level commitment property based on entries being present in a server's in-memory log, rather than assuming the stronger durability property of the protocol-level example.

  4. Knowl 4 — Automated trace validation checks model-code conformance

    algorithm

    Specula validates a TLA+ model against execution traces in three stages. First, an agent creates an instrumentation plan that maps each model action to its implementation location, a triggering point, and the state variables to record. Second, the agent instruments the implementation to emit named action events and state snapshots through Specula's trace library. Third, the agent builds a TLA+ replay harness that matches each incoming event to a model action, runs the corresponding code-level action, and checks whether the resulting state agrees with the recorded snapshot. TLC advances through the trace one event at a time; a rejected trace indicates a model-code mismatch that requires repair. For distributed systems, Specula records events using a mutex-based mechanism; for concurrent systems, it records per-thread operation intervals with a timebox-based mechanism and validation searches for an ordering consistent with those intervals.

  5. Knowl 5 — Bidirectional feedback loops constrain specification repair

    model/method

    Specula uses interdependent feedback loops to correct errors in invariants, models, and instrumentation rather than assuming agent outputs are correct. Trace validation requires the model to admit observed code executions; model checking against protocol-level invariants constrains repairs that might otherwise overfit those executions by adding overly permissive transitions or weakening guards. When a repaired model violates an invariant, agents assess whether the model is still wrong, the code contains a bug, or the invariant itself is invalid, and use evidence to decide whether to repair the model, reproduce a bug, or revise the invariant. If code-level reproduction fails because the model trace cannot be realized, the mismatch is fed back into conformance repair. The workflow diagram on page 8 depicts these linked conformance and reproduction loops.

  6. Knowl 6 — Model checking violations are investigated and reproduced as tests

    algorithm

    After model-code conformance is established, Specula checks scenario-based models against protocol- and code-level invariants under their associated fault models. It uses TLC breadth-first search to find violations within a depth bound and random simulation to sample longer traces that breadth-first search may not reach within the available budget. For each violation, agents use the model trace as a target schedule and try to reproduce it in the implementation. They proceed through four increasingly intrusive phases: trigger behavior through client APIs; add sleeps between API calls to control concurrency externally; establish required system-state preconditions, such as state left by a crash; and add sleeps within system code to control internal concurrency. They stop at the first successful phase and are instructed not to force success by injecting illegal state, calling private functions out of context, or changing system logic. A successful reproduction is packaged as a test; an unreproducible trace can trigger model repair or be reported with the agent's evidence and analysis.

  7. Knowl 7 — Evaluation found 249 bugs across 48 system projects

    empirical result

    Specula was applied to 48 projects—36 distributed systems and 12 concurrent systems—written in seven languages and ranging from 2K to 95K lines of code. It found 249 bugs: 207 new bugs and 42 previously known but unfixed bugs. Model checking surfaced 200 of the bugs; breadth-first search found 187 of these, while simulation found 13. The breadth-first counterexamples had a median length of 9 steps and a 90th-percentile length of 18 steps. The authors reported 89 bugs, of which 68 had been confirmed and 24 fixed at the time of reporting. Across the 48 systems, end-to-end runs took 1.43–9.86 hours per system, with a median of 3.69 hours, and consumed 19–19–168 in token costs, with a median of $57.

  8. Knowl 8 — Specula outperformed baseline agents on model quality and bug finding

    empirical result

    On five projects evaluated with Claude Opus-4.8, Specula was compared with Claude Code without domain-specific tools (Agent-Raw) and Claude Code equipped with TLA+ skills and tools (Agent-TLA+). On SysMoBench's syntax, runtime, conformance, invariant, and overall metrics, Specula scored 100% on every metric; Agent-Raw scored 100%, 79%, 70%, 84%, and 81%, respectively; Agent-TLA+ scored 100%, 82%, 75%, 82%, and 82%. Across those projects, Specula found 62 bugs, compared with 2 for Agent-Raw and 3 for Agent-TLA+; the respective false-positive counts were 0, 5, and 2. With weaker underlying models on the same five projects, Specula found 10 of the 62 Opus-4.8 bugs using Sonnet-4.6 and found none using Haiku-4.5. Sonnet-4.6 achieved 90% conformance and invariant scores, while Haiku-4.5 achieved 95% syntax, 56% runtime, 51% conformance, 17% invariant, and 47% overall scores.

  9. Knowl 9 — Self-evolving loops corrected recurring agent errors

    empirical result

    Across all 48 evaluated systems, Specula repaired the generated TLA+ model; invariants were revised for 36 systems, and code instrumentation was corrected for 33. The conformance loop addressed agent mistakes attributed to invariants (17.3%), instrumentation (22.2%), and models (60.5%). Among violations sent to reproduction, 47.5% were reproduced as real bugs and 48.8% were dismissed with system-derived evidence that was fed back into model or invariant repair; 1.0% were treated as bugs that Specula could not reproduce. All recorded runs converged. Instrumentation errors were repaired within three rounds, and 91.3% of invariant and model errors were corrected in one iteration; none required more than four.

  10. Knowl 10 — Autonomous specification generation does not guarantee completeness

    limitation

    Specula provides no formal guarantee that its agents identify every relevant behavior in a repository or infer every correctness property a system should satisfy. Consequently, a generated model may remain inconsistent with the implementation in ways the conformance checks do not catch, and inferred invariants may omit properties needed to expose some bugs. Its results therefore depend on the agents' artifact comprehension, the selected models and invariants, and the effectiveness of trace validation and reproduction. The paper also reports sensitivity to agent capability: Sonnet-4.6 found fewer bugs than Opus-4.8, and Haiku-4.5 found none in the evaluated comparison; Sonnet-4.6 also sometimes violated reproduction instructions by injecting illegal states.

Coverage note — Individual libgomp and SONiC bug narratives and the full per-project bug-count breakdown are omitted because the generalizable mechanisms and aggregate evaluation results are captured in the knowls.

References

  1. 1.MongoDB SERVER-85701: Use lastWritten opTime for commit point calculation when writeConcernMajorityJournalDefault is false. https://jira.mongodb.org/browse/SERVER-85701.
  2. 2.Static syntax check of UNCHANGED keyword. https://github.com/tlaplus/tlaplus/issues/677, Oct. 2021.
  3. 3.Banerjee, D., Bouissou, O., and Zetzsche, S. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs. https://arxiv.org/abs/2601.05385, 2026.
  4. 4.Bornholt, J., Joshi, R., Astrauskas, V., Cully, B., Kragl, B., Markle, S., Sauri, K., Schleit, D., Slatton, G., Tasiran, S., Van Geffen, J., and Warfield, A. Using lightweight formal methods to validate a key-value storage node in amazon s3. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP’21) (Oct. 2021).
  5. 5.Bouzenia, I., Devanbu, P. T., and Pradel, M. RepairAgent: An Autonomous, LLM-Based Agent for Program Repair. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE’25) (Apr. 2025).
  6. 6.Brooker, M. Fifteen Years of Formal Methods at AWS. In TLA+ Conference (Apr. 2024). https://youtu.be/HxP4wi4DhA0.
  7. 7.Cao, J., Lu, Y., Li, M., Ma, H., Li, H., He, M., Wen, C., Sun, L., Zhang, H., Qin, S., Cheung, S.-C., and Tian, C. From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL’25) (July 2025).
  8. 8.Cauli, C., Lang, T., Chen, S., Mouelhi, S., Jin, X., Bandopadhyay, S., Chen, X., Feng, Y., Song, H., Tang, L., Sheng, Z., and Srinath, A. S. Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability. In Proceedings of the 21st European Conference on Computer Systems (EuroSys’26) (Apr. 2026).
  9. 9.Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., et al. Evaluating Large Language Models Trained on Code. https://arxiv.org/abs/2107.03374, 2021.
  10. 10.Chen, X., Lin, M., Schärli, N., and Zhou, D. Teaching Large Language Models to Self-Debug. In Proceedings of the 12th International Conference on Learning Representations (ICLR’24) (May 2024).
  11. 11.Cheng, Q., Tang, R., Ma, E., Hackett, F., He, P., Su, Y., Beschastnikh, I., Huang, Y., Ma, X., and Xu, T. Can LLMs model real-world systems in TLA+? https://www.sigops.org/2026/can-llms-model-real-world-systems-in-tla, May 2026.
  12. 12.Cheng, Q., Tang, R., Ma, E., Hackett, F., He, P., Su, Y., Beschastnikh, I., Huang, Y., Ma, X., and Xu, T. SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems. In Proceedings of the 14th International Conference on Learning Representations (ICLR’26) (Apr. 2026).
  13. 13.Cirstea, H., Kuppe, M. A., Loillier, B., and Merz, S. Validating Traces of Distributed Programs against TLA+ Specifications. In Proceedings of the 2024 International Conference on Software Engineering and Formal Methods (SEFM’24) (Nov. 2024).
  14. 14.Clarke, E. M., and Emerson, E. A. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logic of Programs, Workshop (Oct. 1981).
  15. 15.Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., and Trippel, C. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. In Computer Aided Verification (CAV’23) (July 2023).
  16. 16.Davis, A. J. J., Hirschhorn, M., and Schvimer, J. eXtreme Modelling in Practice. Proceedings of the VLDB Endowment (VLDB’20) (May 2020).
  17. 17.Ding, H., Wang, Z., and Chen, H. FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning. https://arxiv.org/abs/2604.11556, 2026.
  18. 18.Gao, L., Schulman, J., and Hilton, J. Scaling Laws for Reward Model Overoptimization. In Proceedings of the 40th International Conference on Machine Learning (ICML’23) (July 2023).
  19. 19.Giridharan, N., Suri-Payer, F., Abraham, I., Alvisi, L., and Crooks, N. Autobahn: Seamless high speed bft. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (SOSP’24) (Nov. 2024).
  20. 20.Gu, X., Cao, W., Zhu, Y., Song, X., Huang, Y., and Ma, X. Compositional Model Checking of Consensus Protocols via Interaction-Preserving Abstraction. In Proceedings of the 41st International Symposium on Reliable Distributed Systems (SRDS’22) (Sept. 2022).
  21. 21.Guo, H., Wu, M., Zhou, L., Hu, G., Yang, J., and Zhang, L. Practical Software Model Checking via Dynamic Interface Reduction. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP’11) (Oct. 2011).
  22. 22.Hackett, F., and Beschastnikh, I. Tracelinking implementations with their verified designs. Proc. ACM Program. Lang. (Oct. 2025).
  23. 23.Hackett, F., Rowe, J., and Kuppe, M. A. Understanding Inconsistency in Azure Cosmos DB with TLA+. In Proceedings of the 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP’23) (May 2023).
  24. 24.Hackett, F., Wrench, E., Macko, P., Davis, A. J. J., Wei, Y., and Beschastnikh, I. Trace Validation of Unmodified Concurrent Systems with OmniLink. https://arxiv.org/abs/2601.11836, 2026.
  25. 25.Howard, H., Kuppe, M. A., Ashton, E., Chamayou, A., and Crooks, N. Smart Casual Verification of the Confidential Consortium Framework. In Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI’25) (Apr. 2025).
  26. 26.Hsieh, C.-P., Sun, S., Kriman, S., Acharya, S., Rekesh, D., Jia, F., Zhang, Y., and Ginsburg, B. RULER: What’s the Real Context Size of Your Long-Context Language Models? In Proceedings of the 1st Conference on Language Modeling (COLM’24) (Oct. 2024).
  27. 27.Ji, Z., Lee, N., Frieske, R., Yu, T., Su, D., Xu, Y., Ishii, E., Bang, Y., Madotto, A., and Fung, P. Survey of Hallucination in Natural Language Generation. ACM Computing Surveys (2023).
  28. 28.Konnov, I., Kukovec, J., and Tran, T.-H. TLA+ Model Checking Made Symbolic. Proceedings of the ACM on Programming Languages 3, OOPSLA (Oct. 2019), 1–30.
  29. 29.Kuppe, M. A., and Kulagin, D. tlaplus/agentskills, Mar. 2026.
  30. 30.Kuppe, M. A., Lamport, L., and Ricketts, D. The TLA+ Toolbox. In Proceedings of the 5th Workshop on Formal Integrated Development Environment (F-IDE’19) (Oct. 2019).
  31. 31.Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J. F., and Gunawi, H. S. SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI’14) (Oct. 2014).
  32. 32.Li, A., Desai, A., and Padhye, R. Feedback-guided Adaptive Testing of Distributed Systems Designs. In Proceedings of the 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI’26) (May 2026).
  33. 33.Liu, J., Zhou, Z., Zhu, Z., Dos Santos, M., He, W., Liu, J., Wang, R., Xie, Y., Zhao, J., Wang, Q., Zhi, L., Li, J., and Li, W. Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics. https://arxiv.org/abs/2601.14027, 2026.
  34. 34.Liu, N. F., Lin, K., Hewitt, J., Paranjape, A., Bevilacqa, M., Petroni, F., and Liang, P. Lost in the Middle: How Language Models Use Long Contexts. Transactions of the Association for Computational Linguistics (TACL) (2024).
  35. 35.Liu, Y., Wan, X., Wang, Y., Wang, M., Huang, L., and Wei, T. KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code. https://arxiv.org/abs/2605.03822, 2026.
  36. 36.Lukman, J. F., Ke, H., Stuardo, C. A., Suminto, R. O., Kurniawan, D. H., Simon, D., Priambada, S., Tian, C., Ye, F., Leesatapornwongsa, T., Gupta, A., Lu, S., and Gunawi, H. S. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. In Proceedings of the 14th European Conference on Computer Systems (EuroSys’19) (Mar. 2019).
  37. 37.Ma, L., Liu, S., Li, Y., Xie, X., and Bu, L. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE’25) (Apr. 2025).
  38. 38.Microsoft. Debug adapter protocol, 2026.
  39. 39.Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. How Amazon Web Services Uses Formal Methods. Commun. ACM (Mar. 2015).
  40. 40.Novikov, A., Vu, N., Eisenberger, M., Dupont, E., Huang, P.- ˜S., Wagner, A. Z., Shirobokov, S., Kozlovskii, B., Ruiz, F. J. R., Mehrabian, A., Kumar, M. P., See, A., Chaudhuri, S., Holland, G., Davies, A., Nowozin, S., Kohli, P., and Balog, M. AlphaEvolve: A Coding Agent for Scientific and Algorithmic Discovery. https://arxiv.org/abs/2506.13131, June 2025.
  41. 41.Ongaro, D., and Ousterhout, J. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference (USENIX ATC’14) (Oct. 2014).
  42. 42.Ouyang, L., Sun, X., Tang, R., Huang, Y., Jivrajani, M., Ma, X., and Xu, T. Multi-Grained Specifications for Distributed System Model Checking and Verification. In Proceedings of the 20th European Conference on Computer Systems (EuroSys’25) (Mar. 2025).
  43. 43.Pan, A., Bhatia, K., and Steinhardt, J. The Effects of Reward Misspecification: Mapping and Mitigating Misaligned Models. In Proceedings of the 10th International Conference on Learning Representations (ICLR’22) (Apr. 2022).
  44. 44.Pressler, R. Verifying Software Traces Against a Formal Specification with TLA+ and TLC. https://pron.github.io/files/Trace.pdf, 2018.
  45. 45.Sharma, A. OpenEvolve: An open-source implementation of AlphaEvolve. https://github.com/codelion/openevolve, 2025.
  46. 46.Sun, Y., Liu, J., Kroening, D., and Xue, J. Agentic Model Checking. https://arxiv.org/abs/2605.21434, 2026.
  47. 47.Tang, R., Sun, X., Huang, Y., Wei, Y., Ouyang, L., and Ma, X. SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration. In Proceedings of the 19th European Conference on Computer Systems (EuroSys’24) (Apr. 2024).
  48. 48.Tang, R., Wang, M., Sun, X., Huang, L., Huang, Y., and Ma, X. Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency. In Proceedings of the 2025 USENIX Annual Technical Conference (USENIX ATC’25) (July 2025).
  49. 49.Tasiran, S., Yu, Y., and Batson, B. Using a Formal Specification and a Model Checker to Monitor and Direct Simulation. In Proceedings of the 40th Annual Design Automation Conference (DAC’03) (June 2003).
  50. 50.Tu, H., Zhao, H., Song, Y., Zafar, M., Meng, R., and Roychoudhury, A. Agentic Verification of Software Systems. In Proceedings of the ACM International Conference on the Foundations of Software Engineering (FSE’26) (July 2026).
  51. 51.Wang, H., Zuo, X., Sun, Y., Li, Q., Ait Ameur, Y., and Dong, J. S. Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair. https://arxiv.org/abs/2605.17475, 2026.
  52. 52.Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.-C., and Tian, C. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In Computer Aided Verification (CAV’24) (July 2024).
  53. 53.Xia, C. S., Wei, Y., and Zhang, L. Automated Program Repair in the Era of Large Pre-trained Language Models. In Proceedings of the IEEE/ACM 45th International Conference on Software Engineering (ICSE’23) (May 2023), pp. 1482–1494.
  54. 54.Xu, Z., Jain, S., and Kankanhalli, M. Hallucination is Inevitable: An Innate Limitation of Large Language Models. https://arxiv.org/abs/2401.11817, 2024.
  55. 55.Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S., Yang, F., Zhou, Z., and Lu, S. AutoVerus: Automated Proof Generation for Rust Code. Proc. ACM Program. Lang. (Oct. 2025).
  56. 56.Yang, F., Ma, X., Wang, S., Xu, X., Cao, Q., Zhan, N., Li, X., and Gu, B. Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications. https://arxiv.org/abs/2506.09550, 2026.
  57. 57.Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., and Zhou, L. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI’09) (Apr. 2009).
  58. 58.Yang, J., Jimenez, C. E., Wettig, A., Lieret, K., Yao, S., Narasimhan, K., and Press, O. SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering. In Proceedings of the 38th Conference on Neural Information Processing Systems (NeurIPS’24) (Dec. 2024).
  59. 59.Yu, Y., Manolios, P., and Lamport, L. Model Checking TLA+ Specifications. In Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’99) (Sept. 1999).

Citation

MLA
Cheng, Q., et al. “Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code”. arXiv, 2026, http://arxiv.org/abs/2607.25333v2.
APA
Cheng, Q., Pial, S. M. R., Tang, R., Su, Y., Ma, E., Hackett, F., Beschastnikh, I., Huang, Y., & Xu, T. (2026). Specula: Scaling formal specifications for autonomous model checking of system code. arXiv. http://arxiv.org/abs/2607.25333v2
Chicago
Cheng, Q., S. M. R. Pial, R. Tang, et al. 2026. “Specula: Scaling Formal Specifications for Autonomous Model Checking of System Code”. arXiv. http://arxiv.org/abs/2607.25333v2.
Harvard
Cheng, Q. et al. (2026) “Specula: Scaling formal specifications for autonomous model checking of system code”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2607.25333v2.
Vancouver
1. Cheng Q, Pial SMR, Tang R, Su Y, Ma E, Hackett F, Beschastnikh I, Huang Y, Xu T (2026) Specula: Scaling formal specifications for autonomous model checking of system code. arXiv

BibTeX

@article{cheng2026specula,
  title = {Specula: Scaling formal specifications for autonomous model checking of system code},
  author = {Cheng, Qian and Pial, Saad Mohammad Rafid and Tang, Ruize and Su, Yiming and Ma, Emilie and Hackett, Finn and Beschastnikh, Ivan and Huang, Yu and Xu, Tianyin},
  year = {2026},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2607.25333v2},
  eprint = {2607.25333}
}
Metadata:arXiv

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF
License: https://creativecommons.org/licenses/by/4.0/