Verification Techniques (we don't use)

Direct

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

Empirical

• Test over a large number of problems
• Check result against expected result
• Example: Otter is accepted as sound
• It's a social situation

Syntactic

• Repeat each inference step using a trusted system
• Example: TESC and SC-TPTP
• Example: IVY checks Otter
• Doomed to failure

Higher Order

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