Far as TCB, Jared Davis, who used ACL2 on x86 processors, built a self-verifying prover for a logic going in ACL2's direction. It was verified to assembly using Magnus Myreen's techniques.
ACL2 is a proof assistant, at least, but it's not based in type theory, so that's probably why they didn't use or improve it. ACL2 looks like it's specifically intended to aid in proving theorems about models of software systems, as well, which probably makes its logic system a bit clunky to use when expressing theorems about mathematical structures.
2. A model checker most certainly provides 100% guarantees. This is why it's called a model-checker: it checks that a system's Kripke structure is a model (i.e. a satisfying assignment) for a formula. It's just that model checkers often fail to check infinite state spaces and so people often check a finite instance of a specification. While model checkers have occasionally found errors in (informal but peer-reviewed) "proofs", I am not aware of any cases to the converse (obviously, when a finite instance was used for an infinite-state system). Both model checkers and deductive proofs have limitations and are generally complementary, but currently model checkers are considered to be much more scalable.
Also, model checkers don't "simulate a model some number of times." (the model-checking algorithm for temporal logic won the Turing award for its inventors). Even in finite state cases, model checkers check temporal formulas on infinite behaviors (e.g. that every request is eventually matched by a response).
ACL2 was designed for real hardware and software. That's what many use it for. Rockwell-Collins builds CPU's, separation kernels, and low-level software for NSA with it. I agree author maybe dodged cuz it's not type theory.
Yeah, focusing on stuff closer to your direction of type theory makes sense. Thanks for writing up your work and good luck on your project.
... And it's not really clojure-specific except if you want to try LaTTe:
(Edit missing link)