EthSystems hoàn thành xác minh hình thức của bể riêng tư, bao gồm quy định đến mã byte Sepolia

Công ty công nghệ bảo mật của Ethereum, EthSystems, đã thông báo hoàn thành việc xác minh hình thức cho bể bảo mật của mình (shielded pool), từ quy định bằng văn bản cho đến mã byte chạy trên mạng thử nghiệm Sepolia. Việc xác minh được thực hiện theo từng lớp bằng các công cụ khác nhau: mô hình, mạch và hàm băm sử dụng Lean, hợp đồng sử dụng Halmos và Kontrol, ví sử dụng Aeneas và Verus, và các trình xác minh và triển khai được kiểm tra bằng cách tái tạo từng byte.

Vấn đề double-spending và bảo toàn giá trị đã được xác minh bởi máy định lý Lean. Trong quá trình xác minh, nhóm đã phát hiện ra 6 vấn đề, trong đó 3 vấn đề xuất phát từ chính công cụ xác minh. Nhóm cũng đã liệt kê các giả định mà họ vẫn phụ thuộc: hàm băm không có va chạm, trình xác minh sẽ từ chối chứng minh giả mạo, hành vi hợp đồng nhất quán với mô hình.