This was a project between ORA and Charles Stark Draper Laboratories (CSDL). NASA Langley and the Army had been funding CSDL to build fault-tolerant computer systems for over two decades. During this project CSDL became interested in the use of formal methods to increase confidence in their designs. ORA was given the task od formally specifing a key circuit (called the scoreboard) of the Fault-Tolerant Parallel Processor (FTPP) in Caliban.
The formal verification uncovered previously unknown design errors. When the scoreboard chip was fabricated, it worked without any error manifestation. It was the first time that CSDL produced a chip that worked ``perfectly'' on a first fabrication. CSDL credits VHDL-development tools and formal methods for the success.