Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped first-order subset of Pure Lisp (and later Common Lisp with ACL2)), but there are a lot of similarities! It also integrates computable counterexamples in a really cool way (they're first-class values reflected in the runtime and you can directly compute with them, including counterexamples to higher-order goals which involves function synthesis!). Imandra is used a lot for formal verification in finance, for example.