Boris Cherny의 트윗으로 TLA+가 인터넷에 알려지다, 그 다음은?
The internet discovers TLA+. Now what?
Boris Cherny가 Claude Agent SDK 일부를 TLA+와 Lean으로 모델링한 트윗이 100만 뷰를 기록하며 TLA+에 대한 관심이 폭발했다. Reasonable 팀은 TLA+의 기본 개념과 한계를 설명하고, 16,000개 이상의 TLA+ 명세를 3,000개 이상의 Verus 증명으로 자동 변환하는 파이프라인을 소개한다. 이는 명세와 구현 사이의 간극을 좁히는 중요한 진전이다.
TLA+ gives us a compact language for saying what a system is allowed to do and what must always or eventually be true of it.
HN 토론
62- lopatin
저는 모든 분들이 자기에게 그런 문제가 있다면, 자기 완결적이고 상태 기계 같은 문제에 이걸 시도해 보시길 권합니다. 제 회사에서는 몇몇 전문가들이 클러스터링과 페일오버 로직을 최적화하면서 상태를 조금 더 추가하고 있었습니다(따라서 복잡성도 증가했죠). 저는 그 분야의 전문가가 아님에도 불구하고, TLA+로 무장한 Opus를 그 문제에 투입해서 치명적인 버그를 찾아내고 막을 수 있었습니다. 그 버그는 시스템의 이전 구현에서는 불가능했던 것이었고, 그것을 유발하는 일련의 단계에 대해 단위 테스트를 작성할 생각을 아무도 하지 못했기 때문에 처음에는 눈에 띄지 않았습니다. 유일하게 그것을 잡아낸 것은 TLA+ 불변식이었는데, 네, 그것도 Opus가 작성한 것이었습니다.
덧붙이자면, 요즘 프로그래밍이 더 이상 성취감을 주지 않는다는 이야기가 많습니다. 하지만 위의 작업은 아마 제가 오랫동안 엔지니어링하면서 느낀 가장 즐거운 경험이었고, 개인적으로 AI 없이는 거의 불가능했을 것입니다. 아마 TLA+라는 것의 새로움 때문이었을 수도 있지만, 저는 이것이 단순히 Claude에게 예전에 수동으로 하던 일을 시키고 엔터를 누르는 것을 넘어서, 미래에 우리의 일이 실제로 어떤 모습일 수 있는지에 대한 단면을 보여준다고 생각합니다. 여기에는 훨씬 더 야심차고 성취감 있는 활용 사례들이 있습니다.
- stevefan1999
저는 https://github.com/quint-co/quint 를 통해 간접적으로 TLA+를 사용합니다. 저는 "어떤 기능이든 구현하기 전에 Quint를 사용해 모델링하고 시스템 전체에 대해 반례가 없는지 확인하세요. 또한 Quint로 설계를 반복하고 문서와 구현이 형식 모델과 문서를 따르는지 확인하세요"라는 지침을 추가했습니다.
그 결과는, 시간이 훨씬 더 오래 걸리긴 하지만, 꽤 마법 같습니다. 이런 단순한 지침 하나만으로도 많은 트랜잭션 및 원자성 버그가 발견되고 수정되었습니다.
하지만 때로는 특히 외부 리소스와 관련해서는 모든 것이 마법 같지는 않습니다. 안타깝게도 Cloudflare는 때때로 D1과 KV에서 타임아웃이 발생하는데, 이는 어느 정도 불가항력입니다.
다행히도, 그렇다면 저는 그 동작을 이진 이벤트로 모델링해야 합니다. 즉, 트랜잭션이 우리가 보장된다고 생각했던 대로 완료되지 않을 수 있으므로, 그 주위에 추가 가드를 넣어 상태를 재시도해야 합니다.
지금까지는 그런 식으로 우회할 수 있었습니다. 조건과 제약이 많을수록 NP 규모이기 때문에 CPU가 더 강력해야 할 수 있다는 점을 명심하세요.
- peterus
TLA+의 실제 응용 사례: https://foundation.tlapl.us/industry/index.html.
인텔 논문은 TLA+가 하드웨어 기술 설명을 작성하기 전 단계로 어떻게 적용되었는지 보여줍니다. 이것이 널리 퍼졌는지는 잘 모르겠습니다. 요즘에는 다른 도구들이 사용되는 것 같은데, 여기 VLSI 업계에 계신 분 중에 아시는 분 있나요?
- pron
저는 시스템을 정확하면서도 간결하게 설명하고 그것에 대해 추론하는 데 TLA+를 좋아합니다. 하지만 수년간 소프트웨어 개발을 돕기 위해 형식 방법을 사용해 온 사람으로서, 이렇게 멋진 수학적 언어와 Lean 같은 다른 언어들을 AI와 연결하여 사람들로부터 추론을 숨기는 수준에 이르기까지 하는 도구 산업 전체가 저를 혼란스럽게 합니다.
프로그램의 정확성을 종단 간(즉, 코드에서 고수준 속성까지) 증명하는 것은 — 이 회사와 다른 회사들이 하겠다고 주장하는 것처럼 — 너무 어려워서 인간은 아주 작은 프로그램(~10KLOC)에 대해서만 해낼 수 있었고, 그마저도 프로그램이 매우 특별한 방식으로 작성된(종종 성능을 희생하면서, 성능은 종종 더 복잡한 알고리즘을 필요로 하기 때문에) 매우 특수한 경우에만 가능했습니다. 만약 AI가 소프트웨어 개발에서 인간보다 최소한 한 자릿수 더 뛰어나게 된다면, 이 작업에 필요한 것이 바로 그것인데, AI가 이 작업을 돕는 다양한 도구와 하네스를 작성하는 데 우리의 도움을 필요로 할까요? 결국, 이런 도구를 작성하는 것은 그 목표를 위해 사용하는 것보다 훨씬 쉽기 때문에, 저는 여기서 AI 능력에 대한 가설을 이해하지 못하겠습니다.
이 회사는 "이러한 정확성 보장을 모든 소프트웨어 엔지니어가 접근할 수 있도록 하는 에이전트 프레임워크를 개발 중"이라고 말합니다. 하지만 그 모든 것을 개발하는 것은 쉬운 부분입니다! 만약 AI가 어려운 부분을 할 수 있다면, 왜 그것을 접근 가능하게 만드는 데 우리의 도움이 필요할까요? 분명히 그 쉬운 부분을 스스로 할 방법을 찾을 수 있을 텐데요! 마치 "곧 우리는 기계를 갖게 될 텐데 […]"라고 말하는 것과 같습니다.
- bsenftner
이걸 찾는 데 10분이 걸렸습니다: TLA+는 반응형 시스템을 설계, 모델링, 문서화 및 검증하기 위해 개발된 형식 명세 언어입니다.