러스트 코드의 오류를 수학적으로 100% 증명해준다는 아마존의 신규 검증 도구 '베루스'

요약 아마존 사이언스 블로그에 따르면, 최근 소프트웨어 개발 현장에서 C 언어 수준의 고성능을 내면서도 타입 시스템으로 메모리 오류를 방지하는 러스트(Rust) 언어 도입이 늘고 있습니다. 하지만 러스트 역시 배열 인덱스 초과 시 충돌을 일으키며 멈추거나, 개발자가 의도한 정확한 연산 결과 도출 및 기밀 유출 방지까지 수학적으로 보장해주지는 못합니다. 이러한 한계를 해결하기 위해 등장한 오픈소스 자동 프로그램 검증 도구가 바로 '베루스(Verus)'입니다. 베루스는 작성된 러스트 코드가 사전에 정의된 수학적 명세서와 일치하는지 모든 가능한 입력값에 대해 기계적으로 전수 검증합니다. 개발자는 러스트 문법과 유사한 형태로 선행 조건(preconditions)과 후행 조건(postconditions)을 소스코드에 직접 어노테이션으로 명시할 수 있으며, 1초 미만의 빠른 피드백 루프를 제공합니다. 또한 최근에는 AI 에이전트가 증명 생성 과정을 보조하는 데에도 활용되고 있습니다. 특히 러스트에서 성능 최적화를 위해 안전성 검사를 우회하는 'unsafe' 코드 블록이나 복잡한 동시성 잠금 체계도 베루스를 통하면 기계적으로 검증된 안전성을 다시 확보할 수 있습니다. 아마존은 핵심 인프라인 AWS 니트로 격리 엔진(Nitro Isolation Engine)의 주요 기본 구성 요소 검증에 베루스를 실적용하고 있으며, 인증서 유효성 검증 라이브러리, 데이터 포맷 파서, 쿠버네티스 컨트롤러 등 다양한 오픈소스 분산 시스템 프로젝트로도 활용 범위가 확장되고 있습니다.