Hanzo, AI 에이전트 인프라를 위한 형식 증명을 공개하다

오늘 Hanzo AI 인프라 스택에 대한 기계 검증 형식 증명을 오픈 소스로 엽니다. 테스트도 감사도 아닙니다. Lean 4 타입 검사기가 확인하는 수학적 보증입니다.

증명된 것

에이전트 안전 (증명 6개)

• 능력 한계: 에이전트는 부여된 권한을 넘을 수 없다
• 상승 방지: 어떤 행동 서열도 허가되지 않은 능력에 이르지 않는다
• MCP 도구 호출: 컨텍스트 창은 호출 사이에 보존된다
• 위임의 단조성: 위임된 권한은 좁아질 뿐 넓어지지 않는다
• 작업 흐름 순서: DAG 실행은 의존 간선을 지킨다
• 기억 격리: 에이전트의 회상은 추가만 되고 관련성으로 제한된다

컴퓨팅 계층 (증명 4개)

• Proof of AI 합의: TEE 증명 사슬의 무결성과 비잔틴 장애에서의 품질 점수 수렴
• 기밀 컴퓨팅: 엔클레이브 격리와 증명의 신선도
• 스웜 조율: 작업 분배의 공정성과 부하 분산의 수렴
• 과금의 정확성: 측정된 사용량은 결코 더 청구되지 않는다

게이트웨이와 플랫폼 (증명 6개)

• 토큰 검증, 속도 제한의 공정성, 슬라이딩 윈도의 정확성
• blue-green 배포의 롤백 안전과 무중단 불변식
• SBOM 공급망의 완전성과 취약점 추적의 단조성

KMS (증명 1개)

• 비밀 접근 목록의 강제: 마스터 키는 HSM 경계를 넘지 않는다

숫자로

• Lean 4 파일 17개, sorry 0, 빌드 오류 0
• 공리 3개. 모두 하드웨어 경계를 모형화한다 (TEE 격리, HSM 둘레, 외부 인증)
• Lean 4.14.0 + Mathlib 4.14.0, 고정되어 재현 가능
• Apache 2.0 라이선스

AI 에이전트에 형식 검증이 필요한 이유

에이전트는 자율성을 얻고 있습니다. 도구를 쓰고, 돈을 다루고, 결정을 내립니다. 에이전트가 API 키와 데이터베이스와 고객에 닿을 때 «대체로 동작한다»는 충분하지 않습니다.

형식 검증은 가능한 어떤 실행도 안전 성질을 깨지 않음을 증명합니다. «1만 건을 시험했다»가 아닙니다. 전부입니다. 에이전트가 권한을 높일 수 없다는 증명은 확률이 아닙니다. 수학입니다.

링크

• 증명: github.com/hanzoai/proofs
• 논문: github.com/hanzoai/papers — 2014년부터 2026년까지의 연구 논문 34편
• 사이트: proofs.hanzo.network

형식 검증 작업은 AI 게이트웨이부터 에이전트 인프라까지 Hanzo 생태계 전체를 덮습니다. hanzoai/proofs도 보세요.