Can LLM agents explore codebases and reason about code semantics without executing the code? We study this capability, which we call agentic code reasoning, and introduce semi-formal reasoning: a structured prompting methodology that requires agents to construct explicit premises, trace execution paths, and derive formal conclusions. Unlike unstructured chain-of-thought, semi-formal reasoning acts as a certificate: the agent cannot skip cases or make unsupported claims. We evaluate across three tasks (patch equivalence verification, fault localization, and code question answering) and show that semi-formal reasoning consistently improves accuracy on all of them. For patch equivalence, accuracy improves from 78% to 88% on curated examples and reaches 93% on real-world agent-generated patches, approaching the reliability needed for execution-free RL reward signals. For code question answering on RubberDuckBench Mohammad et al. (2026), semi-formal reasoning achieves 87% accuracy. For fault localization on Defects4J Just et al. (2014), semi-formal reasoning improves Top-5 accuracy by 5 percentage points over standard reasoning. These results demonstrate that structured agentic reasoning enables meaningful semantic code analysis without execution, opening practical applications in RL training pipelines, code review, and static program analysis.
Figures & tables
Figure 1: Motivating example from Django (django-13670): Standard reasoning assumes format() is Python’s builtin; semi-formal analysis traces the actual definition and discovers a module-level function with different semantics, causing Patch 1 to raise AttributeError . See Appendix C for a detailed semi-formal proof walkthrough.
Term
Definition
Code Patch
A diff that modifies repository source code to fix a bug or add functionality.
Test Patch
A diff that adds or modifies test files (the F2P tests introduced with a bug fix).
Fail-to-Pass (F2P) Tests
Tests introduced alongside a bug fix that fail before the patch and pass after. These validate that the fix addresses the reported issue.
Pass-to-Pass (P2P) / Regression Tests
Existing tests in the repository that must continue passing after the patch is applied.
Correct Patch
A patch that causes all F2P tests to pass while not breaking any P2P tests.
Table 1: Key terminology for patch equivalence
Figure 2: Condensed semi-formal certificate template for patch equivalence. The agent must fill in every bracketed field with evidence gathered from the codebase. The full template includes additional fields for pass-to-pass tests, confidence levels, and alternative hypothesis checks. Templates for other tasks follow the same structure but with task-specific premises and claims. The full prompt appears in Appendix A .
Reasoning
Overall Accuracy
Avg Steps
Non-Equiv Acc
Equiv Acc
Standard
78.2%
10.08
78.6%
78.0%
Semi-formal
88.8%
28.17
82.9%
93.0%
Table 2: Comparison of reasoning approaches using Opus-4.5 as the verifier model
Model
Mode
Accuracy
Avg Steps
difflib
Best threshold=0.4
73%
-
Sonnet-4.5
Single Call (Standard)
80.0%
1
Sonnet-4.5
+ File Context (Standard)
82.0%
1
Sonnet-4.5
Agentic (Standard)
84.5%
20.67
Sonnet-4.5
Agentic (Semi-formal)
91.5%
43.23
Opus-4.5
Single Call (Standard)
86.0%
1
Table 3: Verification accuracy with test patches available
All
Any
Mode
Exploration
Top-1
Top-3
Top-5
Top-1
Top-3
Top-5
Standard
Single-shot
36.1%
55.6%
55.6%
47.2%
69.4%
69.4%
Semi-formal
Single-shot
41.7%
58.3%
63.9%
55.6%
75.0%
77.8%
Standard
Agentic
46.5%
60.5%
60.5%
65.1%
79.1%
81.4%
Semi-formal
Agentic
53.5%
67.4%
72.1%
72.1%
83.7%
88.4%
Table 4: Fault localization accuracy on Defects4J (Opus-4.5). “All” requires every ground-truth hunk to be covered; “Any” requires at least one.
All
Any
Model
Mode
Top-1
Top-3
Top-5
Top-1
Top-3
Top-5
Sonnet-4.5
Standard
20.0%
30.0%
31.1%
35.6%
51.1%
51.1%
Sonnet-4.5
Semi-formal
16.7%
25.6%
30.0%
30.0%
43.3%
50.0%
Opus-4.5
Standard
30.0%
42.2%
43.3%
53.3%
64.4%
65.6%
Opus-4.5
Semi-formal
34.4%
47.8%
47.8%
58.9%
68.9%
68.9%
Table 5: Agentic fault localization on 100-bug sample. “All” requires every ground-truth hunk to be covered; “Any” requires at least one.
Model
Mode
Accuracy
Avg Steps
Opus-4.5
Single-shot
76.2%
1
Opus-4.5
Agentic (Standard)
78.3%
10.8
Opus-4.5
Agentic (Semi-formal)
87.0%
19.7
Sonnet-4.5
Single-shot
78.7%
1
Sonnet-4.5
Agentic (Standard)
84.2%
17.6
Sonnet-4.5
Agentic (Semi-formal)
84.8%
25.3
Table 6: Code question answering accuracy on RubberDuckBench
Appendix figures & tables1 asset
Supplementary material from the paper’s appendix.
Appendix
Language
Questions
Accuracy
C++
5
88.0%
Python
5
87.5%
Java
5
85.5%
Appendix
Table 7: Code QA accuracy by language (Opus-4.5, Semi-formal)