lauren(@poteto)이 pstack의 형식 검증 스킬과 짝을 이룰 상태 차트 스킬을 곧 낸다고 예고했다. 그 차트는 kepano의 Mermaid 렌더러 Pele로 그린다.
lauren(@poteto) · X 인용 포스트 · 2026-10-23 07:33 KST(2026-10-22 22:33 UTC) · 원문 포스트
읽기 전에
에이전트가 그린 상태 차트를 형식 검증 스펙과 맞춰 보는 스킬은 지금 어디까지 공개됐나?
lauren(@poteto)은 2026-10-23 07:33 KST(2026-10-22 22:33 UTC) X에, 에이전트가 그린 상태 차트를 pstack의 /create-formal-verification-skill로 만든 스펙과 대조하게 돕는 동반 스킬을 곧 낸다고 썼다(본 글). 차트를 그리는 /statechart 스킬은 그보다 16시간 앞선 2026-10-22 06:08 UTC에 이미 공개 저장소 cursor/plugins main에 병합됐다(PR #741). 본 글이 내세운 Pele 렌더는 2026-10-23 기준 공개 main 스크립트에 없다(statechart.mjs). 이 글은 빈자리에 내는 신기능 발표가 아니라 공개된 /statechart의 렌더러를 바꾼 다음 판 예고에 가깝다.
멘탈 모델
세 글은 한 사슬이다: 형식 검증 스펙을 만드는 메타 스킬 공지(2026-10-19, pstack 공지) → 그 스펙 옆에 사람이 읽는 상태 차트를 두는 사용법(2026-10-21, 인용된 글) → 에이전트가 차트를 그려 스펙과 맞추는 동반 스킬 예고(2026-10-23, 본 글). 상태 차트는 모델 검사기가 스펙에서 찾은 결과를 사람이 사용자 흐름으로 읽게 하는 화면이다(인용된 글 · /statechart SKILL.md).
먼저 알아 둘 낱말
상태 차트(statechart)
상태 기계 그림에 상태를 묶는 계층과 병렬 구역을 더한 표기로, David Harel이 1987년 논문에서 제안했다(Harel 1987). 본 글 그림에서 'Host active' 상자가 여러 상태를 묶는 것이 그 계층이다(본 글).
형식 검증과 불변식
저자는 형식 검증을 시스템의 성질을 수학적으로 증명하는 일로, 불변식(invariant)을 언제나 참이어야 하는 성질로 정의한다(pstack 공지). 같은 글은 별도 언어로 모델을 적는 TLA+ 방식과 검증 대상 언어 안에서 바로 검사하는 방식을 나눈다(pstack 공지). 뒤쪽 예인 Kani는 Rust 프로그램의 정의되지 않은 동작·패닉·산술 오버플로를 자동으로 검사한다(Kani 문서). Bend에서는 법칙을 정리로 적으면 타입 검사기가 그 증명을 확인한다(HigherOrderCO/Bend).
TLA+와 TLC
TLA+는 Leslie Lamport가 만든 명세 언어다(Lamport의 TLA+ 페이지). TLC는 TLA+ 명세가 닿는 상태를 모두 탐색해 불변식 위반을 찾는 모델 검사기다(같은 페이지).
메타 스킬과 pstack
/create-formal-verification-skill은 검증하고 싶은 특성에 맞춰 새 스킬과 형식 검증 묶음을 만드는 메타 스킬(스킬을 만드는 스킬)이다(pstack 공지). 이 스킬은 PR #709로 2026-10-18 06:20 UTC 병합됐다(PR #709). PR 설명의 동작 순서는 속성 하나 선택 → 질문에 맞는 도구 선택 → 일부러 망가뜨린 변형에서 속성이 깨지는지 확인 → 다음 에이전트가 다시 돌릴 프로젝트 로컬 스킬 작성이다(PR #709). pstack은 Cursor의 공개 플러그인 저장소 cursor/plugins 안에 있다(cursor/plugins/pstack). 그 plugin.json의 저자 표기는 Lauren Tan이다(cursor/plugins/pstack).
Mermaid와 Pele
/statechart는 차트를 텍스트 다이어그램 문법인 Mermaid로 적는다(SKILL.md). 공개 main 스크립트는 PNG를 npx @mermaid-js/mermaid-cli로 렌더한다(statechart.mjs). Pele는 Obsidian CEO kepano(Steph Ango)가 2026-10-17 공개한 Mermaid 문법 호환 렌더러다(kepano 발표 · 소스 · 문서). 같은 발표는 Pele를 의존성 없는 MIT 라이선스 코드이자 다음 Obsidian 버전의 렌더러로 소개한다(kepano 발표).
@SpaceXSI와 grok bot
저자 X 소개란은 2026-10-23 캡처 기준 "grok @bot at @SpaceXSI", React Compiler 코어 팀, 이전 Cursor·Meta·Netflix를 적는다(@poteto 프로필). SpaceXSI는 SpaceX가 2026-02-02 인수한 xAI의 현재 브랜드 'SpaceX Super Intelligence'다(Wikipedia). xAI의 X 계정은 2026-10-10 이 이름으로 바뀌었다(Wikipedia). React Compiler v1.0 발표 글(2025-10-07) 저자 목록에는 Lauren Tan이 있다(react.dev). 소속은 이 소개란의 진술로만 확인된다.
읽는 순서
본 글(2026-10-23) — 예고 세 줄과 호스트 상태 차트 한 장이다. 무엇을 예고하는지 먼저 정해 두면 뒤의 두 글이 그 예고의 근거로 읽힌다.
2026-10-21 인용된 글 — 상태 차트를 그린 뒤 TLA+로 버그를 찾는 사용법과 회색·빨강·초록 범례의 예시 그림이 있다. 본 글이 바로 인용한 글이라 두 번째에 둔다.
2026-10-19 pstack 공지 — 차트가 대조할 스펙을 만드는 도구와 형식 검증 정의가 있는 사슬의 맨 앞이다. 정의는 위 낱말 풀이와 겹치므로 도구 공지 부분을 중심으로 세 번째에 읽는다.
대화 속 작성자 답글 — Pele를 개선할 점을 묻는 kepano에게 저자가 grok bot 데스크톱·모바일에서 better-mermaid를 Pele로 바꿨다고 답한 한 줄이다(답글). 본 글의 'Pele를 쓴다'를 스킬 밖 제품까지 넓히는 단서라 원문 끝에서 본 글과 짝으로 읽는다.
요약 — 네 글을 한 사슬로 합친 요지다. 원문을 다 읽은 뒤 빠진 고리를 맞춰 보는 자리라 원문 다음에 둔다.
팩트체크 — 예고 문장을 공개 코드와 대조하는 블록이다. '곧 출시'를 현재 사실로 읽지 않도록 마지막에 확인한다.
이 글이 답하는 질문
곧 낸다는 스킬과 이미 공개된 /statechart는 어떤 관계인가?
예고의 '차트 그리기'는 공개된 /statechart가 이미 한다: TLC가 탐색한 상태 그래프에서 사용자가 보는 것을 차트로 그려 TLC가 찾은 버그를 번호 붙은 경로로 표시한다(SKILL.md). 합의된 차트에서 TLA+ 뼈대를 만드는 반대 방향(from-chart)도 같은 스킬에 있다(SKILL.md). 이 스킬을 넣은 PR #741은 pstack 버전을 0.15.29에서 0.15.30으로 올렸다(PR #741). → 본 글 · 팩트체크
2026-10-21 그림 속 버그는 실제로 찾은 것인가?
아니다. 저자는 그 그림을 가상 예시(hypothetical example)라고 적었다(인용된 글). 실제 발견의 근거는 버그 목록 없이 '이미 여러 버그를 찾았다'고 적은 2026-10-19 저자 진술 하나다(pstack 공지). → 2026-10-21 글 · 2026-10-19 글
본 글 그림은 무엇을 보여 주나?
작업이 도는 동안 호스트가 활성 상태에서 reaper의 판단을 거쳐 주차(parked) 상태로 가는 흐름이다(본 글). 'Breaks a rule' 빨간 테두리는 요청 직후 주차된 호스트, 주차 직전 호스트, 체크포인트 뒤에서 기다리는 작업에 붙었다(본 글). → 본 글
Executive Summary
lauren(@poteto)은 2026-10-23 07:33 KST X 글에서 에이전트가 상태 차트를 그려 형식 검증 명세와 대조하게 하는 pstack 동반 스킬을 예고한다. 16시간 앞서 /statechart로 병합된 같은 스킬과 견주면, 새 부분은 2026-10-23 공개 main 스크립트에 아직 없는 kepano의 Pele 렌더링이다.
신뢰도 B — 도구와 개념 설명은 공개 저장소와 맞지만 버전 번호·'곧 출시'·Pele 적용은 공개 기록보다 앞서 나간 표기다. → 팩트체크
3편 · 약 4일
2026-10-19 06:05 KST 출시 글, 2026-10-21 11:44 KST 예시 글, 2026-10-23 07:33 KST 본 글이 차례로 앞 글을 인용한다.
/statechart 병합(2026-10-22 06:08 UTC)이 본 글의 출시 예고(2026-10-22 22:33 UTC)보다 앞선 간격이다.
0회
2026-10-23 기준 공개 main의 statechart.mjs에 Pele가 나오는 횟수다. 같은 스크립트는 npx @mermaid-js/mermaid-cli로 렌더한다.
예고된 스킬은 공개 저장소에 이미 병합돼 있다
저자가 '곧 출시'라고 쓴 동반 스킬은 예고 글보다 먼저 공개 저장소에 들어가 있다(PR #741). 저자는 상태 차트를 그려 명세와 대조하는 동반 스킬을 작업 중이라고 쓴다(P1). 출시 시점은 '곧'이라고만 밝힌다(P1). /statechart 스킬은 2026-10-22 06:08 UTC cursor/plugins main에 병합됐다(PR #741). 병합 시점의 pstack 버전은 0.15.30이다(PR #741). 이 스킬은 TLA+ 모델에서 사용자가 보는 것을 Mermaid 상태 차트로 그린다(PR #741).
동작하는 상태는 회색, 아직 틀린 상태는 빨강, 수정된 상태는 초록으로 칠한다(PR #741). 공개 기록에 맞는 해석은 예고 대상이 스킬 자체보다 Pele로 그리는 다음 판이라는 쪽이다.
Pele 렌더링은 공개 코드에 아직 없다
Pele 채택은 2026-10-23 현재 저자의 자기 보고로만 확인된다(statechart.mjs · R1). 저자는 차트가 보기 좋은 이유로 kepano의 Pele 사용을 든다(P1). 2026-10-23 공개 main의 statechart.mjs는 npx @mermaid-js/mermaid-cli로 PNG를 만든다(statechart.mjs). 같은 스크립트에는 Pele 호출이 없다(statechart.mjs). 저자는 kepano의 답글에 Pele가 매우 좋다고 답한다(R1). 같은 답글에서 grok bot 데스크톱·모바일 앱의 better-mermaid를 Pele로 이미 바꿨다고 보고한다(R1).
Pele는 kepano(Steph Ango, Obsidian CEO)가 2026-10-17 공개한 Mermaid 문법 호환 렌더러다(kepano 발표). 라이선스는 MIT다(obsidianmd/pele). 속도와 번들 크기 수치는 독립 측정이 아닌 개발자 본인의 발표다(kepano 발표).
상태 차트는 형식 검증의 결과를 사용자 흐름으로 보여 준다
저자가 그리는 상태 차트는 TLA+ 같은 형식 검증이 찾은 버그를 사용자가 겪는 흐름 위에 표시한다(P2). 저자는 에이전트에게 상태 차트를 그리게 한 뒤 /create-formal-verification-skill로 만든 스킬로 버그를 찾는 방식을 흥미롭다고 평한다(P2). 이 방식으로 코드와 사용자 흐름을 함께 이해하게 된다는 것이 저자의 주장이다(P2). 사용자가 겪었을 문제를 미리 고칠 수 있다고도 쓴다(P2).
예시 글 첨부 이미지는 저자가 가상 예시로 밝힌 메시지 알림 흐름이다(P2). 그림은 TLA+가 찾은 버그 4개를 빨강, 수정한 4개를 초록으로 칠한다(P2). 버그 하나는 채널만 연 상태에서 스레드 답글이 읽음 처리되는 경우다(P2). 나머지 셋은 폰에서 이미 연 메시지로 폰이 울리는 경우, 방해 금지 시작 뒤 자리를 뜨자 폰이 울리는 경우, 폰에서 읽은 메시지가 깨운 노트북에서 안 읽음으로 남는 경우다(P2).
본 글 차트는 작업 하나가 도는 동안 호스트가 활성·파킹·체크포인트 작성 상태를 오가는 흐름이다(P1). 요청 직후 파킹된 호스트, 파킹 직전 작업이 도는 세션, 체크포인트 뒤에서 기다리는 태스크가 빨간 테두리 상태에 들어간다(P1). 차트 노트는 모델에서 유휴 시계가 이 지점의 호스트 파킹을 시작하지 않는다고 적는다(P1). 두 그림은 검증기가 찾은 반례를 사용자와 운영자가 읽는 상태 이름으로 옮긴다.
바탕은 형식 검증 스킬을 만드는 메타 스킬이다
동반 스킬의 바탕은 2026-10-18 cursor/plugins에 병합된 /create-formal-verification-skill이다(PR #709). 병합 시각은 06:20 UTC다(PR #709). pstack 버전은 같은 날 20:18 UTC 0.15.27로 올랐다(PR #713). 저자의 출시 글은 그 47분 뒤인 21:05 UTC에 올라왔다(P3). 저자는 이 스킬을 아직 베타라고 쓴다(P3). /create-verification-skill처럼 검증하려는 특성에 맞춰 새 스킬과 형식 검증 스위트를 만드는 메타 스킬이라는 설명이다(P3).
저자가 드는 예는 상태 기계와 동시성 시스템을 모델링하는 TLA+, Rust의 정의되지 않은 동작을 검사하는 Kani다(P3). 저자는 형식 검증을 항상 참이어야 하는 속성·불변식, 곧 시스템의 '법칙'을 수학적으로 증명하는 일로 설명한다(P3). 보통은 TLA+ 같은 별도 언어로 쓴 모델에 솔버를 돌린다는 설명이 이어진다(P3). Kani와 Bend는 별도 언어를 두지 않는다고 저자는 쓴다(P3). Kani 사용자는 검증 코드를 Rust로 쓴다(P3). 프로그래밍 언어인 Bend는 증명을 자기 타입 시스템의 법칙으로 표현한다(P3).
저자는 형식 검증이 주류가 되지 못한 이유로 모델링과 증명 작성의 어려움을 든다(P3). 비즈니스 요구사항을 모델로 옮겨 코드와 맞춰 두기가 어렵다는 진단이다(P3). 저자는 형식 검증의 혁신이 늘어난다고 전망한다(P3). 코드가 의도대로 동작함을 형식으로 검증하는 능력이 에이전트의 정확한 코드 작성에 큰 힘이 된다는 주장이다(P3). 저자는 TLA+로 자기 코드를 모델링해 이 메타 스킬이 만든 스킬로 버그 여러 개를 이미 찾았다고 보고한다(P3).
형식 검증 메타 스킬은 2026-10-18에(PR #709), 그 결과를 그리는 /statechart는 2026-10-22에 공개됐다(PR #741). 본 글의 새 정보는 Pele 렌더링 예고와 호스트 작업 차트 한 장이다(P1).
본 글 첨부 차트는 작업 하나가 도는 동안의 호스트 상태와 빨간 테두리로 표시된 규칙 위반 상태 5개를 보여 준다(P1).
원문 주장 전수
저자 글 네 편의 주장 전수. 위치는 P1 = 본 글(2026-10-23), P2 = 본 글이 인용한 예시 글(2026-10-21), P3 = P2가 인용한 출시 글(2026-10-19), R1 = 본 글 스레드의 저자 답글(2026-10-23)이다. 성격은 사실 진술 = 저장소·공개 기록으로 확인할 수 있는 내용, 의견·예측 = 저자의 판단이나 전망, 예고 = 아직 공개되지 않은 출시 계획, 자기 보고 = 저자만 확인할 수 있는 작업·사용 경험이다.
등급: A = 판정 대상이 모두 사실이거나 불확실이 의견·예측에 그친다. B = 핵심 기술 사실은 맞지만 버전·시점·수치 같은 세부가 흔들린다. C = 핵심 주장 일부가 근거 없이 서 있다. D = 핵심 주장 하나 이상이 거짓이다. F = 핵심 주장 대부분이 거짓이거나 출처가 없다.
B
정합성 한줄평: 도구와 개념 설명은 공개 저장소와 맞지만 버전 번호·'곧 출시'·Pele 적용은 공개 기록보다 앞서 나간 표기다.
저자와 소속
부분 사실
주장: 저자는 React Compiler 코어 팀이다. 이전 소속은 Cursor·Meta·Netflix다. (위치: 프로필 소개란)
주장: 소개란의 'grok @bot at @SpaceXSI'는 SpaceXAI의 Grok Bot 제품 팀을 가리킨다. (위치: 프로필 소개란·R1)
@SpaceXSI는 xAI를 인수한 SpaceX의 AI 법인 SpaceXAI LLC가 2026-10-10부터 쓰는 공식 X 계정이다. 이 회사의 주력 제품은 Grok이다. Grok Bot은 x.ai가 내놓은 AI 팀원형 에이전트 제품이다. Grok Bot 문서는 데스크톱 앱과 모바일 앱을 따로 안내한다. 저자 프로필의 웹사이트 링크도 x.ai/bot 아래 주소다. Cursor는 2026-08-14에 SpaceX의 완전 자회사가 됐다. 소개란의 이전 소속과 현 소속이 지금은 같은 그룹 안에 있다.
주장: pstack v0.15.27이 새 스킬 /create-formal-verification-skill을 싣고 나왔다. (위치: P3)
스킬을 추가한 PR #709는 2026-10-18 06:20 UTC에 병합됐다. 병합 커밋 시점의 plugin.json 버전은 0.15.25다. 다음 plugin.json 범프인 0.15.26은 같은 날 07:31 UTC에 들어갔다. 0.15.27 범프는 같은 날 20:18 UTC에 pstack에 들어갔다. P3는 그 47분 뒤인 21:05 UTC에 올라왔다. 0.15.27에 스킬이 실린 것은 맞다. 스킬이 처음 실린 판은 0.15.26이라 '0.15.27의 새 스킬'은 한 판 늦은 표기다.
베타는 배포자 본인이 P3에서 붙인 단계 표기다. 독립 출처로 참·거짓을 가릴 대상이 아니다. 짝 스킬 /maintain-formal-verification-skill은 2026-10-19 05:06 UTC에 pstack에 추가됐다. 0.15.28 범프를 담은 PR #724는 가이드 문서도 함께 맞췄다. 공개 뒤에도 스킬 묶음이 계속 바뀐다는 점은 베타 표기와 어긋나지 않는다.
주장: /create-verification-skill과 비슷한 메타 스킬이다. 원하는 성질에 맞춰 새 스킬과 형식 검증 묶음을 만든다. (위치: P3)
pstack README 스킬 표에 /create-formal-verification-skill이 있다. 같은 skills 디렉터리에 /create-verification-skill도 있다. PR #709에 따르면 이 스킬은 검증하기 쉬운 대상이 아니라 저장소에서 가장 위험한 속성 하나를 고른다. 스킬은 망가뜨린 변형에서 그 속성이 실패하는 것을 먼저 보인 뒤에 프로젝트 로컬 스킬을 쓴다. 새 스킬과 검증 묶음을 만드는 메타 스킬이라는 P3 설명은 이 동작과 맞는다.
주장: 상태 기계와 동시성 시스템은 TLA+로 모델링한다. Rust에서는 kani로 정의되지 않은 동작을 검사한다. (위치: P3)
PR #709는 TLA+를 동시성·분산 설계의 흔한 출발점으로 제안할 뿐 강제하지 않는다. 도구는 검증하려는 질문에 맞춰 고른다. 같은 PR의 평가에서 스킬은 cJSON에 CBMC를, arrayvec에 Kani를 골랐다. Kani 문서는 Kani를 모델 검사로 Rust 프로그램을 분석하는 오픈소스 검증 도구로 소개한다. Kani는 여러 종류의 정의되지 않은 동작(undefined behavior)을 자동으로 검사한다. 패닉과 산술 오버플로도 자동 검사 대상이다. P3가 예로 든 두 조합은 도구의 실제 성격과 맞는다.
주장: 보통은 프로그램을 TLA+ 같은 별도 언어로 모델링한 뒤 그 명세에 solver를 돌린다. (위치: P3)
TLA+ 명세는 구현 코드와 따로 쓴다. AWS 사용기에 따르면 TLA+ 명세는 시스템이 보일 수 있는 합법 동작 전체를 기술한다. 같은 글은 모델 검사기 TLC가 가능한 실행 경로 전체에서 정확성 속성을 빠짐없이 검사한다고 설명한다. /statechart 역시 TLC가 탐색한 상태 그래프에서 차트를 만든다. 'solver를 돌린다'는 표현은 느슨하다. TLA+의 기본 검사 도구는 식을 푸는 solver가 아니라 실행 경로를 펼쳐 검사하는 모델 검사기다. '보통'의 범위도 넓다. Kani는 별도 명세 언어 없이 Rust 프로그램을 직접 모델 검사한다.
주장: 형식 검증은 모델링과 증명 작성이 어려워 주류가 되지 못했다. 앞으로 형식 검증 혁신이 늘어난다. (위치: P3)
'주류가 된 적 없다'는 큰 산업 사례 앞에서 과장된 일반화다. AWS 엔지니어들은 2011년부터 S3·DynamoDB·EBS 같은 핵심 서비스 설계에 TLA+ 명세와 모델 검사를 썼다. 같은 글에는 여러 엔지니어가 TLA+보다 C 모양의 PlusCal에서 더 생산적이었다는 보고가 있다. 표기법의 문턱이 채택을 가른다는 저자 진단과 같은 방향의 증언이다. 원인 진단과 전망은 둘 다 저자의 의견·예측이다. 에이전트가 검증 스킬을 직접 만드는 pstack 스킬은 그 전망을 겨냥한 한 사례다.
주장: 에이전트에게 상태 차트를 그리게 한 뒤 형식 검증 스킬로 TLA+ 버그를 찾을 수 있다. 첨부 그림은 가상 예시다. (위치: P2)
PR #741의 /statechart는 TLA+를 읽지 못하는 검토자를 위해 앱 사용자가 보는 상태를 Mermaid 상태 차트로 그린다. 차트의 재료는 TLC가 탐색한 상태 그래프다. 공개된 모드는 from-spec·--fixed·--against·from-chart 네 가지다. SKILL.md는 정상 상태를 회색, 아직 틀린 상태를 빨강, 고친 상태를 초록으로 칠한다. TLC가 찾은 버그마다 번호 붙은 경로가 하나씩 생긴다. P2 그림의 범례 Works·Bug TLA+ found·Fixed가 이 세 색과 짝을 이룬다. P2는 2026-10-21 02:44 UTC에 올라왔다. 이 도구가 공개 main에 들어가기 약 27시간 전이다. 저자는 그림이 가상 예시라고 먼저 밝혔다.
주장: 상태 차트를 그리고 형식 검증 스펙과 대조하는 새 동반 스킬을 작업 중이다. 곧 출시한다. (위치: P1)
그 기능을 담은 PR #741은 2026-10-22 06:08 UTC에 병합됐다. P1은 2026-10-22 22:33 UTC에 올라왔다. 병합보다 약 16시간 늦다. 같은 PR이 pstack 버전을 0.15.29에서 0.15.30으로 올렸다. TLA+ 모델에서 차트를 만드는 기능 설명은 공개된 SKILL.md와 맞는다. '곧 출시'는 공개 저장소에 이미 버전이 매겨진 상태와 어긋난다. 출시 대기분이 Pele 렌더링판이라면 문장은 성립한다. 공개 코드에는 아직 Pele가 없다.
2026-10-23 기준 공개 main의 statechart.mjs는 PNG 출력을 npx @mermaid-js/mermaid-cli로 만든다. 같은 파일에 pele라는 문자열은 한 번도 나오지 않는다. P1 이미지의 렌더러는 저자의 미공개 작업분이라 외부에서 확정할 수 없다. 공개 코드 기준으로는 아직 Pele를 쓰지 않는다.
kepano는 2026-10-17 글에서 Pele를 자신의 새 다이어그램·차트 렌더링 라이브러리라고 소개했다. 같은 글은 Pele가 다음 Obsidian 버전의 새 렌더러가 된다고 밝혔다. 저장소 obsidianmd/pele는 2026-10-05에 만들어졌다. 저장소 설명대로 Pele는 Mermaid 문법을 렌더링한다. R0에서 kepano가 직접 개선 의견을 청했다.
주장: Grok Bot 데스크톱·모바일 앱에서 better-mermaid를 Pele로 바꿨다. (위치: R1)
Grok Bot에는 데스크톱 앱과 iPhone·Android용 모바일 앱이 있다. '데스크톱과 모바일'이라는 표현은 이 제품 구성과 맞는다. 공개된 'Better Mermaid'는 확대·팬·PNG 내보내기를 붙이는 Obsidian 플러그인뿐이다. 같은 이름의 공개 패키지는 이 플러그인 말고 특정되지 않는다. 클라이언트 코드가 공개되지 않아 교체 사실은 자기 보고로 남는다.
세 수치와 라이선스는 모두 kepano 본인의 발표에서 나온다. poteto는 P1에서 이 수치를 인용하지 않았다. Obsidian·kepano와 무관하다고 밝힌 학습 사이트 pele.wiki는 Mermaid 12.1.0 내장 다이어그램 전 종류 지원을 적는다. 같은 사이트에 속도·크기 수치는 없다. GitHub API는 obsidianmd/pele의 라이선스를 NOASSERTION으로 표시한다. NOASSERTION은 GitHub이 라이선스를 자동으로 식별하지 못했다는 표시다. 이 값만으로 MIT 여부를 가릴 수 없다. 저장소 별은 2026-10-23 기준 3,109개다. 성능 수치는 독립 측정이 없는 공급자 주장이다.
한동안 좀 조용했지 - 새 동반 스킬(companion skill)을 만드는 중이야. 네 에이전트가 이런 예쁜 상태 차트(statechart)/다이어그램을 그리고, 네가 pstack의 /create-formal-verification-skill로 만든 스펙과 대조해서 검사하도록 도와주는 스킬!
인용된 글 (2026-10-21) — 에이전트가 그린 상태 차트를 TLA+로 검증해 버그 찾기
lauren @poteto·
에이전트한테 상태 차트를 그리게 하고(이 이미지는 가상의 예시야), 네가 pstack으로 만든 /create-formal-verification-skill을 써서 TLA+ 같은 걸로 버그를 찾는 데엔 진짜 멋진 구석이 있어. 코드도, 유저 흐름이 어떻게 돌아가야 하는지도 더 잘 이해하게 되고, 안 그랬으면 유저가 봤을 문제까지 고칠 수 있거든
메시지 하나가 온 뒤 노트북과 폰에 보이는 것을 상황별로 그린 가상 예시다. · 이미지 원본 보기
인용된 글이 인용한 글 (2026-10-19) — pstack v0.15.27과 /create-formal-verification-skill 공개
lauren @poteto·
pstack v0.15.27에 새 스킬 /create-formal-verification-skill이 들어갔어!
아직 베타고, /create-verification-skill이랑 비슷하게 이것도 메타 스킬(meta-skill)이야. 네가 검증하고 싶은 특성을 바탕으로 새 스킬과 형식 검증(formal verification) 스위트를 만들어 주지. 예를 들어 상태 머신(state machine)이나 동시성(concurrency)이 있는 시스템을 TLA+로 모델링하고 싶을 수도 있고, rust에서 kani로 정의되지 않은 동작(undefined behavior)을 검사하고 싶을 수도 있어.
형식 검증이 처음이라면, 시스템의 속성과 불변식(invariant) — 항상 참이어야 하는 무언가 — 또는 '법칙'을 수학적으로 증명하는 거라고 생각하면 돼. 보통은 TLA+처럼 별도 언어로 프로그램을 모델링한 다음 그 스펙에 솔버를 돌린다는 뜻이야. kani나 @bendlang 같은 더 새로운 방식은 접근이 달라서 별도 언어가 없어. kani는 rust로 쓰고, bend는 bend로 쓰는 거지(bend도 프로그래밍 언어고, 증명은 법칙으로 쓰여서 그 타입 시스템으로 표현돼).
역사적으로 형식 검증은 모델링하고 증명을 쓰는 게 어려워서 주류가 된 적이 없어. 비즈니스 요구사항을 모델링하고 그걸 계속 동기화해 두는 건 꽤 어렵거든! 그래도 앞으로 형식 검증에서 혁신이 더 많이 나올 거라고 봐. 코드가 네가 의도한 대로 동작하는지 형식적으로 검증할 수 있으면, 에이전트가 올바른 소프트웨어를 쓰는 데 초능력이 생기니까.
그동안 나는 우리 코드를 TLA+로 모델링하는 실험을 해 왔는데, /create-formal-verification-skill로 만든 스킬로 벌써 버그를 여러 개 찾았어.
원본 (완역) 블록은 lauren의 본 글과, 본 글이 인용한 저자 본인의 2026-10-21 글, 그 글이 다시 인용한 2026-10-19 pstack 공지, 대화 속 작성자 답글 1개를 옮긴다. 작성자가 답한 kepano의 답글 1개는 답글의 맥락으로 함께 싣는다.
수록
본문 전량 수록. 첨부 차트 두 장 속 영어 글자는 그림 아래 표로 옮겼다. 조회수·좋아요 같은 X 화면 요소와 작성자가 답하지 않은 다른 사용자의 답글은 싣지 않는다.
시각
게시 시각은 한국 표준시(KST)로 적고, 본 글은 협정 세계시(UTC)를 함께 적는다. 세 글은 2026-10-19, 10-21, 10-23(KST)에 차례로 올라왔다.
용어
상태 차트(statechart), 형식 검증(formal verification), 불변식(invariant), 메타 스킬(meta-skill), 정의되지 않은 동작(undefined behavior), 모델 검사기(model checker). 차트 속 host·reaper·park·checkpoint는 호스트·회수기(reaper)·파킹(park)·체크포인트로 옮겼다.
고지
원문의 저작권은 lauren(@poteto)과 kepano(@kepano)에게 있다. 한국어 번역과 해설은 작성자들과 무관한 비공식 판이다.
