> 1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do). I agree. In the Metamath community, we also check

> 1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do). I agree. In the Metamath community, we also check all proofs with a collection of verifiers written by different people in different languages, all based on a very small kernel. That provides extremely high confidence in its correctness.