We are studying whether a structured certificate — the model states premises with cited file/line evidence, a trace, and a formal conclusion — makes a language model better at static code-reasoning tasks like fault localization, and whether that structure can be made pluggable and specialized to a target domain. Our target domain is the Linux kernel.
"Agentic Code Reasoning" (arXiv:2603.01896, Ugare & Chandra) reports that a semi-formal prompt beats plain reasoning on static code tasks, and — importantly — that the benefit is model-dependent: some models gain, others regress. If a certificate is a prompt-level artifact rather than a property of the weights, then the certificate is a knob: its premises, evidence rules, and proof obligations can be redesigned and swapped without retraining, and specialized to the failure modes of a particular codebase.
The question we care about is not "does one certificate help on a public benchmark," but "how do we evaluate pluggable certificate designs fairly, and which ones transfer to a real, adversarial, non-memorized target — kernel-style C." Everything below is the baseline that makes that evaluation trustworthy.
An independent, execution-free replication on the paper's two headline models, plus a third model outside the paper. 37 Defects4J bugs (Commons Lang/Cli/Csv/Gson), reconstructed with no JDK and no test runs; the bug set was frozen before any model call. Single-shot, no extended thinking. The grader is the paper's Top-N hunk-overlap, reads only the model's final ranked-predictions block — identically for every condition, never the certificate's citations — so a certificate cannot win by citing more lines.
| Model | Subset | n | Top-1 Any | Top-5 Any | Top-5 All |
|---|---|---|---|---|---|
| Opus-4.5 | all | 37 | +5.4 | +2.7 | +5.4 |
| Opus-4.5 | non-mem | 18 | +0.0 | +5.6 | +5.6 |
| Sonnet-4.5 | all | 37 | +2.7 | −5.4 | −2.7 |
| Sonnet-4.5 | non-mem | 21 | +0.0 | −4.8 | −4.8 |
| gpt-5.2 | all | 37 | +0.0 | −2.7 | −2.7 |
| gpt-5.2 | non-mem | 15 | −6.7 | −6.7 | +0.0 |
Opus-4.5 gains, and the gain is larger on the non-memorized bugs (+5.6pp Top-5 All), so it is not a recall artifact. Sonnet-4.5 regresses, and the regression deepens on the harder bugs. The two paper models split in exactly the directions the paper reports; a third model (gpt-5.2) patterns with the regressing side.
| Model | standard | standard_matched | semiformal | evidence_only |
|---|---|---|---|---|
| Opus-4.5 | 54.1% | 46.0% | 59.5% | 51.4% |
| Sonnet-4.5 | 43.2% | 46.0% | 40.5% | 46.0% |
| gpt-5.2 | 54.1% | 54.1% | 51.4% | 56.8% |
standard_matched = reason at length (a verbosity control);
evidence_only = cite evidence without the formal proof.
Defects4J is a decade-old public benchmark, and every model partly recalls it. A source-free probe — failing-test name and candidate file list, no source code — still localizes a large share of bugs (22/37 for one model). Absolute Top-N is therefore inflated by memory for everyone. The paired semi-formal-vs-standard comparison is unaffected (both conditions face the same recall) and the model-dependence split holds on the non-memorized subset, so the finding survives — but the contamination is real, and it is the reason the baseline cannot be a public Java benchmark. It has to move to a target the model has not seen.
The reproduction is a harness, not a one-off script. It is built
kernel-style: every experiment toggle flows through
Kconfig, so the paper reproduction and the augmented
certificate work are separate, pinned build targets
(make defconfig-code-reason-paper reproduces the paper's
static verifier with the standard and semi-formal conditions;
make defconfig-code-reason adds the knlp certificate
addendums, each independently ablatable). The bugs are reconstructed
execution-free — no JDK, no test runs — from
Defects4J's own metadata and our own buggy→fixed diff, and the bug
set is frozen before any model is called. Grading is one condition-neutral
function that reads only the model's final ranked predictions.
Every run saves the raw model output, and the grader
re-scores offline from that saved text with no API calls
(faultloc_run.py --regrade). A parsing fix, a metric change,
or an audit therefore costs nothing and never re-queries a model —
the numbers on this page can be regenerated from the archived raw
responses alone.
| Model | Access | Calls | Cost (USD) |
|---|---|---|---|
| gpt-5.2 (pre-paper snapshot) | OpenAI API | 185 | $7.77 |
| Opus-4.5 | Anthropic API | 185 | $40.92 |
| Sonnet-4.5 | Anthropic API | 185 | $8.80 |
| total | 555 | $57.49 |
The baseline establishes two things a real program can build on: the certificate is a prompt-level knob with a genuine structural effect, and public Java benchmarks are memorization-capped. The next step is an evaluation framework for pluggable certificate designs — different premise sets, evidence obligations, and proof shapes — measured on a domain-specific, contamination-resistant target rather than a leaderboard.
We are focusing that target on the Linux kernel: kernel-style C, the bug classes that matter there (undefined behavior, memory-safety faults, concurrency and resource errors), and ground truth established by construction and confirmed by sanitizers rather than by recall. The harness is built kernel-style — every experiment toggle flows through Kconfig, grading is blind to the certificate and neutral across conditions, and a surface-matched control gates whether a design is measuring reasoning or leakage before any expensive evaluation runs.
Certificate premises, citation rules, and proof obligations are swappable and independently ablatable, so a domain expert can encode kernel-specific failure modes without retraining a model.
Synthetic, construction-proven C with surface-matched safe/buggy siblings, held-out families, and a leakage gate — so a score reflects reasoning on unseen code, not memory of a benchmark.
The grader reads only the model's committed answer, identically for every condition, and every run re-scores offline from saved raw output — no result depends on a live model call.
Kconfig defconfigs pin each experiment; the reproduction path and the augmented-certificate path are separate, versioned build targets.
This work is under active development and will be evaluated shortly. The baseline above is the fixed point it builds on; the certificate-design and kernel-target results are forthcoming.