Rust는 지난 몇 년 사이 시스템 프로그래밍의 표준 후보로 빠르게 자리 잡았다. C에 준하는 성능과 유연성을 제공하면서도, 정교한 타입 시스템이 메모리 관련 버그와 보안 취약점의 상당수를 컴파일 단계에서 걸러내기 때문이다. 그 결과 '평균보다 더 정확하고 안전한' 코드가 나온다. 문제는 실무자에게 '더 안전함'과 '실제로 올바름'은 전혀 다른 기준이라는 점이다. 아마존이 공개한 Verus 관련 글은 바로 이 간극을 겨냥한다.
Rust가 막지 못하는 것
Rust의 안전성 보장에는 분명한 경계가 있다. 예컨대 C에서 배열 범위를 벗어난 접근은 예측 불가능한 결과로 이어지는 위험한 실수지만, Rust에서는 프로그램을 즉시 중단시킨다. 확실히 더 안전하다. 그러나 애초에 올바른 프로그램이라면 그 범위 밖 접근을 시도하지도 않았을 것이다. 프로그램이 멈추는 것과 프로그램이 의도한 결과를 계산하는 것은 별개의 문제다. 마찬가지로 Rust는 코드가 기대한 값을 산출한다거나, 접근 권한을 가진 비밀 정보를 유출하지 않는다는 점까지 보장하지는 못한다. 타입 시스템은 특정 부류의 실수를 막을 뿐, 로직 자체의 정확성을 검증하지는 않기 때문이다.
Verus는 이 지점에 개입하는 오픈소스 자동 프로그램 검증기다. 프로그램 검증기는 코드가 어떻게 동작해야 하는지에 대한 수학적 명세(specification)를 입력받아, 가능한 모든 입력에 대해 코드가 그 명세를 만족하는지 기계적으로 확인한다. 정렬된 배열에서 특정 값을 찾는 이진 탐색을 예로 들면, 명세는 '함수가 어떤 인덱스를 반환할 때 그 위치의 원소는 찾던 값과 일치한다'고 규정할 수 있다. 검증기는 이 조건이 모든 배열과 모든 목표 값에 대해 성립하는지를 따진다.
테스트와 검증의 차이
전통적인 테스트는 몇 개의 구체적인 배열을 시도해 볼 뿐이어서, 목표 값이 배열의 마지막 원소이거나 아예 존재하지 않는 경우 같은 구석진 사례를 놓치기 쉽다. 반면 검증은 코드가 명세와 일치한다는 수학적 증명을 구성한다. 여기서 흥미로운 설계 지점이 드러난다. 이진 탐색 명세에는 함수가 값을 찾은 경우뿐 아니라 'None을 반환하면 목표 값이 배열에 없다'는 조항도 필요하다. 이 두 번째 조항이 없다면 언제나 None만 반환하는 엉터리 구현조차 명세를 만족시킬 수 있기 때문이다. 좋은 명세를 쓰는 일 자체가 사고를 요구하는 작업이라는 뜻이다.
Verus가 다른 Rust 검증 방식과 구별되는 핵심은, 명세와 증명을 별도의 언어가 아니라 Rust와 유사한 문법으로 소스 코드 안에 직접 작성한다는 점이다. 사전 조건은 'requires', 사후 조건은 'ensures' 키워드로 표현하며, 증명이 실패하면 개발자는 소스 수준의 Rust식 오류 메시지를 받는다. 일반 Rust 컴파일러는 이 주석을 무시하므로, Verus로 검증한 코드는 Cargo를 쓰는 프로젝트를 포함해 검증되지 않은 프로젝트에서도 그대로 소비할 수 있다. 코드를 가장 잘 아는 작성자가 증명 과정에 직접 참여하고, 증명이 코드와 늘 동기화된다는 점이 이 접근의 실무적 이점이다.
속도가 만드는 실용성
검증 도구의 성패는 결국 피드백 속도에 달려 있다. Verus는 여러 솔버를 활용해 증명 의무를 처리하며, 개발자는 보통 1초 이내에 결과를 받는다. VS Code 같은 개발 환경에서 '빨간 물결 밑줄'로 즉시 오류를 확인할 수 있을 만큼 빠른 것이다. 프로젝트 단위로 보면, 과거 검증기들이 함수 하나를 검증하던 시간에 수천 줄 규모의 코드와 증명을 처리한다. 저수준의 지루한 증명 단계는 도구가 자동으로 맡고, 귀납 증명 설정이나 루프 불변식 제공 같은 고수준 판단만 사람이 담당하는 구조다. 그리고 이 자동화 덕분에 AI 에이전트도 증명 작성에 뛰어들 여지가 생긴다. 반복 속도가 빠를수록 에이전트가 시도-수정을 거듭하기 유리하기 때문이다.
Verus의 쓸모가 특히 부각되는 영역은 Rust의 안전망이 걷히는 곳이다. 개발자가 고성능을 위해 명시적으로 'unsafe' 코드를 작성하면 컴파일러의 자동 검사에서 벗어나 정확성이 온전히 개발자 책임이 되는데, Verus는 이 unsafe 코드의 안전성을 수학적으로 증명해 기계 검증된 보장을 되살린다. 동시성 코드에서도 마찬가지다. Verus는 락(lock)에 불변식 속성을 부여해, 락을 획득한 쪽은 그 속성을 만족하는 값을 얻고 반환할 때도 여전히 만족함을 증명하도록 요구하며, 락 구현 자체의 정확성까지 증명할 수 있다. 고성능을 위해 복잡한 맞춤형 락 방식을 쓰는 Nitro Isolation Engine 같은 인프라에서 이런 보장은 특히 중요하다.
한계도 분명하다
아마존은 Rust Foundation 창립 멤버로서 Firecracker, 서버리스 분산 SQL 데이터베이스, Nitro Isolation Engine 등에 Rust를 폭넓게 쓰고 있으며, 이미 Verus로 Nitro Isolation Engine의 핵심 기본 요소와 여러 중요 인프라의 정확성을 증명했다고 밝혔다. 다만 실무자가 유념할 대목은 검증의 신뢰가 전제 위에 서 있다는 점이다. 여느 프로그램 검증기와 마찬가지로 Verus의 보장은 Verus 자체의 정확성, 개발자가 작성한 최상위 명세의 타당성, Rust 표준 라이브러리 같은 런타임에 대한 하위 가정, 그리고 컴파일러 툴체인의 정확성에 의존한다. 잘못된 명세를 증명하면 잘못된 코드가 '증명된' 것처럼 보일 수 있다는 뜻이다. 검증은 만능 스위치가 아니라, 명세를 제대로 세울 수 있는 팀에게 강력한 보증 수단이 된다. Verus가 학계와 산업계 연구자들의 협업으로 개발되는 무료 오픈소스라는 점은, 이 기술을 자사 코드에 실험적으로 적용해 보려는 조직에게 낮은 진입 문턱을 제공한다.