Boris Cherny 트윗으로 떠오른 TLA+, Reasonable은 명세에서 기계 검증 증명까지 잇는 에이전트 파이프라인 공개

CSP(communicating sequential processes)를 발견할 차례 아닌가? CSP는 계속 재발견되는데 대표적인 게 Go였지.

TLA+ 배우는 중인데 CSP는 모름. 둘 중 뭐가 더 나음?

그냥 pi-calculus로 바로 넘어가는 게 빠르더라.

글이 너무 안 읽힘. 쓰기 수업부터 들으라고 하고 싶다.

AI 써서 글 쓴다고 까이더니, 진짜 사람이 쓴 글도 똑같이 까이네. 이 독자를 상대로는 이기기 힘들다.

TLA+ 정의하나 찾는 데 10분 걸렸음. 반응형 시스템을 설계·모델링·문서화·검증하는 형식 명세 언어가 답이더라.

TLA+는 수학자가 설계한 단위 테스트라고 보면 됨.

나는 Quint로 간접적으로 TLA+를 씀. 기능 구현 전에 Quint로 모델링하고 반례 없을 때까지 돌리라는 지시만 넣었는데 트랜잭션·원자성 버그가 잔뜩 잡혔음. 다만 Cloudflare D1/KV 타임아웃 같은 외부 장애는 힘을 못 씀.

TLA+가 뭔지 정의하기 전에 약어가 17번 나옴. 그것도 저 세 글자의 또 다른 쓰임새를 아는 사람이 보면 더 웃김.

예제 읽는 건 되는데, 쓸 만한 invariant를 직접 쓰는 단계가 여전히 제일 어려움.

분산 시스템에 TLA+ 많이 써봤는데 지금도 그 용도가 제일 낫다고 봄. 문제는 코드가 증명한 것과 일치하는지 확인하기가 겁나 어렵다는 거.

클러스터링·페일오버 로직에 Opus에 TLA+를 물려서 치명적 버그를 막았음. 예전 구조에서는 애초에 불가능했던 버그였고 단위 테스트로는 찾을 리가 없었는데 오직 TLA+ invariant가 잡아냄.

UI가 있는 프로젝트면 TLA+가 의외로 잘 먹힘. 상태가 복잡한 SPA면 금방 겸손해질 걸.

Astra로 TLA+랑 Lean 검증 테스트를 붙였더니 버그 33종류가 나옴. 100% 커버리지랑 속성 기반 테스트를 다 돌린 상태였는데도 그랬음.

formalize한 대상이 실제랑 맞는지 확인도 안 하면서 도는 건, 에이전트를 진짜 많이 믿는 거지. 실제 검증 가능한 버그가 나왔다면 그나마 다행임.

vibe-coded TLA+는 에이전트가 일을 더 잘하게 하는 도구일 뿐이고, 코드가 '맞다'는 뜻의 증명은 아니라는 데는 다들 동의하자.