Trusting the Verifier

Soundness and Completeness

• A complete verifier finds every fault
• A sound verifier finds only faults
• Completeness is more important (converse to ATP)

Relying on Trusted Systems

• Incomplete trusted system ⇒ unsound verifier
• Unsound trusted system ⇒ incomplete verifier
• Only emperical verification exits the cycle of doubt
• Lower the limbo bar to enhance the trust
  • A weak trusted system is more trusted
  • A weak trusted system discharges only small steps

Cross Verification

• Every system used as the trusted system for others' derivations
• Either they're all wrong or all right