설계를 명확히 표현하기
구현 자료형이나 세부 코드보다 시스템이 무엇을 하고 어떻게 동작해야 하는지를 모델로 적는다. 막연한 설계에 숨어 있는 근본적인 오류를 발견할 수 있도록 설명을 정확하게 만드는 목적이다.
상태의 연속으로 보는 동작
초기 상태의 조건과 다음 상태로 갈 수 있는 관계로 가능한 실행들을 표현한다. 한 번의 실행은 상태의 연속이며 각각의 단계는 연속한 두 상태의 관계로 볼 수 있다.
불변성과 진행 속성
모든 가능한 상태에서 지켜야 할 불변성과 언젠가 일어나야 할 일을 다루는 진행 속성을 표현할 수 있다. 어떤 속성을 검사하는지에 따라 모델이 확인하는 요구도 달라진다.
도구와 알고리즘 표현
TLC 같은 모델 검사기와 증명 도구로 명세를 확인한다. 알고리즘을 적는 PlusCal은 TLA+ 모델로 번역되며 동시성과 비결정성을 표현하는 다른 진입점이 된다.