About

In our interconnected world, software bugs and security vulnerabilities pose enormous costs and risks. The Deep Specification project addresses this problem by showing how to build software that does what it is supposed to do, no less and (just as important) no more: No unintended backdoors that allow hackers in, no bugs that crash your app, or your computer, or your car. “What the software is supposed to do” is called its specification.

The DeepSpec consortium developed new science, technology, and tools--for specifying what programs should do, for building programs that conform to those specifications, and for verifying that programs do behave exactly as specified. We focused on core software-systems infrastructure such as operating systems, programming-language compilers, and computer chips; with applications such as elections and voting systems, cars, and smartphones.

Experience has shown that it is extremely challenging to write good specifications for software. A maximally useful interface specification must be simultaneously

• rich (describing complex component behaviors in detail)
• two-sided (connected to both implementations and clients)
• formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs)
• live (connected via machine-checkable proofs to the implementation and client code).

We call specifications with all of these properties deep specifications.