Common Prefix đang chính thức xác minh hình thức Giao thức Cho vay $XRP Ledger để chứng minh toán học rằng hệ thống không thể bị rút cạn, mất khả năng thanh toán hoặc vi phạm các quy tắc của nó. Công việc tập trung vào Giao thức Cho vay được giới thiệu thông qua XLS-66. Common Prefix đã giải thích cách tiếp cận của mình trong chuỗi sáu phần, bao gồm lý do họ chọn Lean 4 cho quá trình xác minh. Common Prefix cho biết xác minh hình thức vượt xa kiểm thử phần mềm thông thường bằng cách sử dụng toán học để chứng minh rằng một hệ thống hoạt động chính xác trong mọi tình huống có thể xảy ra. Validator của XRP Ledger, còn được biết đến với tên Hussein Zangana, cho biết xác minh hình thức đã được sử dụng trong các hệ thống rủi ro cao như công nghệ quân sự, phần mềm điều khiển giao thông hàng không, hệ thống điều khiển bay và nhà máy điện hạt nhân. Ông giải thích rằng cách tiếp cận này sử dụng toán học để chứng minh hệ thống vẫn hợp lệ trên mọi đầu vào có thể, chứ không chỉ trong các tình huống mà các nhà phát triển đã kiểm thử. Common Prefix đã xem xét một số công cụ, bao gồm Dafny, Lean 4, TLA+ và P. Nhóm quyết định rằng TLA+ và P không phù hợp với những câu hỏi cụ thể mà họ cần trả lời về giao thức cho vay. Một lý do họ chọn Lean 4 là vì nó không phụ thuộc vào trình giải SMT. Common Prefix phát hiện rằng trình giải của Dafny đôi khi hết thời gian khi xử lý các phép tính phức tạp cần thiết cho việc xác minh. Lean yêu cầu nhiều công việc hơn từ phía con người, nhưng điều này cũng giúp các nhà phát triển dễ dàng phát hiện và sửa lỗi hơn. #Ripple https://t.co/s0YcQ4KAWX