Фирмы по безопасности всё чаще используют ИИ за пределами агентного кода для улучшения аудитов безопасности, создавая кастомные инструменты и формальные модели перед фактической проверкой кода. Например, при обзоре виртуальной машины Miden, которая не имеет инструментов для разработчиков, агенты потратили шесть месяцев на создание сервера LSP, декомпилятора, движка статического анализа и бережливой модели исполнителя виртуальной машины. Эти инструменты выявили значительные уязвимости безопасности, такие как невалидированный вход, предоставленный проверяющим, что могло позволить подделку подписей Falcon и кражу средств. Модель Lean также производила 95 машинно проверенных доказательств корректности для значительной части основной библиотеки Miden. Miden VM, новая виртуальная машина с нулевым уровнем ознавания и собственным ассемблером (MASM), представляла уникальные сложности при проверке из-за архитектуры стек-машин и отсутствия инструментов для разработчиков. Для решения этой проблемы команда сосредоточилась на создании основных инструментов, начиная с LSP-сервера и расширения VS Code для выделения синтаксиса, навигации по коду и документации инструкций. Далее был разработан декомпилятор для процедур MASM для предоставления высокой семантической информации, несмотря на сложности, такие как неявные операции стека и недекларированные сигнатуры. Этот декомпилятор, многомесячный проект, дал ценные внутренние аналитические фреймворки и промежуточное представление для статического анализа. Используя это промежуточное представление, команда создала движок абстрактной интерпретации для статического анализа, реализуя проходы для проверки значений, предоставленных проверяющим, обеспечения соблюдения типовых ограничений и обеспечения локальной инициализации переменных. Это привело к обнаружению более 400 потенциальных улучшений проверки типов и высокосерьёзной ошибки: недоограниченного значения советов в процедуре mod_12289. Эта уязвимость позволила злоумышленнику манипулировать остатками, потенциально подделывая подписи Falcon и опустошая аккаунты Miden. Помимо поиска ошибок, агенты изучали формальную верификацию с помощью Lean, моделируя исполнитель виртуальной машины Miden и автоматически переводя процедуры MASM в Lean. Это формальное моделирование, управляемое агентом, привело к получению 95 доказательств корректности для бинарных арифметических компонентов, выяв две тонкие ошибки, упущенные существующими юнит-тестами: крайний случай в 64-битном правом вращении (rotr) и проблему в 256-битном умножении (wrapping_mul). Эти продвинутые инструменты и формальное моделирование, сделанные возможными благодаря недавним достижениям в AI-агентах, значительно повысили глубину и качество проверки безопасности — уровень подготовки, ранее недостижимый из-за ограничений по времени и ресурсам.