Boris Cherny가 Opus 5.5로 Claude Agent SDK 일부를 TLA+와 Lean으로 모델링한 게시물이 약 100만 조회를 얻으며 30년 된 형식 모델링 도구 TLA+가 주목받고 있다. TLA+는 시스템이 할 수 있는 동작과 항상/언젠가 만족해야 할 속성을 명세하지만 실제 구현의 정확성까지 보장하지는 않는다. Reasonable은 에이전트 파이프라인으로 TLA+ 명세·속성 쌍 16,000여 개를 기계 검증된 Verus 증명 3,000여 개로 변환했다고 소개한다.
Boris Cherny가 Opus 5.5로 Claude Agent SDK 일부를 30년 넘은 형식 모델링 도구 TLA+와 증명 시스템 Lean으로 모델링한 게시물이 약 100만 조회와 수천 건의 북마크를 얻었다. Datadog의 '하네스 우선' 에이전트도 에이전트 코딩에서 TLA+를 활용한 초기 사례로 함께 거론된다.
TLA+는 상태와 전이로 시스템 동작을 기술하고, 나쁜 일이 절대 일어나지 않는 안전성과 좋은 일이 결국 일어나는 활성성을 검사한다. 다만 표준 모델 검사기 TLC는 유한 인스턴스만 탐색하며, 모델을 검증할 뿐 실제 코드가 그 모델과 같은지는 자동 보장하지 않는다. Verus에서는 명세·증명·Rust 구현을 한 언어에 두어 이 간극을 좁힐 수 있다.
핵심은 에이전트가 TLA+를 쓸 수 있느냐를 넘어, 명세·증명·실제 프로그램 사이를 오갈 때 무엇이 가능해지느냐다. Reasonable은 에이전트 파이프라인으로 TLA+ 명세/속성 쌍 16,000여 개를 기계 검증된 Verus 증명 3,000여 개로 변환했다며, 정제 증명과 증명 동반 코드 생성 방향을 제시한다.