# Towards Verified Code Reasoning by LLMs

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 17 of its 35 references that are in the map.
- First posted on arXiv 30 Sep 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)
- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context](https://mlsanity.com/paper/2403.05530/) (2024)
- [CRUXEval: A Benchmark for Code Reasoning, Understanding and Execution](https://mlsanity.com/paper/2401.03065/) (2024)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [NExT: Teaching Large Language Models to Reason about Code Execution](https://mlsanity.com/paper/2404.14662/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [Code to Think, Think to Code: A Survey on Code-Enhanced Reasoning and Reasoning-Driven Code Intelligence in LLMs](https://mlsanity.com/paper/2502.19411/) (2025)
- [Play Favorites: A Statistical Method to Measure Self-Bias in LLM-as-a-Judge](https://mlsanity.com/paper/2508.06709/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning](https://mlsanity.com/paper/2409.12452/) (2024)
- [EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking](https://mlsanity.com/paper/2502.12466/) (2025)
- [Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection](https://mlsanity.com/paper/2405.02318/) (2024)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)
- [CodeMMLU: A Multi-Task Benchmark for Assessing Code Understanding & Reasoning Capabilities of CodeLLMs](https://mlsanity.com/paper/2410.01999/) (2024)
- [Logic.py: Bridging the Gap between LLMs and Constraint Solvers](https://mlsanity.com/paper/2502.15776/) (2025)
- [CRQBench: A Benchmark of Code Reasoning Questions](https://mlsanity.com/paper/2408.08453/) (2024)
- [Disproving Program Equivalence with LLMs](https://mlsanity.com/paper/2502.18473/) (2025)

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

- [Agentic Code Reasoning](https://mlsanity.com/paper/2603.01896/) (2026)
- [interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification](https://mlsanity.com/paper/2602.11202/) (2026)
- [LLMs + Security = Trouble](https://mlsanity.com/paper/2602.08422/) (2026)
- [Infinite Problem Generator: Verifiably Scaling Physics Reasoning Data with Agentic Workflows](https://mlsanity.com/paper/2603.14486/) (2026)

## Abstract (arXiv)

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.