AIが16,000件のTLA+仕様を3,000件のVerus証明に変換

自己完結したステートマシンのような問題を持っている人は、ぜひこれで試してみてほしい。私の会社では、何人かの専門家がクラスタリングとフェイルオーバーロジックを最適化するために、状態を少し増やしていた（つまり複雑さを増していた）。私はその分野の専門家ではないにもかかわらず、OpusにTLA+を装備させて問題に当たらせることで、壊滅的なバグを見つけて防ぐことができた。それは以前のシステム実装では起こり得なかったバグで、それを引き起こす一連のステップについて単体テストを書こうなどとは誰も思わなかったので、最初は見過ごされていた。それを捉えたのはTLA+の不変条件だけだった。そう、それもOpusが書いた。

余談だが、プログラミングがもうやりがいのないものになったという話をよく聞く。しかし、上記の取り組みは、私が長い間エンジニアリングで経験した中でおそらく最も楽しいものだったし、個人的にはAIなしではほぼ不可能だっただろう。TLA+というものの目新しさもあったかもしれないが、これは、単にClaudeに手作業でやっていたことをやらせてEnterを押すだけではない、将来の私たちの仕事が実際にどうなり得るかの一端を示していると思う。もっと野心的でやりがいのあるユースケースがたくさんある。

私は https://github.com/quint-co/quint を通じて間接的にTLA+を使っている。「機能を実装する前に、Quintを使ってモデル化し、システム全体として反例がないことを確認してください。設計もQuintで繰り返し、ドキュメントと実装が形式モデルとドキュメントに従っていることを確認してください」という指示を追加した。

結果は、ずっと時間はかかるものの、かなり魔法のようだ。このような単純な指示だけで、多くのトランザクションやアトミック性のバグが見つかって修正された。

しかし、特に外部リソース周りでは、いつも魔法のようとは限らない。残念ながらCloudflareは時々D1やKVでタイムアウトの不具合を起こす。これはある意味不可抗力だ。

幸いなことに、それはつまり、トランザクションが我々が保証されていると思っていたようには完了しないかもしれないという二値イベントとしてアクションをモデル化し、その周りに追加のガードを設けて、状態をリトライしなければならないようにする必要があるということだ。

今のところ、そうやって回避できている。条件や制約が増えれば増えるほど、NPスケールなのでCPUがより強力になる可能性があることに留意してほしい。

これは何も理解できない。すべてを言っているようで、同時に何も言っていない。TLA+が何であれ、この記事はそれを史上最も退屈でアカデミックなもののように聞かせている。

これを見つけるのに10分かかった: TLA+は、リアクティブシステムを設計、モデル化、文書化、検証するために開発された形式仕様言語である。