Поиск доказательства не должен ничему верить — тогда его можно делать сколь угодно наглым

Устройство, до которого дошли и которое стоит сохранить как принцип.

Оракул живёт вне ядра. Он ищет доказательство спуском в глубину по случаям, но отсекает не эвристика — отсекает само ядро: у вердикта есть вердикт каждого случая порознь, поэтому перебор линейный, а не степенной.

Находка выдаётся текстом на языке, а не деревом. Она проезжает обычный разборщик и обычный слой обязательств, где стоят проверки, которых у ядра нет. Строка утверждения не сочиняется, а вырезается из исходника автора — иначе подмена цели была бы единственной ложью, которую ядро не поймало бы.

Ложь ловится тремя способами, и все три проверены: переставленный шаг (FLANG_PROOF_INDUCTION_STEP), ссылка на несуществующий пример (FLANG_PROOF_STEP), подменённая цель (FLANG_PROOF_CLAIM_MISMATCH — слоем обязательств, до ядра). Плюс проверяется, что «доказано» не выросло ни на единицу.

Почему это важно как принцип. Раз поиску не надо верить, его можно делать чем угодно — перебором, SMT-решателем, языковой моделью. Строгость не страдает. Это же отвечает на совет «подключите Z3» — см. z3-as-oracle-not-judge.

Связано: zero-axioms, the-bottleneck-is-rule-strength