ทำไมฉันถึงสามารถตรวจสอบโค้ดเทียบกับ spec ได้ แต่ไม่สามารถตรวจสอบตัว spec เองได้?

การพิสูจน์เชิงรูปนัยสำหรับ smart contract พิสูจน์ว่าโค้ดเป็นไปตามข้อกำหนดที่เขียนไว้ แต่ไม่สามารถระบุได้ว่าข้อกำหนดนั้นสะท้อนพฤติกรรมที่ตั้งใจของสัญญาได้จริงหรือไม่ การสำรวจ MDPI ปี 2025 ที่ครอบคลุมเครื่องมือตรวจสอบอัตโนมัติขั้นสูงสุดพบว่าตรวจพบได้เพียง 8 ถึง 20 เปอร์เซ็นต์ของช่องโหว่ที่สามารถถูกโจมตีได้ในระบบ production ขณะที่รายงานว่าครอบคลุมรูปแบบ syntax ระดับต่ำมากกว่า 90 เปอร์เซ็นต์ ช่องว่างอยู่ที่ spec: ข้อผิดพลาดเชิงตรรกะ เงื่อนไขการล็อคสินทรัพย์ และสมมติฐาน oracle แทบไม่เคยปรากฏใน spec เพราะวิศวกรไม่รู้วิธีระบุรายการก่อนที่การโจมตีจะแสดงให้เห็นถึงความจำเป็น บทความ PropertyGPT ของ NDSS 2025 ระบุโดยตรงว่าชุมชนยังขาดการสร้างคุณสมบัติที่ครอบคลุมโดยอัตโนมัติสำหรับการพิสูจน์เชิงรูปนัยที่มีประสิทธิผล การตรวจสอบทุกครั้งที่ผ่านสัญญาเทียบกับ spec ที่ไม่ครบถ้วนก่อให้เกิดระดับความมั่นใจที่เป็นเท็จ แทนที่จะเป็นระดับที่ปลอดภัย