Opus 5.5로 Claude Agent SDK를 Lean으로 형식 검증했다

boris · 9월 18일 오후 12:23 · 답글 13개

we have been getting lots of reports like this across cli and desktop <slack link> can you fuzz the cli + desktop apps to trigger de-auths? i think there's a bunch of bugs that can cause this even when the user should still be authenticated. fix any cases you can reliably repro (cli와 데스크톱 전반에서 이런 보고가 많이 들어오고 있어 <slack 링크> cli + 데스크톱 앱을 퍼징해서 de-auth를 유발해볼 수 있어? 유저가 여전히 인증된 상태여야 하는데도 이걸 일으키는 버그가 꽤 있을 것 같아. 안정적으로 재현되는 케이스는 고쳐줘)

boris · 오후 10:33 (이전 날) · 답글 15개

큐에 쌓인 메시지가 모델에 전달되기 전까지 회색으로 표시되도록 하는 CLI UX 요청.

boris · 어제 오후 10:03

Use lean to verify the sdk and Claude.ts state machine (lean으로 sdk와 Claude.ts 상태기계를 검증해)

Claude · 어제 오후 10:05 (작업 목록, 시간이 지나며 수정됨)

SDK와 claude.ts 상태기계를 Lean으로 검증하는 중

• ✱ 코드에서 Lean 4 모델 여섯 개 작성 중 (stream, retry, turn loop, engine, session phase, SDK control).
• ○ 각 모델을 실제 코드와 대조해 독립적으로 리뷰.
• ○ 발견 사항 게시.
• ○ 전 모델 2차 증명 실행.
• ○ 최종 감사: 빌드, 공리, sorry 없음.

같은 작업 목록의 이후 수정본:

• ✓ 코드에서 Lean 4 모델 여섯 개 작성 완료 (stream, retry, turn loop, engine, session phase, SDK control), sorry 없음.
• ✓ 각 모델 독립 리뷰: 반례를 실제 코드에서 재현했고, 실제 트레이스를 모델에 재생했습니다.
• ✓ 발견 사항은 아래에 게시했습니다.
• ✓ 전 모델 2차 증명 완료; engine 모델이 실제 실행 400건을 모두 수용합니다.
• ✓ 최종 감사: lake build 그린, 정리 1,359개 중 1,359개가 표준 공리 세 개 위에서 성립, sorry 없음. 차트와 소스는 아래에 게시했습니다.
• ✓ 초안 수정 PR 여섯 개 오픈: #72128 session phase, #72130 turn loop, #72135 SDK control, #72140 stream, #72145 retry, #72162 engine.

Claude · 오늘 오전 12:08

상태기계 여섯 개를 Lean 4로 모델링하고 증명했습니다 (sorry 없음). 증명이 만들어낸 반례는 모두 실제 코드에서 재현되며, 초안 PR 다섯 개가 이를 고칩니다. 각 PR에는 수정 전에는 실패하고 수정 후에는 통과하는 테스트가 붙어 있습니다:

• #72128 session phase: 샌드박스 네트워크 요청이 권한 프롬프트와 겹치면, 둘 다 응답한 뒤에도 세션이 requires_action에 남고, 때로는 다음 턴 내내 그 상태가 이어집니다.
• #72130 turn loop: 형식이 잘못된 툴 호출에 대한 재시도와 max_tokens 잘림에서의 복구가 서로의 가드를 리셋해서, 두 출력이 번갈아 나오면 무한히 루프하고 --max-turns 1로도 멈추지 않습니다.
• #72140 stream: 응답 도중에 깔끔하게 끝나버린 바디가 성공으로 처리되며, stop reason도 없고 비용도 기록되지 않습니다. 경로에 게이트웨이나 서드파티(3P)가 있어야 발생합니다.
• #72145 retry: persistent 모드에서 429/529 대기가 다른 오류용 예산을 소진하고, Retry-After가 하루인 503은 그 하루를 통째로 잠듭니다.
• #72135 SDK control protocol: 취소됐다가 다시 전달된 권한 요청이 아무도 취소할 수 없는 핸들러를 남기고, transport close가 예외를 던지면 대기 중인 awaiter가 전부 좌초됩니다.

성립한 것: 턴당 결과 하나, 순서대로, init이 먼저; idle 전에 result; 재시도 상한과 abort; 스트림은 닫힌 블록만 내보냄.

engine 모델은 아직 실제 실행 몇 건과 불일치하므로 그 증명은 잠정으로 봐 주세요. 마지막 증명이 끝나면 Lean 소스와 차트를 올리겠습니다.

Claude · 오늘 오전 1:07

이제 여섯 모델 모두 lake build로 빌드됩니다: 정리 1,359개, sorry 없음, 표준 공리 세 개만 사용, 그리고 모든 모델이 재생한 실제 실행을 전부 수용합니다 (재작업한 engine 모델은 이제 400건 중 400건). 타르볼에는 Lean 소스, 빌드 절차가 담긴 README, 각 전이마다 file:line을 인용한 모듈별 스펙, 그리고 각 모델의 명시된 가정과 증명하지 않는 것이 들어 있습니다.

범례: 증명된 불변식(보조 보조정리 포함) / 수정 증명(충분성 + 일치) / 반례 트레이스(정리) / 기타(파일 내 적합성 재생). Lean 4 커널이 검사한 정리 + 보조정리 (sorry 없음; 공리: propext / Quot.sound / Classical.choice만).

첨부: lean-verify.tar.gz

Claude · 오늘 오전 1:12

engine용 여섯 번째 초안 PR: #72162. 턴의 builder가 실패하고 그 뒤에 오는 flush 도중에 consumer가 스트림에서 빠져나가면, 그 턴은 한 번도 취소됐다고 보고되지 않았습니다. consumer가 첫 next() 전에 return()을 호출해도 같은 일이 벌어졌고, 버려진 뒤 늦게 도착한 send()는 조용히 큐에 쌓였습니다. 셋 다 먼저 main에서 재현했습니다 (새 테스트 8개 중 7개가 수정 전 실패, 수정 후 전부 통과). 심각도 낮음: headless 세션은 uuid 없이 턴을 보내므로 SDK 소비자는 오늘 당장 이 문제를 겪을 수 없습니다.

boris · 오늘 오후 12:59

publush all prs (PR 전부 공개해)

Claude · 오늘 오후 1:03

여섯 개 모두 리뷰 준비 완료로 표시했습니다.

boris · 오늘 오후 1:05

take that same proof and simplify the code (그 증명을 그대로 가져다 코드를 단순화해)

and mark all prs merge when ready (그리고 PR 전부 merge when ready로 표시해)

Claude · 오늘 오후 1:06 (작업 목록)

Lean 증명을 바탕으로 코드를 단순화하고, PR 전부 랜딩하는 중

• ✱ 수정 PR 여섯 개에 merge-when-ready 켜는 중.
• ○ 각 모듈을 그 Lean 증명에서 출발해 단순화, 모듈당 초안 PR 하나.

이후 수정본:

• ✓ 수정 PR 여섯 개 중 다섯 개 머지: #72128 session, #72130 turn loop, #72140 stream, #72145 retry, #72162 engine.
• ✱ #72135 SDK control: 새 커밋에서 승인됨, auto-merge 켜짐; 매시간 지켜보는 중.
• ✓ 초안 열 개 모두 공개되고 Boris가 승인; 아홉 개에 merge-when-ready 켜짐: 단순화 #72479, #72503, #72513, #72517, #72516; 후속 수정 #72499, #72508, #72509, #72515.
• ○ #72518 SDK control 단순화: #72135가 랜딩되고 main으로 리타겟되면 auto-merge 켜기.
• ✱ 열 개를 머지까지 몰고 가는 중: 초안에서 벗어났으니 전체 CI를 돌리고, 같은 파일을 건드리는 각 쌍(session, retry, stream, turn loop)에서 첫 번째가 랜딩되는 대로 두 번째를 리베이스.
• ○ 빌드된 CLI를 상대로 후속 수정 네 개의 엔드투엔드 실행.

Claude · 오늘 오후 1:16

여섯 개 모두 auto-merge가 켜졌습니다.

단순화에 관해: 증명에 따르면 거의 모든 플래그와 분기가 도달 가능해서 지울 것이 별로 없습니다. 증명이 허용하는 것은 같은 로직의 복사본들을 하나로 합치는 일입니다. 큰 것 둘은 claude.ts(복사-붙여넣기된 정리 경로 여러 개)와 query.ts(루프가 재시작되는 열 군데 각각이 상태 전체를 손으로 다시 만듭니다)에 있습니다. 모듈당 초안 PR 하나씩 진행 중이며, 각각의 수정 PR 위에 스택했습니다.

정정: turn-loop 수정 #72130은 아직 모든 종료가 터미널 메시지로 끝난다는 것을 보장하지 않습니다. 증명된 변형이 가정하는 것의 일부만 커버합니다. 나머지를 위한 후속 수정을 열겠습니다.

Claude · 오늘 오후 2:32 (이후 취소선 처리·수정됨)

#72135 (SDK control)는 다시 승인이 필요합니다. main과의 충돌을 해소하면서 이전 승인이 무효가 됐기 때문입니다. 나머지 수정 PR 다섯 개는 머지됐습니다.

단순화 PR 세 개가 초안으로 올라와 있고, 테스트는 변경 없음:

• #72479 session: settle 경로 세 개 대신 하나.
• #72503 engine: 트래커 두 개 대신 open-turns 목록 하나.
• #72513 retry: 단순 backoff를 chunked-sleep 루프에 접어 넣음.

stream, turn-loop, SDK-control 것은 뒤따릅니다. 리뷰 코멘트에 대한 수정도 초안으로 올라와 있습니다: #72499 retry, #72508 stream, #72509 session.

Claude · 오늘 오후 2:41

정정: #72135 (SDK control)는 결국 손댈 필요가 없습니다. 이전 승인이 새 커밋으로 이월되어 스스로 머지될 겁니다.

마지막 단순화 초안 세 개가 올라와 총 여섯 개가 됐습니다:

• #72517 stream: 메시지를 닫는 코드 복사본 세 개와 abort 출구 두 개가 각각 하나가 되어, claude.ts에서 105줄 감소.
• #72516 turn loop: continue마다 있던 재시도 가드 리셋이 이제 테이블 하나에서 나옵니다.
• #72518 SDK control: 모든 응답이 write 지점 하나를, 모든 cancel이 헬퍼 하나를 거칩니다. #72135가 머지될 때까지 그 위에 스택되어 있습니다.

turn-loop 리뷰 수정은 초안 #72515에 있으므로 리뷰 후속 네 개도 모두 올라왔습니다. 리뷰하실 때 볼 것 하나: session 후속 #72509는 hasStandingPrompt()도 좁히는데, 이는 리뷰 코멘트가 요청한 것보다 더 나간 변경입니다.

boris · 오늘 오후 2:55

publish and mark merge when ready (공개하고 merge when ready로 표시해)

Claude · 오늘 오후 2:58

열 개 모두 merge-when-ready를 켜서 공개했습니다. 각각 머지되려면 승인이 필요합니다:

• 단순화: #72479 session, #72503 engine, #72513 retry, #72517 stream, #72516 turn loop, #72518 SDK control.
• 리뷰 후속 수정: #72499 retry, #72508 stream, #72509 session, #72515 turn loop.

#72518은 #72135 위에 스택되어 있어, 그것이 랜딩되면 auto-merge를 켜겠습니다. 네 쌍이 같은 파일을 건드리므로 첫 번째가 머지되는 대로 각 쌍의 두 번째를 리베이스하겠습니다.

boris · 오늘 오후 2:59

how many prs was that total? how many bugs caught, lines added/removed (excluding tests), and tests added/removed? (총 PR이 몇 개였지? 잡은 버그 수, 추가/삭제 라인 수(테스트 제외), 추가/삭제된 테스트 수는?)

Claude · 오늘 오후 3:00 (작업 목록)

PR 16개 집계 중

• ✓ PR 16개: 증명에서 나온 수정 여섯, 단순화 여섯, 리뷰 후속 넷.
• ✓ 각 PR의 diff에서 집계: 비테스트 라인 +1,381 / −1,163, 테스트 +94 / −9, 그리고 항목별 버그 목록 (증명이 찾은 19개, 리뷰에서 5개 더, 거기에 1차 수정의 빈틈 6개).
• ✱ 인포그래픽 렌더링 중.

boris · 오늘 오후 3:00

render it as a small infographic (작은 인포그래픽으로 렌더링해)

Claude · 오늘 오후 3:04

PR 16개, 버그 24개 수정: 증명이 찾은 19개와, 이미 main에 있다가 리뷰에서 드러난 5개. 리뷰는 제 1차 수정의 빈틈 6개도 잡아냈고, 후속 PR 네 개가 그것을 닫습니다. 테스트를 제외하면 코드는 순 218줄 늘었고 (+1,381 / −1,163), 단순화 PR 여섯 개만 놓고 보면 195줄을 줄입니다. 테스트 케이스 94개 추가, 9개 제거 (그중 8개는 재작성, 1개는 삭제).

첨부: 인포그래픽 「SDK + claude.ts 상태기계의 Lean 4 검증」 (아래 저자 답글의 이미지와 동일)

Claude · 오늘 오후 4:01

@boris #72515가 승인이 필요한 마지막 하나입니다. 새 head는 블로킹 리뷰 발견 두 건(이미지가 너무 큰 배치가 다음 프롬프트를 다시 실패하게 만들 수 있었음)을 고치고, #72516이 랜딩된 뒤 main을 머지해 넣었습니다. 리뷰는 깨끗하며 승인되면 스스로 머지됩니다. 16개 중 13개 머지됨; #72518과 #72508은 승인되어 랜딩 중입니다.

Claude · 오늘 오후 4:47

PR 16개 모두 머지됐습니다.

chrbx128 (@chrbx128) · 2026-09-23 08:42 KST

참고로, 범용 서브에이전트에서 쿼터 사용량이 높게 나오는데 이를 조정하는 방법에 관한 문서가 거의 없네요. 가이드라인이 있나요?

Boris Cherny (@bcherny) · 2026-09-23 08:44 KST

Claude에게 서브에이전트를 덜 쓰라고 하거나, permissions에서 서브에이전트를 비활성화하라고 하라

Anthony (@anthonyistyping) · 2026-09-23 09:23 KST

그냥 라이브 스트리밍 해주시면 안 되나요, 어떻게 프롬프트하는지 구경하게 xD

Boris Cherny (@bcherny) · 2026-09-23 10:33 KST

위 영상이 나다

Hillel (@hillelogram) · 2026-09-23 10:24 KST

형식 검증 하는 사람으로서 내 경험상, AI는 고수준 시스템 속성을 생각해내는 데 정말 정말 정말 형편없었다(「초보」 수준 정도). 마지막으로 써본 게 Fable 5.1인데, Opus 5.5는 좀 나은가?

Boris Cherny (@bcherny) · 2026-09-23 10:33 KST

내 느낌으로는 훨씬 낫다. 다만 당신 생각이 궁금하다.

그나저나 Practical TLA+ 정말 재밌게 읽었다! 몇 년 전에 읽은 그 책이 이걸 시도해보게 한 계기였다