프로그램과 논리 조건
WhyML로 프로그램과 명세를 직접 작성하거나 다른 언어의 검증기에서 중간 표현으로 사용할 수 있다. 정수와 실수 및 집합 같은 논리 이론과 기본 자료 구조를 위한 라이브러리를 제공한다. 명세에 적은 조건이 구현에서 성립하는지 확인하는 도구이며 요구사항 자체를 자동으로 결정하지는 않는다.
여러 증명기와 연결하기
생성한 검증 조건을 자동 증명기나 대화형 증명기에 전달한다. 어떤 도구가 조건을 해결했는지와 해결하지 못한 조건이 무엇인지 구분해 읽는다. 증명 시간이 끝났다는 결과를 반례 발견과 같은 의미로 보지 않는다. 입력 가정과 변환 및 증명기 구성이 바뀌면 이전 결과가 그대로 유효한지도 확인한다.
실행 코드와 다른 언어
작성한 WhyML 프로그램에서 OCaml 코드를 추출하는 흐름을 제공하며 검증 플랫폼을 라이브러리로 사용할 수도 있다. Rust나 Ada처럼 다른 언어의 검증 과정에서도 활용된다. 중간 모델의 검증과 원래 구현의 대응 관계는 해당 도구 체계가 유지해야 한다. 검증한 성질과 외부 환경의 동작을 구분해 보증 범위를 관리한다.