2026-10-23 lauren(@poteto)의 X 인용 게시물. 에이전트가 상태 차트를 그려 pstack 형식 검증 스킬로 만든 스펙과 대조하게 하는 동반 스킬을 곧 낸다는 예고다. 같은 /statechart 스킬은 예고보다 16시간 앞서 공개 저장소에 병합됐고, 예고의 새 부분인 Pele 렌더링은 공개 코드에 아직 없다(신뢰도 B).
Posts for: #formal-verification
[LINK/SUMMARY] Learn TLA+ 원페이지 요약 — TLA+ 핵심을 한 장으로
『Learn TLA+』 35페이지 전체를 한 페이지로 압축했다. TLA+가 무엇이고 왜 쓰는지에서 시작해 장별 핵심 개념·문법·함정, 치트시트, 원문 주장 팩트체크까지 담았다.
[LINK/번역] TLA+ 배우기 — Learn TLA+ 한국어 완역
Hillel Wayne의 무료 TLA+ 입문서 『Learn TLA+』 35페이지 전체를 한국어로 옮겼다. 연산자·PlusCal·불변식에서 동시성·시간 속성·순수 TLA+까지, 그리고 최적화·예제·표준 모듈 레퍼런스까지. 코드와 스펙 파일은 원문 그대로다(CC BY 4.0).
[LINK/SUMMARY/번역] Opus 5.5로 Claude Agent SDK를 Lean으로 형식 검증했다 — 짧은 프롬프트 몇 개가 PR 16개로
Boris Cherny가 Opus 5.5에게 Claude Agent SDK와 claude.ts 상태기계를 Lean 4로 검증시켜 PR 16개를 얻은 과정의 완역과 팩트체크. 영상의 타임스탬프로 읽으면 ‘프롬프트 몇 개’는 Slack 메시지 6개와 사람의 PR 승인·리뷰였고, 버그 24개 중 증명 출신은 19개, 1차 수정의 구멍 6개는 리뷰가 잡았다.