Anthropic ให้ Claude พิสูจน์เชิงคณิตศาสตร์ว่า fuzz test 239 จุดใน 123 ไลบรารี OSS-Fuzz ไม่มีวัน crash ที่ระดับ binary RISC-V — proof รวม 180 ล้านบรรทัด Rocq เจอบั๊กที่ fuzzer หาไม่เจอ แต่เปิดเผยจริง 60 จุดใน 25 ไลบรารี

22 ต.ค. 2026 ทีม Frontier Red Team ของ Anthropic เผยแพร่งานวิจัย “LLMs are making formal software verification feasible at a much larger scale” ซึ่งทำร่วมกับสตาร์ทอัพ Theorem ทีมให้ Claude เขียนบทพิสูจน์เชิงคณิตศาสตร์ (formal proof) ว่าโค้ดของ 123 ไลบรารีโอเพนซอร์สในโครงการ OSS-Fuzz ของ Google จะไม่ crash ภายใต้เงื่อนไขที่กำหนด ตัว proof ทำงานบน binary RISC-V ที่คอมไพล์แล้ว ไม่ได้ทำบน source code และตรวจด้วย proof checker ของ Rocq (ชื่อใหม่ของ Coq)

Anthropic บอกว่าเท่าที่ทราบ นี่เป็นครั้งแรกที่ใช้ AI ทำ formal verification กับซอฟต์แวร์ production ในระดับ assembly ได้ในสเกลนี้ ผลพลอยได้ที่นักพัฒนาน่าจะสนใจกว่าคือ ระหว่างพยายามพิสูจน์ Claude เจอบั๊กหลายร้อยตัว รวมถึงบั๊กที่ fuzzer แทบไม่มีทางเจอ

เปลี่ยน fuzz test ให้เป็น spec แล้วพิสูจน์ว่ามันไม่มีวันล้ม

ปัญหาแรกของ formal verification คือต้องนิยามให้ได้ก่อนว่า “ถูกต้อง” หมายถึงอะไร ทีมแก้โดยใช้ fuzz test ที่นักพัฒนาเขียนไว้อยู่แล้ว fuzz test คือ entry point ที่ถ้า crash ด้วย input ไหนก็นับเป็นบั๊ก OSS-Fuzz ยังคอมไพล์ C/C++ พร้อม AddressSanitizer (ASan) ด้วย การเข้าถึงหน่วยความจำผิดจึงทำให้ crash ทันที

spec ที่ทีมใช้คือ “fuzz test นี้ไม่ crash กับ input ใดๆ ที่เล็กกว่า 64 MB” ถ้าพิสูจน์ได้ การรัน fuzzer ต่อที่ entry point นั้นก็ไม่มีประโยชน์ เพราะจะไม่เจอบั๊กเพิ่มแล้ว ตัวเลขที่ Anthropic รายงาน:

• พิสูจน์ได้ 239 entry point ใน 123 ไลบรารี ภายในไม่กี่สัปดาห์ โดยบาง entry point ต้องแพตช์บั๊กก่อน
• proof รวมประมาณ 180 ล้านบรรทัด Rocq proof หนึ่งยาวราว 600,000 บรรทัด สำหรับ binary ที่มีมัธยฐานราว 18,000 คำสั่ง RISC-V
• สิ่งที่ต้องเชื่อถือมีแค่ โมเดล RISC-V + โมเดล process ของ Linux, theorem statement และ Rocq kernel proof ที่ยาวขนาดนี้จึงไม่ต้องให้คนอ่านทีละบรรทัด
• ข้อจำกัดของเงื่อนไข: ผลนี้ถือว่าโปรแกรมรันแบบ single-thread เป็น static binary บน RISC-V ลิงก์กับ musl libc และใช้หน่วยความจำจำกัด ซึ่งต่างจากการใช้งานจริงส่วนใหญ่ที่รันบน x86/ARM และลิงก์ glibc แบบ dynamic

ตอนพิสูจน์ proof หนึ่งของ cpp-httplib ให้ผ่าน Claude ต้องพิสูจน์บน machine code ด้วยว่า red-black tree ของ libc++ รักษาความลึกของ tree ไว้ที่ระดับ log ได้จริง เพื่อตัดความเป็นไปได้ที่ stack จะ overflow ตอนเรียก destructor

บั๊กที่ fuzzer หาไม่เจอ

fuzzer มักจำกัด input ไว้ประมาณ 1 MB และอาศัย coverage นำทาง บั๊กที่ Claude เจอระหว่างพิสูจน์จึงต่างจากที่ fuzzer เจอ ตัวอย่างที่บทความยกมา:

• counter underflow ใน decompressor ที่ทำให้เขียนหน่วยความจำนอกขอบเขต แต่เกิดเฉพาะ input ขนาดราว 20 MB ที่จัดเรียงแบบเจาะจงมาก
• out-of-bounds read ใน image decoder ที่ต้องใช้ input 64 MB และหน่วยความจำเกิน 2 GB
• out-of-bounds read ที่ต้องเรียกฟังก์ชันตามลำดับเฉพาะผ่าน 2 handle ที่ชี้ไฟล์เดียวกัน
• เจอ CVE-2026-56132 ใน libexpat ซ้ำ ซึ่งต้องใช้ input ที่ซ้อนกันลึกมาก
• logic bug ที่ไม่ crash เช่น ฟีเจอร์จำกัดไฟล์ที่แอปโหลดได้ ซึ่งไม่ได้ถูกบังคับใช้ทุกกรณี

การทดลองอื่นในบทความ: ให้ Claude เขียน spec ของ RFC 1950 (zlib) แล้วพิสูจน์ว่า zlib ใน Linux kernel ทำตาม spec บน binary x86 โดยใช้ semantics ของ x86 ที่ Claude สร้างเอง ให้ Claude เขียน Python interpreter ด้วย Rust แล้วพิสูจน์ด้วย Verus ซึ่งเมื่อทดสอบกับโปรแกรมสุ่ม 1.7 ล้านตัวให้ผลตรงกับ CPython 99.95% และระหว่างตรวจ PDF reader ตัวหนึ่ง ทีมเจอบั๊ก security ในสัปดาห์เดียวเท่ากับจำนวนที่ปกติมีคนรายงานทั้งปี

ต้นทุนยังสูง proof หนึ่งอาจใช้หลายร้อยล้าน token แต่ Anthropic ให้ข้อมูลว่าในชุดงานทดสอบ 36 งาน Opus 5.5 พิสูจน์ครึ่งหนึ่งได้โดยใช้ token น้อยกว่า Opus 5 ราว 40% และเมื่อให้ agent คัดลอก proof ของกันและกันได้ ใช้ token ลดลงอีก 17% เพราะ proof ส่วนใหญ่เป็นส่วนที่ทุกโปรแกรมมีเหมือนกัน เช่นการเริ่มต้น C runtime และ ASan

สิ่งที่เปิดให้ตรวจได้จริงตอนนี้

ข้อนี้ควรรู้ก่อนอ้างตัวเลข 123 ไลบรารี: repo theorem-labs/oss-verify-proofs (MIT, สร้าง 22 ต.ค.) ระบุใน README ว่ามี proof ของ 60 entry point ใน 25 ไลบรารี เช่น bzip2, cJSON, json-c, libpcap, leptonica, msgpack-c, mbedtls (fuzz_pkcs7) และ OpenSSL (bignum, bndiv) ตรวจด้วย Rocq 9.2.0 Anthropic อธิบายว่าเผยแพร่เฉพาะ proof ของ fuzz test ที่ไม่ต้องแพตช์ และไม่เปิด proof ที่อาจเผยบั๊กที่ยังไม่ได้แก้

README ยังเขียนไว้ตรงๆ ว่าโมเดล process ของ Linux (LPS) ที่ใช้นั้น “best effort and not complete” และ proof จะน่าเชื่อถือได้เท่ากับโมเดลนี้เท่านั้น

Theorem เปิดโครงการ OSS Verify ให้โปรเจกต์โอเพนซอร์สที่ผ่านเกณฑ์ใช้ฟรี วิธีสมัครคล้าย OSS-Fuzz คือเปิด PR ที่ theorem-labs/oss-verify พร้อม project.yaml, Dockerfile และ build.sh ต้อง build เป็น static riscv64 ได้ ถ้าเจอบั๊กระหว่างพิสูจน์ Theorem จะแจ้งเจ้าของโปรเจกต์แบบส่วนตัว นอกจากนี้ยังมี Claude skill (add-project) ใน repo ช่วยพอร์ต build ด้วย

มุมมอง AI Curator

ส่วนที่สำคัญที่สุดของงานนี้ไม่ใช่ตัวเลข 180 ล้านบรรทัด แต่เป็นวิธีที่ทีมใช้ fuzz test ที่มีอยู่แล้วเป็น spec ที่ผ่านมา formal verification ติดอยู่ที่ต้องมีผู้เชี่ยวชาญเขียน spec ซึ่งใช้เวลาเป็นปี งานนี้เลี่ยงขั้นนั้นได้เกือบทั้งหมด ถ้าโปรเจกต์มี fuzz harness ที่ assert คุณสมบัติสำคัญไว้ (เช่น compress แล้ว decompress ต้องได้ข้อมูลเดิม) ก็พิสูจน์คุณสมบัตินั้นได้ทางอ้อม สำหรับทีมพัฒนา ข้อสรุปเชิงปฏิบัติคือ fuzz harness ที่เขียนดีจะมีมูลค่ามากขึ้น เพราะในอนาคตอาจใช้เป็น spec ของ proof ได้

แต่ต้องอ่านเงื่อนไขให้ครบ “พิสูจน์แล้ว” ในที่นี้หมายถึง binary RISC-V แบบ static ที่ลิงก์ musl และรัน single-thread ไม่ใช่ libpcap หรือ OpenSSL ที่ระบบส่วนใหญ่ใช้งานจริงบน x86 พร้อม glibc ส่วนตัวเลข 123 ไลบรารีที่สื่อจะอ้าง ตรวจได้จริงตอนนี้ 25 ไลบรารี เหตุผลที่ไม่เปิดส่วนที่เหลือ (มีบั๊กที่ยังไม่แพตช์) ฟังขึ้น แต่ก็ทำให้ข้อสรุปส่วนใหญ่ยังต้องเชื่อตามที่ Anthropic รายงาน

บริบทก็สำคัญ ช่วงนี้ AI หาช่องโหว่ได้เร็วกว่าที่ maintainer แก้ทัน (กรณี PHP2Shell เมื่อวานเป็นตัวอย่าง) Anthropic กำลังเสนอว่าทางออกระยะยาวคือพิสูจน์ว่าไม่มีบั๊ก ไม่ใช่ไล่หาบั๊กไปเรื่อยๆ สำหรับไทยและ SEA ที่ระบบธนาคาร ภาครัฐ และ IoT จำนวนมากใช้ไลบรารี C ตัวเดียวกันนี้ ผลที่ได้ตรงที่สุดคือ proof ที่ทำครั้งเดียวที่ต้นทางแล้วทุกคนใช้ร่วมกัน ส่วนนักพัฒนาไทยที่ดูแลไลบรารี C/C++ อยู่ใน OSS-Fuzz ควรลองสมัคร OSS Verify ดู เพราะไม่มีค่าใช้จ่าย และอย่างน้อยจะได้รายงานบั๊กที่ fuzzer พลาดไป

แหล่งข่าว

• Anthropic — LLMs are making formal software verification feasible at a much larger scale (22 ต.ค. 2026)
• GitHub — theorem-labs/oss-verify-proofs (proof ที่เผยแพร่, MIT)
• Theorem — OSS Verify: Free formal verification for open source
• GitHub — theorem-labs/rocq-linux-process-semantics