데이비드 슈워츠(David Schwartz) 리플 CTO 명예직이 XRP 레저(XRP Ledger·XRPL) 합의 알고리즘의 형식적 타당성을 증명하는 자료를 발견했다고 밝혔다. 다만 실제 증명서와 전체 검증 결과는 공개되지 않았다.
슈워츠는 8일 X에 “XRPL 합의 알고리즘의 형식적 타당성에 대한 환상적인 증명을 발견했다”고 썼다. X의 글자 수 제한 때문에 내용을 게시할 수 없다고 덧붙였지만, 증명이 어떤 모델과 범위를 대상으로 하는지는 설명하지 않았다.
U.Today는 슈워츠의 발언을 전하면서 구체적인 수학적 증명이나 실질적 의미를 확인할 자료는 제시되지 않았다고 전했다. 따라서 이번 발언만으로 합의 알고리즘 전체의 검증이 끝났다고 보기는 어렵다.
같은 날 마유카 바다리(Mayukha Vadari) 리플X 엔지니어는 XRP 레저의 핵심 구성요소를 형식 검증하고 있다고 밝혔다. 리플X는 형식 검증 업체 커먼 프리픽스(Common Prefix)와 협력해 시스템이 설계대로 작동하는지 수학적으로 확인하고 있다.
형식 검증은 일부 입력값을 시험하는 일반적인 소프트웨어 테스트와 다르다. 시스템의 동작을 수학적 모델로 표현한 뒤 정해진 조건에서 안전성·일관성·생존성 같은 속성이 성립하는지 기계적으로 확인하는 방식이다.
XRP 레저의 합의는 검증인들이 다음 원장에 포함할 거래 집합에 동의하는 과정이다. 검증인들이 같은 결과를 확인하면 해당 원장이 확정되고, 이후 거래 기록의 기준으로 사용된다.
리플X 개발자 비토 투마스(Vito Tumas)는 2025년 12월 공개한 기술 문서에서 커먼 프리픽스와 함께 XRP 레저의 결제 엔진과 합의 프로토콜을 형식화하는 작업을 시작한다고 밝혔다. 문서는 합의 과정의 안전성·생존성·최종성을 수학적으로 검증하는 것을 목표로 제시했지만, 합의 알고리즘 전체의 검증이 끝났다고 밝히지는 않았다.
커먼 프리픽스는 XRP 레저 결제 시스템 사양과 검증 관련 코드를 공개 저장소에서 관리하고 있다. 저장소에는 ‘rippled-formal-verification’ 프로젝트도 있지만, 슈워츠가 언급한 증명이 해당 프로젝트의 어떤 결과인지는 공개 자료로 확인되지 않았다.
XRP 레저에 대출과 단일자산 금고 같은 기능이 추가되는 가운데, 리플X와 커먼 프리픽스는 핵심 구성요소의 동작을 수학적으로 확인하는 형식 검증 작업을 진행하고 있다. 핵심 코드에 포함되는 기능이 늘어날수록 일반 테스트와 보안 감사만으로 모든 상태를 점검하기 어려워 형식 검증을 병행하는 구조다.
형식 검증은 실제 구현과 수학적 사양 사이의 차이를 찾거나 기존 테스트가 놓친 예외 조건을 점검하는 데 활용된다. 다만 형식 검증의 대상 범위와 전제 조건에 따라 확인할 수 있는 안전성의 수준은 달라진다.
커먼 프리픽스는 과거 XRP 레저 합의 과정의 거래 집합 처리 방식과 관련한 취약점도 발견했다. XRP 레저 재단은 악의적으로 조작된 검증인 메시지가 다른 검증인 노드를 충돌시킬 수 있었으며, 수정 사항은 rippled 3.0.0에 반영됐다고 밝혔다.
XRP 레저 재단도 커먼 프리픽스와 합의 메커니즘의 형식 검증 및 보안 분석을 진행하고 있다고 공개했다. 커먼 프리픽스는 바다리의 협력 발표에 반응해 협력 사실을 재확인했다.
다만 이번 발언 직후 XRP 가격이나 거래량이 형식 검증 발표 때문에 변했다는 인과관계는 확인되지 않았다. 이번 사안은 XRP 가격 재료라기보다 XRP 레저의 개발·보안 체계를 코드와 테스트 중심에서 수학적 사양과 기계 검증으로 확장하는 기술적 움직임에 가깝다.
슈워츠는 과거에도 XRP 레저와 리플의 기술·보유 현황에 관한 발언을 내놓은 바 있으며, 그의 리플 지분 발언은 XRP 보유량과 구분해 봐야 한다는 점에서 다뤄졌다. 이번 발언 역시 개인의 설명과 공식 기술 결과를 나눠 해석할 필요가 있다.
현재 공개된 내용은 슈워츠가 합의 알고리즘 관련 증명을 언급했고, 리플X와 커먼 프리픽스가 XRP 레저 핵심 구성요소의 형식화·검증 작업을 진행하고 있다는 점이다. 실제 증명의 범위와 기계 검증 통과 여부는 관련 결과물이 공개된 뒤 판단할 수 있다.

