모델 탐색과 증명 확인
모델 검사기가 선택한 상태 공간을 탐색한다면 TLAPS는 작성자가 제공한 논증의 각 단계를 확인한다. TLAplus의 선언적이고 계층적인 증명 언어로 큰 논증을 작은 의무로 나눌 수 있다. 어떤 매개변수와 가정 아래에서 정리가 성립하는지 증명에 드러내야 한다. 잘못된 요구를 적으면 증명 성공도 의도한 설계를 보장하지 못한다.
증명 관리자와 여러 백엔드
관리자는 증명 상태와 의무를 다루고 SMT solver 및 Zenon, Isabelle의 TLAplus 논리 등으로 연결한다. 각 백엔드는 지원하는 논리와 처리 방식이 다르다. 한 단계가 자동으로 풀리지 않았을 때는 실제 논리 오류인지 추가 설명이나 다른 백엔드가 필요한지 구분해 조사한다.
지원 범위와 버전
TLAplus의 모든 구성과 시간 논리 추론을 모든 배포에서 동일하게 처리한다고 가정하지 않는다. 과거 안내와 개발 버전의 지원 범위가 다를 수 있으므로 실제 사용할 릴리스와 백엔드를 확인한다. 명세와 증명 및 도구 구성을 함께 유지하고 변경 뒤에는 현재 소스에 대해 다시 검사한다. 외부 구현이 명세를 따르는지 확인하는 일은 별도 과제로 남는다.