명세와 실행 모델
TLAplus 명세에서 검사할 상수와 자료 범위를 정해 모델을 구성한다. TLC는 이 모델에서 상태와 전이를 탐색한다. 작은 범위에서도 설계 오류를 찾는 데 도움이 되지만 선택한 크기의 결과가 모든 매개변수에 대한 일반 증명은 아니다. 초기 조건과 환경 동작이 실제 요구를 나타내는지도 확인한다.
모델 검사와 시뮬레이션
모델 검사에서는 선택한 상태 공간의 성질을 분석하고 시뮬레이션에서는 가능한 실행을 관찰한다. 여러 실행을 살펴본 결과를 전체 탐색 결과와 구분한다. 명세가 구문 분석을 통과한 사실도 안전성 검증과는 다르다. 실행 가능한 명세의 지원 범위와 검사할 속성이 무엇인지 설정에 명시한다.
도구 구성과 재현
Java 기반 TLAplus 도구 모음에 포함되어 명령행에서 실행할 수 있다. 다른 도구인 Apalache는 기호 모델 검사를 수행하고 TLAPS는 작성한 증명을 확인한다. 목적에 맞는 도구를 선택한다. 모델과 설정 및 도구 버전을 함께 보존하고 오류 경로가 보고되면 실제 구현에서 가능한 동작과 어떻게 대응하는지 검토한다.