실패한 렌더를 다시 돌리려고 Retry를 눌렀는데, 화면이 바뀌는 사이 한 번 더 눌렀습니다. 그러면 같은 렌더가 동시에 두 번 돌고, 돈도 두 번 나갑니다.
이 앱의 테스트는 240개 전부 통과하던 상태였습니다. 사람이 떠올린 순서에는 이런 경우가 없었기 때문입니다. 이 버그를 찾은 건 일어날 수 있는 모든 순서를 다 넘겨 본 검사였습니다.
이 글에서는 다음을 차례로 봅니다.
- pstack은 무엇이고 누가 만들었나
- 입구 poteto-mode: 코드 한 줄이 에이전트의 행동을 어떻게 바꾸나
- 형식 검증과 TLA+, 쉽게
- 형식 검증 스킬 7단계: 코드 → 설계 이유 → 실제로 일어난 일
- 찾은 버그를 버그 수정 플레이북으로 고치기
- 기획자도 읽는 빨강·초록 그림
- 시간·토큰과 한계
숫자 읽는 법. [공식 문서] 는 만든 쪽이 직접 낸 자료, [직접 측정] 은 저희가 이 맥에서 직접 돌려 잰 숫자입니다. 실습은 pstack 0.15.30, Claude Code(Opus 5.5)로 했습니다.
1. pstack은 무엇인가
pstack은 AI 코딩 에이전트에게 일하는 방식을 가르치는 스킬 묶음입니다. Claude Code나 Cursor에 플러그인으로 깔면, 에이전트가 버그를 고치고 기능을 만드는 순서가 달라집니다.
- 만든 사람은 Lauren Tan입니다. Meta, Netflix를 거쳐 Cursor에서 일했고, React 핵심 팀에서 React Compiler를 만듭니다 [공식 문서] (pstack README 자기소개).
- README 첫 화면에 이렇게 적혀 있습니다. "these are the same skills i use every day to ship high quality code at Cursor." 커서에서 좋은 코드를 내보내려고 매일 쓰는 바로 그 스킬이라는 뜻입니다.
- Cursor는 2026년 8월 14일 SpaceX에 인수가 끝났고, SpaceXAI 팀으로 합쳐지는 중입니다 (SEC Form 8-K, CNBC). 그러니까 pstack은 SpaceXAI의 커서 개발자 한 사람이 실제로 일하는 방식을 공개한 것입니다. 회사 전체가 이렇게 일한다는 뜻은 아닙니다.
- Cursor 공식 플러그인 저장소(cursor/plugins)에 있고, MIT 라이선스라 누구나 무료로 씁니다.
구호는 하나입니다. "빠르게 가려면, 먼저 깊게 가라." 코드를 많이 쓰는 게 아니라, 적게 쓰되 믿을 수 있게 쓰자는 겁니다. 에이전트 하나를 깊이 믿을 수 있어야 여러 개를 동시에 맡길 수 있다는 생각입니다.
Claude Code에서는 명령 두 줄로 설치합니다.
/plugin marketplace add cursor/plugins
/plugin install pstack@cursor-plugins2. 입구 poteto-mode: 코드 한 줄이 행동을 바꾼다
pstack의 입구는 /pstack:poteto-mode 하나입니다. 하고 싶은 일을 한 줄로 부탁하면, 에이전트는 원칙(24개)을 읽고, 일의 종류에 맞는 플레이북(23개, 일 종류별 순서표)을 고른 뒤 일을 시작합니다.
오픈소스라 코드를 직접 열어 볼 수 있습니다. 실제로 버그 수정 세션 기록과 짝지어 봤습니다.
| 코드 (pstack 0.15.30) | 그렇게 만든 이유 | 우리 실행에서 실제로 |
|---|---|---|
poteto-mode/SKILL.md:42 쓰려는 스킬은 끝까지 다 읽어라 | 요약만 보면 중간 단계가 빠진다 | 첫 행동이 playbooks/bug-fix.md 읽기 ✅ |
SKILL.md:125 플레이북 단계를 할 일 목록에 그대로 옮기고, 안 할 단계는 skip: 이유로 남겨라 | 빠진 단계를 사람이 나중에 볼 수 있게 | 다르게 됨. 할 일 목록 도구를 부르지 않았고, "실패 재현을 먼저 커밋" 단계도 이유 없이 건너뜀 ❌ |
SKILL.md:17 이번 세션에 읽은 원칙만 인용해라 | 읽지도 않은 원칙을 갖다 붙이지 못하게 | 원칙 4개를 읽고, 보고서에 정확히 그 4개만 인용 ✅ |
playbooks/bug-fix.md:7 사용자가 보는 화면에서 직접 재현해라 | 실패를 먼저 봐야 "고쳤다"가 증명된다 | 실패하는 화면 테스트 먼저, "카드가 2개가 아니라 3개" 재현 ✅ |
bug-fix.md:5 "도움이 될지도" 모르는 안전장치는 가설일 뿐, 내보내지 않는다 | 혹시 몰라 넣은 코드는 아무도 못 지운다 | 복원 줄을 일부러 빼고 돌려 봄 → Expected 2, Received 1 → 필요해서 남김 ✅ |
scripts/check-plan.mjs 확인 칸은 증거가 있을 때만 체크 | "테스트 통과"만으로 끝내지 못하게 | 이번엔 계획 파일을 안 써서 이 검사기는 돌지 않음 |
스킬은 결국 지시서라서, 모델이 늘 100% 따르지는 않습니다. 위 표처럼 지킨 곳과 안 지킨 곳이 함께 나옵니다. 그래서 결과는 꼭 직접 확인해야 합니다.
3. 형식 검증과 TLA+, 쉽게
테스트는 내가 떠올린 순서 하나를 돌려 봅니다. 렌더 시작 → 실패 → Retry → 끝. 이 길이 잘 되면 통과입니다.
모델 체커는 정해 둔 범위 안에서 일어날 수 있는 모든 순서를 하나도 빼지 않고 돌려 봅니다. 버튼을 누르는 순간, 일이 끝나는 순간, 다시 누르는 순간이 어떻게 섞일 수 있는지 전부요.
- TLA+ 는 Temporal Logic of Actions, 시간에 따라 일어나는 동작을 적는 언어입니다. LaTeX를 만들고 튜링상을 받은 레슬리 램포트가 만들었습니다.
- TLC 는 TLA+ 모델을 받아 모든 순서를 직접 따라가 보는 프로그램(모델 체커)입니다. 둘 다 무료고 Java만 있으면 됩니다.
사진첩으로 생각하면 쉽습니다.
- 상태 = 어느 한 순간을 찍은 사진 한 장 (슬롯 두 칸이 쓰이고, 하나가 기다리는 순간)
- 동작 = 다음 사진으로 넘기는 화살표 (작업 시작, 끝, 실패, Retry)
- 불변식 = 어느 사진에도 나오면 안 되는 장면 (같은 작업이 동시에 두 번 도는 장면)
- 반례 = 나쁜 장면까지 가는 사진 순서
중요한 건, 수식은 사람이 쓰지 않는다는 점입니다. 규칙은 우리말로 적고, TLA+ 모델은 에이전트가 씁니다.
4. 형식 검증 스킬 7단계: 코드 → 이유 → 실제
create-formal-verification-skill은 pstack에서 가장 화제가 된 스킬입니다. 부탁은 이렇게만 했습니다. "렌더 대기열에서 ① 동시에 도는 작업은 3개 이하 ② 같은 작업이 동시에 두 번 돌지 않는다, 이 두 규칙을 검사하는 스킬을 만들어 줘."
| 단계 (SKILL.md 줄) | 그렇게 만든 이유 | 우리 실행에서 실제로 [직접 측정] |
|---|---|---|
| ① 약속 고르기 (:17) "깨지면 사용자가 다치는데 테스트가 잘 못 닿는 약속" | 테스트가 이미 잘 보는 곳은 시간 낭비 | 렌더 대기열 규칙 두 개 |
| ② 도구 고르기 (:21) "질문에 가장 싸게 답하는 도구" | TLA+로 못 박지 않았다 | "나쁜 순서가 있나?"라서 TLA+와 TLC |
| ③ 모델 줄 = 코드 줄 | 모델이 코드와 다르면 PASS가 무의미 | 모델의 IF runningJobs < MaxConcurrentJobs가 앱 코드 editor.ts:747과 같은 조건 |
| ④ 일부러 망가뜨리기 (:26) "한 번도 실패한 적 없는 검사는 아무것도 증명하지 못한다" | 늘 PASS인 검사는 고장 났을 수도 | <를 <=로 바꾼 변형이 잡힘. 진짜 코드에 await를 끼워 넣자 "슬롯 4개 점유"로 잡힘 |
| ⑤ 찾은 건 그대로 (:27) "규칙을 약하게 고치지 마라" | 검사를 느슨하게 해서 초록 불 켜는 꼼수 차단 | 규칙 2가 이미 깨져 있다고 그대로 보고 (F1) |
| ⑥ 범위 밝히기 (:28) | PASS는 정한 범위 안에서만 참 | "작업은 최대 6개까지만 봤다"고 먼저 적음. 슬롯 규칙은 상태 285만여 개 통과 |
| ⑦ 스킬로 포장하고 직접 따라 해 보기 (:35, :39) | 다음 사람이 쓸 수 있게, 그리고 정말 잡는지까지 | pnpm formal:jobs 한 줄 검사 + 프로젝트 스킬 verify-job-queue |
찾은 반례 F1은 이렇습니다.
- 렌더가 실패합니다.
- 카드의 Retry를 누르면 새 작업이 슬롯을 받습니다. (Retry는 같은 작업을 다시 돌리는 게 아니라, 번호가 다른 새 작업을 만듭니다.)
- 그런데 실패한 원래 카드에는 Retry 버튼이 그대로 남아 있습니다.
- 한 번 더 누르면 세 번째 작업도 슬롯을 받습니다. 같은 요청 두 개가 동시에 돕니다.
에이전트는 제품 코드는 고치지 않았습니다. 어떻게 고칠지는 스펙에서 정할 일이라고 남겼습니다. 걸린 시간은 19분 44초였습니다.
5. 버그 수정 플레이북으로 고치기
이번엔 poteto-mode에 부탁했습니다. 완료 조건은 두 가지였습니다. 검사에서 F1이 더는 위반으로 나오지 않을 것, 화면에서 Retry를 두 번 눌러도 카드가 하나만 생길 것.
- 재현 먼저. 처음엔 더블클릭으로 재현이 안 됐습니다. 첫 클릭에 새 카드가 위에 생기면서 두 번째 클릭이 엉뚱한 곳에 떨어졌기 때문입니다. 그래서 같은 버튼을 다시 찾아 누르게 테스트를 고쳤습니다. 진짜 사용자가 하는 그대로요.
- 원인에서 막기. 버튼만 숨기면 MCP 같은 다른 길로 부르는 건 그대로 열려 있습니다. 그래서
retryJob함수에서 "끝난 작업만, 한 번만 재시도"를 막았습니다. - 필요한 줄인지 실험. 복원 줄을 빼고 돌려 테스트가 실패하는 걸 보고서야 남겼습니다.
고친 뒤 검사를 다시 돌리면 F1 자리가 PASS이고, KILLED가 6줄 나옵니다. 일부러 망가뜨린 코드 여섯 가지가 전부 잡혔다는 뜻입니다. 고치기 전의 retryJob도 그중 하나로 남았습니다. 누가 나중에 실수로 되돌리면 바로 빨간불이 켜집니다. 찾은 버그가 다시는 몰래 돌아올 수 없는 구조가 된 겁니다.
6. 기획자도 읽는 빨강·초록 그림
/pstack:statechart는 TLC 결과를 사용자가 보는 화면 기준의 그림으로 바꿉니다. 칸 하나가 화면 하나, 화살표가 사용자가 한 일입니다.
- 빨강 = 고치기 전 버그 경로 (실패 → Retry → 이미 누른 Retry를 한 번 더 → 같은 렌더 두 번)
- 초록 = 고친 코드에서 바뀐 화면 (Retry를 누르는 순간 옛 카드의 버튼이 사라짐)
- 결과: 고쳐진 칸 8개, 남은 버그 0개
코드를 열어 보면 설계가 보입니다. tlc-to-chart.mjs의 firstBad()는 반례를 규칙이 처음 깨진 칸에서 자릅니다. 깨진 뒤의 단계는 잡음이라서요. 그리고 도움말에 이렇게 적혀 있습니다. "TLC decides the status, and a group cannot change it." 칸의 색은 사람이 아니라 TLC가 정합니다. 그림을 그리는 쪽이 보기 좋게 색을 바꿔 결과를 숨기지 못하게 한 겁니다.
7. 시간·토큰과 한계
[직접 측정] 조사(/how) 약 7분, 형식 검증 약 20분, 버그 수정 약 40분, 상태 그림 약 6분이 걸렸습니다. 버그 수정이 길어진 건 저장소의 Stop 훅이 "검사를 통과하기 전엔 끝내지 마라"고 에이전트에게 일을 다시 시켰기 때문입니다.
- pstack은 서브에이전트를 띄우고, 검토하고, 실제로 돌려서 재현까지 하니까 토큰을 많이 씁니다. 오타 고치기 같은 작은 일엔 쓰지 마세요.
- 형식 검증은 모델과 범위 안에서만 보장합니다. 이번엔 작업 6개까지였습니다.
- pstack은 거의 매일 바뀝니다. 검사기 TLC는 촬영 때 1.8.0을 받았는데, 이 버전이 같은 이름으로 다시 빌드되는 프리릴리스라 파일 지문이 바뀌었습니다. 그래서 실습 저장소는 안정판 1.7.4로 고정했습니다.
- 시간 제한 숫자를 늘리는 설정 한 줄은 Claude Code의 auto mode가 두 번 막았습니다. 에이전트는 우회하지 않고 "이 한 줄은 사람이 바꿔 달라"고 남겼습니다.
순서가 꼬일 수 있는 곳, 즉 버튼, 대기열, 재시도, 캐시, 알림 같은 곳에 형식 검증을 써 보세요. 테스트가 떠올리지 못한 순서를 찾아 줍니다.
영상으로 보기
같은 내용을 실제 실행 화면과 함께 영상으로 정리했습니다. 10월 30일 오후 6시(한국시간)에 공개됩니다.
출처
- cursor/plugins · pstack — README,
skills/poteto-mode/SKILL.md,playbooks/bug-fix.md,scripts/check-plan.mjs,skills/create-formal-verification-skill/SKILL.md,skills/statechart/scripts/tlc-to-chart.mjs(0.15.30) - SpaceX, Form 8-K (2026-08-14) · CNBC, SpaceX says it can buy Cursor later this year for $60 billion (2026-04-21)
- TLA+ (tlaplus/tlaplus) — TLC 1.7.4
- Newcombe et al., How Amazon Web Services Uses Formal Methods, Communications of the ACM (2015)
- 실습 저장소: dante01yoon/ComfySims —
harness/formal/job-queue/
