We have been involved in various industrial verification projects including. Our methods and tools are used in a variety of security-oriented processing; our tools have been used to certify arithmetic and encryption/decryption circuitry in commercial microprocessors. using ACL2 ( ‘A Computational Logic for Applicative Common Lisp’), a theorem prover that has seen sustained industrial use since the mid-1990. We are also involved with developing mathematically certified tools.
We developed the first high-speed, mechanically verified SAT proof checker. This certified SAT proof checker is the first one with sufficient performance to determine the correctness of SAT solver results for the International SAT proof solver competition.