Verification Techniques (we don't use)

Direct

• Directly verify the source code
• Generally impossible due to the complexity
  
• Example: IVY verified (kinda) using ACL2

Empirical

• Test over a large number of problems
• Check result against expected result
• Example: Otter is accepted as sound

Syntactic

• Repeat each inference step using a trusted system
• Example: IVY checks Otter

Higher Order

• Convert derivation to type theory and verify types
• Example: Bliksem with Coq