[MOZU] AWS 엔지니어링 도입기 - 타겟 선정과 모델링

최근 AWS와 Microsoft가 클라우드 시스템의 결함을 잡기 위해 TLA+(Temporal Logic of Actions)라는 정형 명세 언어를 사용한다는 사실을 알게 되었습니다. 보통 우리는 기획서만 보고 바로 코드를 짜기 시작합니다. 그러다 보면 꼭 배포 후에야 알 수 없는 버그들(경쟁 상태, 데이터 불일치)을 마주하게 되죠.

현재 운영 중인 교육용 웹 MOZU에도 꽤 복잡한 주식 거래 로직이 들어갑니다. "학생들이 사용하는 웹이라고 대충 만들지 말자. AWS처럼 설계해 보자." 라는 오기가 생겼습니다.

이 시리즈는 MOZU 프로젝트에 AWS식 엔지니어링(TLA+, 상태 머신, 정형 검증)을 도입하여 '절대 고장 나지 않는 거래 시스템'을 구축하는 과정의 기록입니다.

1. 타겟 선정: 가장 위험한 놈을 찾아라

모든 코드를 TLA+로 검증할 순 없습니다. 프로젝트에서 가장 복잡하고, 버그가 터지면 치명적인 기능 하나를 골라야 했습니다.

MOZU의 '주식 매수/매도 시스템'은 다음과 같은 복잡한 요구사항을 가지고 있습니다.

1. 로컬 버퍼링: 학생이 매수/매도 버튼을 눌러도 서버에 즉시 전송되지 않고 로컬 스토리지에 쌓입니다(장바구니 개념).
2. 가상 잔액: 아직 서버에 전송하지 않았지만, 로컬에서 추가한 주문만큼 잔액이 실시간으로 차감되어 보여야 합니다.
3. 차수(Round) 제약: 1교시에 산 주식은 1교시 가격으로, 2교시엔 2교시 가격으로 처리되어야 하며, 같은 차수 내에서는 반대 매매(매수 후 매도)가 불가능합니다.
4. 불변식(Invariant): 어떤 상황에서도 잔액은 마이너스가 될 수 없고, 보유하지 않은 주식을 팔 수 없습니다.

만약 네트워크가 느리거나 사용자가 버튼을 광클했을 때, '돈 복사 버그'나 '마이너스 통장' 사태가 벌어진다면? 생각만 해도 끔찍합니다. 여기가 바로 TLA+가 필요한 지점입니다.

2. 모델링: AI(Claude)를 활용해 진입장벽 넘기

사실 TLA+는 배우기가 다소 어렵습니다. 수학적 기호와 낯선 문법 때문에 시작조차 막막했죠. 그래서 저는 AI Agent(Claude Code)를 러닝 메이트로 활용하는 전략을 썼습니다.

맨땅에 헤딩하는 대신, 이미 작성되어 있던 MOZU의 프론트엔드 비즈니스 로직(React/TypeScript)을 Claude에게 분석시켰습니다.

🤖 Prompt: "현재 MOZU 프로젝트의 BuySellModal.tsx와 useTradeStore.ts 코드를 분석해 줘. 이 로직을 검증할 수 있도록 TradeModel.tla 명세서를 작성해 줘."

결과는 놀라웠습니다. Claude는 제 코드를 읽고 상태(State)와 전이(Transition)를 추출하여 TLA+의 기본 골격을 만들어주었습니다.

TLA+를 처음부터 설계하신다면 기존 예시들을 참고하면 좋습니다.
tlaplus github: https://github.com/tlaplus/Examples?tab=readme-ov-file
List of TLA+ Examples: https://www.hillelwayne.com/post/list-of-tla-examples/

Claude가 분석하고 내가 다듬은 상태(Variables)
Claude는 UI 관련 코드는 다 쳐내고, 검증에 필요한 핵심 데이터만 정확히 뽑아냈습니다.

VARIABLES
    cashMoney,        \* 현재 잔액
    holdings,         \* 보유 주식 수
    tradeOrders,      \* 로컬에 쌓인 주문 대기열 (장바구니)
    currentRound      \* 현재 차수

AI가 초안을 잡아준 덕분에 저는 문법 공부에 시간을 쏟는 대신, "논리가 맞는지" 검토하고 Invariant(절대 깨지면 안 되는 규칙)를 정교하게 다듬는 데 집중할 수 있었습니다.

행동(Action) 정의: 매수(Buy)
"매수 버튼을 누른다"는 행위를 TLA+ 수식으로 정의합니다. 여기서 중요한 건 CanBuy라는 전제 조건(Guard)입니다. 이 조건이 맞지 않으면 매수 행위 자체가 성립되지 않음을 수학적으로 못 박는 것입니다.

\* 매수 가능 조건
CanBuy(stockId, quantity, price) ==
    /\ ~HasOppositeOrder(stockId, "BUY")  \* 반대 주문(매도)이 없어야 함
    /\ (quantity * price) <= cashMoney    \* 잔액이 충분해야 함
    /\ quantity > 0

\* 매수 액션
Buy(stockId, quantity) ==
    LET cost == quantity * stockPrices[stockId]
    IN 
    /\ CanBuy(stockId, quantity, stockPrices[stockId]) \* 조건 체크
    /\ cashMoney' = cashMoney - cost  \* 가상 잔액 즉시 차감
    /\ tradeOrders' = Append(tradeOrders, newOrder) \* 대기열 추가
    /\ UNCHANGED <<holdings, currentRound>>

3. 검증(Model Checking): 모든 경우를 탐색하다

이제 이 설계도가 완벽한지 확인할 차례입니다. TLA+의 모델 체커(TLC)는 발생 가능한 모든 경우의 수를 시뮬레이션합니다.

• 주식 A를 샀다가 취소하고 다시 B를 샀을 때?
• 잔액이 딱 0원일 때 매도를 하면?
• 매수 주문을 100개 쌓아두고 전송하면?

처음 모델을 돌렸을 때, NoNegativeBalance 위반 에러가 떴습니다. 확인해 보니, Buy 액션에서 잔액 체크를 하는 시점과 실제 차감하는 시점의 논리적 구멍이 있었습니다. 코드를 짜기 전에 설계 단계에서 치명적인 버그를 미리 잡아낸 것입니다.

수정 후, 최종적으로 모델 체킹이 통과되었습니다.

이 메시지는 단순히 테스트 통과가 아닙니다. "수학적으로 이 설계에서는 잔액이 마이너스가 되는 일이 불가능하다"는 증명입니다.

4. 결론 및 다음 예고

TLA+ 도입 과정에서 가장 큰 수확은 두 가지였습니다.

1. AI 활용: Claude Code를 통해 기존 코드를 역으로 분석해 TLA+ 명세를 뽑아냄으로써 진입장벽을 획기적으로 낮췄습니다.
2. 확신: 복잡한 로컬 버퍼링 로직을 수식으로 검증하고 나니, 구현에 대한 확신이 생겼습니다.

이제 완벽한 설계도(Blueprint)가 준비되었습니다. 다음 단계는 이 설계를 실제 React + TypeScript 코드로 옮기는 일입니다.

TLA+가 정의한 '상태 머신'을 프론트엔드에서 어떻게 구현했을까요? 단순한 useState가 아닌, Zustand와 상태 패턴을 활용해 무결성 코드를 작성하는 과정을 다음 포스팅에서 다루겠습니다.