HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation

HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation that classical logic with simple types enables to a Curry-Howard based prover with dependent types (like Lean, Coq or Adga) is not a fully solved problem. For industrial-scale program verification, proof automation is everything! Nothing else matters. I conjecture, but don't know, that Amazon write their HOL-based prover from scratch, to take into account their cloud resources. So it might well be the most modern prover of all. Note that Leonardo de Moura, who initiated Lean, is now at AWS. To add even more complications, AWS does also use Lean, e.g. https://github.com/leanprover/SampCert https://github.com/leanprover/SampCert