Maxima 是一款计算机代数系统，是Macsyma 项目的衍生产品。它使用 Common Lisp 构建，可在所有主要操作系统中运行，并支持符号和数值计算。
此外，Maxima 还允许将昂贵的数值代码编译为 Fortran 以加快执行速度。
ACL2 是一款定理证明工具。
AMD 使用 ACL2 对 AMD Athlon 的 IEEE 754 浮点数支持的正确性进行了正式验证。
Motorola Government Systems 使用 ACL2 为 Motorola CAD 信号处理器认证了微代码程序。该模型可用于预测每个周期中的每个内存位。
