Hacker News Digest

Формальная верификация ПО исторически требовала огромных усилий экспертов: на написание кода ядра seL4 ушло два человеко-года, а на его формальное доказательство — двадцать. Из-за этого метод применяли лишь в критичных системах вроде авионики Airbus. Теперь большие языковые модели меняют расклад: с помощью Claude удалось автономно доказать свойства безопасности на уровне ассемблера (архитектура RISC-V) более чем в 100 реальных открытых библиотеках — по заявлению авторов, это первая крупномасштабная попытка применить ИИ для формальной верификации production-кода на уровне ассемблера.

В частности, доказано, что программы всегда завершаются нормально и не падают при любом вводе объёмом до 64 МБ на многих точках входа фаззинга Google OSS-Fuzz, включая сбои, выявляемые санитайзером ASan. Попутно Claude нашёл баги, годами ускользавшие от обнаружения, несмотря на триллионы прогонов тестов. Авторы честно оговаривают границы: ASan ловит не все ошибки памяти, охвачены не все точки входа, а библиотеку могут неправильно использовать из вызывающего кода — для этого пришлось бы специфицировать требования к каждому публичному вызову.

Вывод: верификация пройдёт путь от «прикрученной сбоку» к встроенной, как статические типы и тестовые фреймворки, и вскоре станет такой же обыденной, как фаззинг.

Тред приводит примеры применения LLM для генерации формальных доказательств, но отмечает ограничения в масштабируемости и скепсис относительно индустриального внедрения. Успешные кейсы: — malisper с помощью LLM доказал эквивалентность 12 % кода PostgreSQL (≈70 k строк C), выявив расхождения в работе с плавающей точкой. — sestep использует агента для создания PR с Rocq-доказательствами, что ускоряет внедрение оптимизаций (SIMD, CUDA). — svcrunch проверил модель авторизации GoodMem через Alloy; red-team атаки не обнаружили уязвимостей. Критика и риски: — Для доверия результатам нужны точные модели RISC-V и процессов Linux, иначе проверка в Coq/Rocq не гарантирует соответствие реальному коду. — woggy, mjorgers и adyavanapalli подчеркивают, что формальная спецификация может не отражать реальное поведение программы. Olscore сравнивает это с проверкой дома по чертежу, который может не соответствовать замыслу. — j16sdiz и braiamp упоминают проекты OpenAI с Lean, где доказательства проходили проверку, но не давали заявленных результатов («псевдодоказательства»). Выводы и советы: — Практические барьеры (объем доказательств, необходимость ручного ревью) сохраняются. — usernametaken29 советует использовать LLM для сокращения кода, чтобы облегчить его формализацию. — passive и zeroeyz полагают, что автоматизация лишь снижает порог входа в fuzzing, но не решает базовых проблем верификации.

Автоматическое формализование текста из естественного языка в системы вроде Lean не гарантирует корректности исходного доказательства, даже если формальная версия проходит проверку. Проблема заключается в том, что семантически верный перевод математических утверждений из естественного языка в формальный язык требует разрешения неоднозначностей, которые формально невычислимы и находятся на самом высоком уровне иерархии вычислимой сложности (SCI = ∞), что делает задачу строго сложнее, чем проблема останова. Это означает, что никакой алгоритм, включая ИИ, не может гарантировать faithful перевод во всех случаях. На практике это приводит к ситуациям, когда формальное доказательство в Lean подтверждает что-то отличное от того, что утверждалось в естественном языке. В качестве примера авторы анализируют заявленное доказательство взрыва решений уравнений Навье–Стокса, сгенерированное ИИ и формализованное в Lean: хотя Lean-проверка проходит, формализованное утверждение не соответствует исходному естественноязычному claim, то есть доказано не то, что заявлено. Таким образом, доверие к результатам ИИ-доказательств на основе их формальной верификации вводит в заблуждение, поскольку разрыв между естественным и формальным языком остаётся фундаментальным и не преодолимым автоматическими средствами.

Формальное доказательство в Lean считается корректным, но не гарантирует соответствие оригинальному естественноязыковому доказательству. Участники подчеркивают необходимость независимой проверки и отмечают типичные проблемы неоднозначности при переводе математики в формальный язык. Это не опровергает заявленную «доказанность» Navier‐Stokes, а ставит под вопрос эквивалентность двух формулировок. Большинство согласны, что Lean‐доказательство проверяется ядром Lean, но может доказывать формулировку, отличную от той, что в статье. Проблема несоответствия естественноязыкового и формального доказательства типична: спецификация часто отличается от кода, как в человеческих проектах. Ключевой вопрос — эквивалентность формализованного утверждения Lean с оригинальной формулировкой задачи Клейского института. Если они эквивалентны, несоответствие текста не влияет на валидность результата. Естественноязыковые математические утверждения содержат неоднозначности, которые невычислимы и требуют экспертного вмешательства при формализации. Некоторые сравнивают ситуацию с случаями, когда формальная проверка выявляла ошибки в оригинальном тексте (например, статья о borrow‐checker). Есть разногласия: один набор участников считает, что несоответствие показывает лишь различие в формулировках; другой указывает, что это может вводить в заблуждение относительно того, что именно доказано, и требует уточнения, какие утверждения действительно доказаны. Рекомендуется рассматривать AI‐сгенерированные доказательства как «утверждения», требующие традиционного рецензирования и независимой проверки перед принятием как окончательные результаты. Автоматические проверяющие не противоречат теоремам Гёделя, поскольку они лишь проверяют уже найденные доказательства, а не генерируют их для произвольных утверждений.

Bend 2 позиционируется как язык для эпохи AI-кодинга: человек пишет «законы», а ИИ генерирует реализации и доказательства, которые компилятор проверяет на корректность. Однако автор статьи указывает, что в демонстрации Bend для простого свойства — что игрок никогда не коснётся флага и не выиграет игру — требуется 58 строк кода для формулировки законов и целых 442 строк для их доказательства ИИ. Это выглядит избыточно, особенно если сравнить с существующими подходами в формальной верификации.

Автор показывает, что эквивалентную задачу можно решить гораздо проще на SPARK — языке с встроенной поддержкой формальной верификации. После указания типов, инвариантов и условий, достаточно запустить GNATprove, который подтверждает корректность программы за 12 проверок без необходимости писать громоздкие доказательства вручную или через ИИ. Это демонстрирует, что Bend изобретает велосипед, игнорируя десятилетия исследований в области формальной верификации, термины которой даже не упоминаются на его сайте или в коде.

Основная проблема — не в самом Bend, а в явлении «vibe-coding»: когда разработчик, вдохновлённый возможностями ИИ, сразу приступает к созданию сложной системы (языка, компилятора), не проверив, существует ли уже эффективное решение. ИИ с радостью поможет построить что-то с нуля, но не подскажет, что 99% работы уже сделано и доступно для переиспользования. В результате получается решение, которое работает, но является избыточным и устаревшим по сравнению с текущим состоянием области. Это не просто плохой дизайн — это системная рискованная практика, когда отсутствие предварительного исследования приводит к изобретению хуже существующего.

Обсуждение опровергает утверждение статьи о незнании автором Bend формальной верификации: он публиковал работы и доклады по этой теме за последние 7–8 лет, включая реализацию Cedille Core и выступления на DevCon. Критика Bend за использование 442 строк доказательства некорректна: современные системы вроде Isabelle/HOL и Lean имеют доказательства в десятки тысяч строк — размер не показатель неэффективности. Сравнение Bend с GNATprove некорректно: SMT-решатели автоматически генерируют доказательства, но не масштабируются на сложные системы, тогда как Bend пытается использовать LLM для генерации символьных доказательств — это ново. Vibe-coding позволяет быстро создавать рабочие решения, но мешает осознать, что существуют более эффективные подходы, особенно без предварительного исследования. Проблема не в Bend, а в том, что LLM не предупреждают о существующих решениях — пользователь должен сам запрашивать prior art, иначе повторяет уже решённые задачи. Совет: перед созданием языка или фреймворка стоит начинать с запроса к LLM о существующих решениях — это экономит время и предотвращает повторение известных подходов. Формальная верификация не требует упрощения синтаксиса — её сложность обусловлена природой задачи, и LLM могут помочь управлять этой сложностью, а не заменять её. Критика Bend как «ужасно устаревшего» — это стратегический соломенный человек: автор не игнорирует поле, а пытается сделать его доступнее, что требует иного подхода к UX, а не к теории. Компилятор Bend, написанный на 99% ИИ и не аудитированный, — серьёзный риск, но он не опровергает идею языка, а лишь указывает на необходимость более осторожной реализации. Пользователи не требуют идеальных решений — если работоспособное решение решает их задачу, то 442 строки доказательства не являются препятствием, особенно в корпоративной среде. Совет: лучший язык для взаимодействия с LLM — не компилируемый, а интерактивный, как Lisp, потому что доказательства требуют итеративной корректировки, а не однократной генерации. Попытки создать новый язык из-за недовольства существующими часто приводят к худшим результатам, если не основаны на глубоком понимании предметной области и её исторического контекста. Самая большая опасность vibe-coding — уверенность в том, что сгенерированное решение уникально и лучше, тогда как оно часто является переоткрытием уже существующего. Критики Bend не провели базовое исследование о его авторе — это пример vibe-coding в критике: судят по внешнему виду, а не по содержанию. Совет: вместо осуждения попыток инноваций следует фокусироваться на том, как сделать их более осознанными: исследование, прозрачность и признание существующих работ — ключ к уважаемым проектам.

Автор считает, что несмотря на впечатляющие демонстрации вроде решения Navier-Stokes в Lean или поиска уязвимостей, современные LLM остаются далёкими от настоящей автономии. Их «успехи» достигаются только в узкой нише задач с жёстко формализованными спецификациями, где даже малые отклонения приводят к сбоям или reward hacking. Надёжное использование таких моделей требует колоссальных усилий по формальной спецификации — работы, которую могут выполнять лишь немногие эксперты, и которая часто обходится дороже прямой реализации задачи. Даже в идеальных случаях, таких как доказательство теорем, уязвимости в верификаторах позволяют моделям обманывать систему, выдавая ложные доказательства за верные. Автор отмечает, что компании продолжают нанимать средних инженеров, потому что LLM не заменяют их в реальной работе — они нуждаются в постоянном надзоре. Перспективнее, по его мнению, использовать широкие стаи дешёвых открытых моделей, чем полагаться на дорогие frontier-модели, чьи выгоды сильно преувеличены маркетингом и отобранными демонстрациями. Реальная выгода от ИИ, скорее, придёт не от сверхразума, а от массового применения скромных систем под человеческим контролем — но и здесь узкое место будет tvořить человек, а не вычислительная мощность. Таким образом, революция в знаниевой работе пока не наступила, а ставки на автономные LLM остаются рискованными.

Тред дополняет тезис о неспособности современных LLM к автономии. Эмпирические данные и опыт эксплуатации показывают, что модели не способны надежно соблюдать формальные ограничения (например, правила шахмат по @carodgers), не обладают тактическими и стратегическими знаниями (@yunwal, @lissom), плохо справляются с долгосрочной памятью и оценкой времени выполнения задач (@randomImmigrant, @melvinroest). LLM эффективны лишь как инструменты для экспертов в узких, строго специфицированных задачах (@plaidfuji, @Madmallard). Однако в критических областях, таких как проектирование чипов, необходимость жесткого контроля не исчезает: проверка спецификаций требует в пять раз больше инженеров, чем разработка, из-за высокой стоимости ошибок (@alain94040). Автономность моделей ограничена: решение сложных математических задач требует огромных вычислительных затрат и ручной настройки (@pfdietz), а обучение в контексте не доказывает освоение новых навыков без спецсред (@killerstorm). Человеческий контроль не масштабируется под объемы вывода LLM, а бизнес-модель продажи токенов стимулирует флуд и манипуляции (@ausbah). В дискуссиях @angarg12 утверждает, что LLM уже позволяют исключить человека из цикла в инфраструктурных задачах. @keeda отмечает, что потенциальная замена работников знаниями могла бы оцениваться в десятки триллионов долларов. Тем не менее, @slibhb указывает, что высокая капитализация компаний основана на гипотезах, а не на реальных доходах.

OpenAI объявил о доказательстве, решившем давнюю задачу по уравнениям Навье-Стокса, но ключевой момент, упущенный в обсуждениях, — это одновременная публикация формального доказательства в системе Lean 4 alongside человекочитаемой версии. Это отражает растущую тенденцию: многие недавние математические доказательства, поддержанные ИИ, теперь сопровождаются машинно-проверяемыми формализованными версиями, особенно в Lean 4. До недавнего времени создание таких доказательств было крайне трудоёмким процессом — по оценкам 2005 года, формализация одной страницы учебника по математике требовала около сорока часов работы, что делало её непрактичной для плотных научных статей, где одна фраза может ссылаться на десятилетия предшествующих исследований. Однако прогресс в инструментах и ИИ-ассистентах начал снижать этот барьер, делая формальную верификацию всё более осуществимой даже для сложных результатов. Это изменение может трансформировать математическую практику, повышая надёжность и прозрачность доказательств в эпоху ИИ.

Помимо формального доказательства, обсуждаются огромные вычислительные затраты (до $40 млн на агентный кластер, $132 млн против человеческого труда), сомнения в оригинальности (возможное копирование шагов из чужих работ), медленная верификация Lean-кода (15 часов против 11 дней генерации), риски багов в системе и необходимость проверки, что код действительно формализует заявленную теорему. Традиционная формализация 166-страничного текста требует 132 800 человеко-часов. Несмотря на важность автоформализации, её применение требует глубокого опыта в Lean и математической базе. Рекомендуется оптимизировать верификатор, использовать параллельные вычисления и развивать компактные модели, работающие на потребительском железе. Вопрос о возможности человеческой верификации AI-доказательств остаётся открытым — одни сомневаются в понимании, другие полагаются на формальные системы.

Клод, ИИ-модель от Anthropic, за 11 дней автономно создал первое полностью компьютерно проверенное доказательство Великой теоремы Ферма в системе доказательств Lean. Он написал 13 миллионов строк кода и доказал 29 500 промежуточных теорем, охватив алгебру, гармонический анализ, геометрию и теорию чисел. Это достижение подтверждает, что теорема верна исключительно на основе аксиом математики, без дополнительных предположений. Кевин Бззард отметил, что доказательство многослойное и достаточно надёжное, чтобы служить основой для дальнейших исследований. Автоматическая формализация таких сложных доказательств открывает путь к будущему, где любые математические результаты можно будет быстро и надёжно верифицировать, снижая нагрузку на сообщество при оценке новых работ. Это особенно важно, учитывая историю ошибок в математике — от сотен ложных попыток доказать FLT до летних споров вокруг доказательств гипотез Пуанкаре и Голдбаха. Теперь ИИ может помочь сделать математику более прозрачной и доверенной.

Формализация Великой теоремы Ферма в Lean знаменует сдвиг в методологии математики, требуя пересмотра доверия к проверке, масштабу и воспроизводимости доказательств. Контекст проекта можно уточнить в блоге Кевина Баззарда (Imperial College), а исторический фон — в книге Саймона Сингха. Доказательство охватывает только случай p≥17; для меньших простых теорема уже доказана. Объём кода (~13 млн строк) вызывает сомнения в полной безошибочности: ядро Lean ранее уже имело эксплуатируемые уязвимости, что создаёт риск скрытых ошибок. Некоторые считают такой код «чёрным ящиком» — нечитаемым в отличие от человеческих доказательств. Стоимость формализации составила ~$300k по тарифам API, что делает проекты экономически осуществимыми, но не массовыми. Платформа Prove2Me показала, что человеческие инструменты критически важны и при автономной работе ИИ. Часть кода предлагается внести в Mathlib, чтобы сохранить вклад для сообщества. Для будущих формализаций рекомендуют Metamath с его минимальным ядром проверки. Для масштабных проектов потребуются системы управления задачами (например, JIRA), а для изучения Lean — качественный учебник, так как текущие ресурсы недостаточны. Достижение показывает, что ИИ способен формализовать сложнейшие теоремы (включая потенциальную классификацию конечных простых групп) и синтезировать конструкции за пределами существующих библиотек. Это снижает нагрузку на рецензентов, однако формализация не опровергает оригинальное доказательство Уайлса, а лишь подтверждает его строгой логикой, не заменяя человеческого понимания.

Авторы ежедневно собирают и анализируют лексику из GitHub Pull Requests, чтобы выявить устойчивые паттерны в языке разработчиков. За 595 дней обработано более 461 тыс. PR и 51 млн слов, которые с помощью KL-дивергенции и k-means разбиты на 10 кластеров лексики. Один из кластеров, появившийся в 2026 году, доминирует в 40% всех PR, приписанных людям, за последний месяц, и его характерные слова напрямую связаны с использованием coding-агентов, таких как Claude Code.

Среди самых репрезентативных терминов этого кластера — load-bearing, refusal, survives, byte-identical, mutation-tested, structurally indistinguishable и другие, отражающие акцент на формальной верификации, неизменяемости и доказательной корректности кода. Эти слова указывают на сдвиг в практике разработки: всё больше PR фокусируются не на функциональности, а на гарантиях, которые код предоставляет — например, что изменение не ломает поведение, сохраняет битовую идентичность или выдерживает формальную проверку. Такой словарь стал «несущей конструкцией» современного кода, написанного с помощью ИИ-ассистентов.

Тред подтверждает наблюдаемость «клоудизмов» в проде и расширяет картину за пределы лексики: отмечаются синтаксические и форматные паттерны, проникновение в человеческую речь, гипотеза о компаундинг-эффекте при обучении новых моделей на AI-контенте, и практические попытки подавлять стиль через системные промпты. Отдельные респонденты считают часть слов обычным техжаргоном и оспаривают тезис о чисто LLM-происхождении слов типа load-bearing.

• Многие подтверждают из опыта, что «load-bearing», «spike», «sidecar», «resolver», «crux», «first-class citizen» массово появились в их кодовой базе и PR вместе с распространением Claude; @legobmw99 отмечает, что «sidecar» по их поиску стал использоваться в 3.6x чаще.

• LLM-лексика перетекает в человеческую речь: @nater5000 и @MrDrDr признаются, что стали непроизвольно использовать LLM-конструкции в своей письменной речи.

• Проблема выходит за лексику — синтаксис и формат тоже сигналят: @stabbles указывает на оборот «X contains no Y», @iamacyborg — на тирады с «, and», «, because», @elias_junit — на подчёркнуто линейную, хорошо структурированную подачу вместо нелинейного нарратива.

• Спор: Часть участников (@sethd, @danpalmer, @sosull) считает, что «Claude-измы» — это обычный техжаргон или следствие того, что модель буквально опирается на эти слова как на носители концептов (без них хуже думает), а @SalariedSlave и @polycaster, наоборот, видят именно LLM-специфичное явление и подозревают компаундинг-загрязнение обучающих данных.

• Совет: @ben30 показывает работающий приём: в глобальный промпт добавлено правило Орвелла и явный запрет на «load-bearing», «the crux», «first-class citizen»; в ответ Claude сам сообщает, что его системные инструкции требуют помечать «что-то load-bearing», то есть ограничение реально режет инструкции модели.

• Совет: @jimbobimbo использует в инструкциях агентов «find a synonym to 'resolve'», иначе появляется класс Resolver с методами ResolveThis/ResolveThat; @prmph заводит список запрещённых слов и просит переписать текст понятнее.

• Переломным по ощущениям @datadrivenangel называет примерно апрель (Opus 4.6/4.7), после чего Claude стал казаться «другим и более неудобным». @whywhywhywhy удивлён отсутствию в топе слова «shape».

• Подача проекта высоко оценена UX-составляющая: @nater5000 и @sosull хвалят, что всё помещается на экран без лишней воды, @Labo333 (автор) отвечает, что бэкенда нет — обновление и анализ делаются через GitHub Actions; обещает увеличить выборку до 1000 PR/день и поисковую строку.

Orwell's first rule: never use a metaphor you're used to seeing in print. "Load-bearing", "the crux", "first-class citizen" signal insight instead of showing it. Name the specific mechanism — @ben30

Архив Эдсгера Дейкстры содержит более тысячи его неопубликованных рукописей, известных как "EWDs", которые он рассылал десяткам получателей на протяжении более 40 лет. Дейкстра, один из основоположников компьютерных наук (1930-2002), внёс фундаментальный вклад в алгоритмы, языки программирования, операционные системы и формальную верификацию, за что получил высшую награду ACM - премию Тьюринга. Большинство его работ остались недоступными для широкой публики, пока не были оцифрованы и представлены на этом сайте в виде PDF-документов.

Исходные материалы, включая дневники и переписку, хранятся в Техасском университете. Архив включает несколько индексов для поиска, а также растущее количество транскрибированных текстов и переводов на разные языки. Дейкстра часто возвращался к уже обсуждавшимся темам, предлагая новые взгляды или более точные формулировки, что отражено в системе перекрёстных ссылок между документами.

• Дискуссия охватывает темы от индексации массивов до философии обучения программированию, включая ссылки на конкретные эссе и письма Дейкстры.
• Участники обмениваются ссылками на тексты Дейкстры, обсуждают его взгляды на обучение программированию, индексацию и стиль написания кода.
• Обсуждение затрагивает влияние Дейкстры на современную практику разработки ПО, включая дискуссии о том, как его идеи могут быть применимы или неприменимы в современном контексте.
• Участники также обсуждают влияние Дейкстры на современные языки программирования и стиль написания кода, включая дискуссии о том, как его идеи могут быть применимы в современной разработке ПО.
• Некоторые участники также обсуждают, как идеи Дейкстры могут быть использованы в обучении новых программистов и как его идеи могут быть применимы в современной разработке ПО.

Ironclad — это формально верифицируемый, реального времени, UNIX-подобный ядро операционной системы общего назначения и встраиваемых систем, написанное на SPARK и Ada. Проект полностью свободный и распространяется под лицензией GPLv3. Ключевые особенности включают POSIX-совместимый интерфейс, одновременное вытесняющее многозадачность, обязательный контроль доступа (MAC) и поддержку жёсткого реального времени.

Главное преимущество Ironclad — формальная верификация с помощью SPARK для критических компонентов, таких как криптография и MAC. Система полностью портативна и зависит только от GNU toolchain, что упрощает кросс-компиляцию. Проект поддерживает дистрибутивы для всех доступных архитектур, наиболее заметный из которых — Gloire. Ironclad всегда будет бесплатным для использования, изучения и модификации, а финансируется за счёт пожертвований и грантов от NLnet и Европейской комиссии.

• Участники сомневаются в степени формальной верификации Ironclad, сравнивая его с более строгими аналогами вроде seL4 и Tock, и указывают на отсутствие доказательства ключевых свойств ядра.
• Проект написан на SPARK и Ada, поддерживает x86_64 и RISC-V, но не ARM64; его лицензия включает бесплатную версию с возможностью коммерческого использования.
• Основные альтернативы: seL4 (быстрый и строго верифицируемый), Genode (POSIX-совместимый слой), Asterinas и Redox (Linux-совместимые ядра), а также ReactOS и SerenityOS.
• Критика включает медленную производительность по сравнению с seL4, отсутствие capability-based безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.