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

XRP Ledger(XRPL)의 신규 대출 프로토콜이 자금 흐름과 회계 규칙을 위반하지 않는지 수학적으로 검증하는 작업에 들어갔다. 다만 이 검증이 대출자의 채무불이행이나 신용위험까지 없앤다는 뜻은 아니다.

프로토콜 연구기업 커먼 프리픽스(Common Prefix)는 9월 17일 XRPL 대출 프로토콜을 정리증명 언어 Lean 4로 형식 검증하고 있다고 밝혔다. 검증 대상은 예치·대출·상환·환매 과정이 정해진 회계·안전 규칙을 위반하지 않는지 여부다.

형식 검증은 일부 시나리오를 실행하는 일반적인 테스트와 다르다. 연구진은 전체 xrpld C++ 코드를 직접 증명하는 대신 핵심 로직을 Lean 4 모델로 재현하고, 모델이 지켜야 할 속성을 정의한다.

이후 모델과 실제 구현에 같은 입력을 적용해 결과가 일치하는지 확인한다. 따라서 증명의 범위는 모델에 포함된 상태와 연구진이 설정한 가정으로 제한된다. 커먼 프리픽스는 공개 자료에서 단일자산 금고와 대출 프로토콜의 공식 검증 작업을 설명하고 있다.

이번 작업은 XRPL 대출 기능이 메인넷에서 완전히 활성화됐다는 뜻은 아니다. Ripple 오픈소스 문서는 LendingProtocolV1_1을 폐쇄형 금고와 현금주의 회계를 도입하는 amendment로 설명하고 있으며, 실제 적용에는 메인넷 투표와 합의 절차가 필요하다.

XRPLF가 공개한 xrpld 3.4.0 릴리스 기록에는 LendingProtocolV1_1 관련 기능이 포함돼 있다. 그러나 코드에 기능이 반영된 것과 원장에서 해당 amendment가 활성화되는 것은 별개의 절차다.

LendingProtocolV1_1의 금고는 청약·투자·환매의 세 단계로 운영된다. 청약 단계에서는 자금 예치와 인출이 가능하지만, 투자 단계에서는 자금이 고정돼 신규 대출에 사용되고 대출이 만기돼 상환되면 환매 단계에서 예치자가 지분을 현금화한다.

XRPL 공식 단일자산 금고 문서는 단계별 거래 조건을 제시하고 있다. 이 구조는 예치금이 언제 대출에 투입되고 언제 환매 가능한지 원장 상태에 반영하는 방식이다.

회계 방식도 바뀐다. 기존 구조는 대출이 실행되는 즉시 예정된 이자를 수익으로 인식했지만, LendingProtocolV1_1은 실제 상환금이 들어온 시점에 이자를 반영하는 현금주의 회계를 사용한다.

받지 못한 이자가 금고 자산과 지분가치에 미리 반영되는 문제를 줄이려는 방식이다. 다만 회계 처리 규칙이 정교해져도 차주가 상환하지 않는 위험까지 사라지는 것은 아니다.

앞선 검증 과정에서는 금고 불변식 위반, 대출 상환 검증 오류, 산술 반올림 문제, XLS 사양과 실제 구현의 차이가 발견됐다. RippleX는 관련 수정이 xrpld 3.1.3과 3.2.0에 반영됐다고 개발자 게시물에서 밝혔다.

이 같은 발견은 형식 검증이 단순한 출시 전 점검을 넘어 구현과 사양의 차이를 찾아내는 수단이 될 수 있음을 보여준다. 반대로 검증 모델에 포함되지 않은 상태나 연구진이 설정하지 않은 가정은 증명 대상에 포함되지 않는다.

XRPL 대출 프로토콜의 신용위험은 별도로 남는다. XRPL 대출 프로토콜 문서는 담보와 자동 청산 대신 대출자의 신용평가와 인수심사를 오프체인에서 수행한다고 설명한다.

대출 브로커가 제공하는 선순위 손실부담 자본은 일부 손실을 흡수할 수 있지만, 차주의 부도 자체를 없애지는 않는다. 따라서 이번 검증이 확인하는 것은 차입자가 반드시 상환하는지가 아니라 원장 내부의 예치·대출·상환·환매 회계가 정의된 규칙대로 작동하는지에 가깝다.

XRPL의 기관 대출 인프라 논의는 앞서 본지에서도 다뤄졌다. 이번 형식 검증은 이런 대출 기능을 실제 원장에 적용하기 전 회계와 상태 전이의 안정성을 점검하는 단계다.

메인넷 활성화 여부와 최종 검증 범위가 확정되기 전까지 XRPL 대출시장의 안전성이 입증됐다고 보기는 어렵다. 향후에는 LendingProtocolV1_1 amendment의 승인 여부와 오프체인 대출심사 구조가 확인 대상이 된다.