Maxima is a computer algebra system descended from the
Macsyma project. It’s built in Common Lisp, runs an all major
operator systems, and supports both symbolic and numerical computation.
Maxima also allows expensive numerical code to be compiled to Fortran to
speed up execution.
ACL2 is a theorem prover.
AMD used ACL2 to formally verify the correctness of AMD Athlon’s
IEEE 754 floating-point support.
ACL2 was used by Motorola Government Systems to certify microcode
programs for the Motorola CAD signal processor. The model could be
used to predict every bit of memory at every cycle.