Rust 검증 도구 Creusot 0.14 공개, 증명 작성·코드 탐색 개선

Rust 코드의 동작을 수학적으로 검증하는 오픈소스 도구 Creusot이 0.14.0 버전을 공개했다. 프로젝트 공식 개발 블로그와 GitHub 릴리스에 따르면, 10월 12일 배포된 이번 버전은 프로그램 안에서 논리적 증명을 적용하는 방식과 편집기의 명세 탐색 기능을 개선했다.

Creusot은 함수가 어떤 조건에서 호출되고 어떤 결과를 내야 하는지 명세로 작성한 뒤, 코드가 이를 만족하는지 확인하는 도구다. 프로그램을 실행하는 테스트와 달리 정적으로 검증하며, Why3 플랫폼과 SMT 솔버를 이용해 증명 조건을 처리한다. 개발자는 함수의 사전·사후 조건과 루프 불변식 등을 직접 작성해야 한다.

이번 버전의 핵심은 Rust 프로그램 안에 논리식을 넣는 ‘스냅샷(snapshot)’에서 검증 조건을 생성하는 기능이다. 이를 통해 증명에 쓰이는 논리 함수를 스냅샷 안에서 호출하고, 호출에 필요한 전제 조건과 그로부터 얻는 결론을 해당 인수에 맞춰 적용할 수 있다.

기존에도 일반 Rust 함수를 이용해 비슷한 증명을 작성할 수 있었지만, 실제 함수 호출이 생기고 빌림 검사기의 제약도 따라야 했다. 반면 스냅샷은 컴파일 과정에서 제거된다. 개발팀은 이 방식이 실행 코드와 증명 코드를 구분하고, 범위를 벗어난 인덱싱처럼 명세에 포함된 실수를 더 일찍 찾는 데 도움이 된다고 설명했다.

편집기 연동도 달라졌다. Creusot의 명세 언어 Pearlite에서 rust-analyzer의 ‘정의로 이동’을 사용할 수 있도록 매크로가 생성하는 코드의 위치 정보를 정밀하게 추적한다. 기존에는 한 표현식의 위치 정보가 여러 식별자에 걸쳐 있어 관련 없는 정의까지 탐색 결과에 나타났는데, 이번 수정은 이 문제를 줄였다.

공식 사용자 가이드는 프로젝트별 rust-analyzer 설정으로 Pearlite 코드의 저장 시 타입 검사와 정의 탐색을 활성화하는 방법을 안내한다. 설정에는 Creusot이 사용하는 nightly Rust 도구 체인을 지정해야 하며, 예시의 환경 변수 설정은 rustup 사용자 기준으로 제시됐다.

변경 로그에는 라이브러리 명세 보강과 ARM64 Linux 설치 지원, 동시성 검증 예제 추가도 포함됐다. 개발 블로그가 함께 소개한 부분 순서 지원은 이번에 처음 추가된 기능이 아니라 0.13.0부터 적용된 변경이다.

다만 Creusot은 여전히 실험적 소프트웨어다. 프로젝트는 자료구조나 알고리즘 구현의 검증에 더 적합하고 외부 환경과 빈번하게 상호작용하는 시스템에는 상대적으로 덜 적합하다고 명시했다. 모든 증명이 자동화되는 것도 아니다. 이번 릴리스는 Rust 프로그램의 정확성을 검토하는 작업 흐름을 개선한 것으로, 컴파일 성공만으로 임의의 프로그램이 올바르다고 보장하는 업데이트는 아니다.

출처: Creusot 공식 개발 블로그 https://devlog.creusot.rs/v0-14-0/ ; Creusot 공식 GitHub 릴리스 https://github.com/creusot-rs/creusot/releases/tag/v0.14.0 ; Creusot 0.14.0 공식 변경 로그 https://raw.githubusercontent.com/creusot-rs/creusot/v0.14.0/CHANGELOG.md ; Creusot 공식 홈페이지 https://creusot.rs/ ; Creusot 공식 사용자 가이드 https://guide.creusot.rs/quickstart/editor_config.html