EthSystems เสร็จสิ้นการตรวจสอบอย่างเป็นทางการของพูลความเป็นส่วนตัว ครอบคลุมตั้งแต่ข้อกำหนดจนถึงไบต์โค้ดบน Sepolia

องค์กรเทคโนโลยีความเป็นส่วนตัวสำหรับสถาบันบน Ethereum EthSystems ประกาศว่าได้เสร็จสิ้นการตรวจสอบอย่างเป็นทางการสำหรับพูลความเป็นส่วนตัว (shielded pool) ของตน ตั้งแต่ข้อกำหนดที่เขียนขึ้นจนถึงไบต์โค้ดที่ทำงานบนเครือข่ายทดสอบ Sepolia การตรวจสอบใช้เครื่องมือต่าง ๆ ในแต่ละชั้น: โมเดล วงจร และแฮชใช้ Lean สัญญาใช้ Halmos และ Kontrol กระเป๋าเงินใช้ Aeneas และ Verus ส่วนผู้ตรวจสอบและการติดตั้งได้รับการตรวจสอบผ่านการตรวจสอบการสร้างใหม่แบบไบต์ต่อไบต์ การใช้จ่ายซ้ำและการอนุรักษ์มูลค่าได้รับการตรวจสอบโดยเครื่องพิสูจน์ทฤษฎีบท Lean ในระหว่างการตรวจสอบพบปัญหาทั้งหมด 6 รายการ โดย 3 รายการพบในเครื่องมือตรวจสอบเอง ทีมยังได้ระบุสมมติฐานที่ยังต้องพึ่งพา ได้แก่ ความต้านทานการชนกันของแฮช ผู้ตรวจสอบจะปฏิเสธหลักฐานปลอม และพฤติกรรมของสัญญาสอดคล้องกับโมเดล