Certifying the Judge: Falsifiable Properties for LLM-Based Evaluation of Formal Code

LLM judges are increasingly central to evaluating AI-generated code, tests, and formal specifications, yet their reliability is still checked in the least scalable way possible: fresh human ratings for every new judge, prompt, model, and threshold. We challenge this validation loop by asking whether human judgment can be amortized and scaled through falsifiable behavioral properties. We propose a property-certification protocol for LLM judges of Lean 4 theorem and specification quality, where each judge is scored by four automatically testable conditions: identity, bug monotonicity, specification monotonicity, and repeat/prompt stability. Our variance-aware trust index TIvar is one calibrated instantiation of these diagnostics. Rather than presenting a single fitted weighting as a universal evaluator constant, we contribute a reusable certification protocol that converts falsifiable behavioral properties into an auditable trust signal for LLM judges. On eight judge configurations spanning frontier prompts, weaker baselines, edit-distance, and random controls, TIvar strongly predicts judge-level human alignment on that calibration suite, reporting validation-set Spearman correlations of 0.833 (avg labels), 0.905 (pass1), and 0.738 (pass2). Property-level analysis shows that monotonicity under removed specifications is the strongest single predictor of human agreement, followed by monotonicity under injected bugs, while identity and stability are weaker standalone signals. Applied to VeriBench, the protocol illustrates how a small human calibration set can support scalable, auditable judge selection for AI-generated code, tests, theorems, and formal specifications, without claiming universal or deployment-time guarantees.