Почему можно математически доказать 100% отсутствие багов в программе, ни разу её не запустив? Наука формальной верификации