Boris Cherny показал TLA+ в деле: интернет требует объяснений
The internet discovers TLA+. Now what?
Твит Бориса Черни о моделировании Claude Agent SDK на TLA+ и Lean набрал миллион просмотров, и многие впервые услышали о формальной верификации. Разбираем, что такое TLA+ и зачем он нужен: описание возможных поведений системы и проверка свойств безопасности и живости. Но модель — не реализация, а TLC проверяет лишь конечные конфигурации. В Reasonable пошли дальше: агентный конвейер превратил более 16 000 пар спецификаций TLA+ в 3 000 машинно-проверенных доказательств на Verus.
TLA+ — это компактный язык для описания того, что системе разрешено делать и что всегда или в конечном счёте должно быть истинно.
- lopatin
Я бы посоветовал всем попробовать это на каких-нибудь самодостаточных задачах, похожих на конечные автоматы, если такие есть. В моей компании несколько экспертов оптимизировали логику кластеризации и отказоустойчивости, добавив немного состояния (а значит, и сложности). Несмотря на то, что я не эксперт в этой области, мне удалось найти и предотвратить катастрофический баг, направив Opus, вооружённый TLA+, на эту проблему. Это был баг, невозможный в предыдущей реализации системы, и никто не додумался написать юнит-тесты для последовательности шагов, которая его вызывает, так что сначала он остался незамеченным. Единственное, что его поймало — это инварианты TLA+, которые, да, тоже были написаны Opus.
Как побочное замечание: много говорят о том, что программирование больше не приносит удовлетворения. Но описанное выше упражнение было, пожалуй, самым весёлым, что я делал в инженерии за долгое время, и лично для меня оно было бы почти невозможно без ИИ. Возможно, это была новизна TLA+, но, думаю, это даёт представление о том, чем на самом деле может быть наша работа в будущем — не просто говорить Claude делать то, что вы раньше делали вручную, и нажимать Enter. Для этого есть гораздо более амбициозные и приносящие удовлетворение сценарии использования.
- stevefan1999
Я косвенно использую TLA+ через https://github.com/quint-co/quint. Я добавил инструкции: «прежде чем реализовывать любую функцию, смоделируй её с помощью Quint и убедись, что нет контрпримера для системы в целом; также пересмотри дизайн с помощью Quint и убедись, что твои документы и реализация соответствуют формальной модели и документации».
Результат, хотя и занимает гораздо больше времени, довольно волшебный. Множество ошибок транзакций и атомарности было найдено и исправлено только благодаря такой простой инструкции.
Однако иногда всё не так волшебно, особенно когда речь заходит о внешних ресурсах. Cloudflare, к сожалению, иногда даёт сбои на D1 и KV с таймаутами, что более или менее форс-мажор.
К счастью, это означает, что мне придётся смоделировать действие как бинарное событие — что транзакция может не завершиться так, как мы считали гарантированным, — и добавить дополнительную защиту вокруг неё, чтобы состояние пришлось повторить.
Пока мне удавалось обходить это таким образом. Учтите: чем больше условий и ограничений, тем мощнее может понадобиться процессор, поскольку это по масштабу NP.
- peterus
Реальные применения TLA+: https://foundation.tlapl.us/industry/index.html.
В статье Intel показано, как TLA+ применялся как шаг перед написанием описания аппаратуры. Не уверен, прижилось ли это; похоже, сейчас используются другие инструменты. Кто-нибудь здесь из индустрии СБИС знает?
- pron
Я люблю TLA+ за возможность точно и в то же время кратко описывать системы и рассуждать о них. Но как человек, много лет использующий формальные методы для помощи в разработке ПО, я не понимаю всю эту индустрию вокруг инструментов, соединяющих такой замечательный математический язык — и другие подобные, вроде Lean — с ИИ, до такой степени, что рассуждения скрываются от людей.
Доказательство корректности программ от начала до конца (то есть от кода до высокоуровневых свойств) — как это якобы делают эта компания и другие — настолько сложно, что люди смогли сделать это лишь для очень маленьких программ (~10 тысяч строк кода), да и то в очень специализированных случаях, когда программы написаны сверхпростым способом (часто в ущерб производительности, потому что производительность часто требует более сложных алгоритмов). Если ИИ станет хотя бы на порядок способнее людей в разработке ПО, а именно это потребуется для такой задачи, нужна ли ему будет наша помощь в написании различных инструментов и обвязок, помогающих с этой задачей? В конце концов, писать эти инструменты настолько проще, чем использовать их для этой цели, что я не понимаю гипотезу о возможностях ИИ здесь.
Эта компания говорит: они «разрабатывают агентные фреймворки, чтобы сделать эти гарантии корректности доступными для всех инженеров-программистов». Но разработать всё это — лёгкая часть! Если ИИ может сделать трудную часть, зачем ему наша помощь, чтобы сделать доступной лёгкую часть, — он наверняка сам найдёт способ сделать эту лёгкую часть! Это как говорить: «Скоро у нас будет машина, кото […]
- bsenftner
Потребовалось 10 минут, чтобы найти это: TLA+ — это язык формальной спецификации, разработанный для проектирования, моделирования, документирования и верификации реактивных систем.