CertJudge: Evaluating Lean Formal-Code With Falsifiable Properties

LLM judges are increasingly used to evaluate AI-generated code, tests, theorems, and formal specifications. In our setting, a judge scores the quality of a candidate Lean 4 artifact relative to a gold reference, but validating each new judge, prompt, model, or threshold with fresh human ratings is expensive and does not scale. We ask whether this validation can be amortized through behavioral checks that are automatic and falsifiable. We propose CertJudge, a property-certification protocol for LLM judges of Lean 4 theorem and specification quality. Instead of treating human agreement as the only validation signal, CertJudge tests whether a judge behaves correctly under controlled perturbations measuring identity, bug monotonicity, specification monotonicity, and stability. These diagnostics are combined into a variance-aware trust index, TI_var, which provides a summary of judge reliability rather than a universal evaluator constant. On a human-labeled validation suite, TI_var strongly predicts judge-level human alignment, reporting validation-set Spearman correlations of 0.833 (avg labels), 0.905 (pass1), and 0.738 (pass2) (Appendix G). On VeriBench (Section 5.1), we use the calibrated judge to rank theorem-generation methods, illustrating how a small human calibration set can support scalable judge selection. These results are validation-set calibration evidence, not a claim of universal reliability or deployment-time generalization. Subsequent to the accepted workshop version of this paper, we analyzed the independent five-reviewer annotation pool (343 labels over 78 pairs) that had been collected as the held-out test set; Section 6.1 reports the outcome. The direct frozen test is confounded by an annotation-protocol revision—the pool's labels are nearly uncorrelated with the calibration labels (Spearman ≈ 0.13 on shared items)—and a pre-registered re-anchored screen over 32 judge configurations found no label-free property signal meeting its registered success bar. Cross-protocol transfer therefore remains an open question that these results bound but do not settle.