ข้อบกพร่องของ @Zcash นำไปสู่การตรวจสอบแบบเป็นทางการของวงจรการชำระเงิน Orchard ฉันชื่นชอบและสนับสนุนมัน ฉันยังต้องการเน้นว่า @Starknet ได้ดำเนินการนี้—การตรวจสอบแบบเป็นทางการ—มานานกว่า 5 ปีแล้ว เป็นสิ่งสำคัญที่จะต้องสนับสนุนโครงการที่ยอดเยี่ยมเช่น Zcash ที่สามารถตอบสนองอย่างรวดเร็ว เช่น ในกรณีนี้ และยังสำคัญที่จะต้องยอมรับโครงการที่มีความพร้อมสำหรับอนาคตและนำหน้าผู้อื่น เช่น Starknet (รายละเอียดอยู่ในบทความด้านล่าง) ฉันเคยพูดบ่อยว่า Starknet คือระบบที่มีสิ่งที่โซ่อื่นอ้างว่าจะมีในเร็วๆ นี้ ซึ่งเป็นความจริงมาหลายเรื่องแล้ว เราอยู่แถวหน้าของทางเลือกที่ไม่เป็นที่นิยมหลายอย่าง ซึ่งตอนนี้ทุกคนตระหนักแล้วว่าสำคัญ รวมถึง ZK-STARKs ที่ปลอดภัยจากควอนตัมซึ่งเป็นโซลูชันที่ดีที่สุดสำหรับการขยายขนาดและความเป็นส่วนตัว, zkVMs แบบเบา (Cairo ดีที่สุด), การมีอยู่ของข้อมูล Validium และการตรวจสอบแบบเป็นทางการ การตรวจสอบแบบเป็นทางการหมายถึงการใช้เครื่องมืออัตโนมัติ เช่น ระบบ Lean เพื่อพิสูจน์ทางคณิตศาสตร์ว่าโค้ดของคุณปลอดภัย การจับทุกแง่มุมของความหมายว่า “โค้ดปลอดภัย” นั้นยากมาก แต่ภายใต้การนำของ CTO ของเรา @LiorGoldberg2 (ผู้ร่วมสร้าง Cairo zkVM และภาษา) เราได้ดำเนินการมานานกว่า 5 ปีแล้ว งานวิจัยชิ้นแรกเกี่ยวกับการตรวจสอบแบบเป็นทางการของข้ออ้างที่เกี่ยวข้องกับ ZK (ศาสตราจารย์ Jeremy Avigad, Yoav Seginer และอื่นๆ) แสดงให้เห็นว่าชุดข้อจำกัดพหุนามที่กำหนด Cairo VM นั้นถูกต้อง หากคุณติดตามข่าวในช่วงไม่กี่วันที่ผ่านมา ข้อบกพร่องที่ถูกค้นพบโดย AI และตอนนี้ได้รับการแก้ไขสำหรับ Zcash (อีกโครงการหนึ่งที่ฉันร่วมก่อตั้ง และฉันรู้สึกภาคภูมิใจและสนับสนุนอย่างมาก) เกี่ยวข้องกับข้อจำกัดที่หายไป การตัดสินใจตรวจสอบโค้ดของพวกเขาเพื่อป้องกันข้อบกพร่องอื่นๆ เช่น นี้ เป็นขั้นตอนที่ถูกต้อง การดำเนินการตรวจสอบแบบนี้สำหรับ Cairo core VM ได้ให้ความแน่นอนทางคณิตศาสตร์แก่ทีม StarkWare ว่าไม่มีข้อจำกัดใดหายไปใน Cairo VM ของเรา ดังนั้น นอกจากการพิสูจน์ Cairo core VM แล้ว เรายังได้พิสูจน์ระบบ S-two STARK ส่วนหนึ่งของคอมไพเลอร์ และฟังก์ชันจำนวนมากในไลบรารีมาตรฐานของ Cairo งานเสร็จแล้วหรือยัง? ยังไม่เสร็จ มีอีกหลายสิ่งหลายอย่างที่สามารถพิสูจน์แบบเป็นทางการได้ แต่เรายังคงมุ่งมั่นที่จะดำเนินการพิสูจน์แบบเป็นทางการต่อไปสำหรับคุณสมบัติหลักทั้งหมดที่เกี่ยวข้องกับความถูกต้องและความปลอดภัยของระบบของเรา เป็นเรื่องดีที่เห็นโครงการอื่นๆ เริ่มรับเอาการตรวจสอบแบบเป็นทางการเป็นเครื่องมือสำคัญ ฉันภูมิใจที่ StarkWare เป็นผู้นำเส้นทางในด้านนี้เช่นกัน นี่คือสิ่งที่ “บล็อกเชนที่พร้อมสำหรับอนาคต” หมายถึงสำหรับเรา ต้องการเรียนรู้เพิ่มเติม? นี่คือรายงานโดยละเอียดเกี่ยวกับความพยายามในการพิสูจน์ด้วย Lean ของเราในช่วงไม่กี่ปีที่ผ่านมา