あなたの書いたコード、どこまで「保証」できますか？エンジニアが直面する信頼性の境界線

あなたが開発したソフトウェアについて、自信を持って「これだけは絶対に大丈夫」と断言できることは何でしょうか？バグゼロ？メモリリークの完全排除？それとも期待通りの挙動？皆さんが現場でどのような基準を持ってソフトウェアの品質を保証しているのか、ぜひ意見を聞かせてください。

形式手法（formal verification）は、多くのアプリ開発者にとって利用するにはまだ制限が多すぎる。記事では、返金処理の正確性を証明するためにEコマースプラットフォームで活用する例を挙げているけど、その後でこう認めているね。

今日現在、形式的に検証されたコアは、インバリアントや遷移、競合解決といった副作用のないロジックのほとんどを扱える。しかし、UI、ネットワーク呼び出し、データベースとのやり取りは通常、検証境界の外側にある。検証はコアを完璧にするけれど、エンドツーエンドの正確性を保証するものではない。

つまり、Eコマースの返金処理ロジックが正しいことは形式的に証明できても、実際に「返金が処理された」ことの証明はできない。データベースに返金が記録されたことすら証明できないし、決済プロセッサとのやり取りについては言うまでもない。

もしアプリがほとんど複雑なロジックだけで構成されていてI/Oが少ししかないなら、それはかなり特殊なアプリだし、Eコマースアプリであるはずがない。EコマースアプリはほとんどがCRUDアプリで、コードの99%はデータベースやUI、サードパーティAPI（決済プロセッサなど）とのI/Oだからね。

プロパティベーステストでさえ、こうしたEコマースアプリにはほとんど役に立たない。

形式手法は、プロパティベーステストのランタイムパフォーマンスを向上させるもの、くらいの感覚でいたほうがいい。もしプロパティベーステストがアプリに有効なら（たぶん有効じゃないだろうけど）、一部のテストを形式的な検証に変換できるかもしれない。

正直なところ、予算をたっぷり使ったとしても無理だろうけどね。

間違っているならぜひ証明してほしいけれど、そのやり方は、意味のあるオープンソースコードをプロパティテストを使って形式的に証明することだ。Postgresの重要な部分を形式検証できたら面白いかもね！（まあ無理だと思うけど）

大学の授業でDafnyを使って簡易デジタルウォレットを作る課題をやったけど、楽しかったよ。ただ、授業のメインテーマじゃなかったから、あまり深いところまでは学べなかったな。

ACMが今やクリックベイト系のYouTuberレベルまで落ちぶれるとはね。最高だよ。

もはや、専門の証明エンジニアを雇う予算のある安全クリティカルなシステムのためだけではない。証明する価値のあるプロパティを持つすべての人に向けたものだ

……そして、それを証明するためにAIへ支払う予算がある人のために、だね。

形式手法にはかなり経験があるけど、この記事の主張は理解できない。余談だけど、大規模なプログラムの正確性をAIが確実に証明できるというのは現時点では理論上の話に過ぎない。まあ、それが可能だとしてもだ。記事の主張は、「100行のプログラムを証明するために1万行の証明を書くのは非常にコストがかかる、だから普及しない」というもの。でも、このコスト増はAIを使っても同じことじゃないか！人に証明書を書かせるにせよ、LLMに書かせるにせよ、どちらにせよコストはかかる。「検証はAIの問題だ」と言うのは、「それはエンジニアの問題だ」と言うのと大差ない。どちらにせよ自分で作業するわけじゃないが、費用は自分が払うんだからね。

もし「証明を書くコストがテストの100倍高い」というのが前提なら、LLMが作業したとしてもなぜそれが100倍高いままじゃないのか、その理由を示唆するものはこの記事には何もない。

（ちなみに、専門の証明エンジニアが少ないのは需要がないからだよ。彼らは同レベルの他のエンジニアよりも特別高い給料をもらっているわけじゃないんだ）

これに興味がある人は、私が開発中のQedプロジェクトをチェックしてみて。形式的に検証されたWebフロントエンドだよ。 https://github.com/JacobAsmuth/qed

何が人々の理解を妨げているのか、よくわからないな。特に「金融の保存（financial conservation）」なんていう、定義が曖昧で馬鹿げたコンセプトを持ち出しているあたり。「一体何の話？」って感じだ。

じゃあ、発送はされたけど地震で配送トラックが全焼したモデルを考えてみてよ。あるいは、発送はされたけど注文者が受け取り前に亡くなっていて、遺族が受け取りを拒否している場合は？

みんな、オンライン注文のモデルを店舗での購入と同じように扱いたがる。じゃあ、顧客が商品を店から持ち出した瞬間に、店はその商品に関するあらゆる義務から解放されるのか？

これらの答えはすべて、実行されるべきプロセスが存在するということになるはずだ。中には、問題を解決済みのステータスに戻すために、実行状態の上書きが必要なものもあるだろう。

さて、通常のコード実行によって「未解決のステータス」に陥らないようにしたいか？もちろんしたいよ。多くの人は、争点となるステータスが存在しないような世界をモデル化できると思いたがっている。私には疑問だけどね。ただ、予期せぬ結果に驚かされることが少しでも減るような取り組みなら歓迎するよ。

最近、形式手法についてよく考えている。以前少しかじったことはあるけれど、狭い研究コミュニティでしか使われていないのは明らかだし、おもちゃのようなコード以上のものを検証する労力は膨大だった。AIを使って検証プロセスの面倒な部分を自動化できる可能性が非常に高いという著者の意見には同意するよ。さらに、小さなセキュリティ欠陥がすぐに悪用される現在のセキュリティ環境を考えると、証明可能なセキュアなコードこそが未来なのかもしれない。

形式手法を多くのアプリケーションコードに適用するのは難しすぎるという指摘は正しい。でも、今日でも適用可能なドメインはあるし、そこで使われていない主な理由は開発者に時間とノウハウがないからだ。例えば、ファイルフォーマットのパーサーは攻撃を受けやすいけれど、形式検証できるくらいにはシンプルだよ。

「証明は仕様の良さに依存する」。これが形式手法の墓石に刻まれる言葉になるだろうね。

問題は常に仕様にある。仕様の欠陥が顧客に起因するものだろうが、開発者が仕様の穴を誤って埋めてしまった結果だろうが関係ない。

もしシステム全体を構築したのに、仕様書にアクセス制御ロジックの言及がなかったら、形式手法はそのソフトウェアがセキュアかどうかを証明も反証もできない。単に仕様に含まれていないだけだからね……。

どのようなセキュリティプロパティが必要かを正確に知っていなければならない。それを簡潔かつ正確に仕様として書き上げた時点で、同じ内容をコードとして簡潔かつ正確に書き上げているのと変わらないんじゃないかな。

仕様書はコードと同じくらい詳細でなければならないし、同じくらいミスが起こりやすいものだよ。

開発プロセスの一部として形式手法を使っているよ。証明の必要性がコードの開発をガイドするし、その逆もまた然りだ。結果として、デバッグの手間が最小限で済むので、よりクリーンでシンプル、かつ軽量で効率的なプログラムをはるかに速く開発できる。もちろん、完全なテストケースも作成する。コード変更に伴う証明のメンテナンスは面倒だから、LLMや他のツールがサポートしてくれると嬉しいね。通常のプロセスで書かれたコードを形式検証しようとは絶対に思わないけど！

それにバグが含まれていること。それだけが100%保証できることだよ。