arXiv:2605.06184v1 [cs.SE] 7 May 2026
Teaching LLMs Program Semantics via Symbolic Execution Traces
Jonas Bayer∗ University of Cambridge
Stefan Zetzsche† Amazon Web Services
Olivier Bouissou Amazon Web Services
Remi Delmas Amazon Web Services
Michael Tautschnig Amazon Web Services
Soonho Kong Amazon Web Services
Abstract We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025, and evaluate 14 models across six families. We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length. To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ∼3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4× larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.
1
Introduction
How well do LLMs understand low-level code? For higher-level languages, code understanding evaluations are approaching saturation [37], but C requires reasoning about memory safety, pointer arithmetic, and undefined behavior, where models remain less reliable [29]. Yet there is no established evaluation framework that isolates this kind of semantic reasoning for C. We introduce an evaluation framework built on SV-COMP 2025 [6], the Software Verification Competition. Given a C program and a property (memory safety, absence of overflows, termination, reachability, or absence of data races), models must determine whether the property holds or is violated, with ground truth established by formal verification tools. We evaluate 14 models across six families and find that while most models achieve over 90% accuracy on confirming properties hold, violation detection is far weaker: four of fourteen models correctly identify fewer than 50% of actual violations, and accuracy drops sharply with program length, with one model falling below 10% on programs of just 100–200 lines (Figure 2). Notably, this does not correlate straightforwardly with model size or code specialization; for instance, GPT-OSS-20B detects violations more reliably than Mistral Large 3 675B and Qwen3-Coder-480B, suggesting that training data and objectives play a ∗ Work done during an internship at Amazon Web Services. † Corresponding author: [email protected]
Preprint.
Accuracy (%)
Property Holds 95.1
100
91.9
91.8
91.3
89.6
Overall
89.5
84.2 84.4
Property Violated 76.2
74.0
70.0
69.7
68.1
67.8
50
D 2 evst 12 ra 3B l Co Qw de en r3 3 0B M in 3 istr 8B al
Q w 32 en3 B La M rg ist e 3 ra 67 l 5B Q w 8B en3
C So lau n. de 4 D .5 ee pS R1 ee k G PT 20 -OS B S Co Qw de en r4 3 80 B
K K imi 2 D .5 ee V pSe 3. ek 2 G PT 12 -O 0B SS
O
Cl pu aud s4 e .7
0
Figure 1: Baseline accuracy on our benchmark, sorted by overall performance. Numbers above each bar show overall accuracy (%). All models detect property holds more reliably than violations, with the gap widening dramatically for the Mistral and Qwen families regardless of scale. Figure 2 shows that violation detection degrades sharply already within the 100–200 LOC range.
larger role than scale. A failure analysis (Appendix B.5) reveals that models fail by missing triggering edge cases, making incorrect logical or arithmetic reasoning steps, or identifying the violation but incorrectly concluding it is benign. To improve violation detection, we explore using formal verification artifacts as training data. Prior work combining LLMs with formal methods has largely focused on inference time; the training-time direction is less explored. Existing efforts have targeted theorem proving with Lean proofs [27, 30] and training on concrete Python execution traces [13]. We extend this idea to C, where a mature ecosystem of symbolic execution tools exists, yet their artifacts remain untapped for LLM training. We focus on symbolic execution, which reasons about all possible inputs simultaneously rather than sampling concrete values. Symbolic execution artifacts capture program semantics in a form wellsuited for training: they trace execution paths, track memory states, and reveal the precise conditions under which properties are violated. We use Soteria [4], an open-source symbolic execution engine that is fast, produces detailed traces, and supports both C and Rust. Starting from the GitHub CodeParrot dataset [12], we filter to 1 million self-contained C files and run Soteria on each, yielding approximately 34,000 usable traces. The reduction stems from timeout and parser limitations in Soteria; we expect the yield to improve as the tooling matures. We conduct extensive ablation studies on Qwen3-8B to understand how different aspects of the training data affect performance. Our main finding is that filtering to manifest bug traces (where Soteria proves a violation occurs on all feasible inputs), combined with chain-of-thought reasoning at inference time, yields a 17.9 percentage point improvement on detecting property violations. The reported holds accuracy drops from 90.7% to 78.0%, but this is driven entirely by responses that exhaust the output token budget; on parseable responses, holds accuracy is preserved (90.8% vs. 91.2% baseline) while violated accuracy improves by +26 pp. This gain depends on careful curation: training on all Soteria traces degrades performance, and training on the underlying C files alone also hurts, confirming that improvement derives from the semantic information in Soteria’s traces rather than simply increased code exposure. Importantly, the training data is entirely independent of our benchmark, drawn from arbitrary open-source C code, demonstrating that improvements transfer to unseen verification tasks. Our contributions are: • An evaluation framework of 500 verification tasks across five property types, with ground truth from SV-COMP 2025. A baseline evaluation of 14 models reveals that violation detection varies widely — from 92% for the best model down to below 40% — a deficit often masked by strong performance on holds cases, which inflates overall accuracy. • A scalable, fully automated, annotation-free training pipeline: run Soteria on generic opensource C code, filter to manifest bug traces, and continue pretraining. Just 3,208 traces and ∼10 minutes of training improve Qwen3-8B violation detection by +17.9 pp while also improving overall accuracy. Although the training traces primarily target memory safety 2
LOC
0 1– 40 20
20 0 10 1–
–1 00 51
–5 0 26
0– 25
40 0
100 80 60 40 20 0
20 1–
00
(b) Property violated
10 1– 2
0 51 –1 0
50 26 –
0– 25
Accuracy (%)
(a) Property holds
100 80 60 40 20 0
LOC
Claude Opus 4.7
DeepSeek R1
Kimi K2.5
DeepSeek V3.2
GPT-OSS 120B
Claude Son. 4.5
GPT-OSS 20B
Qwen3-Coder 480B
Qwen3-32B
Mistral Large 3 675B
Devstral 2 123B
Ministral 3 8B
Qwen3-8B
Qwen3-Coder 30B
Figure 2: Baseline accuracy on our benchmark by program length for all models. Holds accuracy (a) remains stable for most models. Violation detection (b) degrades sharply with program length. and overflows, violation detection improves across all five evaluation properties, suggesting the model acquires general verification reasoning. • Extensive ablations (28 configurations) showing that gains are driven by the semantic content of symbolic execution traces, not code volume, and that trace format, curation, and thinking mode interact non-obviously: CPT (continued pretraining) and thinking are individually weak but superadditive in combination (+17.9 pp vs. +7.3 pp and −1.4 pp alone), and preserving the original structured trace format is critical for chain-of-thought to succeed.
2
Related Work
LLMs for Code Understanding. Benchmarks for semantic code understanding remain limited. CRUXEval [18] evaluates input-output prediction for Python but not low-level languages; CoRe [37] tests data and control dependencies across Python, C, and Java but is approaching saturation; LoCoBench [29] evaluates long-context understanding across 10 languages with lower C/C++ performance. In security, recent work observes that models struggle more with detecting vulnerabilities than classifying benign code [15, 22], consistent with the holds–violated asymmetry we document. Concurrent with our work, Sultan et al. [32] evaluate LLMs on SV-COMP 2025 termination tasks, and Wei et al. [35] benchmark invariant synthesis. Training on Program Behavior Artifacts. Training on Lean proofs has improved mathematical reasoning [30, 1, 9, 34, 20]. Verified code generation is active, with training pipelines [11, 5] and benchmarks [39, 33, 7] for Lean, Dafny, and Verus. Sakharova et al. [31] use CrossHair (Python symbolic execution) to improve RL reward signals. Several approaches train on concrete execution traces: ET-CoT [16] fine-tunes on traces to predict outcomes, NExT [28] uses traces for repair, and Chen et al. [10] show execution supervision promotes general reasoning. CWM [13] and others [23, 3] train on Python execution traces. These focus on high-level languages and concrete execution; we train on symbolic execution traces for C, reasoning over all possible inputs. Symbolic Execution and Program Verification. SV-COMP [6] is an annual competition benchmarking verification tools on properties like memory safety, overflow absence, termination, and reachability. For C, prominent tools include CBMC [21], Infer [8], and UAutomizer [19], the winner in many categories of SV-COMP 2025; Kani [2] targets Rust, and Soteria [4], while language-agnostic, currently offers backends for C and Rust. We use SV-COMP for evaluation and Soteria for training data due to its speed and detailed logs. Hybrid Approaches. Tool-augmented approaches combine LLMs with formal methods at inference time. Lemur [36] integrates LLMs with automated reasoners for program verification, using LLMs to generate invariants and annotations. SatLM [38] has LLMs generate declarative specifications solved by automated theorem provers. SkipAnalyzer [26] combines LLMs with Infer for bug detection and false-positive filtering. Mächtle et al. [25] use execution traces to minimize code context for vulnerability prediction. Fedoseev et al. [17] train models to generate Z3 specifications for constraint 3
typedef enum { false , true } bool ; extern unsigned int _ _ V E R I F I E R _ n o n d e t _ u i n t ( void ) ; int main () { unsigned int x ; x = _ _ V E R I F I E R _ n o n d e t _ u i n t () ; if ( x > 0) { while ( x != 0) { x = x - 2; } } return 0; }
Figure 3: Example from our benchmark: does this program always terminate? When x is odd, unsigned wrapping causes an infinite cycle. Mistral Large 3 675B identifies the wrapping but incorrectly concludes the sequence must eventually reach zero (Appendix B.5). solving. Maaz et al. [24] use an LLM agent to synthesize and execute property-based tests across the Python ecosystem. These approaches require formal tools at inference time; we use formal tool artifacts purely for training, requiring no tool invocation at inference.
3
Evaluation Framework
To measure how well LLMs understand low-level code semantics, we need a benchmark that isolates semantic reasoning from other capabilities like code generation. We construct an evaluation framework where models perform binary classification: given a C program and a property, determine whether the property holds or is violated. 3.1
Benchmark Construction
Source Data. We use SV-COMP 2025 [6], which contains approximately 40,000 verification tasks across a repository of roughly 76,000 C files, with ground truth established by formal verification tools.3 An earlier evaluation on CBMC regression tests [14] showed models performed too well to differentiate improvements (Appendix A). Preprocessing. SV-COMP 2025 was designed for evaluating verification tools, not LLMs, so some preprocessing is needed. We restrict to single-file tasks that do not require custom header files (standard library includes like pthread.h and stdlib.h are permitted), reducing the pool to about 15,000 files. This constraint could be relaxed in future work by providing multi-file context to the model. We apply additional filtering to ensure data quality, and strip comments from source code, as formal tools ignore them but LLMs may extract ground truth from them. The full list of preprocessing steps is provided in Appendix B.2. Holdout Curation. The original dataset contains approximately 80% tasks where the property holds and 20% where it is violated, so a model could achieve 80% accuracy by always predicting “property holds.” SV-COMP addresses this with an asymmetric scoring scheme that penalizes incorrect claims more heavily; we instead use simple accuracy on a balanced holdout set of 500 tasks (reporting the macro-average of holds and violated accuracy, which weights each side equally regardless of the natural class distribution): • 100 tasks for each of five core property categories: memory safety, absence of overflows, termination, reachability, and absence of data races • 50/50 split between property holds and property violated for each property • Varying program lengths (0–400 lines), balanced within each length bin 3 SV-COMP 2025 benchmarks are publicly available on GitLab and Zenodo. The competition infrastructure is licensed
under Apache 2.0.
4
Informalize (LLM) CodeParrot (14M C files)
Filter to self-contained (1M files)
Soteria
Trace configurations
optional
SV-COMP 2025 Train Qwen3-8B
Benchmark (500 tasks)
C files only (no traces)
Figure 4: Overview of our data generation and training pipeline. Starting from CodeParrot, we filter to self-contained C files and run Soteria to produce symbolic execution traces. We explore multiple trace configurations (varying format, filtering, and composition; see Appendix C.1), with optional informalization. Each configuration is used to train Qwen3-8B and evaluate on our benchmark.
Prompt Design. For each property, we construct a prompt containing the C code, a property-specific description, and output format instructions, including explanations of SV-COMP primitives such as __VERIFIER_nondet_X(). Full details are in Appendix B.3; Figure 3 shows an example. We use a relaxed answer parser that tolerates common formatting variations, avoiding the need for instruction tuning solely to match a rigid output format. Scope and Limitations. In the standard SV-COMP setting, tools must also produce a machinecheckable witness justifying the claim. We evaluate only the binary verdict; requiring witness generation would be substantially harder [32]. 3.2
Baseline Performance
We evaluate 14 models on our benchmark. Twelve are accessed via Amazon Bedrock; Qwen3-8B and Qwen3-32B are evaluated self-hosted via vLLM. All baseline evaluations use greedy decoding (temperature=0, except Claude Opus 4.7 which does not support temperature parameters) without chain-of-thought reasoning; we explore the effect of enabling thinking in Section 5. All 14 models are evaluated 4 times and we report the mean across runs; standard deviations on overall accuracy are below 1.5 percentage points for all models, confirming high reproducibility across inference runs. Variance over the broader distribution of C programs is addressed by the diversity of SV-COMP tasks, which are drawn from real software projects and designed to challenge state-of-the-art verifiers. Per-property variance can be higher due to the smaller sample size (50 tasks per property per side), so per-property comparisons should be interpreted with caution. Figure 1 visualizes the results; per-property breakdowns are in Appendix B.4. Tasks that exceed the input context window, produce unparseable responses (output budget exhaustion), or time out are all counted as incorrect. The results reveal a consistent pattern: confirming that a property holds is easier than detecting violations. Frontier models handle both well (Claude Opus 4.7: 98.3% holds, 92.0% violated), but four of fourteen models correctly identify fewer than 50% of actual violations despite all achieving over 84% on holds. This does not correlate with model size or code specialization: GPT-OSS-20B (84.1% violated) outperforms Qwen3-Coder-480B (74.8%), and the entire Mistral family achieves 41–51% on violations regardless of scale (8B to 675B). Comparing DeepSeek R1 with V3.2 shows no meaningful improvement from built-in chain-of-thought, suggesting that training data matters more than scale for verification tasks. Per-Property Patterns. The per-property breakdown (Table 2) shows memory safety violations are hardest to detect (even Claude Opus 4.7 at 86%), overflow violations show the widest spread (30–100%), and data race detection varies considerably (37–97%). Manual review confirms these are genuine reasoning failures, not prompt artifacts (Appendix B.5). Effect of Program Length. Figure 2 shows that holds accuracy remains stable across length bins, while violation detection degrades sharply. For Qwen3-32B, violation accuracy drops from 90.0% (0–25 LOC) to 32.1% (101–200 LOC). Even Claude Opus 4.7 dips to 77.7% on programs of 101–200 lines. Since our benchmark contains only single-file programs under 400 lines, this represents a lower bound on real-world difficulty. 5
Failure Analysis and Implications. An LLM-as-judge analysis of all 1069 false negatives (Appendix B.5) reveals five failure modes: missing the triggering edge case (44%), identifying the bug but rationalizing it away (27%), incorrect reasoning (19%), universal/existential confusion (8%, concentrated in termination), and superficial analysis (1%). These diverse patterns suggest no single intervention will address all failure modes.
4
Data Generation and Training
Given that training data and objectives appear to matter more than model size for violation detection, we now describe our pipeline for generating training data from symbolic execution artifacts (Figure 4). 4.1
Primary Training Data
We use Soteria [4], a symbolic execution engine for C and Rust, to generate training data. Unlike concrete execution, which runs a program on specific inputs, symbolic execution reasons over all possible inputs simultaneously, exploring execution paths by treating inputs as symbolic variables and tracking the conditions under which each path is taken. Soteria produces detailed traces that capture memory states, branch conditions, and the reasoning behind property violations, making implicit program semantics explicit. We use only its built-in checks for memory safety, buffer overflows, and undefined behavior, avoiding the need for property synthesis and allowing the pipeline to scale to arbitrary C code without annotation. An example trace is provided in Appendix C.4. As our source corpus, we use the GitHub CodeParrot dataset [12]4 , which contains over 14 million C files. We filter to approximately 1 million self-contained C files (no #include or #import statements) to keep traces simple. Running Soteria yields approximately 34,000 usable traces. The main bottlenecks are parser limitations (Soteria does not yet support all C variants), files without meaningful control flow, and Soteria’s internal path-exploration bounds. Despite this modest volume, our downstream results show meaningful improvement, suggesting room for gains as tooling matures. This training data is independent of our benchmark: we use arbitrary open-source C code, not SV-COMP programs, allowing us to assess whether improvements transfer to unseen verification tasks. While CodeParrot and SV-COMP both draw from open-source repositories, we did not perform explicit deduplication; even in the unlikely event of overlap, Soteria traces would not reveal ground truth for the benchmark properties (termination, reachability, data races) that Soteria does not check. 4.2
Training Configurations
We use Qwen3-8B as our base model for most experiments (with Qwen3-32B as a scale reference), as it is open-weights and tractable for training while still performing reasonably on our baseline evaluation. Our primary training method is continued pretraining (CPT), where traces are concatenated and the model is trained with a standard language modeling objective. We also explore LoRA supervised fine-tuning (SFT) and two-stage CPT+SFT approaches (Appendix C.1). To test whether symbolic execution artifacts can improve code understanding, and if so, which aspects matter most, we systematically vary the training data along several dimensions. Trace Filtering. Not all Soteria traces are equally informative. Traces fall into three categories: manifest bugs, where the symbolic executor proves a violation occurs on all feasible inputs; latent bugs, where an error path is found for some inputs but universality is not proven; and no-violation traces, where Soteria completes analysis without finding any violation. We systematically vary the training data composition: manifest bugs only (3,208 traces), manifest plus latent bugs (754 manifest + 4,294 latent = 5,048 traces), bug and no-violation traces excluding incomplete analyses (16,234 traces), all traces (34,495 traces), and a balanced 50/50 bug/non-bug split (6,416 traces). We also test trace simplification (stripping to error-relevant lines) and training for multiple epochs. Trace Format. Soteria produces interactive HTML reports with collapsible sections, CSS classes for log levels, and HTML-encoded entities (see Appendix C.4). We compare training on this HTML output (with non-semantic metadata such as timestamps removed) versus plain-text traces (HTML 4 CodeParrot is publicly available on Hugging Face. Individual files are subject to their original repository’s license. We
use this data for research only and do not distribute the model.
6
100
70.0
63.8
Overall
Property Violated 76.2
61.8
66.7
68.3
86.5
72.7
62.6
50 32 (th B b in ase k)
3 (n 2B o ba th se in k)
bu (th g H in T M k) L
+
8B (th ba in se k)
+ (n bug o p th la in in k)
+ b (n ug H o th TM in L k)
+ a (n ll H o th TM in L k)
+ (n C o fil th es in k)
0 8 (n B b o th ase in k)
Accuracy (%)
Property Holds
Figure 5: Accuracy on our benchmark by training configuration, split by property holds and violated. Numbers above each bar show overall accuracy (%). All 8B models use Qwen3-8B as the base model; “think” denotes inference with chain-of-thought reasoning enabled. Bug traces with thinking achieve the best 8B violation detection (67.3%), outperforming the 32B base model on violations (56.9%).
tags and metadata removed, entities decoded) and informalized traces, where we prompt an LLM to summarize the symbolic execution in natural language (see Appendix C.5). We also evaluate the effect of enabling Qwen3’s internal chain-of-thought reasoning (“thinking”) at inference time, which appears to benefit strongly from the trace format. Trace vs. Code. To isolate the contribution of symbolic execution artifacts from the effect of simply training on more C code, we compare training on Soteria traces versus training on the same 3,208 underlying C files alone (without traces), controlling for the number of programs seen. Training details including hyperparameters and compute resources are provided in Appendix C.
5
Results
The results of training Qwen3-8B in the configurations described above are shown in Figure 5 (key patterns) and Table 1 (per-property breakdowns). The clearest finding is that continued pretraining on Soteria’s manifest bug traces in HTML format, combined with thinking at inference time, yields the strongest improvement in violation detection (+17.9 pp vs. the no-thinking baseline, p<0.01 paired t-test across 4 runs; per-task McNemar’s test confirms significance across the task distribution: p<10−7 ) and a net gain in overall accuracy (+2.7 pp, p<0.05), while other configurations either underperform or introduce trade-offs. Bug Traces and Trace Curation. CPT on 3,208 HTML-formatted manifest bug traces increases violation detection from 49.4% to 56.7% (+7.3 pp) without thinking. With thinking, CPT improves violation detection from 48.0% to 67.3% (+19.3 pp). The synergy is superadditive: thinking alone provides no benefit (−1.4 pp), but combined with CPT adds +10.6 pp beyond CPT alone. Training on all 34,495 HTML traces (including latent bugs and no-violation traces) hurts violation detection (39.9%), as does training on C source files alone (40.2%), both below the 49.4% baseline. This confirms that semantic signal in Soteria’s bug traces, not code volume, drives the improvement. Dataset Size. The best CPT dataset consists of just 3,208 traces (∼4.6M tokens), trained for a single epoch (∼10 minutes on 8 GPUs). Larger datasets consistently performed worse: 5,048 traces yielded 50.2% violated, 16,234 traces yielded 47.5%, and 34,495 traces yielded 39.9%, all below the 56.7% achieved by 3,208 traces. The expanded and filtered datasets also differ in bug composition (the 5,048-trace set subsamples manifest bugs to 754), so the size effect is partially confounded with curation; the consistent pattern nonetheless suggests signal concentration matters more than quantity. Trace Format. Preserving Soteria’s HTML markup yields better results than plain text. On 3,208 bug traces without thinking, HTML achieves 56.7% violated versus 53.7% for plain text (−3.0 pp). However, per-property differences are large: plain text outperforms HTML on overflow (68.0% vs. 51.0%) and data race (73.0% vs. 65.5%), while being far worse on memory safety (22.0% vs. 39.0%), suggesting the relationship between format and performance may be property-dependent. 7
Table 1: Per-property accuracy (%) for selected configurations. Full results in Appendix C.2. Configuration 8B base (no thinking) + C files only + All traces (HTML) + Bug traces (HTML) + Bug traces (plain text) 8B base (thinking) + Bug traces (HTML) 32B base (no thinking) 32B base (thinking)
Total 90.7±0.6 87.4±0.4 83.8±1.8 80.0±0.7 71.6±2.9 85.4±1.7 78.0±2.1 95.4±0.6 95.2±0.3
Configuration 8B base (no thinking) + C files only + All traces (HTML) + Bug traces (HTML) + Bug traces (plain text) 8B base (thinking) + Bug traces (HTML) 32B base (no thinking) 32B base (thinking)
Total 49.4±2.1 40.2±2.7 39.9±2.3 56.7±1.0 53.7±0.3 48.0±2.0 67.3±1.6 56.9±1.5 77.8±0.7
Property Holds Mem. Safety Overflow 96.0±1.4 89.0±2.2 94.0±2.4 91.0±3.3 83.0±4.1 88.5±1.7 93.0±1.7 79.0±1.0 81.5±1.7 60.0±5.1 95.5±1.7 79.0±3.3 79.5±3.0 71.0±4.1 97.5±0.9 94.0±3.7 98.0 93.0±1.7 Property Violated Mem. Safety Overflow 19.0±3.6 37.5±1.7 22.5±3.8 33.0±3.3 20.5±4.8 25.5±4.1 39.0±4.1 51.0±3.0 22.0±1.4 68.0±3.7 24.5±2.2 44.5±4.6 47.0±1.7 66.0±2.4 39.0±4.4 52.5±3.6 69.0±3.0 72.5±1.7
Termin. 96.0±1.4 96.5±0.9 94.5±2.6 93.5±1.7 88.0±3.5 94.5±1.7 83.0±2.2 94.5±0.9 92.5±2.2
Reach. 89.5±4.6 83.5±3.3 83.0±1.0 77.0±2.2 76.0±6.8 81.5±1.7 80.5±3.6 94.0±2.4 93.5±0.9
Data Race 83.0±5.0 72.0±2.4 70.0±7.5 57.5±4.3 52.5±5.9 76.5±3.8 76.0±5.1 97.0±1.0 99.0±1.0
Termin. 78.5±1.7 59.0±7.3 65.5±3.0 79.5±1.7 66.0±4.0 82.5±3.3 94.5±1.7 88.5±1.7 95.5±1.7
Reach. 54.5±5.2 43.0±2.2 32.0±3.7 48.5±3.0 39.5±4.6 43.5±3.0 60.0±1.4 55.0±4.1 77.5±0.9
Data Race 57.5±1.7 43.5±1.7 56.0±4.9 65.5±3.0 73.0±3.0 45.0±4.1 69.0±8.5 49.5±2.2 74.5±1.7
With thinking, the gap widens dramatically: HTML reaches 67.3% while plain text collapses to 33.2% with a 45% unparsed rate. Informalized traces (LLM-generated natural-language summaries) collapsed to 25.2% overall with 62% unparsed (Appendix C.1), confirming that structured tool output matters, not just semantic content. Per-Property Patterns. Table 1 shows that the best configuration (HTML bug traces + thinking) improves violation detection across all five properties compared to the base model without thinking. Overflow sees the largest gain (+28.5 pp to 66.0%, p<0.001), followed by memory safety (+28.0 pp to 47.0%, p<0.01), termination (+16.0 pp to 94.5%, p<0.01), data races (+11.5 pp to 69.0%), and reachability (+5.5 pp to 60.0%). The data race and reachability improvements do not reach significance at p<0.05 with 4 runs and 50 tasks per cell, though both show consistent positive trends. Memory safety remains the hardest property (47.0%). Scale Comparison. The best 8B configuration (72.7% overall) approaches the Qwen3-32B base model without thinking (76.2%) while substantially outperforming it on violation detection (67.3% vs. 56.9%). The 32B model with thinking reaches 86.5% overall, indicating significant headroom from scaling that CPT at 8B does not close. CPT on the 32B model is a promising direction given the strong CPT–thinking synergy at 8B scale. Figure 8 in the appendix shows that the CPT improvement over the base model holds across all program length bins, though the length-decay pattern persists. Thinking and Output Budget. Thinking mode increases unevaluated response rates (9–45%): the model’s chain-of-thought reasoning frequently exhausts the output token budget before producing a final answer, yielding responses that cannot be parsed into a verdict. The best configuration leaves 13.4% of tasks unevaluated (vs. 1.6% for the base model), so the fixed-denominator numbers (counting unevaluated responses as incorrect) throughout this paper are conservative. Crucially, the unevaluated rate is nearly symmetric across ground truth classes (14.1% on holds vs. 12.7% on violated), ruling out the hypothesis that the model selectively times out on safe programs while searching for nonexistent bugs. On parseable responses only, the best configuration achieves 90.8% holds and 77.1% violated (83.9% overall), compared to 91.2% holds and 50.8% violated (71.2% overall) for the base model — a +26 pp violated improvement with no degradation on holds. Re-evaluating with 3× the output tokens (24,576 vs. 8,192) improved overall accuracy by +1.8 pp, but 10–14% of tasks still time out, suggesting the bottleneck shifts to compute time. Additional Findings. We explored 28 configurations in total (Appendix C.2). LoRA SFT exhibited a sharp capability–stability tradeoff, stripping traces to error-relevant lines degraded performance, and adding an SFT stage after CPT hurt violation detection. As a prompting baseline, we evaluated the base model with two Soteria trace examples (one showing a bug, one showing safe execution) included in the prompt. This few-shot approach hurt violation detection (−8.3 pp to 41.1%) compared to the zero-shot base model, degrading all five properties. The model cannot acquire verification reasoning from in-context examples; CPT is necessary to internalize these patterns. 8
6
Discussion
6.1
Interpreting the Results
The superadditive synergy between CPT and thinking (Section 5) suggests that CPT instills latent verification knowledge the model cannot express without extended reasoning. CPT operates through two channels: it improves reasoning accuracy on the responses the model produces, and it makes chain-of-thought more structured, reducing the fraction of tasks where the model exhausts its output budget. CPT teaches what to reason about, while thinking provides the budget to apply that reasoning. The advantage of HTML traces over plain text likely originates from the explicit hierarchical information (nested tags, log-level annotations) providing anchoring points for multi-step reasoning. The holds–violated gap narrows after training. Memory safety remains the hardest property; Appendix C.6 shows a qualitative example illustrating the pointer reasoning that training enables. 6.2
Generality and Scalability
Our approach requires no labeled data, no task-specific prompts during training, and no manual modification to the tool’s output format, so it can be applied to any formal analysis tool producing structured textual output (bounded model checkers, abstract interpreters, fuzz testing harnesses). Training cost is minimal (∼10 minutes on 8 GPUs for 3,208 traces). Notably, Soteria-only training improved violation detection across all five benchmark properties, including data races and reachability, which Soteria does not specifically analyze. Soteria’s built-in checks cover memory safety, buffer overflows, and undefined behavior, so the training traces overlap with the benchmark’s memory safety and overflow categories. However, comparing CPT against the base model both with thinking enabled, gains extend to termination (+12.0 pp), data races (+24.0 pp), and reachability (+16.5 pp), suggesting the model learns general verification reasoning patterns. 6.3
Limitations
Our experiments use a single base model (Qwen3-8B, with Qwen3-32B as a scale reference), a single symbolic execution engine (Soteria), and a single language (C). We evaluate only binary verdicts on single-file programs; evaluating machine-checkable witnesses or proofs would require substantial additional work. We have not assessed transfer to downstream tasks. Per-property comparisons have limited statistical power with 50 tasks per cell and 4 runs. We have not tested for benchmark contamination, though the ground truth verdicts (whether each property holds or is violated) are established by competition verification tools and are unlikely to appear in pretraining corpora alongside the programs. Each limitation represents a concrete avenue for future work. 6.4
Broader Impact
Improving LLMs’ ability to detect property violations could benefit software reliability by catching bugs earlier, but could also lower the barrier to automated vulnerability discovery if scaled to real-world codebases. We do not release trained model weights.
7
Conclusion
We presented an approach for improving LLM understanding of low-level code by training on symbolic execution artifacts, alongside a benchmark of 500 C verification tasks from SV-COMP 2025. Our baseline evaluation of 14 models revealed that violation detection is consistently harder than confirming properties hold, independent of model size. By training Qwen3-8B on just 3,208 Soteria bug traces with chain-of-thought reasoning at inference time, we achieved a 17.9 pp improvement on violation detection. On parseable responses, accuracy on the property holds case is preserved (90.8%) and violation detection improves by +26 pp, confirming genuine reasoning improvement. Ablations confirm that trace semantics, not code volume, drive the improvement. The pipeline requires no annotation and scales with open-source code availability. Future work includes extending to multi-file programs, incorporating additional formal tools and languages, and using symbolic execution in a reinforcement learning loop. 9
Acknowledgments and Disclosure of Funding This work was funded by Amazon Web Services. We thank Sacha-Élie Ayoun, Azalea Raad, and Opale Sjöstedt for their help with Soteria.
References [1] Achim, T., Best, A., Bietti, A., Der, K., Fédérico, M., Gukov, S., Halpern-Leistner, D., Henningsgard, K., Kudryashov, Y., Meiburg, A., et al. Aristotle: Imo-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025. [2] Amazon Web Services. Kani rust verifier. https://github.com/model-checking/kani. Accessed February 2026. [3] Armengol-Estapé, J., Carbonneaux, Q., Zhang, T., Markosyan, A. H., Seeker, V., Cummins, C., Kambadur, M., O’Boyle, M. F., Wang, S., Synnaeve, G., et al. What i cannot execute, i do not understand: Training and evaluating llms on program execution traces. arXiv preprint arXiv:2503.05703, 2025. [4] Ayoun, S.-É., Sjöstedt, O., and Raad, A. Soteria: Efficient symbolic execution as a functional library. arXiv preprint arXiv:2511.08729, 2025. [5] Baksys, M., Zetzsche, S., Bouissou, O., Delmas, R., Kong, S., and Holden, S. B. Atlas: Automated toolkit for large-scale verified code synthesis. arXiv preprint arXiv:2512.10173, 2025. [6] Beyer, D. and Strejček, J. Improvements in software verification and witness validation: SVCOMP 2025. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 151–186. Springer, 2025. [7] Bursuc, S., Ehrenborg, T., Lin, S., Astefanoaei, L., Chiosa, I. E., Kukovec, J., Singh, A., Butterley, O., Bizid, A., Dougherty, Q., et al. A benchmark for vericoding: formally verified program synthesis. arXiv preprint arXiv:2509.22908, 2025. [8] Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Papakonstantinou, I., Purbrick, J., and Rodriguez, D. Moving fast with software verification. In NASA Formal Methods Symposium, pp. 3–11. Springer, 2015. [9] Chen, L., Gu, J., Huang, L., Huang, W., Jiang, Z., Jie, A., Jin, X., Jin, X., Li, C., Ma, K., et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025. [10] Chen, N., Li, Z., Bao, K., Lin, J., and Liu, D. Chain of execution supervision promotes general reasoning in large language models. arXiv preprint arXiv:2510.23629, 2025. [11] Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., et al. Automated proof generation for rust code via self-evolution. arXiv preprint arXiv:2410.15756, 2024. [12] CodeParrot. Github code dataset. https://huggingface.co/datasets/codeparrot/ github-code. Accessed: February 2026. [13] Copet, J., Carbonneaux, Q., Cohen, G., Gehring, J., Kahn, J., Kossen, J., Kreuk, F., McMilin, E., Meyer, M., Wei, Y., et al. CWM: An open-weights LLM for research on code generation with world models. arXiv preprint arXiv:2510.02387, 2025. [14] Diffblue. CBMC regression tests. https://github.com/diffblue/cbmc/tree/develop/ regression/cbmc. Accessed: February 2026. [15] Dubniczky, R. A., Horvát, K. Z., Bisztray, T., Ferrag, M. A., Cordeiro, L. C., and Tihanyi, N. CASTLE: Benchmarking dataset for static code analyzers and LLMs towards CWE detection, 2025. URL https://arxiv.org/abs/2503.09433. 10
[16] Eguchi, K. and Akiba, T. Making LLMs program interpreters via execution trace chain of thought. In ICML 2025 Workshop on Programmatic Representations for Agent Learning. [17] Fedoseev, T., Dimitrov, D. I., Gehr, T., and Vechev, M. Constraint-based synthetic data generation for llm mathematical reasoning. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. [18] Gu, A., Rozière, B., Leather, H., Solar-Lezama, A., Synnaeve, G., and Wang, S. I. CruxEval: A benchmark for code reasoning, understanding and execution. arXiv preprint arXiv:2401.03065, 2024. [19] Heizmann, M., Chen, Y.-F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., et al. Ultimate automizer and the search for perfect interpolants: (competition contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 447–451. Springer, 2018. [20] Hubert, T., Mehta, R., Sartran, L., Horváth, M. Z., Žužić, G., Wieser, E., Huang, A., Schrittwieser, J., Schroecker, Y., Masoom, H., et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, pp. 1–3, 2025. [21] Kroening, D. and Tautschnig, M. CBMC–C bounded model checker: (competition contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 389–391. Springer, 2014. [22] Li, Y., Li, X., Wu, H., Xu, M., Zhang, Y., Cheng, X., Xu, F., and Zhong, S. Everything you wanted to know about LLM-based vulnerability detection but were afraid to ask. arXiv preprint arXiv:2504.13474, 2025. [23] Liu, C., Lu, S., Chen, W., Jiang, D., Svyatkovskiy, A., Fu, S., Sundaresan, N., and Duan, N. Code execution with pre-trained language models. arXiv preprint arXiv:2305.05383, 2023. [24] Maaz, M., DeVoe, L., Hatfield-Dodds, Z., and Carlini, N. Agentic property-based testing: Finding bugs across the python ecosystem. arXiv preprint arXiv:2510.09907, 2025. [25] Mächtle, F., Loose, N., Schulz, T., Sieck, F., Serr, J.-N., Möller, R., and Eisenbarth, T. Trace gadgets: Minimizing code context for machine learning-based vulnerability prediction. arXiv preprint arXiv:2504.13676, 2025. [26] Mohajer, M. M., Aleithan, R., Harzevili, N. S., Wei, M., Belle, A. B., Pham, H. V., and Wang, S. SkipAnalyzer: A tool for static code analysis with large language models. arXiv preprint arXiv:2310.18532, 2023. [27] Moura, L. d. and Ullrich, S. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pp. 625–635. Springer, 2021. [28] Ni, A., Allamanis, M., Cohan, A., Deng, Y., Shi, K., Sutton, C., and Yin, P. NExT: Teaching large language models to reason about code execution. arXiv preprint arXiv:2404.14662, 2024. [29] Qiu, J., Liu, Z., Liu, Z., Murthy, R., Zhang, J., Chen, H., Wang, S., Zhu, M., Yang, L., Tan, J., et al. LocoBench: A benchmark for long-context large language models in complex software engineering. arXiv preprint arXiv:2509.09614, 2025. [30] Ren, Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., et al. DeepSeek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025. [31] Sakharova, M., Anand, A., and Mezini, M. Integrating symbolic execution into the fine-tuning of code-generating llms. arXiv preprint arXiv:2504.15210, 2025. [32] Sultan, O., Armengol-Estape, J., Kesseli, P., Vanegue, J., Shahaf, D., Adi, Y., and O’Hearn, P. LLMs versus the halting problem: Revisiting program termination prediction. arXiv preprint arXiv:2601.18987, 2026. 11
[33] Thakur, A., Lee, J., Tsoukalas, G., Sistla, M., Zhao, M., Zetzsche, S., Durrett, G., Yue, Y., and Chaudhuri, S. Clever: A curated benchmark for formally verified code generation. arXiv preprint arXiv:2505.13938, 2025. [34] Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. [35] Wei, A., Suresh, T., Sun, T., Wu, H., Wang, K., and Aiken, A. InvBench: Can LLMs accelerate program verification with invariant synthesis? arXiv preprint arXiv:2509.21629, 2025. [36] Wu, H., Barrett, C., and Narodytska, N. Lemur: Integrating large language models in automated program verification. In International Conference on Learning Representations, 2024. [37] Xie, D., Zheng, M., Liu, X., Wang, J., Wang, C., Tan, L., and Zhang, X. CoRe: Benchmarking LLMs code reasoning capabilities through static analysis tasks. arXiv preprint arXiv:2507.05269, 2025. [38] Ye, X., Chen, Q., Dillig, I., and Durrett, G. SatLM: Satisfiability-aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36:45548–45580, 2023. [39] Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., and Song, D. Verina: Benchmarking verifiable code generation. arXiv preprint arXiv:2505.23135, 2025.
A
CBMC Regression Tests
We initially evaluated models on the CBMC regression tests [14], a collection of approximately 1,000 self-contained C files where ground truth is established by the CBMC verifier. We constructed prompts to have LLMs act as static analyzers, producing binary judgments (property holds or violated). All models were evaluated via a commercial inference API. Manual inspection of model responses revealed several systematic issues with the evaluation. Some test cases involved uninitialized variables, strict aliasing violations, or behavior dependent on system specifics, compiler version, or C standard interpretation, making ground truth ambiguous. In other cases, CBMC command-line options contained information crucial to the verdict that was not provided to the model. We filtered out these problematic cases, reducing the evaluation set to 179 tasks with unambiguous ground truth. Among the remaining model errors, we observed failures in basic arithmetic, missing knowledge about C standard library semantics or memory layout, off-by-one errors in array index reasoning, and misinterpretation of compiler warnings as runtime errors. As shown in Figure 6, all models achieve 79–89% accuracy on the filtered set, with accuracy too clustered to meaningfully differentiate improvements. This motivated the construction of our benchmark. A.1
Prompt Template
The following prompt template was used for evaluation on CBMC regression tests: You are an expert in programming with C and are asked to analyse the code below. Your task is to verify that this code would run correctly without producing the following types of runtime errors: • Buffer overflows • Array bounds violations • Pointer safety • Memory leaks • Division by zero • Assertion violations 12
Please go through the code carefully step-by-step and consider which conditions hold throughout its execution. You should keep track of variables and pointers and at every step of the execution think about whether a runtime error will occur. {c_code} Please end your answer with the precise string “Final answer: ERROR” if you identified runtime errors or “Final answer: OKAY” if there are no errors. A.2
Results Claude Sonnet 4.5
89.4
DeepSeek-R1
88.3 79.3
Claude Sonnet 3.5 Qwen3-Coder-30B-A3B
82.1
Qwen3-32B
82.1
0
10
20
30
40 50 60 Accuracy (%)
70
80
90
100
Figure 6: Model performance on CBMC regression tests (% correct out of 179 tasks). High accuracy across models indicates the benchmark is too easy to differentiate improvements.
B
Benchmark and Baseline Evaluation
B.1
Statistics
Number of programs
Figure 7 shows the distribution of program lengths in our benchmark. 200
186 157
150 100 50
49
50
46
101–200
201–400
0 0–25
26–50
51–100
Lines of code Figure 7: Distribution of program lengths in our benchmark (488 unique programs across 500 tasks, median 56 LOC, range 8–398). B.2
Preprocessing
The original SV-COMP 2025 benchmark was not designed for LLM evaluation. We apply preprocessing steps including the following (see Section 3.1 for additional curation such as balancing the dataset): • Exclude files with incorrect specifications (from InvalidTasks-Def file) • Exclude additional invalid files identified by SV-COMP validation scripts • Exclude tasks referencing multiple C files • Exclude tasks with malformed YAML metadata 13
• Exclude files with #include of custom headers • Remove comments from C code • Adjust prompts for correct treatment of uninitialized memory • Adjust prompts to include (__VERIFIER_atomic_begin/end)
SV-COMP
specification
details
• Ensure model returns "ERROR" only for violations of the specified property B.3
Evaluation Prompt
For evaluation on our benchmark, we use a prompt with property-specific descriptions and instructions. B.3.1
Prompt Template You are an expert in programming with C and are asked to analyse the code below. Your task is to verify that this code would run correctly {property_description} Please go through the code carefully step-by-step and consider which conditions hold throughout its execution. You should keep track of variables and pointers and at every step of the execution think about whether an error will occur. Note that this program uses the {data_model} data model. Note: • The code may contain functions like __VERIFIER_nondet_X(). You should assume that this returns an arbitrary value of the indicated type (no side effects). You can assume that these functions are implemented according to the following template: X __VERIFIER_nondet_X() {{ X val; return val; }} • __VERIFIER_atomic_begin() and __VERIFIER_atomic_end(): In a multi-threaded run-time environment, if a list of statements is placed between two function calls you can assume that they are executed atomically. That is, you can assume that the execution between those calls is not interrupted. • malloc(), free(): Assume that the functions malloc and alloca always return a valid pointer, i.e., the memory allocation never fails, and function free always deallocates the memory and makes the pointer invalid for further dereferences. {c_code} {property_instruction}
The {data_model} placeholder is populated with the task’s data model from SV-COMP metadata (ILP32 for 397 tasks, LP64 for 91 tasks), which determines integer and pointer sizes. B.3.2
Property Descriptions
No Overflow: without producing an overflow error. For the context of this task, overflow error means the following: It can never happen that the resulting type of an operation is a signed-integer type but the resulting value is not in the range of values that are representable by that type. A violation of this property matches what C11 defines as undefined behavior. (Hence, conversions to signed-integer types do not violate this property.) Memory Safety: without memory safety violations. This means that the following three conditions have to hold: 1. Valid Deallocating: All memory deallocations are valid (counterexample: invalid free). More precisely: There exists no execution of the program on which an invalid memory deallocation occurs. 2. Valid Dereferencing: 14
All pointer dereferences are valid (counterexample: invalid dereference). More precisely: There exists no execution of the program on which an invalid pointer dereference occurs. 3. Valid Memory Tracking: All allocated memory blocks are tracked. The set of tracked blocks is defined as the smallest set of blocks satisfying the following two rules: A block is tracked whenever there is a pointer to this block (not necessarily pointing to the beginning of the block) or to the first address after this block (see 6.5.6 of C11 standard) stored in a program variable. The variable can be of a pointer type or of a compound type containing a pointer. The variable does not have to be in the current scope, it can be global or on the call stack. If some pointer in a tracked block points to another block (again, not necessarily to the beginning of the block) or to the first address after this block, this pointed block is also tracked. In particular, a leaked memory block is not tracked. Hence, a program with a memory leak does not satisfy this property. Note that reading uninitialised memory is considered okay in the context of this task. You are meant to check issues with (de)allocation, but not initialisation. Termination: and will always terminate. In the context of this task, termination means that every execution path finally reaches the end of the program. Unreachable Call: without calling the error function. This means that the function reach_error is not called in any finite execution of the program. No Data Race: without any data races occurring. For the context of this task, data race means the following: If there exist two or more concurrent accesses to the same memory location and at least one is a write access, then all accesses must be atomic. B.3.3
Property Instructions
No Overflow: Please end your answer with the precise string “Final answer: OKAY” if the code does not run into overflow errors. Otherwise, you should end your answer with “Final answer: ERROR”. Even if there are problems with the code, as long as no overflow error occurs you should respond with “Final Answer: OKAY”. Memory Safety: Please end your answer with the precise string “Final answer: OKAY” if the code is memory safe. Otherwise, you should end your answer with “Final answer: ERROR”. Even if there are problems with the code, as long as none of the mentioned memory safety issues occurs you should respond with “Final Answer: OKAY”. Remember that the focus is on (de)allocation and that accessing uninitialised memory is not considered a problem in the context of this task. Termination: Please end your answer with the precise string “Final answer: OKAY” if the program terminates. Otherwise, you should end your answer with “Final answer: ERROR”. Even if there are problems with the code, as long as it terminates you should respond with “Final Answer: OKAY”. Unreachable Call: Please end your answer with the precise string “Final answer: OKAY” if the error function reach_error is not called. Otherwise, you should end your answer with “Final answer: ERROR”. Even if there are problems with the code, as long as the error function is not called you should respond with “Final Answer: OKAY”. 15
No Data Race: Please end your answer with the precise string “Final answer: OKAY” if there are no data races. Otherwise, you should end your answer with “Final answer: ERROR”. Even if there are problems with the code, as long as there is no data race you should respond with “Final Answer: OKAY”. B.4
Detailed Baseline Results
Aggregate accuracy is shown in Figure 1 in the main text. Table 2: Baseline per-property accuracy (%) on our benchmark across all program lengths. Top: property holds; bottom: property violated. Model Claude Opus 4.7 Mistral Large 3 675B Kimi K2.5 Qwen3-Coder-30B Devstral 2 123B DeepSeek R1 DeepSeek V3.2 Qwen3-32B Claude Sonnet 4.5 Ministral 3 8B Qwen3-Coder-480B GPT-OSS 120B Qwen3-8B GPT-OSS 20B
Total 98.3±0.2 97.8±0.4 97.7±0.8 97.5±1.1 97.2±0.3 93.7±0.7 95.8±0.4 95.4±0.6 94.9±1.0 93.8±0.8 93.7±1.1 91.9±0.9 90.7±0.6 84.8±1.0
Property Holds (1–400 LOC) Mem. Safety Overflow 100.0 93.5±0.9 98.0±1.4 96.0 98.5±1.7 93.0±1.0 97.0±1.7 96.0±1.4 98.5±0.9 94.0±1.4 93.5±1.7 88.0±2.4 96.5±0.9 91.5±1.7 97.5±0.9 94.0±3.7 94.5±1.7 90.5±3.0 96.5±1.7 91.0±3.0 92.0±1.4 88.0±4.5 99.0±1.7 92.0±2.4 96.0±1.4 89.0±2.2 93.0±3.0 73.5±2.6
Termin. 98.5±0.9 100.0 99.0±1.0 99.0±1.0 99.0±1.0 97.5±1.7 97.5±1.7 94.5±0.9 98.0±1.4 99.0±1.0 97.5±0.9 76.5±1.7 96.0±1.4 81.0±5.4
Reach. 100.0 98.5±0.9 100.0 98.5±0.9 99.5±0.9 94.0±2.4 96.5±0.9 94.0±2.4 99.5±0.9 91.0±2.2 97.0±1.0 93.0±1.0 89.5±4.6 82.5±4.6
Data Race 99.5±0.9 96.5±2.6 98.0±1.4 97.0±2.2 95.0±1.0 95.5±3.0 97.0±1.0 97.0±1.0 92.0±1.4 91.5±2.2 94.0±2.0 99.0±1.0 83.0±5.0 94.0±1.4
Model Claude Opus 4.7 GPT-OSS 120B DeepSeek V3.2 DeepSeek R1 Kimi K2.5 Claude Sonnet 4.5 GPT-OSS 20B Qwen3-Coder-480B Qwen3-32B Mistral Large 3 675B Qwen3-8B Devstral 2 123B Ministral 3 8B Qwen3-Coder-30B
Total 92.0±0.6 90.8±0.6 87.8±1.9 85.2±1.3 86.1±1.1 84.2±0.7 84.1±1.3 74.8±1.5 56.9±1.5 50.2±1.3 49.4±2.1 42.1±2.1 41.7±0.9 38.7±2.3
Property Violated (1–400 LOC) Mem. Safety Overflow Termin. 85.5±1.7 100.0 89.0±3.6 88.5±1.7 92.0±1.4 100.0 83.5±5.7 87.5±0.9 91.5±3.6 81.5±5.9 78.0±3.7 94.0±1.4 85.0±3.6 84.5±1.7 94.0±1.4 86.5±0.9 85.5±2.2 85.0±2.2 81.5±3.0 81.5±1.7 97.5±2.2 73.0±2.2 81.5±2.2 81.5±3.0 39.0±4.4 52.5±3.6 88.5±1.7 47.0±4.6 50.0±2.8 47.5±4.8 19.0±3.6 37.5±1.7 78.5±1.7 33.5±1.7 40.5±9.5 51.5±1.7 32.5±3.0 39.0±1.0 58.5±1.7 27.5±3.0 30.0±2.4 53.0±3.0
Reach. 89.0±1.0 84.0±1.4 84.5±3.0 82.0±2.4 73.5±1.7 67.5±2.6 79.0±1.0 64.0±2.4 55.0±4.1 52.0±4.2 54.5±5.2 44.5±3.8 32.5±3.8 46.0±5.8
Data Race 96.5±1.7 89.5±3.3 92.0±2.4 90.5±2.2 93.5±3.0 96.5±1.7 81.0±4.1 74.0±3.5 49.5±2.2 54.5±3.6 57.5±1.7 40.5±4.6 46.0±4.2 37.0±6.1
Table 3: Baseline per-property accuracy (%) on our benchmark restricted to programs of 101–400 lines. Compared to Table 2, violation detection collapses for most models while holds accuracy remains high. Model Devstral 2 123B Mistral Large 3 675B Claude Opus 4.7 DeepSeek V3.2 Kimi K2.5 Qwen3-Coder-30B Ministral 3 8B Qwen3-32B DeepSeek R1 Claude Sonnet 4.5 Qwen3-Coder-480B Qwen3-8B GPT-OSS 120B GPT-OSS 20B
Total 99.0±1.0 98.5±0.9 98.0 97.4±0.9 96.9±1.0 96.4±3.0 96.4±0.9 97.4±1.7 94.4±1.7 92.3±1.7 90.8±3.4 89.3±2.7 88.8±1.0 73.5±3.2
Property Holds (101–400 LOC) Mem. Safety Overflow Termin. 100.0 95.0±5.0 100.0 100.0 92.5±4.3 100.0 100.0 90.0 100.0 100.0 90.0 97.2±4.8 100.0 90.0 94.4±5.6 100.0 97.5±4.3 100.0 90.0±7.1 100.0 100.0 100.0 95.0±5.0 94.4±5.6 97.5±4.3 87.5±4.3 97.2±4.8 97.5±4.3 90.0 91.7±4.8 77.5±4.3 90.0 97.2±4.8 97.5±4.3 90.0±7.1 100.0 100.0 85.0±5.0 58.3±4.8 85.0±5.0 72.5±10.9 66.7±11.1
16
Reach. 100.0 100.0 100.0 100.0 100.0 97.5±4.3 95.0±5.0 100.0 90.0±7.1 100.0 92.5±8.3 87.5±4.3 97.5±4.3 45.0±15.0
Data Race 100.0 100.0 100.0 100.0 100.0 87.5±8.3 97.5±4.3 97.5±4.3 100.0 82.5±4.3 97.5±4.3 72.5±8.3 100.0 97.5±4.3
Model GPT-OSS 120B Claude Opus 4.7 DeepSeek V3.2 DeepSeek R1 Kimi K2.5 Claude Sonnet 4.5 GPT-OSS 20B Qwen3-Coder-480B Qwen3-8B Qwen3-32B Ministral 3 8B Qwen3-Coder-30B Devstral 2 123B Mistral Large 3 675B
B.5
Total 84.9±0.9 82.8±1.7 75.5±7.1 71.4±3.7 68.8±2.9 67.7±3.8 66.7±4.4 58.3±5.1 34.9±4.3 34.4±1.8 17.7±4.3 16.1±4.0 13.5±1.0 12.5±2.6
Property Violated (101–400 LOC) Mem. Safety Overflow Termin. 85.0±5.0 77.5±4.3 100.0 72.5±4.3 100.0 70.0±7.1 62.5±19.2 60.0±12.2 80.0±10.0 72.5±13.0 37.5±4.3 92.5±8.3 70.0±7.1 50.0±7.1 85.0±5.0 75.0±5.0 52.5±4.3 75.0±5.0 55.0±8.7 52.5±10.9 100.0 67.5±4.3 37.5±4.3 72.5±10.9 12.5±4.3 7.5±4.3 82.5±4.3 5.0±5.0 10.0±7.1 92.5±8.3 20.0 15.0±5.0 27.5±4.3 12.5±4.3 7.5±4.3 35.0±5.0 12.5±4.3 5.0±5.0 20.0±7.1 17.5±10.9 10.0 5.0±5.0
Reach. 70.0 80.0 82.5±10.9 67.5±8.3 62.5±10.9 42.5±10.9 52.5±13.0 52.5±13.0 42.5±13.0 45.0±5.0 15.0±8.7 22.5±14.8 22.5±8.3 17.5±4.3
Data Race 93.8±10.8 93.8±6.2 96.9±5.4 90.6±10.4 78.1±5.4 100.0 75.0±12.5 62.5±8.8 28.1±13.6 15.6±5.4 9.4±10.4 0.0 6.2±10.8 12.5
Failure Analysis
We analyze failures from a single representative run (run_1) across all 14 models, observing 1217 incorrect answers and 57 unparseable responses out of 6994 total evaluations. Among the incorrect answers, 1069 are false negatives (model says OKAY on a violated property) and 148 are false positives (model says ERROR on a property that holds), a 7.2:1 ratio confirming the systematic overoptimism discussed in the main text. To systematically categorize failure modes, we combine manual review of a subset of responses (representative examples below) with an LLM-as-a-judge approach for the full set: reviewing all 1217 incorrect responses manually is infeasible, so we use Claude Opus 4.7 to classify each parseable incorrect response into predefined categories. Tables 4 and 5 summarize the results for the 1069 parseable false negatives and 148 parseable false positives.
False Negatives. The most common failure mode is missing edge cases (44%): models analyze the code but fail to consider the specific inputs or execution paths that trigger the violation. This is the dominant mode for memory safety (68%) and data race (51%) violations, where models typically trace the “happy path” without exploring adversarial inputs. The second most common is identified but dismissed (27%): models correctly identify the bug mechanism but rationalize it away. This is especially prevalent for memory safety (28%) and data race (35%), where models often appeal to practical runtime behavior rather than applying the formal specification. Incorrect reasoning (19%) is most common for reachability (33%) and overflow (27%), where models make control flow or arithmetic errors. Universal/existential confusion (8%) is concentrated almost entirely in termination (49%), where models confuse “can terminate” with “must terminate” — a qualitatively distinct failure reflecting a misunderstanding of the verification task rather than the code.
Table 4: False negative failure modes classified by Claude Opus 4.7 as judge (all 14 models). Mem. Safety Overflow Termination Reachability Data Race Total
Missed edge case
Ident. but dismissed
Incorrect reasoning
∀/∃ confusion
186 85 9 88 106
77 68 25 50 72
8 57 36 79 27
1 4 66 13 0
1 0 0 11 0
273 214 136 241 205
474 (44%)
292 (27%)
207 (19%)
84 (8%)
12 (1%)
1069
Superficial Total
False Positives. The dominant failure mode is incorrect reasoning (49%): models make errors in their analysis that lead them to flag non-existent bugs. Overly conservative judgments (26%) are concentrated in overflow and data race, where models flag operations that are technically safe. Misunderstood specification (19%) is most common for termination, where models misinterpret the property being checked. Fabricated bugs (5%) are most common for data race, where models claim a race condition exists in code that is actually safe. 17
Table 5: False positive failure modes classified by Claude Opus 4.7 as judge (all 14 models). Mem. Safety Overflow Termination Reachability Data Race Total
Incorrect reasoning
Misunderstood spec
Fabricated bug
Overly conservative
Superficial Total
8 25 7 21 12
5 0 23 0 0
2 0 0 0 5
5 20 1 4 9
0 0 0 1 0
20 45 31 26 26
73 (49%)
28 (19%)
7 (5%)
39 (26%)
1 (1%)
148
The following examples illustrate these failure modes in detail. B.5.1
Termination: Unsigned Wrapping
The model correctly identifies unsigned integer wrapping but incorrectly reasons that the wrapped sequence must eventually reach zero, missing a non-termination bug. This response is from Mistral Large 3 675B on termination-crafted/Cairo_step2-3.c. Program: typedef enum { false , true } bool ; extern unsigned int _ _VE RI FIE R_n on det _u int ( void ) ; int main () { unsigned int x ; x = __V ERI FI ER_ no nde t_ uin t () ; if ( x > 0) { while ( x != 0) { x = x - 2; } } return 0; }
Model response (excerpt): If x is odd, it will eventually become 1, and then the next subtraction will underflow (since unsigned int wraps around). For example: If x = 1, then x = x 2 will wrap around to UINT_MAX - 1 [...] However, this is not a problem for termination because [...] repeated subtractions of 2 will eventually bring it to 0 (since UINT_MAX is odd, and subtracting 2 repeatedly from an odd number will eventually reach 0). Final answer: OKAY Ground truth: Property violated (non-termination). When x is odd, subtracting 2 yields 1 → 232 − 1 → 232 − 3 → . . ., cycling through odd values and never reaching 0. The model correctly identifies the unsigned wrapping but incorrectly claims the sequence must reach 0. In fact, since 232 − 1 is odd and subtracting 2 preserves parity, the value cycles through odd numbers indefinitely. B.5.2
Reachability: Missing Fall-Through
The model fails to trace control flow after a recursive call returns, missing that execution continues to an error label rather than returning from the function. This response is from Ministral 3 8B on recursive-simple/afterrec-1.c. Program: void reach_error () { __assert_fail ( " 0 " , " afterrec -1. c " , 3 , " reach_error " ) ; }
18
void f ( int n ) { if (n <3) return ; n - -; f(n); ERROR : { reach_error () ; abort () ;} } int main ( void ) { f (4) ; }
Model response (excerpt): The recursion terminates naturally when n becomes less than 3. The reach_error function is only called if the code reaches the ERROR label, which it never does in this execution flow. Final answer: OKAY Ground truth: Property violated (reach_error is called). When f(3) calls f(2), the inner call returns immediately (since 2 < 3), but execution in f(3) continues past the recursive call and falls through to the ERROR label. The model incorrectly assumes the function returns after the recursive call. B.5.3
Memory Safety: Out-of-Bounds Write
The model correctly identifies that a memset call writes one byte beyond the struct, but rationalizes the violation away by arguing it is “still within the stack.” This response is from Devstral 2 123B on ldv-memsafety/memset2_-write.c. Program: typedef unsigned int __u32 ; struct compstat { __u32 unc_bytes ; __u32 unc_packets ; __u32 comp_bytes ; __u32 comp_packets ; __u32 inc_bytes ; __u32 inc_packets ; __u32 in_count ; __u32 bytes_out ; double ratio ; }; int main () { struct compstat cstats ; memset (( void *) (& cstats ) , 0 , 41 UL ) ; return 0; }
Model response (excerpt): The size 41 is slightly larger than the actual size of the struct (40 bytes), but since cstats is a local variable and not a dynamically allocated block, accessing one byte beyond the allocated memory (which is still within the stack) does not cause a segmentation fault. [...] This is acceptable. Final answer: OKAY Ground truth: Property violated (invalid dereference). The struct is 40 bytes, but memset writes 41 bytes, overwriting one byte beyond the struct’s bounds. The model correctly computes the size mismatch but incorrectly dismisses it as harmless because the memory is on the stack. While the write may not cause a crash in practice (the extra byte likely lands on accessible stack memory), the SV-COMP memory safety property requires that every dereference stays within the bounds of the allocated object. The model defaults to reasoning about practical runtime behavior rather than applying the formal specification it was asked to check. 19
B.5.4
Termination: Oscillating Variables
Multiple models fail to detect non-termination when two variables swap values in a way that prevents monotonic decrease. 7 of 14 models answer incorrectly, including Claude Sonnet 4.5 and Mistral Large 3 675B. Claude Opus 4.7 and DeepSeek R1 correctly identify the issue. Responses shown are from termination-restricted-15/Flip2.c. Program: typedef enum { false , true } bool ; extern int _ _ V E R I F I E R _ n o n d e t _ i n t ( void ) ; int main () { int i , j , t ; i = _ _ V E R I F I E R _ n o n d e t _ i n t () ; j = _ _ V E R I F I E R _ n o n d e t _ i n t () ; t = 0; while ( i > 0 && j > 0) { if ( i < j ) { t = i ; i = j ; j = t ; } else if ( i > j ) { j = i ; } else { i = i -1; } } return 0; }
Claude Sonnet 4.5 response (excerpt): The key insight: Eventually, through this process, i keeps getting decremented (at least every few iterations), and once i ≤ 0, the loop terminates. Since i is decremented regularly and will eventually become ≤ 0, the loop must terminate. Final answer: OKAY DeepSeek R1 response (excerpt): [. . . ] the loop runs indefinitely. This occurs when i and j alternate between values like 4 and 5, leading to no net decrease in either variable. Final answer: ERROR Ground truth: Property violated (non-termination). When i < j, the swap makes i the larger value; then i > j triggers j = i, equalizing them; then i == j decrements i by 1, making i < j again. For example, starting with i=4, j=5: the cycle (4,5) → (5,4) → (5,5) → (4,5) repeats indefinitely. Claude Sonnet 4.5 incorrectly assumes i decreases monotonically. B.5.5
Termination: Nondeterministic Loop Exit
Mistral Large 3 675B and several other models fail to recognize that a nondeterministic loop condition can prevent termination. This response is from loop-lit/mine2017-ex4.7.c. Program: extern _Bool _ _ V E R I F I E R _ n o n d e t _ b o o l () ; extern void abort ( void ) ; void reach_error () { assert (0) ; } void _ _ V E R I F I E R _ a s s e r t ( int cond ) { if (!( cond ) ) { ERROR : { reach_error () ; abort () ;} } } int main () { int x = 0; while ( _ _ V E R I F I E R _ n o n d e t _ b o o l () == 0) { _ _ V E R I F I E R _ a s s e r t (0 <= x ) ; _ _ V E R I F I E R _ a s s e r t ( x <= 40) ; if ( _ _ V E R I F I E R _ n o n d e t _ b o o l () == 0) { x ++; if ( x > 40) x = 0;
20
} } return 0; }
Mistral Large 3 675B response (excerpt): The loop will terminate because __VERIFIER_nondet_bool() can return 1 (terminating the loop) at any point. Final answer: OKAY Ground truth: Property violated (non-termination). The loop condition depends on __VERIFIER_nondet_bool(), which returns an arbitrary boolean. There exists an execution path where it always returns 0, causing the loop to run forever. The model confuses “can terminate” with “must terminate”: the property requires that every execution path reaches the end of the program, not just that some path does.
C
Training Details and Experiment Configurations
Inference. Evaluation uses vLLM with tensor parallelism across 8 GPUs, greedy decoding (temperature 0), and a maximum output length of 8192 tokens. Prompts exceeding 4096 tokens are excluded. C.1
Experiment Configurations
Table 6 lists all training configurations evaluated in this work. Unless otherwise noted, CPT configurations use Qwen3-8B, AdamW, LR 1×10−5 , cosine schedule, 1 epoch, batch size 64, FSDP across 8 NVIDIA A100 GPUs (40GB for 8B training and evaluation, 80GB for 32B evaluation). We use a single epoch without a validation set; the learning rate was chosen based on a single comparison (LR 5×10−6 underperformed on the best configuration) rather than a systematic search. “Thinking” refers to Qwen3’s internal chain-of-thought mode; “no thinking” disables it. All evaluations use 4 runs; we report mean±std.
Table 6: Training configurations and evaluation settings. ID
Description
qwen3-8B-base-no-thinking qwen3-8B-base-thinking qwen3-32b-base-no-thinking qwen3-32b-base-thinking qwen3-8b-cpt-html-bugs-no-thinking qwen3-8b-cpt-html-bugs-thinking qwen3-8b-cpt-html-bugs-lr5e6-no-thinking qwen3-8b-cpt-html-expanded-no-thinking qwen3-8b-cpt-html-expanded-thinking qwen3-8b-cpt-html-all-no-thinking qwen3-8b-cpt-html-all-thinking qwen3-8b-cpt-html-mixed-thinking qwen3-8B-soteria-bug-traces-plaintext-no-thinking qwen3-8b-plaintext-bugs-thinking qwen3-8b-cpt-bugs-only-no-thinking qwen3-8b-cpt-bugs-only-3ep-no-thinking qwen3-8b-cpt-filtered-no-thinking qwen3-8B-soteria-all-traces-plaintext-no-thinking qwen3-8B-soteria-balanced-no-verdict-no-thinking qwen3-8b-cpt-bugs-stripped-no-thinking qwen3-8b-cpt-code-only-no-thinking qwen3-8b-cpt-informalized-no-thinking qwen3-8b-cpt-sft-verdicts-no-thinking qwen3-8b-lora-sft-v2-no-thinking qwen3-8b-lora-sft-v3-no-thinking qwen3-8b-lora-sft-v4-no-thinking qwen3-8b-lora-sft-v5-no-thinking qwen3-8b-lora-sft-v6-no-thinking qwen3-8B-base-fewshot-no-thinking
C.2
Baselines Qwen3-8B base model (no fine-tuning). No thinking. Qwen3-8B base model. Thinking enabled. 14k max tokens. Qwen3-32B base model (no fine-tuning). No thinking. Qwen3-32B base model. Thinking enabled. CPT on HTML Traces Full CPT on 3,208 HTML bug traces (manifest violations only). No thinking. Same model. Thinking enabled. Same as html-bugs but LR 5×10−6 . No thinking. CPT on 5,048 HTML traces (754 manifest + 4,294 latent; manifest subset sampled to control the manifest/latent ratio). No thinking. Same model. Thinking enabled. CPT on all 34,495 HTML traces (bugs + non-bugs). No thinking. Same model. Thinking enabled. CPT on 1,754 HTML traces (754 manifest + 1k latent). Thinking. CPT on Plain-Text Traces CPT on 3,208 plain-text bug traces (HTML removed, manifest only). No thinking. Same model. Thinking. Collapsed: 45% unparsed. CPT on 5,048 plain-text traces (754 manifest + 4,294 latent). No thinking. Same dataset, 3 epochs. No thinking. CPT on 16,234 plain-text traces (filtered, no incomplete). No thinking. CPT on 34,495 plain-text traces (all). No thinking. CPT on 6,416 plain-text traces (50/50, verdict removed). No thinking. CPT on 5,048 stripped traces (error-relevant lines only, 72% reduction). No thinking. CPT on Other Data CPT on 3,208 C source files only (no traces). Ablation. No thinking. CPT on 5,048 traces informalized by Claude Opus 4.7. Collapsed: 62% unparsed. CPT + SFT (Two-Stage) CPT on 5,048 bug traces, then LoRA SFT r4 on 1,508 verdict examples (input: C code + property question; output: brief reasoning + “ERROR”/“OKAY” verdict). No thinking. LoRA SFT (No CPT) LoRA SFT on 13,155 examples (5.7% bugs). Input: C code + “trace the execution” instruction; output: full Soteria trace. r16, α32, LR 2×10−4 . No thinking. LoRA SFT r4, α8 on 2,504 examples (30% bugs). LR 1×10−4 . No thinking. LoRA SFT r4, α8 on 5,004 examples (15% bugs). LR 1×10−4 . No thinking. LoRA SFT r8, α16 on 5,004 examples. LR 1×10−4 . Collapsed: 70% unparsed. LoRA SFT r8, α16 on 5,004 examples. LR 2×10−5 . No thinking. Prompting Baselines (No Training) Base model with 2 Soteria trace examples in prompt (1 bug, 1 no-bug). No thinking.
Detailed Training Results
Tables 7 and 8 show per-property accuracy for all training configurations on our benchmark (1–400 LOC). Each value is the mean across 4 runs; ± indicates standard deviation. 21
Table 7: Per-property accuracy (%) on our benchmark — property holds (1–400 LOC). Configuration qwen3-32b-base-thinking qwen3-32b-base-no-thinking qwen3-8b-lora-sft-v4-no-thinking qwen3-8b-lora-sft-v3-no-thinking qwen3-8B-base-no-thinking qwen3-8B-base-fewshot-no-thinking qwen3-8b-lora-sft-v6-no-thinking qwen3-8b-cpt-code-only-no-thinking qwen3-8B-base-thinking qwen3-8b-cpt-bugs-stripped-no-thinking qwen3-8b-cpt-sft-verdicts-no-thinking qwen3-8b-cpt-html-all-no-thinking qwen3-8b-cpt-html-expanded-no-thinking qwen3-8b-cpt-bugs-only-no-thinking qwen3-8b-cpt-html-expanded-thinking qwen3-8b-cpt-html-bugs-thinking qwen3-8b-cpt-html-all-thinking qwen3-8b-cpt-html-mixed-thinking qwen3-8b-cpt-html-bugs-lr5e6-no-thinking qwen3-8b-cpt-filtered-no-thinking qwen3-8b-cpt-html-bugs-no-thinking qwen3-8B-soteria-all-traces-plaintext-no-thinking qwen3-8b-cpt-bugs-only-3ep-no-thinking qwen3-8b-lora-sft-v2-no-thinking qwen3-8B-soteria-balanced-no-verdict-no-thinking qwen3-8B-soteria-bug-traces-plaintext-no-thinking qwen3-8b-plaintext-bugs-thinking qwen3-8b-cpt-informalized-no-thinking qwen3-8b-lora-sft-v5-no-thinking
Total 95.2±0.3 95.4±0.6 92.0±0.8 91.7±1.5 90.7±0.6 92.2±0.9 89.8±1.8 87.4±0.4 85.4±1.7 86.4±1.2 86.8±1.0 83.8±1.8 83.7±1.5 84.6±1.8 78.7±1.2 78.0±2.1 77.9±1.4 77.2±1.3 79.9±1.2 82.5±0.9 80.0±0.7 80.9±1.2 79.5±1.8 77.9±1.0 75.0±1.5 71.6±2.9 54.6±2.1 28.9±1.0 26.3±1.4
Mem. 98.0 97.5±0.9 98.0 96.5±1.7 96.0±1.4 88.5±4.6 95.5±1.7 94.0±2.4 95.5±1.7 95.5±1.7 92.0±2.8 83.0±4.1 93.5±1.7 91.5±3.0 84.5±4.3 79.5±3.0 85.5±5.5 80.0±5.8 93.5±4.3 93.5±0.9 93.0±1.7 85.0±1.7 95.5±0.9 82.5±0.9 82.0±3.2 81.5±1.7 70.5±3.8 13.0±1.7 35.0±2.2
Over. 93.0±1.7 94.0±3.7 87.0±3.6 89.0±1.7 89.0±2.2 95.0±4.1 93.5±2.2 91.0±3.3 79.0±3.3 92.0±3.7 86.0±2.8 88.5±1.7 86.5±2.2 89.0±2.2 67.0±1.0 71.0±4.1 79.5±2.6 66.0±2.4 75.0±5.4 83.0±3.3 79.0±1.0 92.5±2.6 81.0±3.3 72.5±4.1 70.0±3.7 60.0±5.1 47.5±5.4 25.5±4.6 30.5±3.3
Term. 92.5±2.2 94.5±0.9 97.5±0.9 97.0±3.0 96.0±1.4 96.0±1.4 96.0±1.4 96.5±0.9 94.5±1.7 95.5±1.7 95.0±1.7 94.5±2.6 91.5±0.9 96.0±1.4 87.5±1.7 83.0±2.2 85.0±4.6 89.5±3.8 93.5±1.7 92.0±1.4 93.5±1.7 91.5±3.0 89.0±3.0 87.0±3.0 87.5±1.7 88.0±3.5 60.5±6.7 36.0±4.7 30.5±3.0
Reach. 93.5±0.9 94.0±2.4 93.5±0.9 94.0±1.4 89.5±4.6 93.0±2.2 86.0±4.5 83.5±3.3 81.5±1.7 82.0±2.4 91.5±2.2 83.0±1.0 79.0±3.6 88.0±3.2 80.5±4.6 80.5±3.6 69.5±3.0 80.0±3.2 79.5±0.9 83.0±1.7 77.0±2.2 86.5±5.7 78.5±3.3 90.5±3.0 79.0±6.7 76.0±6.8 53.5±0.9 46.0±2.0 17.5±2.2
Race 99.0±1.0 97.0±1.0 84.0±3.2 82.0±2.4 83.0±5.0 88.5±2.6 78.0±2.0 72.0±2.4 76.5±3.8 67.0±4.1 69.5±3.8 70.0±7.5 68.0±4.7 58.5±5.4 74.0±4.2 76.0±5.1 70.0 70.5±4.3 58.0±5.1 61.0±1.0 57.5±4.3 49.0±6.6 53.5±7.4 57.0±1.7 56.5±3.6 52.5±5.9 41.0±3.0 24.0±3.7 18.0±2.4
Table 8: Per-property accuracy (%) on our benchmark — property violated (1–400 LOC). Configuration qwen3-32b-base-thinking qwen3-8b-cpt-html-bugs-thinking qwen3-8b-cpt-html-expanded-thinking qwen3-8b-cpt-html-mixed-thinking qwen3-8b-cpt-html-bugs-no-thinking qwen3-32b-base-no-thinking qwen3-8b-cpt-html-bugs-lr5e6-no-thinking qwen3-8B-soteria-bug-traces-plaintext-no-thinking qwen3-8b-cpt-html-expanded-no-thinking qwen3-8b-cpt-bugs-only-3ep-no-thinking qwen3-8b-cpt-html-all-thinking qwen3-8B-base-no-thinking qwen3-8B-base-fewshot-no-thinking qwen3-8b-cpt-bugs-only-no-thinking qwen3-8B-base-thinking qwen3-8b-lora-sft-v2-no-thinking qwen3-8b-cpt-filtered-no-thinking qwen3-8b-lora-sft-v6-no-thinking qwen3-8b-cpt-bugs-stripped-no-thinking qwen3-8B-soteria-balanced-no-verdict-no-thinking qwen3-8b-cpt-code-only-no-thinking qwen3-8B-soteria-all-traces-plaintext-no-thinking qwen3-8b-cpt-html-all-no-thinking qwen3-8b-lora-sft-v3-no-thinking qwen3-8b-cpt-sft-verdicts-no-thinking qwen3-8b-plaintext-bugs-thinking qwen3-8b-lora-sft-v4-no-thinking qwen3-8b-cpt-informalized-no-thinking qwen3-8b-lora-sft-v5-no-thinking
C.3
Total 77.8±0.7 67.3±1.6 62.2±0.9 62.0±1.2 56.7±1.0 56.9±1.5 53.6±1.7 53.7±0.3 50.2±1.3 51.2±1.9 48.4±1.6 49.4±2.1 41.1±1.0 49.4±1.5 48.0±2.0 47.6±0.5 47.5±0.7 46.3±1.6 40.4±1.5 42.2±1.6 40.2±2.7 41.9±1.2 39.9±2.3 41.2±1.0 38.0±1.8 33.2±3.5 33.4±1.9 21.5±0.9 5.5±0.8
Mem. 69.0±3.0 47.0±1.7 33.5±1.7 36.0±5.5 39.0±4.1 39.0±4.4 24.5±3.6 22.0±1.4 17.5±1.7 18.0±3.5 26.5±5.0 19.0±3.6 24.0±2.0 14.0±2.8 24.5±2.2 46.5±0.9 16.0±2.0 17.0±1.0 13.5±2.2 14.5±1.7 22.5±3.8 13.0±2.2 20.5±4.8 12.5±0.9 8.5±2.2 22.0±4.5 22.0 5.5±0.9 7.0±1.7
Over. 72.5±1.7 66.0±2.4 62.0±3.2 60.0±2.4 51.0±3.0 52.5±3.6 55.0±6.4 68.0±3.7 51.5±4.6 48.0±2.4 35.5±1.7 37.5±1.7 26.5±1.7 50.5±5.0 44.5±4.6 50.0±2.8 39.5±2.6 31.5±7.4 30.5±2.6 49.5±1.7 33.0±3.3 25.5±4.3 25.5±4.1 29.0±1.7 35.0±5.4 23.5±4.6 37.0±4.1 33.0±1.0 3.0±1.0
Term. 95.5±1.7 94.5±1.7 89.0±1.0 90.0±3.2 79.5±1.7 88.5±1.7 78.0±2.8 66.0±4.0 73.5±3.0 70.0±4.5 85.0±6.4 78.5±1.7 73.0±1.7 70.5±2.6 82.5±3.3 63.0±3.6 69.0±4.1 73.0±4.1 61.0±3.0 47.0±3.0 59.0±7.3 65.5±3.8 65.5±3.0 62.0±4.5 50.0±4.5 62.5±4.6 47.0±3.3 24.0±2.0 8.0±2.4
Reach. 77.5±0.9 60.0±1.4 58.0±5.7 53.5±4.1 48.5±3.0 55.0±4.1 44.0±3.7 39.5±4.6 44.0±1.4 44.5±7.0 46.0±4.7 54.5±5.2 36.0±3.2 42.5±4.8 43.5±3.0 24.5±2.6 43.0±3.3 49.5±2.2 37.5±7.4 40.5±4.1 43.0±2.2 35.5±2.6 32.0±3.7 44.5±2.6 37.5±2.6 14.5±4.8 30.0±2.4 32.5±1.7 7.0±1.7
Race 74.5±1.7 69.0±8.5 68.5±3.0 70.5±4.3 65.5±3.0 49.5±2.2 66.5±4.8 73.0±3.0 64.5±3.6 75.5±6.1 49.0±2.2 57.5±1.7 46.0±3.2 69.5±3.8 45.0±4.1 54.0±1.4 70.0±5.7 60.5±2.2 59.5±1.7 59.5±3.8 43.5±1.7 70.0±5.8 56.0±4.9 58.0±3.2 59.0±1.7 43.5±4.3 31.0±1.0 12.5±3.0 2.5±0.9
Effect of Program Length on Training Configurations
Figure 8 shows accuracy by program length for selected training configurations, split by holds and violated. As with the baseline (Figure 2), holds accuracy remains relatively stable across length bins. On the violation side, bug trace CPT with thinking lifts the curve uniformly, with the largest absolute gains in the 101–200 LOC bin where the baseline is weakest. 22
LOC
0 1– 40 20
20 0 10 1–
–1 00 51
–5 0 26
0– 25
40 0
100 80 60 40 20 0
20 1–
00
(b) Property violated
10 1– 2
0 51 –1 0
50 26 –
0– 25
Accuracy (%)
(a) Property holds
100 80 60 40 20 0
LOC 8B base (nt)
8B base (t)
+ C files (nt)
+ all HTML (nt)
+ bug HTML (nt)
+ bug HTML (t)
+ bug plain (nt)
32B base (nt)
32B base (t)
Figure 8: Accuracy on our benchmark by program length for selected training configurations. (a) Holds accuracy degrades modestly with training on bug traces; the sharp drops at 201–400 LOC for thinking-enabled models reflect output budget exhaustion on longer programs (the model’s chainof-thought reasoning times out before producing a verdict). (b) Bug trace CPT with thinking (red) improves violation detection across all length bins, but the length-decay pattern persists: accuracy drops from 91.7% (0–25 LOC) to 57.1% (101–200 LOC), compared to the base model’s drop from 80.8% to 30.4%. “nt” = no thinking, “t” = thinking.
C.4
Soteria Trace Example
The following shows a real example from our training data: Soteria’s output for an uninitialized variable read, in both the original HTML format (used by cpt-html-* configurations) and the plain-text format (used by cpt-bugs-* and soteria-*-plaintext configurations). The plain-text conversion removes HTML tags, CSS classes, log-level prefixes, and decodes HTML entities while preserving the semantic content. Program (from CodeParrot): void exit ( int status ) ; int main () { int x ; if ( x ==10) exit (1) ; assert ( x !=10) ; }
HTML trace (excerpt): < div class =" log - msg DEBUG " > Executing statement : { signed int x ; if ( rvalue ( x ) == 10) func tion_d ecay ( exit ) (1) ; else ; assert ( rvalue ( x ) != 10) ; } </ div > < div class =" log - msg DEBUG " > STORE : ( ( x_563 , { kind = Uninit ; ty = signed int }) ) </ div > < div class =" log - msg DEBUG " > Executing statement : if ( rvalue ( x ) == 10) fun ction_ decay ( exit ) (1) ; else ; </ div > < div class =" log - msg TRACE " > Using state to error ! </ div > < div class =" log - msg TRACE " > Obtained summary : After_exec ({ args = []; pre = []; pc = []; post = { heap = []; globs = [] }; ret = ( Error ( Accessing uninitialized memory , [ Triggering operation : file_0537382 . c :6:6 -7]) ) }) </ div > < div class =" log - msg DEBUG " > Bug is manifest !! </ div >
23
Plain-text trace (excerpt): Executing statement : { signed int x ; if ( rvalue ( x ) == 10) func tion_d ecay ( exit ) (1) ; else ; assert ( rvalue ( x ) != 10) ; } STORE : ( ( x_563 , { kind = Uninit ; ty = signed int }) ) Executing statement : if ( rvalue ( x ) == 10) fun ction_ decay ( exit ) (1) ; else ; Using state to error ! Obtained summary : After_exec ({ args = []; pre = []; pc = []; post = { heap = []; globs = [] }; ret = ( Error ( Accessing uninitialized memory , [ Triggering operation : file_0537382 . c :6:6 -7]) ) }) Bug is manifest !!
Soteria tracks variable x as Uninit in the store. When the program reads x in the condition x==10, Soteria detects an access to uninitialized memory and reports the error with the precise source location. “Bug is manifest” indicates the error occurs on all feasible execution paths. C.5
Informalized Trace Example
The following shows a real example from our informalized training data, generated by prompting a frontier LLM to analyze C code in natural language based on Soteria’s symbolic execution output. Each training example contains the C code followed by a step-by-step analysis. Program: extern void __VERIFIER_error () __attribute__ (( __noreturn__ ) ) ; void __VERIFIER_assert ( int cond ) { if (!( cond ) ) { ERROR : __VERIFIER_error () ; } return ; } int main ( void ) { unsigned int x = 0; unsigned short N ; while ( x < N ) { x += 2; } __VERIFIER_assert ( x % 2) ; }
Informalized analysis (excerpt): Looking at this code , I need to trace through what happens in ‘ main ‘: 1. ‘x ‘ is declared as ‘ unsigned int ‘ and initialized to ‘0 ‘. 2. ‘N ‘ is declared as ‘ unsigned short ‘ but ** never initialized ** -- it holds an indeterminate value . Then we hit the loop :
24
while ( x < N ) { x += 2; } The loop condition compares ‘x ‘ ( which is ‘0 ‘) against ‘N ‘ , but ‘N ‘ has never been assigned any value . Reading ‘N ‘ here is accessing uninitialized memory , which is undefined behavior in C . Now let ’ s suppose we get past the UB and consider the assertion : __ VER IFI ER_ ass er t ( x % 2) ; Here ’ s the thing -- ‘x ‘ starts at ‘0 ‘ and is only ever incremented by ‘2 ‘. So ‘x ‘ remains even through every iteration of the loop . That means ‘x % 2 ‘ is always ‘0 ‘ , regardless of what ‘N ‘ is or how many times the loop runs . So ‘ __V ERI FIE R_a sse rt (0) ‘ is passed in . Since ‘ cond ‘ is ‘0 ‘ , ‘! cond ‘ is true , and we branch into the error label , calling ‘ __VERIFIER_error () ‘. So there are really two issues here : 1. ** Uninitialized read of ‘N ‘** -- undefined behavior at the loop condition . 2. ** Assertion violation ** -- even ignoring the UB , ‘x ‘ is always even , so ‘x % 2 ‘ is always ‘0 ‘ , and the assertion will always fail . The reachability of the error is guaranteed regardless of the value of ‘N ‘.
The informalized trace presents the analysis in natural language with explicit reasoning about execution paths, variable states, and the root cause of the violation. Unlike the raw Soteria output, it uses no tool-specific notation (no STORE, HEAP, or block labels), making it more accessible but less precise. C.6
Qualitative Example: CPT Model vs. Base Model
The following shows a case from our benchmark where the best-performing 8B CPT model with thinking (qwen3-8b-cpt-html-bugs-thinking) correctly detects a memory safety violation that the base model with thinking misses. The program searches for the first zero element in a nondeterministically initialized array: # define N 1024 int main () { int A [ N ] , i ; for ( i = 0; i < N ; i ++) A [ i ] = __VE RIFIE R_nond et_in t () ; for ( i = 0; A [ i ] != 0; i ++) { if ( i >= N ) break ; } __VERIFIER_assert ( i <= N ) ; }
Base model with thinking (incorrect — says OKAY, excerpt): < think > The array A is declared as int A [ N ] , which is a static array . The code accesses A [ i ] in the loops . Since the array is allocated on the stack , the pointers here are valid . The code doesn ’ t have any pointers that are dereferenced after being freed or invalid . So no invalid dereferences here . </ think > Final answer : OKAY
The base model incorrectly concludes that all array accesses are valid because the array is stackallocated, without considering the actual index values. CPT model with thinking (correct — says ERROR, excerpt): < think > ... The loop body checks if i >= N . If i is less than N , it does nothing . But if i reaches N , then the loop breaks . Wait , but the loop condition is A [ i ] != 0. So when i is N , the loop condition would check A [ N ] , which is out of bounds . Wait , the array A has indices from 0 to N -1. So if i reaches N , then A [ i ] is accessing A [ N ] , which is beyond the array ’ s bounds . That ’ s a problem . So during each iteration , the loop checks A [ i ] != 0. But if i is N -1 , then after incrementing , i becomes N . Then the loop condition checks A [ N ] , which is out of bounds . So this would cause an out - of - bounds access .
25
... </ think > Final answer : ERROR
The CPT model correctly identifies that when i reaches N after incrementing, the loop condition A[i] != 0 accesses A[N], which is beyond the array’s bounds (indices 0 to N−1). This result is consistent across all runs: the base model answers incorrectly in all 8 evaluations (4 with thinking, 4 without), while the CPT model answers correctly in all 4. This reasoning about boundary conditions and array indexing mirrors how Soteria’s symbolic execution systematically tracks array bounds and explores all feasible paths, including the worst case where every nondeterministic value is non-zero.
26