Amazon, Rust 코드의 정확성을 수학적으로 증명하는 Verus 공개

Developing provably correct Rust code with Verus

Rust는 C에 버금가는 성능과 안전성을 제공하지만, '더 안전하다'는 '실제로 올바르다'와는 다르다. Amazon이 밀고 있는 오픈소스 자동 프로그램 검증기 Verus는 수학적 명세에 따라 모든 입력에 대해 코드가 맞는지 기계적으로 검사한다. 개발자는 Rust와 유사한 문법으로 사전·사후 조건을 주석처럼 달고, 1초 이내의 빠른 피드백을 받으며, AI 에이전트의 도움으로 증명을 생성할 수도 있다. Verus는 Rust의 unsafe 블록과 커스텀 잠금을 쓰는 동시성 코드까지 검증해, AWS Nitro Isolation Engine 같은 성능-critical 구현에 기계 검증된 안전성을 되돌려준다.