EG-VAR: A Verified Lean 4 Runtime for Empirical-Reasoning Failures in Tool-Using LLMs

Tool-using LLMs can fail even when every tool call succeeds: the answer may be formally checked against the wrong empirical claim. EG-VAR targets these failures, where a Verified output disagrees with the intended source reading. It combines a failure taxonomy with a Lean 4 runtime that produces replayable, machine-checked proofs for empirical claims. The taxonomy splits verified-but-wrong outputs into three categories: attestation gaps, deduction gaps, and formalizer mistakes. Every accepted output ships with a proof file and its tool-call evidence; rejections return typed Abstain. The mkVerified gate admits Verified only from runtime-attested tool evidence (Theorems 3.1, 3.2). On TableBench numerical reasoning (n=120), EG-VAR attains 120/120 versus a 95% same-tool baseline. Across 5 counterfactual domains × 2 models, EG-VAR stays 100% source-faithful while the same-tool baseline drops to 80–90%. With an LLM formalizer at deployment, residual semantic formalizer error is 3.3% on Sonnet and 1.7% on Opus; ambiguities, benchmark issues, and abstentions are reported separately.