FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

FM-Agent is a novel framework that enables automated compositional reasoning for large-scale systems using LLMs, addressing the challenges of applying Hoare-style logic in complex codebases. It automatically generates function-level specifications based on caller expectations, thereby alleviating the burden of manual specification writing. In evaluations, FM-Agent successfully analyzed systems with up to 143k lines of code in under two days, uncovering 522 previously undetected bugs, highlighting its potential to enhance the correctness of LLM-generated software.