Common Prefixは、$XRP Ledgerレンディングプロトコルを形式的検証し、それが資金を奪われることなく、破綻することなく、ルールを破ることもないことを数学的に証明しています。 この作業は、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は手動での作業量が増えますが、その分開発者がエラーを見つけやすく修正しやすくなります。#Ripple https://t.co/s0YcQ4KAWX