From Judge to Verifier: Formally Verified Faithfulness for Evidence-Grounded Generation

LLM-as-a-Judge offers no independent trust boundary: the same class of model that may introduce unsupported claims is trusted to detect them. We study claim-level grounding as a checkable criterion: every atomic claim in a generated artifact must be entailed by its upstream evidence. We introduce VerLean, a neurosymbolic verifier in which an LLM translates evidence and claims into a finite-domain model and entailment queries, and a deterministic Lean 4 kernel decides each formalized query. We develop it on a proof-of-concept regulatory-compliance dataset with two transformation tasks (1,624 claims: fact-to-summary and summary-to-requirement), test generalization on 444 public legal summaries, and stress-test on a synthetic benchmark of typed errors from public contracts (5,550 judgments). Across the three settings with a direct LLM-as-a-Judge comparison, VerLean raises F1 (0.747 to 0.917 fact-to-summary, 0.752 to 0.894 summary-to-requirement, 0.806 to 0.943 legal summaries), and on the typed benchmark detects unsupported claims at 0.895 recall and 0.935 F1. Its residual misses trace to neural translation, not the kernel; an ablation attributes the accuracy to the formalization, not the evaluator that reads it. The grounding decision is then a settled, mechanical check. The kernel decides it with no further LLM call, returning identical verdicts across runs. It thus dominates an LLM evaluator, which only matches that accuracy while adding cost and non-reproducible variance (LLM judges disagree on up to 44% of the subtlest errors). Failed queries yield counterexamples that repair more outputs, and sooner, than free-form judge rationales (first-attempt recovery up 4.3–12.9 points, reaching 90.9–97.0% in six attempts). Grounding decisions become reproducible, auditable, and, through their counterexamples, repairable.