최근 연구를 통해 확률적 프로그램을 형식적으로 검증하는 많은 기법들이 개발되었습니다. 하지만, 기존의 확률적 프로그램 검증 프레임워크들은 검증을 위해 설계된 이상적인 언어에 국한되어 있습니다. 그 결과, 표준 언어로 작성된 상용(off-the-shelf) 확률적 프로그램들을 검증하는 데 사용될 수 없습니다. 반면에, 비확률적 프로그램의 경우, 현재 Go, C, Rust와 같이 널리 사용되는 언어로 작성된 실제 코드를 검증하는 것을 지원하는 많은 검증 도구들이 존재합니다. 이러한 언어들로 작성된 확률적 프로그램을 검증하기 위해서는, 그러한 도구들에 투입된 광범위한 개발 작업을 최대한 재사용할 수 있는 것이 유용할 것입니다. 본 논문은 확률적 Rust 프로그램 검증을 위한 프레임워크인 Alerus를 제시합니다. Alerus는 SMT 기반 자동화와 separation-logic에서 영감을 받은 추론 기능을 지원하는 Rust의 검증 도구 Verus를 기반으로 합니다. Alerus는 이러한 표현력 있는 기능들을 유지하면서 확률적 추론에 대한 지원을 추가하여 Verus를 확장합니다. 이를 위해, Alerus는 Eris 프로그램 논리에서 도입된 무작위화 추론을 위한 일종의 유령 상태(ghost state) 형태인 확률적 오류 크레딧(probabilistic error credits)의 경량 인코딩을 사용합니다. 오류 크레딧을 사용하여 적절한 명세(specification)를 도출함으로써, Alerus는 무작위 샘플링 알고리즘의 정확성 검증을 지원합니다. 우리는 이 기법을 활용하여 이산 분포에 대한 여러 샘플링 루틴들, 여기에는 이산 가우시안 분포용 샘플러, alias method, 그리고 fast loaded dice roller를 포함한 것들을 검증합니다. 우리는 Verus의 최근 개발된 논리 관계 모델인 VerusBelt를 적응함으로써 오류 크레딧 확장의 건전성(soundness)을 입증합니다. VerusBelt는 그 기능을 Iris separation logic의 관점에서 인코딩합니다. 이를 위해, 우리는 이 모델에서 Iris의 표준 약한 전제조건(weakest precondition) 사용을 Eris의 확률적 약한 전제조건으로 대체합니다. 결과로 나온 건전성 증명은 Rocq에서 완전히 기계화되었습니다.