23 сентября 2026 г.
Гонки можно искать формальной моделью: Opus 5.5 подготовил 16 PR для Agent SDK
22 сентября Борис Черны проверил Claude Agent SDK в Lean с Opus 5.5 и получил 16 PR с исправлениями багов и race conditions. Несколько коротких промптов помогли модели описать работу SDK формально и найти проблемы в параллельной работе.
Boris Cherny
@bcherny
Я использовал Opus 5.5 и Lean, чтобы формально проверить Claude Agent SDK. Несколько коротких промптов дали 16 PR с исправлениями разных багов и race conditions. Видео приложено. С TLA+ тоже хорошо работает. Иногда я сочетаю Lean и TLA+, чтобы искать проблемы в потоках данных, параллельной работе и управлении состоянием. Я плохо знаю оба языка, но Claude отлично справляется с обоими. Этот подход очень полезен: он помогает формально описать ваш код и найти баги, которые человек, скорее всего, не заметил. Станет ли формальная проверка будущим программирования? Или хотя бы поиска багов?
· 143,5 тыс. просмотров
Официальный пример Claude Agent SDK поручает агенту искать и исправлять баги в репозитории. Теперь Черны сначала проверил устройство SDK в Lean, а затем получил исправления для найденных проблем.
Связка для проекта. Claude Agent SDK ставится через npm или pip и читает ключ из переменной `ANTHROPIC_API_KEY`. Lean рекомендуют установить через расширение для VS Code. TLA+ можно добавить для поиска ошибок в потоках данных, параллельной работе и управлении состоянием.
TLA+ дополняет Lean при поиске ошибок в потоках данных, параллельной работе и состоянии.
Первоисточник
