ИИ нашёл 418 ошибок в CPython, формализовав его на Lean

ИИ нашёл 418 ошибок в CPython, формализовав его на Lean
Исследователи использовали Claude Opus 5.5, чтобы переписать части CPython на Lean - языке программирования для математически проверяемых доказательств.

Масштаб проекта: 613 318 строк Lean, 1 539 файлов и 18 898 теорем и лемм.

Каждую функцию сравнивали с настоящим Python минимум на 50 000 входных данных, а затем проверяли математическими доказательствами и независимыми ИИ-агентами.
Результат: обнаружено 418 ошибок CPython. Около 55 из них могут приводить к падению интерпретатора или повреждению памяти.
Среди найденных проблем:
dict.setdefault() в определённых сценариях вызывает Segmentation Fault.
Операции с XML-элементами могут повреждать память.
Некоторые функции на C и Python возвращают разные результаты.
Есть важный нюанс: математическое доказательство подтверждает корректность формальной модели, но не гарантирует, что сама модель точно повторяет исходный код. Поэтому исследователи дополнительно сравнивают её с реальным CPython.
Пока проверена только часть проекта: 4 071 из 26 004 функций (15,7%).

Проект: https://broyojo.com/python-formalization/
Код: https://github.com/Broyojo/python-formalization