Spec # - это язык программирования, который является существенным расширением для C #. Это добавляет возможность определять контракты по методам. Контакты - это условия, которые должны быть истинными, чтобы метод был действительным. В качестве примера контакта можно указать, что конкретный параметр не должен быть нулевым при запуске метода.
Включает в себя инструмент, который можно запустить и который пытается доказать, гарантированно ли выполнены условия.
Это был исследовательский проект Microsoft, от которого сейчас отказались, но проделанная работа лежит в основе контрактов кода в .net 4.0 .
Spec # в Википедии