Harmonic 27 октября открыла Aristotle для формальной проверки программ на C и описаний цифровых схем на Verilog. Прежде компания развивала систему как ИИ для математических доказательств. Теперь она предлагает инженерам проверять, выполняет ли код заданные требования: не только прогонять отдельные тесты, но и получать машинно проверяемое доказательство для всех допустимых входных данных в рамках описанной системы.

Aristotle предлагает свойства для проверки, сообщает, какие удалось доказать, и перечисляет допущения. Инженер должен проверить сами требования: доказать неправильно сформулированное условие — не значит решить исходную задачу. Утверждённые свойства можно хранить рядом с кодом и перепроверять после каждого изменения. Сервис уже доступен с оплатой по использованию; для организаций Harmonic также предлагает развёртывание в собственной инфраструктуре или частном облаке.

Один из примеров — LibTomMath, библиотека арифметики больших чисел. По отчёту Harmonic, Aristotle исправил три ошибки в версии 1.2.0, оптимизировал две арифметические функции и доказал соответствие ускоренного кода тем же требованиям. В тестах производителя модульное возведение в степень стало быстрее в 1,31–1,38 раза по сравнению с уже исправленной исходной версией. Для чисел, помещающихся в один внутренний разряд библиотеки, скорость возведения в квадрат практически не изменилась. Измерения проводились на Xeon Platinum 8375C с GCC 14.2; переносить выигрыш на любые программы нельзя.

В проекте Tensordyne система проверяла сложный блок будущего чипа. Из 241 свойства она доказала 185 и опровергла 56, предоставив воспроизводимые контрпримеры. Сама Aristotle сформулировала 100 свойств, остальные 141 уже находились в коде разработчиков. Вместе с более ранними проверками отдельных частей эта работа помогла команде найти восемь ошибок на ранней стадии проектирования. Это результаты, опубликованные поставщиком вместе с заказчиком, а не независимый аудит.

Граница гарантий хорошо видна в примере LibTomMath: доказательства охватывают выбранные функции и их вспомогательный код при оговорённых условиях. Вся операция модульного возведения в степень измерена в тесте, но целиком не доказана; завершение вычислений, остальная библиотека и скорость также вне доказательства. Новый инструмент связывает генерацию и оптимизацию кода с проверкой конкретных требований — полноту этих требований всё ещё приходится определять людям.