1.2. Trust the checker, not the producer🔗

Search, simulation and model checking are untrusted: they emit certificates. A checker proved sound in Lean adjudicates each certificate, and only its verdict is relied on.