ผู้ร่วมก่อตั้ง Ethereum Vitalik Buterin เผยแพร่บทวิเคราะห์เชิงลึกเมื่อวันที่ 18 พฤษภาคม โดยหารือถึงสถานะและแนวโน้มของเทคนิคการพิสูจน์ความถูกต้องเชิงรูปแบบ (Formal Verification) โดยเห็นว่า การพิสูจน์ความถูกต้องเชิงรูปแบบที่ได้รับความช่วยเหลือจาก AI จะกลายเป็น “รูปแบบสุดท้ายของการพัฒนาซอฟต์แวร์” และชี้ว่า Ethereum จะเป็นส่วนสำคัญของสถาปัตยกรรม “แกนความปลอดภัย” ในอนาคต
หลักการแกนกลางของการพิสูจน์ความถูกต้องเชิงรูปแบบและกรณีใช้งานที่เหมาะสม
จากบทความของ Vitalik ระบุว่า การพิสูจน์ความถูกต้องเชิงรูปแบบเหมาะเป็นพิเศษกับสถานการณ์ที่ “เป้าหมายยากกว่าการทำให้สำเร็จ” เขาระบุชิ้นส่วนเทคโนโลยีหลัก 4 ประเภทของการอัปเกรดครั้งถัดไปของ Ethereum อย่างชัดเจน:
ลายเซ็นต้านทานควอนตัม：งานพิสูจน์ความถูกต้องเชิงรูปแบบสำหรับตัวแปรลายเซ็นของ SPHINCS แล้วมีอยู่
ระบบพิสูจน์ STARK：โปรเจกต์ Arklib มุ่งสร้างการใช้งาน STARK ที่ผ่านการพิสูจน์ความถูกต้องเชิงรูปแบบอย่างครบถ้วน
อัลกอริทึมฉันทามติทนต่อความผิดพลาดแบบไบแซนไทน์：ขณะนี้มุ่งทำให้มีการกำหนดและพิสูจน์คุณสมบัติความปลอดภัยของฉันทามติ Lean อย่างเป็นทางการ
ZK-EVM：โปรเจกต์ evm-asm ตั้งใจสร้างการใช้งาน EVM ที่ผ่านการพิสูจน์ความถูกต้องเชิงรูปแบบอย่างครบถ้วน (เขียนด้วยภาษาแอสเซมบลี RISC-V โดยตรง)
Vitalik อ้างคำกล่าวของ Yoichi Hirai และเรียกวิธีนี้ว่า “รูปแบบสุดท้ายของการพัฒนาซอฟต์แวร์”
ทิศทางการพัฒนาสถาปัตยกรรม “แกนความปลอดภัย” ตามที่ Vitalik อธิบาย
จากบทความของ Vitalik ระบุ เขาอธิบายรูปแบบการพัฒนาสถาปัตยกรรมซอฟต์แวร์ในอนาคต:
แกนความปลอดภัย：เสริมความแข็งแกร่งอย่างต่อเนื่องด้วยวิธีการเชิงรูปแบบ เพื่อรองรับระดับความไว้วางใจสูงสุด Vitalik ระบุชัดว่า Ethereum แกนหลักของระบบปฏิบัติการ และแอปพลิเคชันที่เกี่ยวข้องกับ IoT จะกลายเป็นแกนความปลอดภัย
ขอบเขตที่ไม่ปลอดภัย：ส่วนประกอบรันในสภาพแวดล้อมแบบแซนด์บ็อกซ์ ให้สิทธิ์ขั้นต่ำที่จำเป็นต่อการทำงานให้สำเร็จ หากส่วนประกอบขอบเขตล้มเหลว แกนความปลอดภัยจะให้การปกป้อง
ขีดจำกัดในการยืนยันและรูปแบบความล้มเหลวของการพิสูจน์ความถูกต้องเชิงรูปแบบ
Vitalik ยอมรับว่าการพิสูจน์ความถูกต้องเชิงรูปแบบไม่ได้เป็นทุกคำตอบ โดยอ้างงานของนักวิจัยอย่าง Nadim Kobeissi (Cryspen) และยืนยันรูปแบบความล้มเหลวหลัก 3 ประเภท: การพิสูจน์บางส่วนถูกละเลย (พิสูจน์แค่บางส่วนของโค้ด แต่ส่วนที่ยังไม่ได้พิสูจน์กลับมีข้อบกพร่องสำคัญ) การละเลยข้อกำหนด (ข้อกำหนดด้านความปลอดภัยเองผิด หรือมีสมมติฐานผิดอยู่ในการพิสูจน์) การโจมตีแบบช่องทางข้าง (การโจมตีผ่านช่องทางด้านที่บริเวณเส้นแบ่งระหว่างซอฟต์แวร์และฮาร์ดแวร์นั้น ยากที่จะถูกจับด้วยโมเดลที่มีอยู่)
Vitalik เน้นว่า “ความถูกต้องที่พิสูจน์ได้” ในแก่นแท้แล้วคือการตรวจสอบความสอดคล้องภายในระหว่างเจตนาที่แตกต่างกัน ไม่ใช่การเทียบได้แบบแน่นอนกับเจตนาจริงของมนุษย์
เครื่องมือสำหรับการพิสูจน์ความถูกต้องเชิงรูปแบบที่ช่วยโดย AI
จากเครื่องมือที่ Vitalik ยืนยันว่าใช้งานได้: Lean (ภาษาพิสูจน์ทางคณิตศาสตร์ ที่ตรวจสอบทฤษฎีบทได้อัตโนมัติ) Claude และ Deepseek 4 Pro (Vitalik ยืนยันว่าเพียงพอสำหรับการเขียน Lean proofs) Leanstral (โมเดลน้ำหนักแบบโอเพนเวต 1190 ล้านพารามิเตอร์ ปรับแต่งเฉพาะทางสำหรับการเขียนโค้ด Lean สามารถรันในเครื่องได้ และผลการทดสอบสมรรถนะดีกว่าโมเดลเอนกประสงค์ขนาดใหญ่จำนวนมาก)
คำถามที่พบบ่อย
ทำไม Vitalik ถึงมองว่า Ethereum ควรเป็น “แกนความปลอดภัย”?
จากบทความของ Vitalik Ethereum คล้ายกับแกนหลักของระบบปฏิบัติการ โดยแบกรับระดับความไว้วางใจสูงสุดในกระบวนการดิจิทัลไลเซชันของสังคม เขาระบุว่าเป้าหมายการออกแบบแกนความปลอดภัยคือทำให้ความปลอดภัยถึงมาตรฐานที่ไม่อนุญาตให้โค้ดที่มีช่องโหว่แพร่หลาย และนำกำลังประมวลผลเพิ่มเติมที่ AI นำมามุ่งเพื่อยกระดับความปลอดภัยของแกนความปลอดภัย
ทำไมการพิสูจน์ความถูกต้องเชิงรูปแบบถึงเหมาะเป็นพิเศษกับ STARK, ZK-EVM และเทคโนโลยีที่คล้ายกัน?
จากการวิเคราะห์ของ Vitalik จุดร่วมของเทคโนโลยีเหล่านี้คือ “เป้าหมายยากกว่าการทำให้สำเร็จ” ซึ่งคุณสมบัติความปลอดภัยสามารถนิยามได้อย่างชัดเจนด้วยภาษาคณิตศาสตร์ แต่การนำไปใช้งานจริงนั้นซับซ้อนมาก—นี่คือกรณีที่การพิสูจน์ความถูกต้องเชิงรูปแบบสามารถทำงานได้อย่างเต็มที่
Vitalik แนะนำให้ผู้พัฒนาใช้งานการพิสูจน์ความถูกต้องเชิงรูปแบบที่ช่วยด้วย AI อย่างไรในทางปฏิบัติ?
จากบทความของ Vitalik เขาแนะนำให้ให้ AI เขียนโค้ด Lean และคณิตศาสตร์สำหรับการพิสูจน์ โดยผู้ใช้ปลายทางเพียงตรวจสอบว่าประโยคที่ถูกพิสูจน์ตรงกับความคาดหวังหรือไม่ ไม่จำเป็นต้องเขียนโค้ดพิสูจน์ระดับล่างที่ยุ่งยากด้วยตนเอง เขายืนยันว่า Claude, Deepseek 4 Pro และ Leanstral เป็นเครื่องมือหลักที่ใช้งานได้ในปัจจุบัน
