did anyone know that there was a phd dissertation written about Clojure? "TRANSLATING CLOJURE TO ACL2 FOR VERIFICATION" by RYAN LEE RALSTON to the University of Oklahoma?

I skimmed it a few years ago

kinda sounds up your alley

you do lots of verification in ocaml right?

indeed, and our logic is modelled kinda closely to that of ACL2's (PRA + TI(epsilon_0))

though it's, of course, typed