Skip to content

Software Quality

AI tooling for formal methods

The artifact AI produces here is a specification, and an engine that can refuse it stands behind every entry. The field moves quickly, and these entries may be out of date.

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

The artifact is the spec: AI drafts it, the engine or checker is the oracle; the inverse also appears — the artifact (a statechart, a decision service) constrains an LLM operating under it. No independently-evaluated AI tooling exists at this tier. The commercial features — Camunda's FEEL/BPMN Copilots, Trisotech's AI authoring, Stately Studio AI — are vendor-reported; the rest is 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-from-legal-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, reports good syntactic validity but weak conformance to the system code, so end-to-end synthesis claims warrant skepticism.

Theorem proving

  • AlphaProof (DeepMind 2024)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

No dedicated tool. OSS-Fuzz-Gen's harness-generation pattern transfers; angr+LLM exploration is a 2024–25 research line.

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. DeepMind. 2024. AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/. ↩

  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. ↩