โค้ดของ AlphaProof พิสูจน์ว่าการเข้ารหัสของ Signal ถูกต้อง — ถึงระดับไบนารีที่คอมไพล์แล้ว

หกล้านห้าแสนบรรทัดของ Lean ผลิตขึ้นในสี่สัปดาห์ โดยทีมเอเจนต์ที่ไม่มีมนุษย์ช่วยเขียน นั่นคือตัวเลขพาดหัวที่ Google DeepMind เผยแพร่เมื่อวันที่ 10 พฤศจิกายน 2026 สำหรับ AlphaProof Code กรอบงานแบบเอเจนต์สำหรับการตรวจสอบเชิงรูปแบบที่ห้องแล็บใช้ตรวจสอบด้วยเครื่องซึ่งแกนการเข้ารหัสของโปรโตคอล Signal — และที่ผิดปกติคือตรวจสอบในระดับไบนารี AArch64 ที่คอมไพล์แล้ว แทนที่จะเป็นเอกสารการออกแบบที่อยู่เหนือขึ้นไป โมเดลที่ทำงานนี้เป็นอีกคำถามหนึ่ง คีย์ API หนึ่งคีย์ในราคาตามรายการของผู้ให้บริการ โดยมีมาร์กอัป 0% เอนจินของเอเจนต์ที่ทำการพิสูจน์ไม่ใช่สิ่งที่เราให้บริการ

เฟรมเวิร์กนี้ไม่ใช่โมเดลที่คุณเรียกใช้ได้ แต่เป็นฮาร์เนส: ผู้เชี่ยวชาญที่เป็นมนุษย์เป็นผู้กำหนดว่าอะไรต้องเป็นจริง โมเดลหลากหลายชนิดจะเปลี่ยนเป้าหมายเหล่านั้นให้เป็นสเปกใน Lean จากนั้นทีมของเอเจนต์ที่เขียนบทพิสูจน์ — ในบล็อกระบุชื่อ G​emini Carbon เป็นเอนจิน — จะเติมบทพิสูจน์ให้สมบูรณ์จนเคอร์เนลของ Lean ยอมรับ สิ่งที่เผยแพร่พร้อมประกาศคือชุดอาร์ติแฟกต์ที่ github.com/google-deepmind/code-verification และบทความทางเทคนิคที่ตรงไปตรงมาเรื่องขอบเขตของผลลัพธ์มากกว่าบล็อกโพสต์มาก สิ่งที่จะกล่าวต่อไปส่วนใหญ่มาจากบทความนั้น เพราะบทความคือที่ที่ตัวเลขที่น่าสนใจอยู่

อะไรที่ได้รับการพิสูจน์จริง ๆ และพิสูจน์กับอะไร

เป้าหมายคือ libsignal v0.105.4 พร้อม spqr v1.6.0 ซึ่งสร้างโดย rustc 1.98.1 รุ่นปกติ ลิงก์แบบสแตติกกับ musl และสร้างออกมาเป็นไฟล์ปฏิบัติการ Linux AArch64 ไฟล์เดียว รายละเอียดนี้สำคัญกว่าเบนช์มาร์กใด ๆ เพราะการพิสูจน์นั้นเกี่ยวกับไบต์ที่จะทำงานบนโทรศัพท์ ไม่ใช่เกี่ยวกับฟังก์ชัน Rust ที่ไว้วางใจให้คอมไพเลอร์แปลอย่างซื่อตรง ทีมงานตรวจสอบซอร์สโค้ด libsignal ประมาณ 560 KB คำสั่ง AArch64 ประมาณ 140,000 คำสั่ง และทำเช่นนั้นโดยการเขียนแบบจำลอง Lean ของชุดคำสั่ง — 467 คำสั่งและ 31 system call ใน 7,578 บรรทัด — แล้วพิสูจน์ว่าอิมเมจ ELF จริง เมื่อโหลดและเรียกทำงานภายใต้แบบจำลองนั้น ยังคงรักษาคุณสมบัติด้านความปลอดภัยไว้

คุณสมบัติเหล่านี้คือสิ่งที่วิศวกรด้านโปรโตคอลต้องการ ทฤษฎีบทเชิงสัญลักษณ์สิบข้อครอบคลุม forward secrecy, post-compromise security, ความลับของผู้เริ่มต้นและผู้ตอบสนอง, การพิสูจน์ตัวตน และข้อสรุปย่อยห้าข้อของทฤษฎีบทที่ 1 ของ PQXDH ผลลัพธ์หลักมีชื่อว่า signal_session_secure_placed. นอกจากนี้ยังมีเส้นทางการวิเคราะห์เชิงคำนวณที่มีขอบเขตเป็นรูปธรรม และเส้นทางทั้งสองใช้แบบจำลองผู้โจมตีที่แตกต่างกัน: ฝั่งสัญลักษณ์ (Dolev–Yao ผ่านเฟรมเวิร์ก DyLean) ยังครอบคลุมผู้โจมตีควอนตัมที่ทำลาย Diffie–Hellman หลังการจับมือกันได้ด้วย ในขณะที่ฝั่งการคำนวณครอบคลุมเฉพาะผู้โจมตีแบบคลาสสิกเท่านั้น

หกล้านบรรทัดเหล่านั้นไปที่ไหน

“กว่าหกล้านบรรทัด” เป็นถ้อยคำที่บล็อกใช้ และมันถูกต้องแต่หยาบเกินไป ส่วนการแจกแจงรายละเอียดในเอกสารวิชาการคือส่วนที่มีประโยชน์ และควรอ่านในฐานะตารางต้นทุนมากกว่าการอวด

• การพิสูจน์สำหรับไบนารี — 5.3 ล้านบรรทัด ซึ่งเป็นส่วนใหญ่ของงาน ครอบคลุมอรรถศาสตร์ของโค้ดเครื่องและการรีไฟน์เมนต์จากแบบจำลองเชิงสัญลักษณ์ลงไปจนถึงโปรแกรมที่เรียกทำงานได้

• การพิสูจน์เชิงคำนวณ — ประมาณ 860,000 บรรทัด

• การพิสูจน์เชิงสัญลักษณ์ — ประมาณ 350,000 บรรทัด

• การพิสูจน์การหักล้างบั๊ก — ประมาณ 140,000 บรรทัด สำหรับช่องโหว่สองรายการที่ถูกนำกลับมาโดยเจตนาตามที่อธิบายไว้ด้านล่าง

• หลักฐานของตัวจัดสรร — ประมาณ 70,000 บรรทัด

เกือบเจ็ดล้านบรรทัดหากนับคอมเมนต์และบรรทัดว่าง ซึ่งบทความวิชาการนับแต่บล็อกไม่นับ ไม่ว่าจะทางไหน อัตราส่วนที่สำคัญคือระหว่างบทพิสูจน์กับสิ่งที่ถูกพิสูจน์: Lean 6.5 ล้านบรรทัดเพื่อพิสูจน์คุณสมบัติของไบนารีขนาด 560 KB อัตราส่วนนี้คือมาตรวัดที่ซื่อตรงว่าวิธีนี้ยังห่างไกลจากการเป็นเรื่องปกติเพียงใด และเป็นตัวเลขที่ควรอ้างอิงเมื่อมีคนถามว่าการตรวจสอบอย่างเป็นทางการมีต้นทุนต่ำแล้วหรือไม่

ฐานที่เชื่อถือได้นั้นเล็กกว่าการพิสูจน์ และนั่นคือประเด็นสำคัญ

ข้อพิสูจน์จะดีได้เพียงเท่ากับสิ่งที่มันตั้งสมมติฐานไว้เท่านั้น บทความระบุเรื่องนี้อย่างเจาะจง และความเจาะจงนั้นเองคือสิ่งที่ทำให้มันแตกต่างจากข่าวประชาสัมพันธ์ สเปกที่เชื่อถือได้มีประมาณ 18,000 บรรทัด (28,000 บรรทัดเมื่อรวมเอกสารประกอบ) ภาคความหมายของ AArch64 ประมาณ 8,000 บรรทัด และการเข้ารหัสโค้ดเครื่องใน Lean ประมาณ 95,000 บรรทัด มีรูทีน 37 รูทีนที่ถูกแทนด้วยสัญญาแทนที่จะถูกตรวจสอบยืนยัน ได้แก่ การบีบอัด SHA-256 และ SHA-512, AES-256-CBC, X25519, การดำเนินการบนเส้นโค้ง Edwards, Kyber1024 และ ML-KEM-768 และ libcrux HMAC จุดเข้าสู่ panic 18 จุดก็ถูกตั้งสมมติฐานในทำนองเดียวกันแทนที่จะถูกพิสูจน์

ดังนั้นข้อกล่าวอ้างจึงไม่ใช่ “ทุกสิ่งได้รับการพิสูจน์แล้ว” ข้อกล่าวอ้างคือตรรกะของโปรโตคอลการเข้ารหัสลับ เครื่องสถานะของเซสชัน และการรีไฟน์เมนต์จากตรรกะนั้นไปยังคำสั่งที่ถูกดำเนินการจริงนั้นได้รับการพิสูจน์แล้ว ขณะที่ primitive พื้นฐานที่อยู่ข้างใต้ได้รับความเชื่อถือในแบบที่ทุกโครงการตรวจสอบความถูกต้องเชื่อถือ primitive ของตน คอมไพเลอร์ Rust ที่น่าสังเกตคือ ไม่ได้อยู่ในฐานความเชื่อถือ — ทีมหลีกเลี่ยงความจำเป็นในการเชื่อถือมันโดยใช้การให้เหตุผลในระดับโค้ดเครื่อง ซึ่งเป็นกลเม็ดเดียวกันกับที่ทำให้พวกเขาหลีกเลี่ยงคอมไพเลอร์ที่ผ่านการพิสูจน์แล้วได้ทั้งหมด เพื่อให้เห็นบริบทด้านขนาด เอกสารวิจัยอ้างอิง seL4 ที่ประมาณ 20 คน-ปี และ CompCert ที่ประมาณ 6 คน-ปี

บั๊กสองตัว ใส่กลับไปโดยเจตนา

ระบบตรวจสอบยืนยันที่พูดได้เพียงว่า "ถูกต้อง" เท่านั้นไม่สามารถทดสอบได้ ดังนั้นทีมจึงนำช่องโหว่สองรายการที่เคยถูกค้นพบและแก้ไขแล้วในโค้ดของ Signal — บั๊กสถานะอ่อนแอและบั๊กกลุ่มย่อยขนาดเล็ก — ใส่กลับเข้าไปในสำเนาที่แยกออกมา และรันไปป์ไลน์อีกครั้ง ในทั้งสองกรณี AlphaProof Code สร้างการพิสูจน์ที่ตรวจสอบโดยเครื่องว่าฉบับที่มีบั๊กไม่ผ่านทฤษฎีบทด้านความปลอดภัย: ข้อความเชิงสัญลักษณ์ให้ผลเป็น ¬Sec(Asm_bug)

บทความนี้เพิ่มข้อแม้ที่หน้าเพจการตลาดคงตัดทิ้ง นั่นคือการหักล้างเชิงคำนวณทฤษฎีบทสำหรับบั๊กเหล่านั้น "ยากกว่ามาก" และถูกทิ้งไว้เป็นคำถามเปิด กล่าวอีกนัยหนึ่ง การทดสอบเชิงลบทำงานได้อย่างราบรื่นบนเส้นทางสัญลักษณ์ และยังใช้ไม่ได้บนเส้นทางเชิงคำนวณ นี่คือความไม่สมมาตรแบบที่ผู้อ่านควรรู้ก่อนจะถือว่ากรอบงานนี้เป็นตัวตรวจจับบั๊ก

วิธีการรันเอเจนต์

นักวิจัยห้าคนตลอดสี่สัปดาห์ โดยแต่ละคนรันเอเจนต์อย่างไม่หยุดพัก การเขียนพิสูจน์นั้นทำโดยทีมเอเจนต์ 40 ถึง 80 ตัว โดยแต่ละทีมรันเป็นเวลา 24 ถึง 72 ชั่วโมงบนเครื่องเดียว และมีเอเจนต์ผู้ดูแลอยู่เหนือตัวประสานงานของทีม เอเจนต์ผู้เฝ้าประตูจะตรวจสอบแต่ละผลงานที่ส่งมาด้วย ตัวเปรียบเทียบเทียบกับสำเนาข้อกำหนดที่ถูกเก็บไว้แยกต่างหาก และเทียบกับเคอร์เนลของ Lean — เป็นการป้องกันไม่ให้เอเจนต์พิสูจน์เวอร์ชันที่อ่อนแอลงอย่างแนบเนียนจากสิ่งที่ถูกขอ

งานของมนุษย์ถูกจัดไว้ล่วงหน้าหนักในส่วนข้อกำหนด ข้อกำหนดทุกข้อได้รับการตรวจทานโดยผู้เชี่ยวชาญก่อนเริ่มงานพิสูจน์ และการตรวจสอบของเอเจนต์เองได้flagged ประมาณ 1% ของฐานโค้ดให้มนุษย์ให้ความสนใจ ไม่มีมนุษย์เขียนโค้ดพิสูจน์ บทความยังพูดตรง ๆ เกี่ยวกับงานวิศวกรรมด้วยว่า การบิลด์แบบสะอาดอาจใช้เวลาหลายชั่วโมง ในช่วงแรก การแก้ไขซอร์สเพียงเล็กน้อยหรือไบนารีที่คอมไพล์ใหม่ทำให้ต้องซ่อมแซมการพิสูจน์ขนาดใหญ่ และมี "พื้นที่มากมายสำหรับการปรับให้เหมาะสม" ทั้งใน proofs ที่สร้างโดย AI และในเทคนิคการพิสูจน์เอง

สิ่งที่การพิสูจน์ไม่ได้ครอบคลุม

ข้อจำกัดเหล่านี้ยาวพอที่จะเป็นส่วนที่สำคัญที่สุดของบทความ และถูกระบุไว้อย่างตรงไปตรงมา ไม่มีการรับประกันหลังควอนตัมสำหรับคุณสมบัติการฟื้นตัวของ SPQR — ทฤษฎีบทของ ratchet สมมติว่าผู้โจมตีเป็นผู้เลือกคีย์ SPQR ความเป็นส่วนตัวของเพย์โหลดไม่ได้รับการพิสูจน์ การพิสูจน์ตัวตนของผู้ตอบไม่ได้รับการพิสูจน์สำหรับข้อความแรกของแฮนด์เชกที่ไม่เคยถูกเลื่อนขึ้นเป็นเซสชัน แบบจำลองอนุญาตให้มีหนึ่งเซสชันต่อการเลื่อนขึ้นเป็นเซสชัน กำหนดความยาวข้อความคงที่ ไม่มีสถานะแบบหลายอุปกรณ์ และใช้คีย์ระบุตัวตนแบบ trust-on-first-use

ยังมีค่าขอบเขตอีกค่าหนึ่งที่กลายเป็นไม่มีนัยสำคัญ พจน์การปลอมแปลง MAC ขนาด 8 ไบต์มีค่าอย่างน้อย 2⁻⁶⁴ ต่อความพยายามหนึ่งครั้ง และเพิ่มขึ้นแบบกำลังสองตามจำนวนข้อความและจำนวน epoch ซึ่งหมายความว่าค่าขอบเขตนั้นไม่ให้ข้อมูลใด ๆ อีกต่อไปสำหรับเซสชันเดียวที่มีข้อความประมาณ 25,000 ข้อความ หรือสำหรับ 2²⁰ เซสชันที่มี 2¹⁰ ข้อความ และสิ่งที่การพิสูจน์นี้ครอบคลุมคือบิลด์ libsignal-cli ของทีมที่ทำงานเป็นโปรเซสใหม่ — ไม่ใช่แอป Signal บนโทรศัพท์ของคุณ สมมติฐานเกี่ยวกับสภาพแวดล้อมหลายข้อถูกให้เหตุผลอย่างไม่เป็นทางการแทนที่จะพิสูจน์

ไม่มี API ไม่มีราคา และไม่มีโมเดลให้เรียกใช้

นี่คือส่วนที่จะทำให้ใครก็ตามที่มาจากลีดเดอร์บอร์ดของโมเดลต้องผิดหวัง AlphaProof Code เป็นเฟรมเวิร์กงานวิจัยและชุดอาร์ติแฟกต์ที่เผยแพร่แล้ว ไม่มีเอนด์พอยต์ ไม่มีตารางราคาต่อโทเคน ไม่มีรายการรอ และไม่มีน้ำหนักโมเดล: รีโพซิทอรีมีงานพัฒนา Lean, semantics ของ AArch64, ไบนดิง libsignal และข้อกำหนดต่าง ๆ ไม่ใช่เช็กพอยต์ บล็อกระบุว่าอาร์ติแฟกต์เป็นโอเพนซอร์ส ส่วนแลนดิงเพจไม่ได้ระบุสัญญาอนุญาต ซึ่งควรตรวจสอบก่อนที่ใครจะวางแผนสร้างต่อยอดจากมัน

ส่วนโมเดลที่ลงมือทำงานจริงนั้นเป็นอีกคำถามหนึ่ง บทความระบุชื่อ Gemini 4 Carbon สำหรับเอเจนต์พิสูจน์ และกล่าวว่า Claude Opus 5.5 ถูกใช้ควบคู่กับโมเดลอื่นในการร่างและตรวจทานข้อกำหนด Claude Opus 5.5 อยู่ในแค็ตตาล็อกของ OrcaRouter วันนี้ในราคา 4 ดอลลาร์ต่ออินพุตหนึ่งล้านโทเค็น และ 20 ดอลลาร์ต่อเอาต์พุตหนึ่งล้านโทเค็น โดยราคาตามรายการของผู้ให้บริการถูกส่งต่อในอัตรากำไร 0% — ดังนั้นหากสิ่งที่คุณต้องการนำไปใช้จริงคือ "รันลูปการร่างข้อกำหนดด้วยโมเดลที่บทความใช้" ส่วนนั้นก็เป็นการเรียก API ตามปกติ และหากผู้ขายเปลี่ยนราคา การเปลี่ยนแปลงนั้นก็ตกมาถึงฝั่งเราในวันเดียวกัน เครื่องยนต์ของเอเจนต์พิสูจน์ไม่ใช่สิ่งที่เราให้บริการ และไม่มีอะไรในที่นี้บ่งชี้ว่าเราโฮสต์ AlphaProof Code เอง

ทำไมสิ่งนี้จึงเป็นเรื่องใหญ่กว่าผลลัพธ์ของ Signal

การตรวจสอบยืนยันของ Signal นั้นน่าประทับใจในตัวเอง — เป็นการพิสูจน์ยืนยันอย่างเป็นทางการครั้งแรกของส่วนการนำไปใช้งานของโปรโตคอลที่ถูกใช้งานอย่างแพร่หลาย ด้วยวิธีใดก็ตาม ไม่ว่าจะใช้ AI หรือไม่ ตามข้อมูลของ DeepMind และเป็นครั้งแรกที่ AI ได้ตรวจสอบยืนยันโปรโตคอลการเข้ารหัสลับที่ใช้งานจริงในระดับความลึกเช่นนี้ แต่ข้ออ้างที่ถ่ายทอดไปใช้ได้คือกระบวนการทำงาน ทีมห้าคน ภายในสี่สัปดาห์ ด้วยขั้นตอนการทบทวนข้อกำหนดและเอเจนต์ที่ทำหน้าที่เฝ้าประตู ได้ผลิตชุดหลักฐานการพิสูจน์ซึ่งแต่ก่อนจะเป็นโครงการที่ใช้เวลาหลายปี หากอัตราส่วนนั้นยังคงอยู่แม้เพียงคร่าว ๆ ชุดระบบที่สามารถจ่ายค่าตรวจสอบยืนยันได้ก็จะเปลี่ยนไป: เฟิร์มแวร์ของอุปกรณ์การแพทย์ ซอฟต์แวร์โครงข่ายไฟฟ้า โค้ดประเภทที่ในปัจจุบันได้แค่การรีวิวโค้ดและภาวนา

ว่ามันจะยืนได้หรือไม่นั้นยังไม่ได้ทดสอบ ระบบเข้ารหัสของ Signal มีการระบุรายละเอียดไว้ดีเป็นพิเศษ ทีมได้ให้วิศวกรของ Signal เองเป็นผู้ตรวจทานระเบียบวิธี และ primitives ถูกจ้างบุคคลภายนอกให้ดำเนินการแทนที่จะได้รับการตรวจสอบยืนยัน ระบบถัดไปจะไม่อำนวยเช่นนี้ กรอบที่ตัวบทความวางไว้เอง — การจับคู่การตรวจสอบยืนยันเชิงรูปแบบกับเอเจนต์ป้องกันอัตโนมัติอย่าง CodeMender — คือรูปทรงที่ตรงไปตรงมาของข้อเสนอ: การตรวจสอบยืนยันบอกคุณว่าอะไรเป็นความจริง และต้องมีอย่างอื่นมาแก้ไขสิ่งที่ยังไม่ใช่

ดูอะไรดี

มีสามสิ่งที่จะยกระดับงานนี้จากเปเปอร์สำคัญไปสู่เทคนิคระดับอุตสาหกรรม หนึ่ง ฐานโค้ดอิสระชุดที่สองที่ได้รับการตรวจสอบโดยคนนอก G​oogle และในอุดมคติคือชุดที่ต้องเขียนสเปกตั้งแต่ศูนย์แทนที่จะดัดแปลงจากการวิเคราะห์ที่มีอยู่ สอง ตัวเลขต้นทุน — ชั่วโมงของเอเจนต์ ชั่วโมงการใช้งานตัวเร่ง และจำนวนดอลลาร์ — เพราะสี่สัปดาห์กับทีมเอเจนต์ขนาด 40 ถึง 80 ตัวไม่ใช่หน่วยที่ผู้จัดการวิศวกรรมคนใดจะใช้ตั้งงบประมาณรองรับได้ และสาม การหักล้างบั๊กในเส้นทางการคำนวณ ซึ่งเปเปอร์ยังเปิดประเด็นไว้ และเป็นความแตกต่างระหว่างระบบที่พิสูจน์คุณสมบัติได้ กับระบบที่บอกคุณได้ด้วยการคำนวณว่าไบนารีเฉพาะตัวหนึ่งมีข้อบกพร่อง

จนถึงตอนนั้น ให้อ่านคลังอาร์ติแฟกต์แทนการอ่านประกาศ ข้อพิสูจน์อยู่ที่นั่น Lean ตรวจสอบข้อพิสูจน์เหล่านั้น และบทความบอกคุณอย่างชัดเจนว่าข้อพิสูจน์เหล่านั้นตั้งสมมติฐานอะไรไว้