While a system as complex as ACL2, Coq, or Isabelle most likely will have bugs, the really interesting question is if the proof verifier that is run on the gene

While a system as complex as ACL2, Coq, or Isabelle most likely will have bugs, the really interesting question is if the proof verifier that is run on the generated proof is too complex or has bugs. In my view, one should preferably have several independent proof verifiers that have been manually inspected for there to be sufficient trust. It is ok if such verifiers are slow, simplistic, and use lots of memory, given that they should preferably be used as a final check that the verification process worked correctly.