실행 코드와 명세 구분
exec는 실제로 컴파일하고 실행할 코드이며 spec는 프로그램의 성질을 기술한다. proof는 그 성질을 만족함을 보이는 역할을 한다. 명세와 증명 코드는 실행 코드와 다른 용도를 가지므로 실행 시간에 검사를 더하는 방식과 구분한다. 검증하려는 요구를 명세로 옮기는 과정이 중요하다.
전체 입력과 전제조건
검증은 작성한 명세와 허용한 조건 아래에서 코드의 성질을 확인한다. 필요한 가정이 빠지면 증명이 어려워지고 가정이 과하면 실제 사용 범위를 충분히 다루지 못할 수 있다. 도구가 성공했다고 요구사항 자체가 옳다는 결론까지 자동으로 얻는 것은 아니다. 구현과 계약을 함께 검토한다.
지원 기능과 유지보수
Rust 전체를 제한 없이 지원하는 도구는 아니며 일부 저수준 코드도 별도 검증 구성을 통해 다룬다. 공식 안내는 개발 중인 기능과 문서의 불완전성을 설명한다. 도입할 때는 대상 코드가 지원 범위에 있는지 확인한다. 증명 코드와 실행 코드가 바뀔 때 같은 명세를 계속 만족하는지 다시 확인하는 흐름이 필요하다.