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.