Reasonable은 TLA+가 시스템의 상태 전이와 안전성 및 진행 속성을 기술하지만 실제 구현 전체를 자동으로 검증하는 도구는 아니라고 설명했습니다. 주요 모델 검사기는 유한한 사례를 탐색하므로 명세와 구현의 간극이 남습니다. 팀은 Verus에서 Rust 구현과 증명을 연결하는 방향을 소개하며 16,459개 명세와 속성 쌍에서 3,000개 넘는 기계 검증 증명을 만든 에이전트 파이프라인을 보고했습니다. 수치는 회사의 연구 결과이며, 가정을 바꾸거나 검증을 무력화하는 편법을 별도 통제해야 합니다.