программное обеспечение с нулевым уровнем дефектов(созданное за счёт использования средств контрактного программирования в исходном коде и проверки контрактов в исходном коде с помощью автоматизированного доказывателя теорем. Под контрактами понимаются предусловия, постусловия методов, инварианты типов данных и циклов. Alex_Odeychuk)