A Trust Ledger and an Execution Check for CPG-Based C-to-Lean 4 Autoformalization: Separating Declined from Silently Incorrect Translations
Ishan K Singavarapu, Manish Bhatt
cs.PL
Sep 28, 2026 · v2
cs.CR
TL;DR
Translates C (SQLite) via a Joern code-property-graph exporter into terms of a fuel-indexed Lean 4 definitional interpreter, with Lean-checked specifications and axiom sweeps.
Abstract
Verifying large C codebases requires translating them into formally checkable semantics, but most autoformalization work reports a single aggregate success rate that conflates two different failure modes: code the translator declined to handle and code the translator translated incorrectly. We present a deterministic code-property-graph (CPG)-based exporter that translates C source into a small Lean 4 core semantics under a three-tier correctness discipline: hole-free, call-closed, and dynamic-hole-risk, that keeps these modes distinct. Applied to a re-export of the SQLite source tree (8{,}602 functions, over 1.5 million AST nodes), the exporter translates 5{,}222 functions (60.7%) hole-free, of which only 2{,}134 (24.8%) are call-closed, a $2.4\times$ gap a single rate would hide. Both figures are reported in a full per-construct trust ledger rather than a single score. Our main contribution is methodological: a protocol for separating constructs that are fundamentally unresolvable by whole-program static analysis (such as public API boundaries) from constructs that only look that way. For example, we retracted our own “impossible” classification of function-pointer/vtable dispatch after tracing a concrete counterexample in the target codebase. Separately, a search for “more holes closed” surfaced a latent silent-wrong-answer bug: a translation that succeeded with an incorrect result rather than declining, a failure mode we argue is more dangerous than any hole, and one a hole-count-only evaluation would never surface.
Problem
C-to-formal autoformalization pipelines usually report one aggregate success rate. That rate mixes constructs the translator declined to handle with constructs it translated incorrectly. Silently incorrect translations type-check and count as translated, so coverage metrics cannot detect them.
Approach
A deterministic pipeline exports Joern code property graphs to JSON and prints them as terms of a small, total, fuel-indexed Lean 4 interpreter for a core language. Declined constructs become holes labeled by cause. Coverage is reported in three tiers (hole-free, call-closed, dynamic-hole risk) with a per-construct trust ledger. Translated programs are also executed and compared against compiled C, alongside mutation gates and an axiom sweep with kernel replay.
Results
On SQLite (8,602 functions, about 1.5M AST nodes), 5,222 functions (60.7%) are hole-free but only 2,134 (24.8%) are call-closed, a 2.4x gap. Six documented cases show coverage and fidelity moving independently, including character-literal, do-while and variadic mistranslations that left the metric unchanged. A seventh finding exposes instability in the cause taxonomy itself, and an earlier 'impossible' classification of vtable dispatch was retracted.
| Metric | Value |
|---|
| Functions | 8,602 |
| Hole-free | 5,222 (60.7%) |
| Call-closed | 2,134 (24.8%) |
| Residual holes / causes | 14,260 / 70 |
| Dynamic-hole risk constructs | 216,730 |
SQLite export coverage tiers
