Hanzo công bố chứng minh hình thức cho hạ tầng tác nhân AI

Hôm nay chúng tôi mở mã nguồn các chứng minh hình thức được máy kiểm tra cho chồng hạ tầng Hanzo AI. Đây không phải bài kiểm thử hay cuộc kiểm toán. Đó là những bảo đảm toán học mà bộ kiểm tra kiểu của Lean 4 xác minh.

Những gì đã được chứng minh

An toàn tác nhân (6 chứng minh)

• Biên năng lực: tác nhân không thể vượt quyền đã cấp
• Ngăn leo thang: không chuỗi hành động nào dẫn tới năng lực chưa được phép
• Gọi công cụ MCP: cửa sổ ngữ cảnh được giữ qua các lần gọi
• Tính đơn điệu của ủy quyền: thẩm quyền được ủy chỉ thu hẹp, không bao giờ nới
• Thứ tự quy trình: thực thi DAG tôn trọng các cạnh phụ thuộc
• Cô lập bộ nhớ: hồi tưởng của tác nhân chỉ được nối thêm và bị chặn bởi mức liên quan

Tầng tính toán (4 chứng minh)

• Đồng thuận Proof of AI: toàn vẹn chuỗi chứng thực TEE và hội tụ điểm chất lượng khi có lỗi Byzantine
• Tính toán bảo mật: cô lập enclave và độ tươi của chứng thực
• Phối hợp bầy: phân việc công bằng và hội tụ cân bằng tải
• Tính đúng của tính phí: mức dùng đã đo không bao giờ tính thừa

Cổng và nền tảng (6 chứng minh)

• Xác thực token, tính công bằng của giới hạn tốc độ và tính đúng của cửa sổ trượt
• An toàn khi hoàn tác triển khai blue-green và bất biến không thời gian chết
• Đầy đủ chuỗi cung ứng SBOM và tính đơn điệu của việc theo dõi lỗ hổng

KMS (1 chứng minh)

• Thực thi danh sách truy cập bí mật: khóa chủ không bao giờ vượt biên HSM

Bằng con số

• 17 tệp Lean 4, 0 sorry, 0 lỗi biên dịch
• 3 tiên đề, tất cả mô hình hóa biên phần cứng (cô lập TEE, vành đai HSM, xác thực bên ngoài)
• Lean 4.14.0 + Mathlib 4.14.0, được ghim và tái lập được
• Giấy phép Apache 2.0

Vì sao xác minh hình thức cho tác nhân AI

Tác nhân đang tự chủ hơn. Chúng dùng công cụ, quản lý tiền và ra quyết định. «Thường thì chạy được» là chưa đủ khi tác nhân cầm khóa API, cơ sở dữ liệu và khách hàng của bạn.

Xác minh hình thức chứng minh rằng không lần thực thi nào có thể xảy ra vi phạm các tính chất an toàn. Không phải «chúng tôi thử 10.000 trường hợp». Mà là tất cả. Chứng minh rằng tác nhân không thể nâng đặc quyền không mang tính xác suất. Nó là toán học.

Liên kết

• Chứng minh: github.com/hanzoai/proofs
• Bài báo: github.com/hanzoai/papers — 34 bài nghiên cứu từ 2014 đến 2026
• Trang: proofs.hanzo.network

Công việc xác minh hình thức bao trùm hệ sinh thái Hanzo, từ cổng AI tới hạ tầng tác nhân. Xem thêm hanzoai/proofs.