Towards Automated Formal Verification of Backend Systems with LLMs

TL;DR

This paper introduces a framework that uses functional programming, type systems, and LLMs to automatically verify backend system correctness, reducing manual testing workload and costs.

Contribution

It presents a novel pipeline translating Scala code into formal Lean representations and leveraging LLM-based provers for automated verification.

Findings

Verifies over 50% of test requirements automatically.

Cost-effective verification at $2.19 per API.

Potential to automate half of testing engineer workload.

Abstract

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.