Инженер Anthropic попросил Opus 5.5 доказать корректность SDK — вышло 16 правок

Инженер Anthropic Борис Черни рассказал, что проверил Claude Agent SDK формальными методами — доказательством свойств кода на языке Lean, где корректность выводится математически, а не проверяется тестами.

По его словам, нескольких коротких запросов хватило, чтобы модель Opus 5.5 выдала 16 pull request с исправлениями багов и состояний гонки — ошибок, возникающих при одновременном доступе к общим данным. Он также применяет TLA+ — язык описания поведения систем — и иногда комбинирует оба инструмента для проверки потоков данных и управления состоянием.

Пост собрал больше пяти тысяч лайков — формальная проверка раньше требовала отдельного специалиста и недель работы.

Boris Cherny@bcherny

I used Opus 5.5 to formally verify the Claude Agent SDK using Lean. A couple short prompts = 16 PRs fixing various bugs and race conditions. Video attached. TLA+ also works well. I sometimes combine Lean and TLA+ to look for issues around data flow, concurrency, and state mgmt. https://t.co/C0PLNLow9p

5 30922 сентября 2026