원래 코드와 검증 모델 사이
다른 언어의 검증기는 소스의 동작과 계약을 Boogie 모델로 옮길 수 있다. 공통 중간 언어를 사용하면 각 언어마다 모든 증명 절차를 새로 만드는 부담을 줄인다. 하지만 원래 언어의 의미를 올바르게 옮겼는지는 변환하는 검증기의 역할이다. 중간 모델의 성공을 소스 전체의 보증으로 해석하려면 이 연결도 확인해야 한다.
검증 조건과 solver
도구는 일부 불변식을 추론하고 검증 조건을 생성해 외부 증명기로 보낸다. 기본 구성은 Z3를 사용하며 다른 증명기 지원은 조건과 성숙도가 다르다. 시간 안에 증명하지 못한 결과와 실제로 조건이 깨지는 결과를 구분한다. 입력의 가정과 단언이 실제 확인하려는 요구를 나타내는지도 중요하다.
순차 코드와 동시성 확장
순차 프로그램의 모델링과 검증에 사용되어 왔으며 Civl 확장을 통해 동시 및 분산 시스템도 다룬다. 확장 기능이 존재한다고 임의의 병렬 프로그램을 자동으로 완전히 검증하는 것은 아니다. 사용하는 모델과 지원 범위를 맞추고 도구 및 solver의 버전을 함께 기록해 결과를 재현한다.