「Common Prefix」は、#XRP の「Ledger Lending Protocol（レジャー・レンディング・プロトコル）」を形式的に検証し、引き出されることがなく、債務超過にならず、またルールを破らないことを数学的に証明することに取り組んだ。

この取り組みは、XLS-66を通じて導入されたレンディング・プロトコルに焦点を当てている。「Common Prefix」は、検証プロセスにLean 4を選んだ理由を含む6部構成のシリーズで、そのアプローチを説明した。

「Common Prefix」は、形式的検証は通常のソフトウェアテストを超えるものであり、数学を用いて、あらゆる可能な状況でシステムが正しく機能することを証明すると述べた。

XRP LedgerのバリデータであるVet（Hussein Zanganaとしても知られる）は、形式的検証は軍事技術、航空交通ソフト、飛行制御、原子力発電所といったハイリスクなシステムで、すでに使われていると語った。

同氏は、その手法は、開発者がテストした状況だけでなく、考えられるあらゆる入力に対してシステムが有効であり続けることを数学によって示すものだと説明した。

「Common Prefix」は、Dafny、Lean 4、TLA+、Pなど複数のツールを検討した。同チームは、レンディング・プロトコルに関して自分たちが答える必要のある特定の問いに対しては、TLA+とPが適していないと判断した。

Lean 4を選んだ理由の一つとして、SMTソルバに依存しない点が挙げられる。「Common Prefix」は、Dafnyのソルバが検証に必要な複雑な算術を扱う際に、時にタイムアウトすることがあると分かった。Leanは手作業での負担が増えるが、その分、開発者が誤りを見つけて修正しやすくなる。

#CryptoNewsCommunity