На прошлой неделе Boris Cherny, изобретатель Claude Code, упомянул, что Opus смог использовать TLA+ для поиска состояний гонки в коде. Теперь все говорят о формальной верификации. Как давний преподаватель и сторонник TLA+, это захватывающе. Но новая эйфория меня беспокоит. Формальные методы не решат проблему агентной разработки программного обеспечения раз и навсегда.

Правильные проекты не автоматически превращаются в правильный код. Чтобы проверить свойство, нам нужно свойство для проверки. TLA+ делит систему на поведения, каждое из которых представляет собой последовательность состояний. В каждом состоянии мы можем выражать булевы выражения с помощью трех темпоральных операторов: `[]P` (всегда P), `P'` (P в следующем состоянии) и `<>P` (в конечном итоге P).

`[]P` означает, что P истинно в каждом состоянии каждого поведения, что называется инвариантом. `[](x' >= x)` — это свойство действия. Это свойства безопасности: плохое никогда не случается. Свойства живости используют `<>`: `[]<>P` означает, что P истинно хотя бы в одном будущем состоянии каждого состояния; `<>[]P` означает, что P становится истинным и остается истинным навсегда; `[](P => <>Q)` означает, что P в конечном итоге вызывает Q.