Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

Tool access alone does not prevent two structural failures in LLM empirical reasoning: accepted outputs need not descend from attested evidence, and accepted deductions need not hold up under formal scrutiny. We present EG-VAR (Evidence-Grounded Verified Agentic Reasoning), a Lean4-based tool-calling architecture in which the Lean kernel is the sole minter of VERIFIED claims via tool-attestation axioms. The architectural guarantee is that every verified output structurally descends from an attested tool call (Theorem 3.1) and a kernel-checked chain of valid inference (Theorem 3.2); residual outputs are honest ABSTAIN with a replayable audit trail. On a subcollection of TableBench numerical reasoning ($n=120$), EG-VAR attains 120/120 versus 95\% same-tool baseline; on counterfactual stress tests (5 domains $\times$ 2 models), EG-VAR stays 100\% source-faithful while same-tool drops to 80--90\% (no-tool 50--80\%). With the LLM as deployment-time formalizer, residual semantic-formalization error is 3.3\% on Sonnet and 1.7\% on Opus. We position this as a constructive path toward eliminating hallucination in empirical inference: the kernel guarantee eliminates unsupported VERIFIED outputs today, and the remaining semantic-formalization residual becomes an auditable accuracy target that can shrink through formalizer fine-tuning, consensus formalization, and a longer-term formalization flywheel in which sources and LLM-generated documents increasingly expose typed sidecar representations.