인터넷이 TLA+를 발견했다. 이제 무엇을 할까?

TLA+ 는 시스템이 할 수 있는 동작과 항상 또는 언젠가 만족해야 할 속성을 명세하는 언어로, 에이전트 코딩에서도 형식 모델의 활용 가능성이 주목받고 있음 시스템의 상태와 전이를 모델링하고, 잘못된 일이 발생하지 않는 안전성과 좋은 일이 결국 발생하는 활성성을 검사함 표준 모델 검사기 TLC는 유한한 모델만 탐색하며, 모델 검증만으로 실제 구현의 정확성까지 보장하지는 않음 Verus에서는 명세, 증명, Rust 구현을 함께 둘 수 있어, 실제 코드가 추상 모델을 따르는지 증명하는 방향으로 나아갈 수 있음 반복적인 증명 작업은 AI 에이전트 자동화에 적합하며, 명세와 증명, 구현을 연결하면 정제 증명, 증명 동반 코드 생성, 프로토콜 탐색으로 확장할 수 있음 에이전트 코딩에서 주목받는 TLA+ Boris Cherny는 TLA+ 관련 게시물에서 Opus 5.5를 사용해 Claude Agent SDK 일부를 TLA+와 Lean으로 모델링함 게시물이 약 100만 조회와 수천 건의 북마크를 얻으며, 30년이 넘은 형식 모델링 도구가 관심을 모음 Datadog의 하네스 우선 에이전트도 에이전트 코딩에서 TLA+를 활용한 초기 사례임 중요한 질문은 에이전트가 TLA+를 작성할 수 있는지를 넘어, 명세, 증명, 실제 프로그램 사이를 오갈 때 무엇이 가능해지는지임 Reasonable은 에이전트가 이를 일관되고 신뢰성 있게, 빠르게 수행하도록 모델을 훈련하고 있음 TLA+의 기본 구조와 리더 선출 예제 TLA+(Temporal Logic of Actions) 는 전이 시스템과 시간적 속성이라는 두 종류의 대상을 기술함 전이 시스템은 시스템의 스냅샷인 상태와, 상태를 바꾸는 한 단계인 동작으로 구성됨 시간적 속성은 실행이 시간에 따라 어떻게 진행되어야 하는지를 규정함 대화형 실습은 세 컴퓨터 a, b, c가 리더를 선출하는 과정을 5개 단계로 구성함 상태에는 후보, 투표 대상, 리더가 포함되고, 동작에는 선거 시작과 투표가 포함됨 데이터베이스는 올바른 리더 선출에 의존하며, 예제는 두 리더가 동시에 존재하지 않아야 한다는 조건을 요구함 사용자는 동작을 직접 실행하며 테스터처럼 하나의 가능한 실행 경로를 탐색할 수 있음 모델은 허용되는 상태와 전이를 정의함 초기 상태에서는 a, b, c 중 어느 컴퓨터든 자신에게 투표하며 선거를 시작할 수 있고, b는 a나 c에게 투표할 수 있음 전이의 순서를 고정하거나 사건 발생의 확률분포를 모...