힐렐 웨인은 TLA+가 불변식과 동작, 활성 속성을 표현하는 데 강하지만 모든 요구사항을 그대로 검증하지는 못한다고 설명합니다. 어떤 실행이 존재하는지 묻는 조건, 여러 실행을 비교하는 하이퍼속성, 확률적 성질은 기본 표현만으로 다루기 어렵고 보조 변수나 모델 변환에도 비용이 따릅니다. 관련 형식 기법 해설도 명세 검증이 구현 테스트를 대체하지 않는다고 강조합니다. 핵심은 도구에 맞춰 요구를 억지로 단순화하지 않고, 표현, 모델, 구현 각각의 보장 범위를 분리하는 것입니다.