CINDER: Differential and Symbolic Equivalence Checking for Diffcolic Analysis of LLM-Based C-to-Rust Translation

Abstract

Cinder is a verification and evaluation framework for diagnosing behavioral mismatches introduced by Large Language Model (LLM) generated translations from C to Rust. LLMs can accelerate migration of legacy system code, but they frequently produce subtle semantic regressions (e.g., integer overflow, undefined behavior, or mis-translation of low-level idioms). Cinder addresses this by combining three complementary components: (1) contract-aware differential testing that produces empirical pass rates k/n together with exact Clopper–Pearson confidence intervals; (2) Satisfiability Modulo Theories (SMT) based equivalence checking in Z3 that models machine semantics using fixed-width bit-vectors so that proofs and counterexamples reflect real overflow and wrap behavior; and (3) a configurable, consensus-aware evidence synthesizer that aggregates formal and empirical signals into an interpretable overall confidence score. Cinder is designed both to validate individual translations and to serve as an auditable diagnostic instrument for comparing multiple LLMs on a common metric suite: per-translation empirical statistics, formal-prover outcomes, error-taxonomy labels (e.g., overflow difference, undefined behavior, semantic difference), and performance ratios. Implementation work reported here includes migrating Z3 encodings to BitVec semantics, hardening the differential runner to emit reproducible failing traces and Confidence Interval (CI) backed outputs, and exposing verifier weights and sensitivity analysis to support robust interpretation of results. Using Cinder as a diagnostic tool, this thesis investigates classes of program fragments and their error-prone tendencies under LLM translation, as well as providing a reproducible methodology for comparing LLMs along these diagnostic dimensions. The outcome shows a direction indicating where automated translation is reliable and where human or additional formal review is required in regard to handling with LLM translation.