Rust 코드의 '진짜 올바름'을 증명한다 — Verus 프로젝트 들여다보기

테스트로는 부족한 순간이 있어요

우리가 보통 코드가 맞는지 확인할 때 쓰는 방법은 테스트예요. 유닛 테스트, 통합 테스트, 프로퍼티 테스트까지 잘 깔아두면 대부분 버그를 잡을 수 있죠. 그런데 가끔은 이걸로 부족한 영역이 있어요. 예를 들어 운영체제 커널, 블록체인 컨센서스, 암호화 라이브러리, 금융 시스템의 잔고 계산 같은 곳은 "거의 다 맞음"이 허용되지 않아요. 엣지 케이스 하나가 전체를 무너뜨릴 수 있거든요.

이런 영역에서 쓰는 기법이 형식 검증(formal verification)이에요. 수학적으로 "이 함수는 모든 가능한 입력에 대해 이런 성질을 만족한다"를 증명하는 방식이에요. 기존에는 Coq, Isabelle, Lean 같은 증명 보조기를 쓰거나, Dafny, F\* 같은 전용 언어를 썼어요. 다 훌륭하지만, 실제 서비스 코드는 C나 Rust로 짜고 증명만 따로 한다는 괴리가 컸어요. 그래서 "증명한 코드"와 "실제 돌아가는 코드" 사이에 번역 오류가 생길 수도 있었고요.

Verus는 이 간극을 메우려는 프로젝트예요. Rust 코드 위에 직접 사양(specification)을 적고, 그걸 SMT 솔버가 자동으로 검증해주는 도구예요. 마이크로소프트 리서치와 CMU, UW 등이 협력해서 만들고 있고, 이미 오픈소스로 공개돼 있어요.

어떻게 생긴 도구인가

Verus는 Rust 컴파일러 위에 붙는 레이어예요. 기존 Rust 코드에 requires, ensures, invariant, decreases 같은 키워드로 사전조건, 사후조건, 루프 불변식, 종료 증명 조건을 붙여요. 예를 들어 정렬 함수를 작성한다면 "출력은 입력의 순열이다"와 "출력은 오름차순이다"라는 두 조건을 ensures에 적고, Verus가 이걸 만족하는지 자동 증명해주는 식이에요.

내부적으로는 Rust 코드를 중간 표현으로 바꾸고, 조건들을 Z3 SMT 솔버에 넘겨서 풀어요. SMT 솔버는 "이 조건이 거짓이 될 수 있는 입력이 존재하는가?"를 자동으로 탐색하는 도구인데, 반례가 없으면 증명 성공이에요. 이 과정이 재미있는 이유는, 개발자가 루프 불변식이나 보조 정리(lemma)를 힌트로 제공해야 솔버가 풀 수 있는 경우가 많다는 점이에요. 완전 자동은 아니지만, Coq처럼 한 줄 한 줄 손으로 증명하는 것보다는 훨씬 생산적이에요.

또 하나 중요한 설계 선택은 소유권과 라이프타임을 그대로 활용한다는 점이에요. Rust의 보로우 체커가 이미 메모리 안전성을 보장해주기 때문에, Verus는 그 위에서 "이 함수의 비즈니스 로직이 올바른가?"에만 집중할 수 있어요. 보통 검증 언어가 메모리 모델링부터 다시 해야 하는 것과 대조적이에요.

Ghost 코드와 실행 코드의 분리

Verus의 또 다른 특징은 spec 코드, proof 코드, exec 코드를 명시적으로 구분한다는 점이에요. spec 함수는 증명용으로만 쓰이는 수학적 함수라 런타임에는 실행되지 않고, exec 함수가 실제 바이너리에 컴파일되는 코드예요. 덕분에 증명을 위해 느린 수학 표현을 써도 실제 성능에는 영향이 없어요. 예를 들어 "이 해시 테이블 구현이 정말로 순수 함수형 맵과 동등하게 동작한다"를 증명할 때, 스펙 쪽은 그냥 Seq<K, V>처럼 느리지만 명확한 표현을 쓰고, exec 쪽은 고성능 해시 구조를 쓰는 거죠.

업계 흐름에서의 위치

형식 검증은 오래된 분야지만, 최근 몇 년 실무 언어에 직접 붙는 검증 도구가 늘고 있어요. 자바의 KeY, C의 Frama-C, Ada의 SPARK가 기존 사례였고, Rust 쪽에는 Prusti, Creusot, Kani가 앞서 나왔어요. Verus는 이 중에서 SMT 솔버 활용과 자동화 수준이 높은 편이고, 특히 시스템 프로그래밍(파일시스템, 분산 합의, 커널)을 타겟으로 한다는 점이 차별화 포인트예요. 실제로 MS 연구팀은 Verus로 검증된 분산 KV 스토어나 파일시스템 프로토타입을 논문으로 발표해오고 있어요.

한편 AWS는 Kani라는 모델 체커를, Aria Network 같은 블록체인 프로젝트는 Move Prover를 쓰는 등, 인프라 레벨에서 검증 도입이 늘고 있어요. LLM이 코드를 생성하는 시대에, AI가 짠 코드를 사람이 다 읽을 수 없으니 자동 검증으로 안전망을 치자는 흐름과도 맞물려요.

한국 개발자에게 시사하는 것

대부분의 웹 서비스 개발에는 Verus를 쓸 일이 없을 거예요. 투자 대비 비용이 맞지 않거든요. 하지만 블록체인, 스마트 컨트랙트, 임베디드 제어, 보안 프로토콜을 다루는 분들에게는 지금 익혀둘 가치가 충분해요. 특히 Rust를 쓰는 국내 팀(토스 보안 인프라, 크래프톤 분산 시스템, 일부 블록체인 팀)에서는 점진적으로 도입해볼 수 있는 선택지예요.

초심자에게도 추천하는 이유는, Verus 튜토리얼을 따라가다 보면 "내 코드는 정확히 무엇을 약속하고 있는가?"를 언어로 적는 훈련이 되거든요. 이건 검증 도구를 실제로 쓰지 않더라도, 주석과 타입과 테스트를 설계하는 방식에 큰 영향을 줘요.

마무리

핵심 한 줄은, Verus는 Rust로 짠 실제 코드에 수학적 증명을 직접 붙일 수 있게 해주는 도구예요. 여러분의 프로젝트 중에 "여기만은 절대 틀리면 안 된다" 싶은 모듈이 있다면 어디일까요? 그 모듈이 바로 형식 검증의 후보예요.