ACL2 is a modeling and analysis tool, which is regularly used to help ensure the correctness and security of computing system.
The ACL2 system is written in Common Lisp, and OpenMCL is used for ACL2 development and deployment. Enhancements and extensions so OpenMCL will better support analysis and theorem proving is being funded, in part, by DARPA and the NSF under subcontract from the University of Texas.
Please contact Professor Warren A. Hunt, Jr.,