Ребёнок собирает в Scratch простую игру: персонаж появляется в центре и мгновенно перепрыгивает в угол. Первое перемещение пропадает между кадрами — его никто не видит. Убрать такую команду безопасно. Но как автоматический оптимизатор узнает об этом? Сегодня в репозитории Scratch десятки миллионов проектов, написанных юными авторами. Ошибка улучшателя способна незаметно исказить их замысел.

Решение напоминает таможенный досмотр. Непроверенный оптимизатор сканирует проект, строит граф зависимостей и предлагает удалить, скажем, неиспользуемый костюм или мёртвую команду. К правке прилагается «сертификат» — цифровая декларация с указанием типа изменения и условий безопасности. Доверенный инспектор-контролёр, не веря ни единому слову, заново разбирает обе версии программы. Он пересчитывает все условия. Линза наблюдения (набор событий, видимых игроку) служит главным ориентиром: если запись в ресурс перезаписывается до того, как её можно наблюдать, её можно удалить. Это центральная теорема о кооперативном фрейме, доказанная в Lean. Никакой хитрости сертификат не скроет.

Эксперимент на 300 реальных проектах показал: хотя бы одно безопасное улучшение получили 283 проекта, то есть 94,3%. В основном чистили неиспользуемые ресурсы, но в 17 случаях убрали и семантически мёртвые записи. Самое важное — состязательная атака из 4278 правок с намеренно вплетёнными ошибками не прорвалась ни разу. Контролёр отверг все опасные варианты. Дифференциальный оракул, сравнивший поведение исходной и оптимизированной программ на виртуальной машине, не зафиксировал ни одного расхождения.

Впервые для параллельного событийно-ориентированного языка построена система, где каждое изменение несёт проверяемый сертификат. Это переносит дисциплину верифицированных компиляторов в мир, где цена ошибки особенно высока. Теорема о кооперативном фрейме параметризована типом ресурса и линзой наблюдения — одно доказательство покрывает целый класс оптимизаций. Она обеспечивает информационную полноту условий корректности, отсекая любые неожиданные каналы наблюдения. Доверенный базис компактен: 9 921 строка на Python и 5 909 строк доказательств в Lean — объём, посильный для аудита небольшой командой. При этом подход не нуждается в вероятностных предположениях или байесовском выводе: он даёт абсолютные гарантии. Программу можно рассматривать как динамическую систему, а её проверку — как детерминированный анализ, а не стохастический процесс.

Таможня для кода уже работает. В будущем она сможет проверять правки, предложенные искусственным интеллектом, и станет основой для доверенных AI-ассистентов. А пока инспектор готов к труду: когда ребёнок нажмёт «запустить», его замысел останется нетронутым.