Разработчик создал первую формально верифицированную операцию пересечения 3D-сеток для constructive solid geometry (CSG) — mesh intersection. Реализация написана на Lean 4, а корректность доказана относительно короткой спецификации всего в 93 строки. Главный фокус проекта — практически исключить необходимость вручную проверять AI-код. Человеку достаточно прочитать эти 93 строки и запустить Lean checker, а 1000+ строк самой реализации и 60 000 строк формальных доказательств, сгенерированных автономно агентами (Claude Opus 4.8 и Fable 5), остаются чёрным ящиком. Никакого доверия к LLM при этом не требуется — гарантию даёт детерминированная проверка компилятором Lean.
Ядро верифицировано так, что при корректных входных mesh-объектах выходная сетка всегда описывает в точности пересечение соответствующих им тел, а сетка остаётся «хорошо сформированной» (well-formed): водонепроницаемая, без вырожденных треугольников и самопересечений, но допускаются касания по рёбрам или вершинам — это ослабление необходимо, иначе пересечение двух корректных сеток не всегда можно представить как strict 2-manifold. Спецификация компактна, потому что вся сложность обработки вырожденных геометрических случаев, ускоряющих структур вроде bounding volume hierarchy и исправлений T-junctions вынесена в реализацию, за которой следит формальное доказательство.
Производительность невысока: вычисление точного пересечения двух 70-тысячетреугольных моделей Stanford bunny занимает 24 секунды на M4 Pro. Приоритетом была минимизация усилий рецензирования, а не скорость. Код считает на точных рациональных числах, без аппаратно-ускоренной плавающей арифметики, что также увеличило время.
Для сравнения тот же набор требований дали агенту без формальной верификации — попросили написать аналогичный C++ kernel. Реализация тоже заняла более 1000 строк, и несмотря на юнит-тесты, другой агент позже нашёл в ней три различных бага, проявляющихся только в редких геометрических конфигурациях (например, когда вершина лежит одновременно на ребре и на грани, или каскадное попадание лучей в рёбра). Без машинно-проверенного доказательства исключить наличие новых ошибок невозможно.
Автор управлял проектом, пошагово усложняя спецификацию и оставляя агентам реализацию с доказательствами. Сперва формализовал математическую работу Фейто и Риверо по симплициальным цепочкам, затем добавлял ограничения на выходную сетку, убирал требование общего положения входных данных — каждый шаг требовал от агента новой реализации с полным доказательством. На финальном этапе спецификацию упростили для лёгкого рецензирования. Параллельно агенты оптимизировали код: при этом спецификация оставалась неизменной, и рецензировать заново ничего не требовалось.
Разработчик отмечает, что у подхода есть и минусы: формально верифицированное ПО склонно получаться медленнее, написание формальных доказательств тратит на порядки больше токенов, и далеко не для каждой практической задачи есть простая спецификация. Но с ростом возможностей AI-агентов формальная верификация способна сохранить контроль над программами, которые людям всё сложнее рецензировать вручную. Попробовать работу ядра можно в веб-демо — скомпилированный Lean-код исполняется локально в браузере через WebAssembly, данные на сервер не уходят.