Giao thức cho vay XRPL bắt đầu kiểm chứng hình thức bằng Lean 4

Giao thức cho vay mới của XRP Ledger(XRPL) đã bắt đầu được kiểm chứng bằng toán học để xác định liệu dòng tiền và các quy tắc kế toán có vi phạm quy định hay không. Tuy nhiên, quá trình này không có nghĩa là loại bỏ được tình trạng vỡ nợ hoặc rủi ro tín dụng của bên vay.

Common Prefix, một công ty nghiên cứu giao thức, ngày 17 tháng 9 cho biết đang kiểm chứng hình thức giao thức cho vay XRPL bằng ngôn ngữ chứng minh định lý Lean 4. Phạm vi kiểm chứng tập trung vào việc các quy trình gửi tiền, cho vay, hoàn trả và mua lại có tuân thủ các quy tắc kế toán và an toàn đã định trước hay không.

Kiểm chứng hình thức khác với hoạt động kiểm thử thông thường vốn chỉ chạy một số kịch bản. Thay vì trực tiếp chứng minh toàn bộ mã C++ của xrpld, nhóm nghiên cứu tái hiện logic cốt lõi trong mô hình Lean 4 và xác định các thuộc tính mà mô hình phải tuân thủ.

Sau đó, nhóm áp dụng cùng đầu vào cho mô hình và phiên bản triển khai thực tế để kiểm tra xem kết quả có trùng khớp hay không. Vì vậy, phạm vi chứng minh bị giới hạn bởi các trạng thái được đưa vào mô hình và những giả định do nhóm nghiên cứu thiết lập. Common Prefix đã mô tả trong các tài liệu công khai hoạt động kiểm chứng chính thức đối với kho tiền đơn tài sản và giao thức cho vay.

Công việc này không đồng nghĩa tính năng cho vay XRPL đã được kích hoạt hoàn toàn trên mainnet. Tài liệu mã nguồn mở của Ripple mô tả LendingProtocolV1_1 là một amendment đưa vào kho tiền đóng và cơ chế kế toán tiền mặt, trong khi việc áp dụng thực tế vẫn cần cuộc bỏ phiếu trên mainnet và quy trình đồng thuận.

Bản ghi phát hành xrpld phiên bản 3.4.0 do XRPLF công bố có bao gồm các tính năng liên quan đến LendingProtocolV1_1. Tuy nhiên, việc tính năng được đưa vào mã nguồn và việc amendment đó được kích hoạt trên sổ cái là hai quy trình riêng biệt.

Kho tiền của LendingProtocolV1_1 vận hành qua ba giai đoạn: đăng ký, đầu tư và mua lại. Ở giai đoạn đăng ký, người dùng có thể gửi và rút tiền. Trong giai đoạn đầu tư, tiền được khóa để sử dụng cho các khoản vay mới. Khi khoản vay đáo hạn và được hoàn trả, người gửi tiền có thể chuyển đổi phần sở hữu thành tiền mặt ở giai đoạn mua lại.

Tài liệu chính thức của XRPL về kho tiền đơn tài sản đưa ra các điều kiện giao dịch theo từng giai đoạn. Cấu trúc này phản ánh trên trạng thái sổ cái thời điểm tiền gửi được đưa vào khoản vay và thời điểm có thể mua lại.

Cơ chế kế toán cũng được thay đổi. Trong cấu trúc hiện tại, lãi dự kiến được ghi nhận là doanh thu ngay khi khoản vay được giải ngân. LendingProtocolV1_1 sử dụng kế toán tiền mặt, ghi nhận lãi khi tiền hoàn trả thực tế được nhận.

Cách tiếp cận này nhằm giảm vấn đề phần lãi chưa thu đã được phản ánh trước vào tài sản của kho tiền và giá trị phần sở hữu. Tuy nhiên, dù quy tắc kế toán được hoàn thiện hơn, rủi ro bên vay không hoàn trả vẫn không biến mất.

Các đợt kiểm chứng trước đây đã phát hiện vi phạm bất biến của kho tiền, lỗi xác minh hoàn trả khoản vay, vấn đề làm tròn số học và khác biệt giữa đặc tả XLS với phiên bản triển khai thực tế. RippleX cho biết trong một bài đăng dành cho nhà phát triển rằng các sửa đổi liên quan đã được đưa vào xrpld phiên bản 3.1.3 và 3.2.0.

Những phát hiện này cho thấy kiểm chứng hình thức có thể vượt ra ngoài vai trò kiểm tra trước khi phát hành và trở thành công cụ phát hiện khác biệt giữa phiên bản triển khai với đặc tả. Ngược lại, các trạng thái không được đưa vào mô hình hoặc những giả định không được nhóm nghiên cứu thiết lập sẽ không thuộc phạm vi chứng minh.

Rủi ro tín dụng của giao thức cho vay XRPL vẫn tồn tại riêng biệt. Tài liệu về giao thức cho vay XRPL giải thích rằng việc đánh giá tín dụng và thẩm định khoản vay của bên vay được thực hiện ngoài chuỗi, thay vì sử dụng tài sản thế chấp và thanh lý tự động.

Nguồn vốn chịu lỗ ở cấp cao do nhà môi giới cho vay cung cấp có thể hấp thụ một phần tổn thất, nhưng không thể loại bỏ việc bên vay vỡ nợ. Do đó, nội dung được kiểm chứng lần này không phải là liệu bên vay chắc chắn hoàn trả hay không, mà gần với việc xác định liệu hoạt động kế toán gửi tiền, cho vay, hoàn trả và mua lại bên trong sổ cái có vận hành theo các quy tắc đã định hay không.

Cuộc thảo luận về hạ tầng cho vay tổ chức của XRPL từng được TokenPost đề cập trước đó. Lần kiểm chứng hình thức này là bước kiểm tra độ ổn định của kế toán và quá trình chuyển đổi trạng thái trước khi các tính năng cho vay được áp dụng vào sổ cái thực tế.

Trước khi tình trạng kích hoạt trên mainnet và phạm vi kiểm chứng cuối cùng được xác định, chưa thể nói rằng mức độ an toàn của thị trường cho vay XRPL đã được chứng minh. Trong thời gian tới, sự chú ý sẽ tập trung vào việc amendment LendingProtocolV1_1 có được phê duyệt hay không và cơ chế thẩm định khoản vay ngoài chuỗi sẽ được triển khai như thế nào.