Semantic Model Verification

• Incompleteness, Soundness, Correctness
• Complexity and experience indicates bugs

• Domains (with attention to types)
• Coverage of all symbols

• Convert model formulae to axioms
• Generate obligation to prove each modelled formula
• Discharge using a trusted system (Otter!)
• Proof that this works