先週、Claude Code の発明者である Boris Cherny 氏は、Opus が TLA+ を使用してコード内の競合状態を発見できたと述べました。今や誰もが形式検証について話しています。長年の教育者であり TLA+ の提唱者として、これはエキサイティングです。しかし、この新たな熱狂は私を心配させます。形式手法はエージェンティックソフトウェア開発の問題を一挙に解決するものではありません。

正しい設計が自動的に正しいコードに変換されるわけではありません。プロパティを検証するには、検証するプロパティが必要です。TLA+ はシステムを動作に分割し、各動作は状態のシーケンスです。各状態では、3 つの時間論理演算子を使用してブール式を表現できます：`[]P`（常に P）、`P'`（次の状態の P）、`<>P`（最終的に P）。

`[]P` は、P がすべての動作のすべての状態で真であることを意味し、不変条件と呼ばれます。`[](x' >= x)` はアクションプロパティです。これらは安全性プロパティです：悪いことは決して起こりません。活性プロパティは `<>` を使用します：`[]<>P` は、P がすべての状態の少なくとも 1 つの将来の状態で真であることを意味します；`<>[]P` は、P が真になり、永久に真のままであることを意味します；`[](P => <>Q)` は、P が最終的に Q を引き起こすことを意味します。