모델의 자료 범위 확장
정수와 실수 및 미해석 함수 등을 이용해 유한 값만으로 표현하기 어려운 상태를 기술할 수 있다. 자료형을 넓힌다고 모든 모델의 검사가 쉽게 끝나는 것은 아니다. 실제 구현의 고정 폭 연산과 수학적 정수 및 실수는 의미가 다르므로 모델이 무엇을 나타내는지 확인한다.
여러 검증 절차
유한 상태와 무한 상태에 서로 다른 분석 기법을 제공한다. 경계 있는 검사와 귀납법 및 보간과 추상화 같은 절차는 보증 범위와 종료 조건이 다르다. 반례에 따라 추상화를 정교하게 만드는 경우에는 보고한 경로가 실제 동작인지 조사한다. 시간 제한 때문에 해결하지 못한 결과도 성공과 구분한다.
연동과 사용 조건
다른 검증 도구의 백엔드로 활용할 수 있으며 C99 API도 제공한다. 입력 모델과 명세 및 알고리즘 설정을 함께 관리해야 상위 도구의 결과를 해석할 수 있다. 공식 배포는 비상업적 또는 학술적 목적의 바이너리 라이선스로 안내되므로 사용 목적에 맞는 조건을 확인한다. 모델 검사 성공이 모델 밖의 구현과 환경까지 자동으로 검증하지는 않는다.