Towards Verified Code Reasoning by LLMs

TL;DR

This work tackles the trust gap in LLM-driven code reasoning by introducing a post-hoc verification framework that converts an agent’s natural-language reasoning into a formal representation and then uses program-analysis tools to check the validity of the reasoning. The approach centers on three concepts: CodeSemantics (ground-truth code behavior), AgentClaims (the agent’s formalized explanations), and VerificationCondition (the properties to verify). It applies the framework to two domains—uninitialized variable (MSAN) bugs and program equivalence—showing that formal verification can validate 13/20 MSAN cases and catch 6/8 incorrect equivalence judgments, with iterative predicate synthesis improving coverage. The results demonstrate that verification can reduce hallucinations and increase trust in code reasoning, suggesting a viable path toward more reliable AI-assisted software engineering. The work also outlines a scalable pipeline using Datalog-based predicates (Soufflé) to represent and verify agent reasoning, highlighting practical implications for build-stable, verifiable AI-assisted code analysis.

Abstract

While LLM-based agents are able to tackle a wide variety of code reasoning questions, the answers are not always correct. This prevents the agent from being useful in situations where high precision is desired: (1) helping a software engineer understand a new code base, (2) helping a software engineer during code review sessions, and (3) ensuring that the code generated by an automated code generation system meets certain requirements (e.g. fixes a bug, improves readability, implements a feature). As a result of this lack of trustworthiness, the agent's answers need to be manually verified before they can be trusted. Manually confirming responses from a code reasoning agent requires human effort and can result in slower developer productivity, which weakens the assistance benefits of the agent. In this paper, we describe a method to automatically validate the answers provided by a code reasoning agent by verifying its reasoning steps. At a very high level, the method consists of extracting a formal representation of the agent's response and, subsequently, using formal verification and program analysis tools to verify the agent's reasoning steps. We applied this approach to a benchmark set of 20 uninitialized variable errors detected by sanitizers and 20 program equivalence queries. For the uninitialized variable errors, the formal verification step was able to validate the agent's reasoning on 13/20 examples, and for the program equivalence queries, the formal verification step successfully caught 6/8 incorrect judgments made by the agent.

Figures (32)

• Figure 1: Basic agentic framework with an LLM function calling loop and extraction of the agent's response.
• Figure 2: An array-bounds example where the code reasoning question (asked to the agent) is asked "Is str[i] access safe?"; the correct answer is unsafe.
• Figure 3: LLM explanation for code in Fig. \ref{['Fi:arraybounds1']}. The agent makes false assumptions about code semantics and incorrectly answers the code reasoning question.
• Figure 4: Correct Explanation for code in Fig. \ref{['Fi:arraybounds1']}, the agent considers various scenarios, doesn't make incorrect assumptions, and correctly answers about the code reasoning question.
• Figure 5: Another array-bounds example where the agent is asked the code reasoning question - "Is the access x[index] safe?", and the answer is that the access is potentially unsafe.

Theorems & Definitions (1)

• definition 1