Welcome to Trustee!
Trustee is a HOL kernel implemented in OCaml, with a few unusual design choices, such as the pervasive use of hashconsing, explicit type application, and de Bruijn indices.
This website shows a proof-checker for opentheory using Trustee. This doubles as a test suite and gives an idea of how performant the tool is.