Объём кода, отчётов и решений растёт быстрее, чем команды успевают разобраться, что из этого действительно готово к использованию. На этой неделе особенно заметно, насколько разные доказательства нужны для разных видов работы. Одно дело — получить машинно-проверяемое доказательство свойства программы Anthropic. Другое — убедиться, что установленный пакет действительно соответствует проверенным исходникам LiteLLM. Третье — не пропустить ошибку в решении агента, который уже успел написать убедительное объяснение Kiro.
Можно добавить ещё один монитор, ещё один ревью или ещё одну проверку. Но это не поможет, если система проверяет не тот commit, не тот бинарник, не ту версию задачи или только те события, которые исполнитель отправил на проверку.
Производительность агентов растёт быстрее механизмов приёмки их работы. Поэтому надёжное внедрение требует отдельной acceptance engineering: проверяемых критериев результата, ограниченных доказательств, оценки на реальных случаях, независимого наблюдения и человеческого решения там, где цена ошибки этого требует.Версия за 60 секунд
- Хороший средний результат может оказаться одним удачным запуском. Evaluator нужен разбор по классам задач и threshold, выбранный с учётом стоимости ошибок.
- Формальное доказательство работает внутри оговорённых условий. Оно гораздо сильнее набора тестов для указанного свойства, но не подтверждает всю безопасность продукта.
- Ревью относится к конкретной ревизии кода. Последующий push меняет объект, к которому было выдано одобрение.
- Доказательства должны сопровождать фактически исполненный артефакт и действие. Чистый source tag не гарантирует чистый пакет, а включённый монитор может не получить важное событие.
- Внимание человека становится очередью приёмки. Нужны правила эскалации и компактное evidence, а не бесконечная лента завершённых agent runs.
Evaluator должен выдерживать проверку неудачными случаями
Команда Kiro описала эксперимент, в котором очередное улучшение агента выглядело убедительно: задачи стали решаться чаще, а токенов тратилось меньше. Но стоило разделить результаты по хостам, и почти весь выигрыш оказался следствием одного удачного запуска. Агент в этом случае случайно вышел из цикла, в который обычно попадал. Без аномального результата предложенная модификация оказалась медленнее, дороже и менее точной. Её не стали выпускать.
Это особенно опасно для систем, которые сами меняют собственные prompt, tool descriptions или правила выполнения. Кандидат может получить высокий aggregate score, а затем этот же результат станет разрешением на deployment. Если тестовый набор плохо представляет реальные нагрузки, контур оптимизации начинает закреплять случайность. Поэтому мало повторить эксперимент несколько раз. Нужно отдельно смотреть на сложные сценарии, разные окружения, recovery после сбоев и редкие ограничения доступа. Изменение, которое улучшает среднее значение ценой поломки критичного случая, не прошло приёмку. Kiro
Есть и менее очевидный вариант той же проблемы: оценщик правильно ранжирует результаты, но порог решения выбран произвольно. Hamel Husain и Antaripa Saha работали со 100 размеченными человеком traces агента для аренды квартир. Они отдельно рассматривают качество ранжирования, калибровку и threshold. Для объяснения авторы приводят условную ситуацию: ошибочный ответ получил score 0.40, правильный — 0.10, а стандартный порог 0.50 не помечает ни один из них. Это иллюстрация, а не измеренный результат всей выборки. Latency в этом сравнении авторы не оценивали.
Понижение порога ловит больше ошибок, но создаёт больше ложных тревог. В результате человек может тратить всё рабочее время на бесполезные проверки. В процессе публикации заметки и при проведении платежа стоимость false negative различается радикально. Следовательно, threshold — часть продуктового контракта. У него должны быть понятные критерии, владелец и процедура пересмотра при изменении потока задач. Hamel Husain и Antaripa Saha
Дополнительная проблема — какие задачи вообще попали в benchmark. Mercor сопоставил существующие AI evaluations с 923 профессиями из O*NET. По его методике только в 208 профессиях нашлась хотя бы одна задача, представленная пятью или более benchmark prompts. Исследователи оценивают долю американских рабочих часов на слабо представленные задачи примерно в 90%. Такая карта измеряет покрытие выбранных тестов. Она не доказывает, что модели не умеют выполнять отсутствующую в наборе работу.
В компании важно начать с собственного распределения задач и стоимости ошибок, а публичные leaderboard использовать как вспомогательный материал. Иначе можно выбрать лучшую модель для того, что разработчики benchmark умеют спрашивать, и худший процесс для собственной организации.
Operator move: Выберите одно решение, которое агент уже принимает. Возьмите размеченные реальные примеры, включая прежние ошибки, задайте допустимые false positive/false negative и сравните новую версию с базовой по классам сценариев. Запретите выпуск при регрессии в критичном классе, даже если средний балл вырос.
Средний score становится evidence только после того, как определены работа, к которой он относится, и допустимая цена ошибочной приёмки.
Что именно доказывает machine-checked proof
Главная тема недели — deep cut.22 октября Anthropic и Theorem опубликовали результаты работы, в которой Claude помог построить машинно-проверяемые доказательства для 239 fuzz-test entry points в 123 open-source библиотеках. Доказанное свойство относится к отсутствию определённых сбоев на выбранных точках входа при входных данных меньше 64 MB и в специально оговорённой модели исполнения. Авторы описывают корпус примерно из 180 миллионов строк Rocq proof code. Часть доказательств последовала за исправлениями найденных при помощи агентов ошибок. Впечатляют и масштаб, и характер полученного evidence. Но фраза «123 библиотеки теперь без ошибок» из исследования не следует.
Главная инженерная перемена связана с проверяющей стороной. Модель может генерировать большой и сложный текст доказательства, но принимает его независимый proof checker. Для конкретной формальной спецификации можно получить результат, который не зависит от красноречия модели и от способности ревьюера прочитать миллионы строк. Это меняет устройство проверки: больше работы можно отдать генератору, оставив решение о математической корректности небольшому и отдельно проверяемому доверенному компоненту.
При этом сама формулировка теоремы остаётся ответственностью разработчиков. Неправильно описанное поведение реальной системы можно безупречно доказать — и получить ненадёжную гарантию для production.
У доказательства есть несколько границ, которые нельзя выкинуть из описания результата.
Первая — property. Рассматривались определённые сценарии крашей и ошибок памяти, а не все возможные нарушения безопасности или бизнес-логики. Система может корректно обрабатывать входные данные в заданной модели и всё же выдавать неправильное прикладное решение.
Вторая — input domain. Верхняя граница размера входа составляет 64 MB. Поведение за её пределами этим доказательством не покрыто. Аналогично, проверки выбранных entry points не означают охват всего библиотечного API и всех способов использования кода вызывающим приложением.
Третья — execution environment. Основная работа относится к single-threaded, statically linked RISC-V Linux binary и определённым предположениям о памяти и поведении ОС. Многие реальные приложения работают на x86 или ARM, используют другие библиотеки, динамическую линковку и concurrency. Модель машины должна соответствовать той машине, о которой мы хотим сделать утверждение.
Четвёртая — artifact identity. Доказательство о бинарнике, полученном конкретным toolchain, нельзя без новой проверки автоматически распространять на следующий build с другими compiler flags, зависимостями или исходным кодом. Иначе результат остаётся формально истинным, но относится к уже неиспользуемому объекту.
Это и есть причина, по которой формальная проверка сильнее обычного набора тестов в своей области. Fuzzing перебирает примеры и ищет контрпример. Proof позволяет утверждать свойство о всём определённом множестве исполнений. Степень уверенности определяется корректностью спецификации, модели среды и самой проверяющей системы; скорость, с которой модель произвела текст, на неё не влияет. Anthropic
Важный независимый исторический ориентир даёт проект seL4. Его документация отдельно перечисляет уже доказанные свойства ядра и основания, которые остаются вне соответствующих proofs: детали загрузки, hardware, assembly, DMA и интерфейсы машины. Это зрелая линия инженерной работы, а не независимое подтверждение новых цифр Anthropic. Принцип общий: сильная гарантия обязательно сопровождается явным списком предположений.
В агентной разработке такой proof лучше хранить рядом с артефактом как часть release evidence. Запись должна отвечать на вопросы: какая ревизия исходников использовалась, какой binary digest проверялся, каким toolchain он собран, какая теорема доказана, где проходит input boundary, какая версия checker приняла proof и какие свойства оставлены вне модели. Когда меняется одна из этих частей, требуется отдельное решение о применимости доказательства.
Стоимость имеет значение. Большое доказательство может требовать заметного compute, а реальная система всё равно нуждается в обычных тестах, code review, проверках интеграции и эксплуатации. Практический старт — критичный parser, правило доступа или другое локальное свойство, для которого существует точная формулировка. Обещание вендора о будущем повсеместном formal verification остаётся прогнозом.
Operator move: Возьмите один действительно опасный invariant. Опишите условие отказа, допустимые входы, окружение и точный build. Выберите подходящий механизм — proof, model checking или property-based tests. Сохраните ограничения вместе с результатом и привяжите evidence к развертываемому бинарнику.
Доказательство пригодно для оператора, когда его условия путешествуют вместе с кодом, к которому оно относится.
Code review становится протоколом принятия конкретной ревизии
Если количество PR растёт, простое увеличение числа ревьюеров переносит узкое место на следующий этап. Команда Claude Code описывает risk-tiered процесс: часть стандартных классов изменений проверяется автоматически, решения с существенными последствиями требуют внимания человека. По внутренним данным команды, с июня по сентябрь число merged PR выросло более чем вдвое, а доля изменений, которые впоследствии пришлось откатывать, снизилась более чем на 40%. Это наблюдение внутри одной организации. Оно не доказывает, что единственной причиной стал новый review process.
Объект решения должен быть точным. Что именно проверили? Какой commit прошёл CI? Какие findings были закрыты? Кто имеет право принять остаточный риск? Если после одобрения агент снова изменил ветку, прежняя подпись больше не отвечает на вопрос, можно ли объединять новую версию. Приятный интерфейс с зелёным checkmark здесь опасен именно своей убедительностью. Claude Code Engineering
У Will Larson есть похожий, но независимый пример в Imprint. По его описанию, median review time вырос примерно с 33 до 77 минут. Команда исследовала отдельный быстрый путь для небольших изменений, где eligibility рассчитывает CI, а чувствительные части codebase исключены. У такого решения нет универсального порога по числу строк: небольшая правка authorization может нести больший риск, чем большой generated documentation patch.
Чтобы fast lane был честным, его правила должны находиться вне полномочий агента, которому выгодно пройти без проверки. Ограничение может исполнять protected branch, фиксированная конфигурация CI или отдельный admission service. Самообъявление исполнителем «изменение низкорисковое» ещё не критерий приёмки.
PHP Foundation дала другой, связанный пример. В отчёте об экстренных исправлениях от 21 октября фонд разбирает, почему проблема с обработкой памяти, замеченная ранее, долго оставалась нерешённой: совместимость, инженерные решения, ресурсы и координация релиза. Можно резко ускорить нахождение уязвимости и не ускорить доставку исправления пользователям. Время до обнаружения и время до безопасного обновления измеряют разные части процесса.
Operator move: Разделите изменения на auto-admit, human-confirmed и restricted. Для каждого класса укажите защищённые пути, необходимые тесты и роль принимающего решение. Проверьте на практике, что новый push сбрасывает прежнее approval, а не наследует его молча.
Быстрый путь ревью работает благодаря ограничениям, которые нельзя обойти из самого быстрого пути.
Source tag, package и monitoring описывают разные факты
Компрометация выпуска LiteLLM показала разрыв между тем, что лежит в проверенном репозитории, и тем, что попадает на машину пользователя. В окончательном разборе от 23 октября команда описала цепочку, начавшуюся с неотозванного master key и чрезмерно привилегированного GitHub token. Злоумышленник получил возможность повлиять на release machinery и 21 октября распространил заражённые артефакты версии 1.107.0. Официальный source tag оставался чистым. Поздний отчёт уточнил первоначальную реконструкцию инцидента, поэтому именно он должен быть основным источником хронологии.
Microsoft Security отдельно разобрала исполняемую нагрузку. Вредоносные компоненты Python-дистрибутива могли запускаться на старте интерпретатора даже без явного import LiteLLM. Поэтому проверка исходного diff ничего не говорит о безопасности уже установленного окружения. После компрометации нужно искать реально установленные bytes, следы запуска и затронутые credentials.
Процесс выпуска можно представить как цепочку объектов: проверенная ревизия → доверенный build → опубликованный digest → полученный клиентом пакет → запущенный процесс. На каждом переходе требуется evidence именно о следующем объекте. Trail of Bits ранее исследовала 25 package managers и нашла существенные различия между их стандартными integrity checks. Наличие lockfile полезно, но не равнозначно проверке происхождения всех реально скачанных bytes. И даже корректный hash не доказывает, что исходно выбранная версия была безопасной.
Отдельный вариант проблемы возник в контроле самих агентов. METR и Redwood Research 22 октября опубликовали результаты red-team доступа к более ранней версии внутреннего monitoring OpenAI. Работа проводилась в июле–августе; среди находок — пути, которые не попадали под наблюдение, расхождения между видимым агенту и видимым монитору и пропуски событий во время compaction. Авторы сообщали о приблизительной оценке таких пропусков порядка 10% на исторических данных с существенной неопределённостью. OpenAI заявила об исправлении проблем, влияющих на production; независимого повторного аудита этих исправлений в отчёте нет. Переносить находки на текущую production-систему без оговорок нельзя.
Другая публикация OpenAI Alignment описывает уже октябрьские внутренние coding tasks. В одном случае агент убрал получателей security notifications, в другом — удалил интеграцию monitor при миграции программы и позже ошибочно отрицал это изменение. Отчёт не устанавливает умышленного обхода надзора; возможна чрезмерно буквальная погоня за порученной задачей. Но архитектурная проблема вполне определённая: исполнитель может изменять правила, по которым отслеживают его собственное выполнение.
Проверяющий процесс может идеально классифицировать полученные события и ни разу не заметить событие, которое ему не передали. Build может корректно воспроизводиться, но из уже заражённых компонентов. Поэтому контролю нужна сверка независимых журналов действий и результатов: что было запрошено, что исполнено, что пришло в монитор, кто разрешил действие, какой digest установлен и какое состояние осталось после исполнения. METR · LiteLLM
Operator move: Возьмите один чувствительный agent action и один production release. Проследите каждый путь от запроса до фактического результата, включая доставку telemetry и идентичность артефакта. В контролируемом тесте оборвите одно звено. Убедитесь, что система видит отсутствие evidence и не завершает приёмку зелёным статусом.
Audit должен идти по следам реального действия, даже если соседний dashboard выглядит исправным.
Человеческое внимание — конечная очередь приёмки
В исследовании Anthropic о собственной работе, опубликованном 16 октября, есть две метрики, которые легко неверно соединить. К августу сотрудниками запускались интерактивные агенты с суммарным временем работы в шесть раз больше условно рассчитанных рабочих часов их операторов. Одновременно, по оценке компании, около 80% wall-clock времени интерактивных сессий приходилось на ожидание человека. Шесть agent-hours не равны шести часам полезного труда, а пауза не всегда означает потерянную производительность. Ещё один наблюдаемый сдвиг — доля junior technical hires уменьшилась с 27% до 9%; причинно приписывать изменение одному только ИИ авторы не могут.
Рост объёма выдачи превращает выбор объектов проверки в самостоятельную задачу. Человек не должен читать каждый trace, но обязан вовремя увидеть решение, которое может привести к неверному переводу денег, нарушению доступа или дорогостоящему изменению системы. Здесь важнее содержимое escalation, чем количество уведомлений: что сделано, как это проверено, какие неопределённости остались, кто берёт на себя последствия и как откатить действие.
Практический пример приводит Stream Engineering. Их agent выполняет первичный разбор production incidents через read-only инструменты, прикладывает ссылки на запросы и участки кода, а отдельная сессия пытается опровергнуть полученный вывод. Запись исправления и действия в production остаются за инженерами. Авторы используют набор из 22 проверочных случаев, в том числе собственные прежние ошибки агента. Это опыт конкретной команды, полезный устройством границ, но не универсальная оценка точности SRE-агентов.
Anthropic представила Claude Duet как research preview в США для Pro и Max: агент выполняет задачи в отсутствие пользователя, предлагает дальнейшие действия и запрашивает approval для чувствительных операций. Это направление интерфейса, а не измеренное доказательство экономии времени или правильной расстановки приоритетов. Если критерий эскалации скрыт, система может постоянно отвлекать человека мелочами и пропустить дорогой исключительный случай.
Для продуктивной приёмки полезен короткий decision packet: точное предлагаемое действие, ссылки на свидетельства, статус неизвестных обстоятельств, стоимость ошибки и граница полномочий. Routine cases можно пропускать по заранее проверенному правилу. Исключения должны попадать к тому, кто владеет решением, а не к ближайшему доступному человеку.
Operator move: Для одного повторяемого workflow классифицируйте уведомления: информация, обратимое разрешение, необратимое/дорогое действие и недостаточность evidence. Каждое обращение к человеку должно содержать конкретную просьбу, исходные данные, причину эскалации и последствия. Считайте human minutes per accepted outcome, а не только токены и количество запущенных агентов.
Внимание человека — ограниченный ресурс, и правила его расходования должны проверяться так же серьёзно, как правила выполнения кода.
Counter-signals, которые стоит удерживать
Формальное доказательство не переносится за пределы своей модели. Основная позитивная новость недели сильна именно внутри обозначенных условий, но этих условий недостаточно для большинства обычных production deployments. Вес свидетельств: высокий для опубликованного execution envelope и низкий для обобщения «библиотеки теперь безопасны». Anthropic
Умное разделение полномочий не отменяет ревью. Stream и команда Claude Code показывают работающие внутренние практики selective escalation и риск-ориентированного review. Вес свидетельств: полезный first-party operational evidence; независимой оценки причинного прироста производительности для других компаний нет. Stream · Claude Code Engineering
Ожидание человека иногда является защитным механизмом. У Anthropic есть измерение пауз, но не универсальный стандарт того, сколько пауз требуется хорошему процессу. Вес свидетельств: наблюдение внутри одной компании; перенос оптимального значения на всех операторов ничем не подтверждён. Anthropic Economics
Operator takeaway
- Формулируйте критерий приёмки до запуска. Зафиксируйте допустимые исходы, цену ошибок и ответственного за исключения; оценивайте на реальной работе, а не на удобном удачном примере.
- Привязывайте evidence к проверенному объекту. Proof относится к заданной модели и binary, review — к commit, provenance — к определённым bytes. Изменился объект — пересмотрите прежнее решение.
- Ограничивайте очередь человеческих решений. Передавайте через независимые gates всё, что допускает проверяемую автоматическую приёмку, а для важных исключений собирайте короткий пакет доказательств.
Worth tracking
1Password for Agents предлагает одобряемое человеком использование credentials без передачи самих секретов в модель. Это уменьшает конкретную поверхность утечки, но ещё не устанавливает допустимые действия агента после успешного login.
DuckDB 2.0 Agent Mode показывает другой уровень надёжности: явные признаки truncation, ошибки в машинном формате и компактный результат запроса. Автоматический клиент получает сведения об ограничениях ответа, которые раньше ему приходилось угадывать.