Лео де Моура, создатель Lean и специалист AWS, объясняет, как ИИ меняет формальную верификацию программ и математики. Lean сочетает язык программирования и помощника доказательств: свойства кода и их доказательства записываются формально и проверяются небольшим ядром. Доказательства можно экспортировать и независимо проверять другими реализациями; уже существуют два верифицированных проверяющих ядра.
Главное отличие от тестирования — универсальность результата. Тесты помогают найти ошибку на выбранных входах, а доказательство устанавливает свойство для всех входов, удовлетворяющих спецификации. Де Моура не противопоставляет методы: сначала тесты повышают уверенность и отсеивают ошибочные утверждения, затем имеет смысл строить доказательство. В качестве примера он приводит перенос zlib на Lean с проверенным свойством, что сжатие и последующее распаковывание возвращают исходные данные. Для Rust применяется связка Aeneas и Lean, которую команда Microsoft SymCrypt использует для криптографической библиотеки.
Новые модели умеют автоматически переводить код и математические тексты в формальные представления. Это снижает основную цену верификации — трудоёмкое ручное построение моделей и доказательств. По словам де Моуры, человеческая библиотека Mathlib за десять лет выросла до 2,5 миллиона строк, тогда как опубликованные созданные ИИ доказательства достигают 50 миллионов строк. Такие тексты не застывшие: их можно сокращать и рефакторить с повторной машинной проверкой.
Однако доказательство не гарантирует, что формальная модель верно описывает исходную программу, а спецификация — намерение заказчика. Для поиска расхождений используют дифференциальное тестирование. Поэтому при заявлении о верифицированном коде де Моура советует спрашивать, какие именно свойства доказаны, по какой спецификации, каким ядром и насколько велика доверенная кодовая база.
Он ожидает смещения работы инженеров к требованиям, формальным моделям и свойствам, хотя низкоуровневое программирование сохранится. Приоритетными направлениями он называет проверенные операционные системы, компиляторы, сетевой стек, песочницы агентов и механизмы их политик. Независимые ядра Lean нужны в том числе для того, чтобы не доверять единственному проверяющему компоненту.