예제 실행과 모델 검사
일반 검사가 선택한 입력을 실행한다면 Kani는 하네스가 허용하는 값들을 모델로 분석한다. 패닉과 산술 오버플로 및 여러 미정의 동작을 확인하고 사용자 단언도 검증 대상으로 삼는다. unsafe 코드처럼 컴파일러만으로 모든 안전 조건을 확인하지 못하는 부분을 조사하는 데 활용할 수 있다.
가정이 정하는 보증 범위
검증 함수가 어떤 입력을 만들고 어떤 조건으로 제한하는지에 따라 확인하는 영역이 달라진다. 결과가 성공하더라도 가정에서 제외한 상황까지 보장되는 것은 아니다. 실제 함수의 사용 조건과 맞는 가정을 작성하고 지나치게 강한 제한으로 문제가 사라진 것처럼 보이지 않는지 확인한다.
루프 경계와 미확정 결과
반복을 포함한 코드는 문제 크기와 펼침 한도를 정해야 할 수 있다. 한도가 부족하면 관련 조건을 충분히 분석하지 못해 미확정 결과가 남는다. 작은 크기에서의 검증을 더 큰 모든 입력에 대한 보증으로 확장해서는 안 된다. 실행 비용과 범위를 함께 기록하고 검증 실패가 실제 오류인지 부족한 경계 때문인지 구분한다.