From the research web site:
The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. The system consists of:
More info: http://research.microsoft.com/SpecSharp/
If you've ever read the Pragmatic Programmer or done contract-based programming before with tools like iContract, you'll instantly see the value of pre- and post- conditions for code.