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

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