# 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](https://quality.stereobooster.com/formal.md) 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](https://alloytools.org/) test cases and formulas (Cunha and Macedo 2026; Hong et al. 2025)[^cunha2025a] [^hong2025], natural-language → postcondition / contract inference (Endres et al. 2024; Zhang et al. 2025; Richter and Wehrheim 2025)[^endres2024] [^zhang2025] [^richter2025], class-invariant synthesis (Sun et al. 2025)[^sun2025], and DMN-from-legal-text (Graus 2026; Etikala 2021)[^graus2026] [^etikala2021]. [P](https://github.com/p-org/P), [UPPAAL](https://uppaal.org/), [NuSMV](https://nusmv.fbk.eu/), [mCRL2](https://www.mcrl2.org/), and [Promela](https://spinroot.com/spin/Man/promela.html) / [SPIN](https://spinroot.com/spin/whatispin.html) have none. As with the heavyweight tier, conformance of the generated artifact to the real system is the unsolved problem. ## Model checking [Specula](https://github.com/specula-org/Specula) synthesizes [TLA+](https://lamport.azurewebsites.net/tla/tla.html) specs from source. **SysMoBench** (Cheng et al. 2025)[^cheng2025], 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)[^deepmind2024] — 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)[^song2024] — open source; runs tactic suggestion, proof search and premise selection natively inside Lean. - **LeanDojo / ReProver** (Yang et al. 2023)[^yang2023] — research benchmark + retrieval-augmented prover. - **Llemma** (Azerbayev et al. 2023)[^azerbayev2023] / **DeepSeek-Prover** (Xin et al. 2024)[^xin2024] — open-weight proof LLMs. - **Proverbot9001** (Sanchez-Stern et al. 2020)[^sanchezstern2020] — research tactic prediction. Most "LLM does proofs" claims are evaluated on miniF2F / mathlib tactics. Project-property verification at [seL4](https://sel4.systems/) / [CompCert](https://compcert.org/) scale by LLM remains essentially unsolved. ## Symbolic execution No dedicated tool. [OSS-Fuzz-Gen](https://github.com/google/oss-fuzz-gen)'s harness-generation pattern transfers; angr+LLM exploration is a 2024–25 research line. ## Referenced by - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^cunha2025a]: Cunha, Alcino, and Nuno Macedo. 2026. "[Validating Formal Specifications with LLM-generated Test Cases](https://arxiv.org/pdf/2510.23350)." *Rigorous State-Based Methods (ABZ 2026)*, Lecture notes in computer science, 279–97. [https://doi.org/10.1007/978-3-032-26204-2\\\_15](https://doi.org/10.1007/978-3-032-26204-2\_15). [^hong2025]: Hong, Yang, Shan Jiang, Yulei Fu, and Sarfraz Khurshid. 2025. *[On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://arxiv.org/pdf/2502.15441)*. . [^endres2024]: Endres, Madeline, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. 2024. "[Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://arxiv.org/pdf/2310.01831)" *Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024)*, 1889–912. . [^zhang2025]: Zhang, Gehao, Zhenting Wang, and Juan Zhai. 2025. *[Breaking the Myth: Can Small Models Infer Postconditions Too?](https://arxiv.org/pdf/2507.10182)* . [^richter2025]: Richter, Cedric, and Heike Wehrheim. 2025. *[Beyond Postconditions: Can Large Language Models Infer Formal Contracts for Automatic Software Verification?](https://arxiv.org/pdf/2510.12702)* . [^sun2025]: Sun, Chuyue, Viraj Agashe, Saikat Chakraborty, et al. 2025. "[ClassInvGen: Class Invariant Synthesis Using Large Language Models](https://arxiv.org/pdf/2502.18917)." *AI Verification (SAIV 2025)*, Lecture notes in computer science, 64–96. [https://doi.org/10.1007/978-3-031-99991-8\\\_4](https://doi.org/10.1007/978-3-031-99991-8\_4). [^graus2026]: Graus, David. 2026. *[From Legal Text to Executable Decision Models: Evaluating Structured Representations for Legal Decision Model Generation](https://arxiv.org/pdf/2604.17153)*. . [^etikala2021]: Etikala, Vedavyas. 2021. "[Extracting Decision Model Components from Natural Language Text for Automated Business Decision Modelling](https://ceur-ws.org/Vol-2956/paper51.pdf)." *Proceedings of the 15th International Rule Challenge, 7th Industry Track, and 5th Doctoral Consortium @ RuleML+RR 2021*, CEUR workshop proceedings, vol. 2956. . [^cheng2025]: Cheng, Qian, Ruize Tang, Emilie Ma, et al. 2025. *[SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://arxiv.org/pdf/2509.23130)*. . [^deepmind2024]: 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/)*. . [^song2024]: Song, Peiyang, Kaiyu Yang, and Anima Anandkumar. 2024. *[Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://arxiv.org/pdf/2404.12534)*. . [^yang2023]: Yang, Kaiyu, Aidan M. Swope, Alex Gu, et al. 2023. "[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://arxiv.org/pdf/2306.15626)." *Advances in Neural Information Processing Systems 36*, 21573–612. . [^azerbayev2023]: Azerbayev, Zhangir, Hailey Schoelkopf, Keiran Paster, et al. 2023. *[Llemma: An Open Language Model For Mathematics](https://arxiv.org/pdf/2310.10631)*. . [^xin2024]: Xin, Huajian, Daya Guo, Zhihong Shao, et al. 2024. *[DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://arxiv.org/pdf/2405.14333)*. . [^sanchezstern2020]: Sanchez-Stern, Alex, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. 2020. "[Generating Correctness Proofs with Neural Networks](https://arxiv.org/pdf/1907.07794)." *Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages*, 1–10. . ## Acronyms - BPMN — Business Process Model and Notation - DMN — Decision Model and Notation - FEEL — Friendly Enough Expression Language (the DMN expression language) - IMO — International Mathematical Olympiad - OSS — open-source software