Vermilion은 Verus 검증 조건을 Lean 증명으로 바꾼다

Vermilion은 Rust 검증기 Verus의 검증 조건을 Lean 정리로 바꾸는 실험적 백엔드다. 기존 Verus 명세를 활용하면서 Lean의 대화형 증명 기능과 수학 라이브러리를 연결하지만, Verus의 일부 기능만 지원하고 변환의 정확성은 아직 증명하지 않았다.

Verus는 Rust 코드와 명세에서 검증 조건을 만들고, 보통 SMT 풀이기 Z3로 이를 자동 증명한다. Vermilion은 이 과정에서 SST 중간 표현을 받아 검증 조건을 Lean 정리로 생성한다. 자동 증명이 실패하면 사용자가 Lean에서 증인을 지정하거나 귀납법과 Mathlib 정리를 활용해 증명을 이어갈 수 있다. VS Code 확장에서는 Rust의 단언문·사후조건·루프 불변식에서 해당 Lean 목표로 이동하고, 반대로 돌아갈 수 있다. 관련 코드와 확인 방법은 저장소 예제에 있다.

저장소의 병합 정렬 사례에는 검증 조건 40개가 있으며, 이 가운데 31개는 자동으로 증명되고 9개는 대화형 증명이 필요했다. 일부 대화형 증명에는 Mathlib에 바로 쓸 수 있는 정리가 없어 새 보조 정리를 작성해야 했다. Vermilion은 루프, 재귀 명세, 컬렉션, 가변 참조, 일부 제네릭 프로그래밍을 포함한 순차 프로그램의 상당 부분을 지원하지만 Verus보다 언어와 라이브러리 지원 범위가 좁다. 안전하지 않은 메모리 연산과 동시성도 아직 지원하지 않는다. 자세한 범위는 지원 목록, 사용 절차는 튜토리얼에서 확인할 수 있다.

정확성에는 중요한 경계가 있다. Lean은 생성된 정리의 증명은 검사하지만, Vermilion이 Rust 프로그램의 의미를 올바른 검증 조건으로 변환했는지는 보증하지 않는다. 변환기와 검증 조건 생성기는 여전히 신뢰 대상이며, 이를 형식적으로 증명하는 작업은 향후 과제로 남아 있다. 관련 경계는 신뢰 문서에 정리돼 있다.

속도도 제약이다. 초기 비교는 작은 공통 사례 5개에서 실행 종료까지 걸린 시간의 중앙값이 4.2배 느렸고, 이후 Verus와의 일치 여부를 확인한 180개 사례에서는 중앙값이 약 16배였다. 두 측정에는 프로세스 시작과 라이브러리 로딩이 포함되므로, 이를 Lean 자동 증명과 SMT 풀이의 보편적인 속도 차이로 볼 수는 없다. 비교 보고서는 측정 조건을 설명한다.

Vermilion은 GitHub에서 공개돼 있다. 개발 방향으로는 일상적인 조건은 Verus의 SMT 백엔드에 맡기고, 상호작용 증명이나 수학 라이브러리가 유용한 경우 Lean을 쓰는 결합 방식이 제시됐다.