딥마인드 AlphaProof Code, Signal 암호 코드를 4주 만에 형식 검증

저렇게 큰 코드베이스가 실용적으로도 안전하고 형식적으로도 안전하다는 게 신기함. Signal 코드 짠 사람들 실력이 대단한 듯.

암호 부분만 안전한 거고 나머지 코드는 장담 못 하지.

이건 Signal 앱을 검증한 게 아니라 암호 프로토콜만 검증한 거임.

OS가 안전하지 않으면 무슨 소용인가 싶기도 함. OS는 훨씬 복잡하고 검증도 더 어렵잖아.

정지 문제는 어떻게 처리함? 형식 증명은 잘 모르겠는데.

정지 문제랑 Lean은 별 상관 없음. 증명을 코드로 인코딩하면 컴파일러가 수학적 제약을 강제해주는 언어라고 보면 됨.

모든 프로그램의 정지 여부를 판별하는 건 불가능하지만, 특정 프로그램이 정지하는지 증명하는 건 여전히 쉬울 수 있음. 실무에서는 별로 문제 안 됨.

텔레그램도 좀 검증해서 '자체 암호 만들지 마라' 논쟁 좀 끝내줬으면.

텔레그램은 자체 암호를 만든 게 아니라 OTP 프로토콜을 이상하게 잘라 쓴 거고, 멀티 디바이스는 포기하고 TLS를 재발명하면서 기기 ID를 암호화 패킷 밖에 둬서 LAN에 영구 ID를 흘림.

작년엔 AI한테 일 맡기면 소프트웨어가 더 버그투성이 될 줄 알았는데, 이런 도구 보면 희망이 생김.

CI 돌릴 때마다 AI가 자기 giant proof 안 깨졌는지 확인하느라 1만 달러씩 나오면 재밌겠네.

우리 회사는 완전 에이전틱 코딩으로 갈아탄 뒤로 장애율이 오히려 떨어짐. 늘어난 개발 속도를 테스트랑 자동 리뷰 강화에 쏟아서 그런 듯. 6개월 지나도 처음 예상과 반대 결과임.

CPU도 언젠가 검증되면 좋겠는데, 오픈소스도 아니고 물리 시뮬레이션까지 필요해서 훨씬 어려움.

이 에이전트는 스펙 자체에 의문을 제기하진 않고 구현만 검증하는 것 같은데, 결국 Lean 코드 쓰면서 코드베이스 반복하는 일반 코딩 에이전트랑 뭐가 다른지 모르겠음.

Lean 프로세서 모델 위에서 도는 컴파일된 Rust 코드가 실제 CPU에서 도는 것과 같다는 건 어떻게 보장함?

이건 다른 AI 회사 홍보문 같은 느낌이 아니라 도구로 쓴다는 게 보임. 중요한 1%만 사람이 리뷰하는 게 똑똑함.

'무엇을 증명할지'는 가치 판단이 걸린 설계 문제라 AI가 대신 못 함.

곧 검증 안 한 소프트웨어를 돌리는 게 텔넷 쓰던 것처럼 미친 짓으로 보일 거임.

검증 가능한 범위는 아직 좁음. '이 프로그램은 안 죽는다' 정도는 되지만 '이 암호는 안전하다'나 GUI가 SQL DB랑 통신하는 프로그램은 거의 불가능하고, LLM 하나 더 얹는다고 될 문제가 아님.