Для экспериментов с формальной верификацией кода (для встраиваемых приложений в первую очередь) у нас появился форк знаменитого инструмента CBMC.

CBMC это инструмент, позволяющий на основе формальной логики доказать отсутствие определённых классов ошибок в коде. Не "проверить, что работает", как инструменты тестирования, а выстроить полную цепочку математического доказательства отсутствия ошибки. Не любой, а строго конкретного вида (проблему останова никто не отменял). К счастью, самые распространённые ошибки известны заранее.

Без нейросетей, на такую работу просто не остаётся времени: научный код слишком сложный для интеграции в него своих концепций, только на поиск места для расширения могут уйти недели. При том, что сам код достаточно просто подтверждается на целевых задачах. Математика - штука строгая, и нарушения в решателе будут заметны сразу. Но даже с нейросетями, нужно сперва знать, а что вообще нужно и имеет смысл делать.

В первую очередь, добавлена полноценная поддержка хорновских дизъюнктов в качестве вывода символьного исчисления. Решаются через Z3 и Golem. Это серьёзно расширяет поддерживаемые классы кодовых выражений, которые покрываются верификатором. В частности, это индукция по рекурсии и сворачивание циклов в одно выражение. То есть, больше кода может стать верифицируемым.

Был вариант использовать SeaHorn и CBMC одновременно, но, во-первых, SeaHorn не настолько зрелый инструмент, и, во-вторых, они работают над разной базой: CBMC покрывает код непосредственно, а SeaHorn - байткод LLVM после конвертации. Потому, корректнее расширить CBMC для покрытия обоих классов.

Во вторую, добавлено четыре новых инструмента для профилирования результата работы верификатора:

--symex-merge-report показывает слияния путей, на которых значение перестаёт быть константой.

--equation-report показывает состав уравнения после среза по месту в коде.

--equation-trace показывает, где именно значение перестаёт быть константой.

--symex-profile считает шаги symex по функциям и строкам и слияния по точкам без потери данных при падении (например, если закончилась оперативка).

Со второй частью - самое интересное. Это даёт возможность инструментировать разработку так, что CBMC подсказывает нейросети, где нужно переписать код, чтобы его верификация не обходилась в часы работы и сотни гигабайт памяти. Без такой инструментации только человек мог подсказать, что вот это конкретное выражение создаёт математическую неоднозначность и тем самым мешает символьному решателю. Даже самые "умные" Claude Opus или OpenAI Astra сами так не могут. С инструментом - может любая.

Подход с CBMC в качестве советника для нейронки открывает новую возможность - поручать ей писать proof-based код. То есть, код, не содержащий ошибок по построению. Сдерживающий фактор здесь один - производительность. Проверки CBMC медленные. На 200 строк кода драйвера (об этом как-нибудь в другой раз) может уйти 12 часов. Но важно, что это 12 часов времени нейросети, а не человека. Человек с опытом, вероятно, справился бы быстрее. Человек без опыта даже не взял бы такой подход, он о нём даже не слышал.

Если смотреть в совокупности, то, условные "вайбкодеры", которые будут писать код с помощью такого подхода, сделают ПО, которое будет в среднем лучше, чем то, что напишут без применения CBMC и только ручным трудом. Да, можно сказать, они сами при этом не научатся этому подходу. Но, будем честны - они в своей жизни и не собирались ему учиться. При этом, самая большая проблема: незаметные и невычитанные ошибки нейросетей в коде - просто исчезает. Код с такими ошибками никогда не пройдёт верификацию.

P.S. Конечно, это далеко не всё, что нужно, чтобы действительно написать код, основанный на доказательстве. В первую очередь, нужен контракт, на который доказательство будет проверять, но это - совсем другая история.