최근 분산 시스템과 AI 에이전트 개발에서 시스템의 신뢰성을 확보하는 것이 중요해지면서, 형식 검증 도구 TLA+(Temporal Logic of Actions)에 대한 관심이 높아지고 있습니다. 이러한 흐름 속에서 AI 에이전트의 견고한 동작을 보장하기 위한 새로운 도구 'Untyped'가 공개되어 주목받고 있습니다. Untyped는 에이전트의 설계(하네스)와 실제 실행 기록을 TLA+ 명세에 따라 검증하여, 재시도(retries)나 시스템 충돌(crashes) 같은 예측 불가능한 상황에서도 에이전트가 올바르게 작동하는지 확인합니다.
Untyped는 특히 '내구성 있는 실행(durable-execution)' 런타임 환경에서 에이전트와 외부 도구 간의 프로토콜을 모델링하고 검증하는 데 초점을 맞춥니다. Temporal, Inngest, Restate, DBOS, LangGraph 같은 런타임은 호출이 중복되거나 유실될 수 있는 복잡한 환경을 제공하는데, Untyped는 이러한 환경에서 에이전트 하네스가 '한 번에 최대 한 번의 효과(AtMostOnce)', '승인 없는 파괴적 효과 금지(ApprovalBeforeEffect)', '예산 초과 호출 금지(BudgetHeld)'와 같은 핵심 불변식(invariant)을 지키는지 확인합니다. 이 도구는 설계 단계의 모델 검증뿐만 아니라, 실제 시스템의 실행 로그(JSONL 파일)를 분석하여 명세 위반 여부를 찾아내는 '추적 검증(trace validation)' 기능도 제공합니다. 예를 들어, 환불 요청이 두 번 처리되는 등의 실제 오류 시나리오를 발견할 수 있습니다.
이러한 검증 방식은 LLM(대규모 언어 모델) 자체의 동작보다는 LLM을 둘러싼 시스템, 즉 에이전트가 외부 도구와 상호작용하는 방식의 안정성을 높이는 데 핵심적인 역할을 합니다. 복잡한 분산 환경에서 에이전트가 예상치 못한 동작을 일으키는 버그는 찾기 어렵고 치명적일 수 있습니다. Untyped는 이러한 버그를 사전에 발견하고 수정함으로써, 개발자들이 더욱 신뢰할 수 있는 AI 에이전트 시스템을 구축하고 운영할 수 있도록 돕습니다. 이는 결국 AI 시스템의 상용화와 확산에 필수적인 요소로 작용할 것입니다.