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 · v1
cs.CR
TL;DR
Translates C code (SQLite) via Joern CPG into terms of a fuel-indexed Lean 4 definitional interpreter, with Lean-checked specifications and execution checks.
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
Autoformalization pipelines for code usually report a single coverage rate. That rate conflates constructs the translator declined to handle with constructs it translated incorrectly. Silently incorrect translations type-check and count as translated, so coverage cannot detect them.
Approach
A deterministic pipeline uses Joern's code property graph to export C source to JSON and then prints it as a term of a small, total, fuel-indexed Core interpreter written in Lean 4. Constructs that cannot be translated faithfully become holes labeled by cause. Coverage is reported in three tiers (hole-free, call-closed, dynamic-hole risk) with a per-cause trust ledger. Translated programs are executed and compared against compiled C to find silent miscompilations.
Results
On SQLite (8,602 functions, 1.5M AST nodes), 60.7% of functions are hole-free but only 24.8% are call-closed, a 2.4x gap. Six documented cases show coverage and fidelity moving independently, including silent bugs in character literals, do-while loops and variadic signatures that no coverage number registered. A vtable-dispatch construct previously classified as impossible was also retracted after a counterexample was found.
| Metric | Value |
|---|
| Functions / AST nodes | 8,602 / 1,513,464 |
| 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
