TLA+가 검증할 수 있는 것과 없는 것

HN의 이 댓글을 통해 Quint를 알게 됐음. 동작의 시제 논리(TLA)를 기반으로, JavaScript에서 동작하며 쓰기 좋은 도구를 갖춘 실행 가능한 명세 언어임. TLA+에 관심이 있다면 꼭 살펴볼 만함. https://github.com/quint-co/quint

TLA+를 실제로 써보려는 사람에게 좋은 글임. 다른 한계로는 원자적 연산과 약한 메모리 의미론처럼 순차적 일관성이 성립하지 않는 동작을 모델링하기 어렵다는 점이 있음. 알고리즘을 PlusCal로 옮기면 순차적 일관성이 있는 것처럼 실행되므로, 그렇지 않은 동작은 TLA+ 논리로 직접 명시해야 하는데 수작업으로 하기에는 복잡하고 오류가 나기 쉬워 보임.
C/C++/Rust 메모리 모델은 상당히 기묘한 동작도 허용함. 변수마다 읽기 캐시와 쓰기 버퍼를 넣고 적절한 위치에 캐시 비우기 명령을 추가해야 할 것 같은데, 더 우아한 방법이 있을지도 모르겠음. Rust에서는 Miri와 Loom으로 순차적 일관성을 따르지 않는 일부 동작을 검사할 수 있으며, Loom은 순차적 일관성 자체를 구현하지 않음.

내가 본 코딩 지침은 잠금에만 acquire/release를, 단순한 카운터에만 relaxed를 허용함. 잠금 없는 해시 테이블이나 RCU처럼 더 복잡한 경우에는 seq_cst를 요구함.
잠금 이외의 상황에서 acquire/release 의미론을 제대로 추론할 수 있는 사람은 극히 적으므로 좋은 제한이라고 봄.

마지막으로 메모리 순서를 검증해야 했을 때는 해당 문제에 맞춘 전용 분석기를 직접 만들었는데 쉽지 않았음. 상태 공간도 엄청나서 컴파일된 코드로 실행해도 일부는 단축해서 처리하고, 나머지는 손으로 증명해야 했음.

TLA+로 이런 시스템을 모델링하는 것은 가능하지만 사용하기 불편한 영역에 속함. 공유 변수를 읽고 쓰는 동시성 프로그램은 컴파일러와 CPU 두 단계에서 실행 순서가 바뀔 수 있음. 일반적인 TLA+ 명세는 각 스레드 내부에서는 선형 순서를 따르고, 스레드 사이에서만 임의로 실행이 섞인다고 가정함. 즉 PlusCal은 기본적으로 각 동작 사이에 배리어와 메모리 펜스가 모두 있는 것처럼 작동함. x86-TSO처럼 강한 메모리 의미론에서도 저장 버퍼를 명세하려면 작은 x86-TSO 구현을 직접 작성해야 함. 한 코어가 쓴 값을 자신은 읽을 수 있지만 다른 코어에는 아직 보이지 않는 동작을 쉽게 가져다 쓸 라이브러리가 없기 때문임.
최근 잠금 없는 알고리즘을 살펴보면서 이를 TLA+로 깔끔하게 명세할 방법을 고민하고 있음.

“테스트만 작성하면 된다”, 최근에는 “정형 검증을 쓰면 된다”며 구현 전체를 LLM에 맡겨도 충분히 안전하다고 여기는 경우가 있음. 하지만 확률적으로 추측하는 기계가 대신 해결해주지는 못함. 자신이 만드는 것을 실제로 이해해야 할 필요는 사라지지 않음.

만드는 것을 이해하려고 노력하는 확률적 추측 기계인 내 입장에서도, 그 접근법이 완벽하지는 않았음.

최근 TLA+를 막 배운 의욕적인 주니어 동료가 모든 문제를 해결할 수 있을 거라 생각해서 이 주제로 대화했음. 구현에 쓰던 LLM에 더 나은 출발점을 줬을 수는 있지만, TLA 명세와 Elixir 구현이 일치하는지는 여전히 제대로 답하지 못하는 부분임. 내게 그 명세는 제안에 가까우므로 문서 폴더에 넣고, 해당 기능의 속성 기반 테스트를 작성하면서 이해하라고 권했음.
불변식을 직접 이해하지 않고 TLA 명세를 바이브 코딩하는 데도 어느 정도 가치는 있겠지만, 기술 업계의 논객들이 지나치게 부풀리고 있음. 직접 코드를 쓰지 않겠다면 그 빈틈을 다른 방식으로 메워야 함.

이런 확률적 추측 기계는 TLA+ 같은 정형 모델 작성과 구현이 명세에 부합하는지 추정하는 데 꽤 유용함. 나는 모델이 구현할 설계의 논리적 타당성을 확보하도록 느슨한 안전장치를 만들 때 주로 활용함. 사람도 마찬가지로, 제대로 된 명세가 있으면 제대로 동작하는 것을 만들기 쉬워짐.
물론 정작 자신은 이해하지 못한 채 넘어갈 위험은 남아 있음.

무엇을 만들고 무엇을 좋은 결과로 볼지 사람이 명세한 기준은 필요함. 다만 사람이 찾아낼 수 있는 특정 결함이라면 소프트웨어로도 찾아낼 수 있어야 함.

LLM에 구현할 내용을 먼저 TLA+로 모델링하라고 하면 구현 품질이 나아질지 궁금함.

일부는 프로그래밍 언어의 한계라고 봄. 대체로 언어가 부분 그래프를 표현할 수 있게 하므로 검증이 기술적으로 어려워짐. 닫힌 그래프 의미론만 노출하는 언어라면 완전하지는 않더라도 모델과 구현 사이의 간극을 줄일 수 있을 것 같음.

TLA+의 문법은 상당히 이상하고, 프로그램을 쓸 만한 문법으로 표현하려면 PlusCal이라는 별도 DSL까지 필요해서 그리 좋다고 보지 않음. LaTeX와 같은 사람이 만들었다는 것이 느껴짐. 정형 모델링 분야에서 Typst에 해당하는 것은 무엇일까?
또 다른 문제는 정형 모델이 검증을 통과해도 실제 언어로 오류 없이 직접 옮겨야 한다는 점임.

PlusCal과 TLA+는 서로 다른 수준에서 작동한다고 느낌. “A 다음 B, 그다음 C” 같은 순차적 단계가 많은 대상을 모델링할 때 주로 PlusCal을 사용함. 프로그램 카운터가 암묵적으로 포함돼 순차 알고리즘에 더 직접적으로 대응함.
일반 TLA+로 작성하는 대상은 대체로 순서 의존성이 훨씬 낮음.

논리곱과 논리합을 세로로 정렬하는 목록처럼 참신하고 좋은 문법도 있음. 하지만 COBOL 시대처럼 키워드를 전부 대문자로 쓰고 열거형에 문자열 값을 사용하게 하는 문법까지 옹호하고 싶지는 않음. 반면 기반 형식 체계는 사고 도구로 매우 훌륭하며, 저마다 TLA+의 후속 언어를 표방하는 P, Quint, FizBee도 이를 활용함.
명세와 구현의 일치 여부를 확인하기 어렵다는 점에도 동의함. P는 PObserve를 통한 실행 추적 검증, 즉 실행 중인 시스템의 로그가 P 명세에서 허용하는 실행인지 확인하는 방식으로 어느 정도 성과를 낸 듯함. 다만 퍼징이나 속성 기반 테스트만큼 널리 알려진 기법은 아님. 사용하기 쉽게 만들려면 제품 차원의 설계가 필요하고, 가상 머신 등에서 시스템 실행 환경 전체를 통제해야 할 수도 있음.

단순화하려는 취지는 이해하지만 도달 가능성에 관한 대목은 이상하게 느껴짐. TLA+에서 []P를 검사하면 모든 실행의 모든 상태에서 P가 참인지 검증할 수 있음. 그 반례는 어떤 실행의 어떤 상태에서 P가 거짓인 경우이므로, 모델 검사기로 []P가 거짓임을 보이면 간접적으로 E<>!P를 증명한 셈임. 여기서 E는 “그런 실행이 존재한다”는 뜻임.
그렇다면 게임에서 이길 수 있음을 증명하려면 “게임에서 절대 이길 수 없다”는 불변식을 모델 검사하고 반례를 찾으면 되지 않을까? 내가 놓친 부분이 있을까?

거의 맞음! 그것은 최소 하나의 시작 상태에서 P에 도달할 수 있다는 제한적인 도달 가능성을 표현함. 글에서도 다뤘듯 TLC는 이제 먼저 부정하는 우회 과정 없이도 이런 속성을 직접 검사할 수 있음.
더 강한 속성은 어떤 상태에서든 특정 상태에 도달할 수 있음임. 예를 들어 최종적 일관성을 갖는 시스템에서는 쓰기가 모두 멈추기 전까지 실제로 수렴하지 않더라도, 언제나 모든 복제본이 같은 상태로 수렴할 가능성은 있는지 알고 싶을 수 있음. 글에 연결된 자료에서 TLA+로 이를 명세하고 검사하는 방법을 다루지만, 사용하기 편한 방식은 아님.
덧붙이면 “P가 참인 실행이 존재한다”에서 P는 임의의 시제 논리식을 뜻하는 것으로 보임. 제시한 방법으로 “<>S를 만족하는 실행이 존재한다” 같은 단순한 식은 표현할 수 있지만, 일반적인 시제 논리식까지 표현할 수 있는 것은 아님.