kani

Kani는 모델 검사 조직에서 개발된 Rust 프로그램용 비트 정밀 모델 검사기이다. 개발자가 Rust 코드의 안전성과 정확성을 모두 확인할 수 있도록 설계되었다. 안전성 측면에서 Kani는 다양한 종류의 정의되지 않은 동작을 자동으로 검사한다. 이는 컴파일러가 일반적인 안전 보장을 강제하지 않는 Rust의 unsafe 코드 블록을 검증하는 데 특히 유용하다. 정확성 측면에서는 패닉(예: None에 unwrap() 호출), 산술 오버플로, 그리고 단언(assert!(...))이나 함수 계약으로 표현된 사용자 정의 정확성 속성을 자동으로 검사한다. 사용법은 테스트와 유사한 워크플로를 따른다. 개발자는 #[kani::proof]로 주석이 달린 하네스를 작성하고 kani::any()를 사용하여 비결정적 입력을 생성한다. 그런 다음 Kani는 모든 유효한 입력이 패닉이나 예기치 않은 동작 없이 명세를 충족하는 출력을 생성함을 증명하려고 시도한다. 튜토리얼과 참조 문서는 Kani book에서 확인할 수 있다. 설치는 Cargo를 통해 이루어진다: cargo install --locked kani-verifier 후 cargo kani setup을 실행한다. 이 도구는 Linux 또는 macOS에서 Rust 1.58+를 지원한다. GitHub Action(model-checking/kani-github-action)을 통해 CI 파이프라인에 통합할 수 있다. 이 프로젝트는 MIT와 Apache 2.0 라이선스로 배포되며, Rust 프로젝트의 코드를 포함한다. 학술 인용(ASE 2026 논문)이 있으며 기여자를 위한 개발자 문서를 제공한다.