Large language models (LLMs) can describe what a piece of code should compute, but they do so in free-form text. Such text cannot be checked against program executions, and it does not reveal whether a statement is correct. We present SemLoc, which turns LLM reasoning into executable, verifiable semantic constraints. With structured semantic grounding, the LLM writes each property as a constraint with a fixed category, attached to an anchor in the code graph, such as a variable definition, branch, loop, or return. SemLoc inserts each constraint as a runtime check and runs the tests, which yields a semantic violation spectrum over passing and failing tests. Counterfactual verification then patches the code at an anchor and reruns the tests; a patch that a constraint suggests counts as verified only if all tests then pass. We study SemLoc on fault localization, where the tests serve as the oracle for verification, with four LLMs on QuixBugs and on SemBugs, a new dataset of 809 real bugs from 750 GitHub projects. The constraints are executable: 99.4% become runtime checks, and on programs where coverage ties the faulty line with at least half of the covered lines, their violations alone rank it first in 40.9% of the cases, compared with 2.2% for spectrum-based fault localization and 7.0% for Daikon invariants. They make the LLM's answers verifiable: 68.4% of SemLoc's top-ranked answers carry a patch that the tests confirm, and 93.6% of these are correct, which the LLM's own confidence cannot match. SemLoc's first-rank accuracy does not differ significantly, for any of the four LLMs, from that of an LLM given the same inputs (81.4% vs. 82.0%), and it far exceeds that of an LLM that sees only the function (50.0%).
Figures & tables
Figure 1: Overview of SemLoc .
Figure 3: SemLoc on the softmax function of Listing 2 . Panels 1 to 4 correspond to Sections 3.1 to 3.4 . In panel 3, rows are tests, columns are constraints, and orange cells mark violations.
Category
Property
PRECONDITION
valid inputs
POSTCONDITION
valid outputs
VALUE_RANGE
bounds of a value
RELATION
relation between values
DERIVED_CONSISTENCY
derived values agree
INVARIANT_LOOP
holds in every iteration
Table 1: Constraint schema: categories (left) and anchor regions (right).
Table 4
SemBugs
Coverage collapse
QuixBugs
Method
Acc@1
Acc@3
Acc@5
% Flagged
Acc@1
Acc@3
Acc@5
Acc@1
Acc@3
Acc@5
All models
SemLoc
81.4
91.5
93.4
35.5
86.3
94.8
96.5
74.2
92.4
96.0
SemLoc w/o CF
80.8
91.4
93.4
35.5
86.4
94.8
96.4
73.0
92.4
96.0
SemLoc candidate lines
80.8
91.3
92.7
25.7
86.4
94.8
95.7
73.0
92.4
95.0
SemLoc w/o semantic indexing
82.0
93.1
96.0
35.2
87.2
95.9
97.7
72.2
89.9
98.7
Table 4: Fault localization accuracy (%). Mean over the runs of each model; SemLoc rows shaded; best LLM-based value per block in bold.
Figure 6
LLM-based
SBFL
Bug pattern
Programs
SemLoc
SemLoc w/o semantic indexing
Direct LLM
Ochiai
Tarantula
D*
Op2
Barinel
Jaccard
Delta debugging
Acc@1
Binary operator
140
87.3
87.4
61.5
16.4
10.0
17.9
17.9
10.0
16.4
2.9
Unary operator
96
89.4
86.5
66.5
17.7
8.3
17.7
18.8
8.3
17.7
4.2
Less specific if
88
65.1
63.8
21.9
5.7
3.4
5.7
5.7
3.4
3.4
0.0
More specific if
82
58.1
65.4
24.5
1.2
1.2
1.2
1.2
1.2
1.2
0.0
Table 5: Accuracy by bug pattern on SemBugs (%). Mean over all runs; best value per row in bold.
Constraints (%)
Primary patches
Model
Constraints per program
Instrumented
Executed
Violated by failing tests
Violated by passing tests
Hold on fixed program
Count
On faulty line (%)
GPT-5.5
4.13
99.8
95.4
67.3
31.5
60.6
1127
89.5
gpt-oss-120b
3.15
99.5
93.8
43.8
33.0
59.4
576
86.6
Qwen3.8-27B
3.28
99.0
93.4
49.5
39.8
54.3
510
91.0
Qwen3.8-Flash
3.01
99.2
93.0
49.3
33.9
60.9
618
93.0
All
3.39
99.4
94.0
53.6
34.4
58.9
2831
90.0
Table 6: Constraints and counterfactual verification on SemBugs. Shares are over all constraints.
Figure 7: Outcome of the hypothesis check on SemBugs, by whether the LLM’s top candidate line is the faulty line. Other: Secondary, Regressing, or PatchInvalid; the 27 program runs without a candidate line are left out.
Region
Share
Anchored at faulty line
Violated by failing tests
Violated by passing tests
Primary
Primary, anchored at faulty line
LINE
29.7
80.4
60.7
37.1
20.9
94.1
AFTER_DEF
25.0
28.6
44.9
30.7
2.6
51.7
BEFORE_USE
22.3
43.7
58.7
42.0
3.3
86.9
AFTER_BRANCH
11.8
53.6
46.1
20.9
6.6
97.3
ANY_RETURN
5.5
12.9
54.4
37.8
1.0
33.3
LOOP_TAIL
3.9
29.6
49.3
26.9
3.5
95.6
Table 7: Constraints by anchor region on SemBugs, all models (%). Primary: CF status of the constraint.
SemBugs
QuixBugs
Property source
Properties per program
Acc@1
Acc@3
Acc@5
Acc@1
Acc@3
Acc@5
Daikon invariants
78.0
3.8
8.2
10.0
0.0
12.1
12.1
Debugging Book invariants
4.5
2.2
2.5
2.6
0.0
9.1
9.1
LLM constraints (all models)
3.4
32.2
58.6
65.0
25.5
55.1
72.0
LLM constraints (gpt-oss-120b, T=0.8 )
3.2
38.4
57.5
61.9
39.4
60.6
69.7
+ Daikon invariants
81.1
31.1
50.7
58.1
24.2
54.5
69.7
Table 8: Fault localization accuracy of LLM constraints and dynamic invariants (%). All rows use the same grounding, runtime checks, and scoring, without candidate lines or CF.
SemLoc
SemLoc w/o semantic indexing
Direct LLM
Model
Calls
In
Out
LLM time
Test time
In
Out
LLM time
In
Out
LLM time
GPT-5.5
2.31
47.2
1.6
39.8
3.0
16.0
0.4
14.5
26.7
0.6
17.5
gpt-oss-120b
2.13
7.5
3.1
238.7
2.9
3.7
1.2
87.4
0.7
0.5
30.6
Qwen3.8-27B
2.20
8.1
0.6
11.2
3.0
3.8
0.2
12.3
0.8
0.2
6.7
Qwen3.8-Flash
2.21
8.2
0.8
23.6
2.8
3.8
0.2
15.8
0.8
0.2
14.4
Table 9: Cost per program on SemBugs. Means over runs; tokens in thousands, time in seconds.