XRPL 대출 프로토콜, Lean 4 형식 검증 착수

본문

커먼 프리픽스가 XRP Ledger 대출 프로토콜의 회계·안전 규칙을 Lean 4로 검증하고 있다. LendingProtocolV1_1의 메인넷 활성화와 최종 검증 완료는 아직 확정되지 않았다. XRP Ledger(XRPL)의 신규 대출 프로토콜이 자금 흐름과 회계 규칙을 위반하지 않는지 수학적으로 검증하는 작업에 들어갔다. 프로토콜 연구기업 커먼 프리픽스(Common Prefix)는 9월 17일 XRPL 대출 프로토콜을 정리증명 언어 Lean 4로 형식 검증하고 있다고 밝혔다. 검증 대상은 예치·대출·상환·환매 과정이 정해진 회계·안전 규칙을 위반하지 않는지 여부다. 연구진은 전체 xrpld C++ 코드를 직접 증명하는 대신 핵심 로직을 Lean 4 모델로 재현하고, 모델이 지켜야 할 속성을 정의한다. 커먼 프리픽스는 공개 자료에서 단일자산 금고와 대출 프로토콜의 공식 검증 작업을 설명하고 있다.

이번 작업은 XRPL 대출 기능이 메인넷에서 완전히 활성화됐다는 뜻은 아니다.

앞선 검증 과정에서는 금고 불변식 위반, 대출 상환 검증 오류, 산술 반올림 문제, XLS 사양과 실제 구현의 차이가 발견됐다. XRPL 대출 프로토콜 문서는 담보와 자동 청산 대신 대출자의 신용평가와 인수심사를 오프체인에서 수행한다고 설명한다. 이번 형식 검증은 이런 대출 기능을 실제 원장에 적용하기 전 회계와 상태 전이의 안정성을 점검하는 단계다. 메인넷 활성화 여부와 최종 검증 범위가 확정되기 전까지 XRPL 대출시장의 안전성이 입증됐다고 보기는 어렵다.