Skip to content

Software Quality

AI tooling for formal methods

The artifact AI produces here is a specification or a proof, and an engine that can refuse it stands behind every entry.

The formal methods family splits into a lightweight tier (decision tables, state machines, executable specifications) and a heavyweight tier (model checking, theorem proving, symbolic execution).

Lightweight tier

At this tier the artifact is the spec: AI drafts it, and the engine or checker is the oracle. The inverse also appears, where a statechart or a decision service constrains an LLM operating under it. No independently-evaluated AI tooling exists at this tier. The commercial features are vendor-reported: Camunda's FEEL/BPMN Copilots, Trisotech's AI authoring and Stately Studio AI. The rest are community proof-of-concept MCP servers and first-party skills (FizzBee, Quint). The research is real but no tool ships it: LLM-generated Alloy test cases and formulas (Cunha and Macedo 2026; Hong et al. 2025)1 2, natural-language → postcondition / contract inference (Endres et al. 2024; Zhang et al. 2025; Richter and Wehrheim 2025)3 4 5, class-invariant synthesis (Sun et al. 2025)6, and DMN generation from natural-language text (Graus 2026; Etikala 2021)7 8. P, UPPAAL, NuSMV, mCRL2, and Promela / SPIN have none. As with the heavyweight tier, conformance of the generated artifact to the real system is the unsolved problem.

Model checking

Specula synthesizes TLA+ specs from source. SysMoBench (Cheng et al. 2025)9, which benchmarks LLM-generated TLA+ models of real-world systems, finds model quality falling with the system's size: high for a spinlock, while on an Etcd Raft implementation only one LLM reached conformance checking, and scored low there. End-to-end synthesis claims warrant skepticism.

Theorem proving

  • AlphaProof (Hubert et al. 2025)10 — closed system; solved three of the six IMO 2024 problems, and with AlphaGeometry 2 scored at silver-medal level.
  • Lean Copilot (Song et al. 2024)11 — open source; runs tactic suggestion, proof search and premise selection natively inside Lean.
  • LeanDojo / ReProver (Yang et al. 2023)12 — research benchmark + retrieval-augmented prover.
  • Llemma (Azerbayev et al. 2023)13 / DeepSeek-Prover (Xin et al. 2024)14 — open-weight proof LLMs.
  • Proverbot9001 (Sanchez-Stern et al. 2020)15 — research tactic prediction.

Most "LLM does proofs" claims are evaluated on miniF2F / mathlib tactics. Project-property verification at seL4 / CompCert scale by LLM remains essentially unsolved.

Symbolic execution

Symbolic execution has no dedicated AI tool. OSS-Fuzz-Gen's harness-generation pattern transfers to it. Research has put an LLM in the solver's place, reasoning over each path in the source language rather than translating it to formulas (Li et al. 2025)16.

Referenced by

References

  1. Cunha, Alcino, and Nuno Macedo. 2026. "Validating Formal Specifications with LLM-generated Test Cases." Rigorous State-Based Methods (ABZ 2026), Lecture notes in computer science, 279–97. https://doi.org/10.1007/978-3-032-26204-2_15. ↩

  2. Hong, Yang, Shan Jiang, Yulei Fu, and Sarfraz Khurshid. 2025. On the Effectiveness of Large Language Models in Writing Alloy Formulas. https://doi.org/10.48550/arXiv.2502.15441. ↩

  3. Endres, Madeline, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. 2024. "Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?" Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024), 1889–912. https://doi.org/10.1145/3660791. ↩

  4. Zhang, Gehao, Zhenting Wang, and Juan Zhai. 2025. Breaking the Myth: Can Small Models Infer Postconditions Too? https://doi.org/10.48550/arXiv.2507.10182. ↩

  5. Richter, Cedric, and Heike Wehrheim. 2025. Beyond Postconditions: Can Large Language Models Infer Formal Contracts for Automatic Software Verification? https://doi.org/10.48550/arXiv.2510.12702. ↩

  6. Sun, Chuyue, Viraj Agashe, Saikat Chakraborty, et al. 2025. "ClassInvGen: Class Invariant Synthesis Using Large Language Models." AI Verification (SAIV 2025), Lecture notes in computer science, 64–96. https://doi.org/10.1007/978-3-031-99991-8_4. ↩

  7. Graus, David. 2026. From Legal Text to Executable Decision Models: Evaluating Structured Representations for Legal Decision Model Generation. https://doi.org/10.48550/arXiv.2604.17153. ↩

  8. Etikala, Vedavyas. 2021. "Extracting Decision Model Components from Natural Language Text for Automated Business Decision Modelling." Proceedings of the 15th International Rule Challenge, 7th Industry Track, and 5th Doctoral Consortium @ RuleML+RR 2021, CEUR workshop proceedings, vol. 2956. https://ceur-ws.org/Vol-2956/paper51.pdf. ↩

  9. Cheng, Qian, Ruize Tang, Emilie Ma, et al. 2025. SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems. https://doi.org/10.48550/arXiv.2509.23130. ↩

  10. Hubert, Thomas, Rishi Mehta, Laurent Sartran, et al. 2025. "Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning." Nature, ahead of print. https://doi.org/10.1038/s41586-025-09833-y. ↩

  11. Song, Peiyang, Kaiyu Yang, and Anima Anandkumar. 2024. Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean. https://doi.org/10.48550/arXiv.2404.12534. ↩

  12. Yang, Kaiyu, Aidan M. Swope, Alex Gu, et al. 2023. "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models." Advances in Neural Information Processing Systems 36, 21573–612. https://doi.org/10.52202/075280-0944. ↩

  13. Azerbayev, Zhangir, Hailey Schoelkopf, Keiran Paster, et al. 2023. Llemma: An Open Language Model For Mathematics. https://doi.org/10.48550/arXiv.2310.10631. ↩

  14. Xin, Huajian, Daya Guo, Zhihong Shao, et al. 2024. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. https://doi.org/10.48550/arXiv.2405.14333. ↩

  15. Sanchez-Stern, Alex, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. 2020. "Generating Correctness Proofs with Neural Networks." Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, 1–10. https://doi.org/10.1145/3394450.3397466. ↩

  16. Li, Yihe, Ruijie Meng, and Gregory J. Duck. 2025. "Large Language Model Powered Symbolic Execution." Proceedings of the ACM on Programming Languages 9 (OOPSLA2). https://doi.org/10.1145/3763163. ↩