모델과 구현 연결
프로그램의 의미를 표현하는 모델을 바탕으로 성질을 조사한다. C는 주로 LLVM을 통해, Java는 JVM 코드를 통해, Rust는 MIR 기반 변환을 통해 연결한다. 특정 형식을 읽을 수 있다는 사실이 그 안의 모든 명령을 검증할 수 있다는 뜻은 아니다. 대상 언어 기능과 실행 경로가 지원되는지 확인한다.
스크립트로 구성하는 검증
SAWScript는 분석 자료를 불러오고 명세와 검증 작업을 연결하는 주된 인터페이스다. 필요한 가정과 확인할 결과를 코드로 남기면 반복 실행과 변경 추적에 도움이 된다. 명세가 실제 요구와 일치하는지, 외부 함수나 환경을 어느 범위까지 가정했는지 함께 살펴야 결과를 해석할 수 있다.
도구 체계의 일치
여러 증명기를 사용할 수 있지만 Cryptol 연동 때문에 Z3 설치가 필요하다. Rust 분석에서는 mir-json과 Rust 컴파일러 및 변환 자료의 스키마 버전을 맞춰야 한다. 예전 중간 파일이 새 도구에서 읽히지 않으면 대응하는 버전으로 다시 생성한다. 검증 입력과 소스 및 도구 구성을 함께 보존해 결과가 다른 구현에 잘못 적용되지 않게 한다.