Rust의 소유권 타입 시스템 (ownership type system)은 안전한 코드에서 메모리 오류를 방지하지만, 특정 바람직한 속성들은 컴파일과 별개로 남아 있습니다: unsafe 연산(예: raw pointer 역참조)의 건전성 (soundness), 기능적 정확성 (functional correctness), 그리고 런타임 패닉 (runtime panics)의 부재입니다. 우리는 경계 모델 체킹 (bounded model checking)을 버그 탐지를 넘어 이러한 속성들에 대한 정확성 보장을 제공하도록 확장한 Rust용 오픈 소스 모델 체커인 Kani를 선보입니다. Kani는 Rust의 중간 단계 중간 표현 (Mid-level Intermediate Representation, MIR)으로부터 증명 하네스 (proof harnesses)를 CBMC의 비트 정밀 검증 엔진 (bit-precise verification engine)으로 컴파일하며, 사용자의 어노테이션 (annotation) 없이도 포괄적인 안전 속성 세트를 자동으로 확인합니다. 검증을 경계 (bounded)에서 무경계 (unbounded)로 확장하기 위해, Kani는 함수 계약 (function contracts), 루프 계약 (loop contracts), 한정사 (quantifiers), 그리고 함수 스터빙 (function stubbing)으로 구성된 명세 언어 (specification language)를 제공합니다. 우리는 산업용 Rust 프로젝트에 대한 사례 연구를 통해 실현 가능성을 입증하였으며, 여기서 계약 (contracts)을 통해 검증 수준을 패닉 프리 (panic-freedom)에서 기능적 정확성 (functional correctness)으로 업그레이드하여 이전에 알려지지 않았던 6개의 버그를 발견했습니다. Kani는 실제 프로덕션 CI 환경에서도 대규모로 작동하며, Rust 표준 라이브러리 검증 캠페인에서는 코드 변경당 16,000개 이상의 하네스가 검증되고 있습니다.