Conclusion Executable Formal Models Program Admittedly unique requirements Identified areas of weaknesses in ACL2 User solutions are possible, but error prone "Blessed" solutions would be better