С>А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.

вид известен, а код — нет, т.к. написать его ни у кого сил не хватает
в отличие от презренных тестов и т.п.