From checked evidence to semantic guarantees

verify applies registered soundness theorems and discharges executable side conditions by kernel reduction. A checker result alone is not a semantic theorem: each supported checker must provide a proved rule, tagged @[verify], connecting its result to the requested property.

This module has no dependency on a particular certificate format, optimizer, or external solver. Domain modules register their own rules. No external process is run by the tactic.

def attrVerify : Lean.ParserDescr

Register a proved soundness rule. Unproved success and domain conditions remain obligations.

def tacticVerify : Lean.ParserDescr

Prove a semantic guarantee using registered soundness rules and checked evidence. Fails unless every obligation is solved. Introduce universal hypotheses explicitly when needed.

def tacticVerify? : Lean.ParserDescr

Prove a semantic guarantee using registered soundness rules and checked evidence. Fails unless every obligation is solved. Introduce universal hypotheses explicitly when needed.