# Towards Automated Formal Verification of Backend Systems with LLMs

arXiv: https://arxiv.org/abs/2506.10998 · HTML: https://mlsanity.com/paper/2506.10998/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 51 references that are in the map.
- First posted on arXiv 13 Apr 2025.

## Builds on (most cited first, 18 of 18)

- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [ChatUniTest: A Framework for LLM-Based Test Generation](https://mlsanity.com/paper/2305.04764/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification](https://mlsanity.com/paper/2403.16750/) (2024)
- [A System for Automated Unit Test Generation Using Large Language Models and Assessment of Generated Test Suites](https://mlsanity.com/paper/2408.07846/) (2024)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Do be do be do](https://mlsanity.com/paper/1611.09259/) (2016)
- [Koka: Programming with Row Polymorphic Effect Types](https://mlsanity.com/paper/1406.2061/) (2014)
- [Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems](https://mlsanity.com/paper/2310.01961/) (2023)
- [Eff Directly in OCaml](https://mlsanity.com/paper/1812.11664/) (2018)

## Built on by (most cited first, 1 of 1)

- [Monadic Context Engineering](https://mlsanity.com/paper/2512.22431/) (2025)

## Abstract (arXiv)

Software testing plays a critical role in ensuring that systems behave as intended. However, existing automated testing approaches struggle to match the capabilities of human engineers due to key limitations such as test locality, lack of general reliability, and business logic blindness. In this work, we propose a novel framework that leverages functional programming and type systems to translate Scala backend code into formal Lean representations. Our pipeline automatically generates theorems that specify the intended behavior of APIs and database operations, and uses LLM-based provers to verify them. When a theorem is proved, the corresponding logic is guaranteed to be correct and no further testing is needed. If the negation of a theorem is proved instead, it confirms a bug. In cases where neither can be proved, human intervention is required. We evaluate our method on realistic backend systems and find that it can formally verify over 50% of the test requirements, which suggests that half of a testing engineer's workload can be automated. Additionally, with an average cost of only 2.19 per API, LLM-based verification is significantly more cost-effective than manual testing and can be scaled easily through parallel execution. Our results indicate a promising direction for scalable, AI-powered software testing, with the potential to greatly improve engineering productivity as models continue to advance.