TLA+와 TLC는 개발자가 고른 입력만 실행하는 단위 테스트와 달리 유한 모델이 허용하는 실행 순서를 탐색해 불변 조건을 깨는 반례를 찾습니다. 각각 순서를 지키는 10단계 작업 두 개만 섞어도 18만4756가지 실행이 생기며, RxJS 공유 연결이 먼저 끝난 작업 때문에 닫히는 사례는 ‘작업이 하나라도 실행 중이면 연결은 열려 있어야 한다’는 작은 명세로 재현할 수 있습니다. AI는 모델 초안 비용을 낮추지만 명세의 타당성 검토는 여전히 필요합니다.