@galdor@emacs.ch I never used it, and I don't know how much it fits in this discussion, but today I found this https://www.cs.utexas.edu/users/moore/acl2/

"ACL2 is an interactive system in which you can model digital artifacts and guide the system to mathematical proofs about the behavior of those models. It has been used at such places as AMD, Centaur, IBM, and Rockwell Collins to verify interesting properties of commercial designs. It has been used to verify properties of models of microprocessors, microcode, the Sun Java Virtual Machine, operating system kernels, other verifiers, and interesting algorithms."