읽는 명세와 실행하는 명세
자연어 설명만으로는 비트 연산이나 자료 배치의 의미가 모호해질 수 있다. Cryptol로 알고리즘을 표현하면 참조 명세를 실제로 실행하며 설계를 확인할 수 있다. 이를 이용해 검사 벡터를 만들거나 구현과 비교할 자료를 준비한다. 명세를 실행할 수 있다는 사실과 명세가 의도에 맞는다는 사실은 구분한다.
무작위 검사와 증명
check는 무작위 입력을 생성해 작성한 술어를 검사한다. prove는 SMT solver를 이용해 허용한 입력 전체에서 성질이 성립하는지 확인하는 방식이다. 일부 입력의 검사 통과를 전체 증명과 혼동하지 않는다. 증명도 타입과 가정 및 작성한 조건의 범위에 해당하며 해결되지 않은 결과는 별도로 조사한다.
구현과의 대응
Cryptol 명세가 맞더라도 별도로 작성한 C나 Java 구현이 자동으로 같은 동작을 하는 것은 아니다. SAW 같은 연계 도구를 사용해 구현과 명세의 대응을 확인하는 흐름이 있다. 사용한 참조 명세와 구현 버전 및 solver 환경을 함께 보존한다. 알고리즘 수준의 성질과 실제 시스템의 키 관리 및 실행 환경에서 생기는 문제도 구분한다.