&Truth ระดมทุนรอบ Seed ได้ 70 ล้านดอลลาร์ เพื่อสร้างเครื่องพิสูจน์ยืนยันโค้ดแบบสากล

&Truth บริษัทเพื่อประโยชน์สาธารณะที่พัฒนาเทคโนโลยีเพื่อพิสูจน์ความปลอดภัยของซอฟต์แวร์ด้วยคณิตศาสตร์ พ้นจากช่วงเก็บตัวเมื่อวันที่ 29 ตุลาคม 2026 พร้อมเปิดเผยว่าได้รับเงินทุนรอบ Seed จำนวน 70 ล้านดอลลาร์ และมีแผนสร้างสิ่งที่บริษัทเรียกว่าเครื่องพิสูจน์ยืนยันโค้ดแบบสากล

ในประกาศเปิดตัว บริษัทระบุว่าก่อตั้งขึ้นเมื่อต้นปี 2026 และได้รับเงินทุนรอบ Seed จำนวน 70 ล้านดอลลาร์จากกลุ่มผู้นำด้านความปลอดภัยของ AI และเงินร่วมลงทุน ซึ่งบริษัทกล่าวว่ามีบทบาทสำคัญในการบุกเบิก บริษัทระบุว่ากำลังสร้างเครื่องพิสูจน์ยืนยันที่อ่านโค้ดได้ทุกภาษาโปรแกรม และพิสูจน์ทางคณิตศาสตร์ได้ว่าโค้ดนั้นปลอดภัย มั่นคง และถูกต้อง โดยทุกคนสามารถตรวจสอบบทพิสูจน์ได้ด้วยตนเอง

ระบบอัตโนมัติสำหรับสร้างบทพิสูจน์ที่พัฒนาบน Lean

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

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

&Truth พัฒนาต่อยอดจาก Lean ซึ่งเป็นระบบพิสูจน์แบบโอเพนซอร์ส และ Mathlib ซึ่งเป็นคลังคำจำกัดความและทฤษฎีบททางคณิตศาสตร์ที่มีโค้ดมากกว่า 2 ล้านบรรทัด รวมถึงเทคโนโลยีโอเพนซอร์สอื่น ๆ เช่น CSLib บริษัทระบุว่าเป้าหมายคือการสร้างชุดคำศัพท์อย่างเป็นทางการแบบสากลสำหรับซอฟต์แวร์ ซึ่งประกอบด้วยแบบจำลองทางคณิตศาสตร์ของภาษาโปรแกรมและระบบต่าง ๆ เทคนิคการพิสูจน์ และข้อกำหนดที่แม่นยำซึ่งช่วยให้ตรวจสอบยืนยันได้โดยอัตโนมัติในภาษาต่าง ๆ &Truth ระบุว่าร่วมงานกับ Lean Focused Research Organization และตั้งใจเผยแพร่คลังพื้นฐานของบริษัทเป็นโอเพนซอร์ส

Clark Barrett ผู้ร่วมก่อตั้งและประธานเจ้าหน้าที่บริหารร่วมกล่าวว่า Lean และ Mathlib มอบภาษาที่แม่นยำให้ AI ใช้ให้เหตุผลทางคณิตศาสตร์ แต่ซอฟต์แวร์ยังขาดรากฐานที่เทียบเท่ากัน ส่วน Ilya Sergey ผู้ร่วมก่อตั้งและประธานเจ้าหน้าที่ฝ่ายวิทยาศาสตร์กล่าวว่า ความเชื่อมั่นในซอฟต์แวร์ควรตั้งอยู่บนบทพิสูจน์ที่ทุกคนตรวจสอบได้ด้วยตนเอง ไม่ใช่คำกล่าวของบริษัทใดบริษัทหนึ่ง

ผู้ก่อตั้งและสำนักงานใหญ่สองแห่ง

Barrett ดำรงตำแหน่งศาสตราจารย์ Corbel ด้านวิทยาการคอมพิวเตอร์ที่ Stanford University เป็นผู้ร่วมก่อตั้งและผู้อำนวยการร่วมคนแรกของ Stanford Center for AI Safety เป็นผู้อำนวยการ Stanford Center for Automated Reasoning เป็นผู้ร่วมสร้าง CSLib และเป็นหัวหน้าโครงการเครื่องมือให้เหตุผลอัตโนมัติ cvc5 ส่วน Sergey ก่อตั้ง VERSE Lab ที่ National University of Singapore และร่วมสร้างเครื่องมือตรวจสอบแบบโอเพนซอร์ส Veil และ Velvet ส่วน Chris Hsu ผู้ร่วมก่อตั้ง ประธานเจ้าหน้าที่บริหารร่วม และประธานกรรมการบริหาร เป็นสมาชิกคณะกรรมการที่ปรึกษาเชิงกลยุทธ์ของ Lean FRO และประธาน Infinitude Foundation ก่อนหน้านี้เขาเคยดำรงตำแหน่งประธานเจ้าหน้าที่บริหารของ Kilometre Capital และกรรมการผู้จัดการของ Citadel Investment Group

ประกาศยังกล่าวถึง Gregory Malecha ซึ่งเคยเป็นผู้นำด้านวิธีการอย่างเป็นทางการที่ BlueRock Security และเป็นสถาปนิกคนสำคัญของกรอบงานตรวจสอบยืนยัน BRiCk; Sebastian Ullrich ผู้ร่วมออกแบบ Lean 4 และผู้ร่วมก่อตั้ง Lean Focused Research Organization; Linus Lee อดีตหุ้นส่วนผู้จัดการของ Kilometre Capital; และ Drew Harman อดีตประธานเจ้าหน้าที่ฝ่ายการพาณิชย์ของ Fastino Labs และหุ้นส่วนฝ่ายปฏิบัติการของ Insight Partners และ Shasta Ventures &Truth ระบุว่าบริษัทต่อยอดจากงานวิจัยด้านการตรวจสอบยืนยันอย่างเป็นทางการและการให้เหตุผลอัตโนมัติที่ดำเนินมาหลายทศวรรษ ณ Stanford University และ National University of Singapore

สำนักงานใหญ่ในสหรัฐฯ ของ &Truth ตั้งอยู่ที่ Palo Alto ส่วนสำนักงานใหญ่ระหว่างประเทศตั้งอยู่ที่ Singapore โดยบริษัทระบุว่าจะขยายสำนักงานแห่งนี้อย่างมาก ทั้งในด้านงานวิจัย วิศวกรรม ผลิตภัณฑ์ และการนำผลิตภัณฑ์ออกสู่ตลาด Low Jin Yong รองประธานอาวุโสและหัวหน้าร่วมของ Digital Industry Singapore กล่าวในประกาศว่า สำนักงานใหญ่แห่งนี้จะช่วยเพิ่มขีดความสามารถด้านความไว้วางใจและความปลอดภัยใน Singapore และเสริมความแข็งแกร่งให้ประเทศในฐานะฐานที่ตั้งของบริษัทที่พัฒนา AI ซึ่งเชื่อถือได้

เว็บไซต์ของบริษัทยังนำเสนอวงเสวนากับ Leonardo de Moura ผู้คิดค้น Lean และรองประธานและนักวิทยาศาสตร์ดีเด่นที่ AWS และ Simone Severini สมาชิกคณะกรรมการที่ปรึกษาเชิงกลยุทธ์ของ Lean FRO และวิศวกรดีเด่นที่ Google

บทความประกอบอธิบายเหตุผลเบื้องหลังของบริษัท

ในบทความประกอบที่เผยแพร่เมื่อวันที่ 29 ตุลาคม 2026 Hsu อธิบายแนวโน้มต่าง ๆ ที่บริษัทระบุว่าทำให้การตรวจสอบยืนยันเป็นเรื่องเร่งด่วน โดยยกคำกล่าวของ Sundar Pichai ซีอีโอของ Google ที่ว่า ปัจจุบันวิศวกรตรวจสอบและอนุมัติโค้ดใหม่ที่ Google ซึ่ง AI สร้างขึ้นคิดเป็น 75% และอ้างถึงการทดสอบของ Veracode ในปี 2026 ซึ่งพบว่าโมเดล AI ทำงานไม่สำเร็จในงานเขียนโค้ดเกือบครึ่งหนึ่งของงานที่ให้ความสำคัญกับความปลอดภัย บทความยังกล่าวถึงแคมเปญในเดือนกันยายน 2026 ซึ่งผู้โจมตีใช้เอเจนต์ AI หลายร้อยตัวเจาะระบบขององค์กร 395 แห่งใน 48 ประเทศ ผ่านช่องโหว่ในซอฟต์แวร์จัดการงานพิมพ์ที่มีการใช้งานอย่างแพร่หลาย และจำนวนช่องโหว่ของซอฟต์แวร์ที่เผยแพร่ในเดือนกันยายน 2026 ซึ่งสูงเป็นประวัติการณ์ที่ 14,959 รายการ โดยบทความระบุว่าตัวเลขนี้มากกว่าจำนวนที่เผยแพร่เมื่อหนึ่งปีก่อนถึง 3.5 เท่า

บทความกล่าวถึงหมุดหมายสำคัญในอดีตของการพิสูจน์ความถูกต้องอย่างเป็นทางการ ได้แก่ การพิสูจน์ครั้งแรกของไมโครเคอร์เนล seL4 ซึ่งใช้ความพยายามจากผู้เชี่ยวชาญราว 20 คน-ปี สำหรับโค้ดประมาณ 8,700 บรรทัด; ในปี 2015 ภายใต้โครงการ HACMS ของ DARPA มีการนำ seL4 ไปติดตั้งในเฮลิคอปเตอร์ Unmanned Little Bird ของ Boeing โดยทีมทดสอบเจาะระบบฝ่ายตรงข้ามมืออาชีพที่ได้รับเวลาหลายสัปดาห์ในการเข้าถึงระบบไม่สามารถเจาะระบบควบคุมการบินได้; และในเดือนกันยายน 2026 โมเดล AI ที่ Anthropic พัฒนาขึ้นได้จัดทำรูปแบบพิสูจน์อย่างเป็นทางการของทฤษฎีบทสุดท้ายของแฟร์มาต์ทั้งหมดใน Lean ภายใน 11 วัน นอกจากนี้ บทความยังระบุว่า ก่อนหน้านั้นในปี 2026 Kim Morrison วิศวกรซอฟต์แวร์วิจัยอาวุโสที่ Lean FRO ใช้ Claude ของ Anthropic โดยได้รับคำแนะนำจากมนุษย์เพียงเล็กน้อย เพื่อสร้างไลบรารีบีบอัดข้อมูล zlib ฉบับ Lean และพิสูจน์ว่าไลบรารีดังกล่าวกู้คืนข้อมูลที่บีบอัดไปได้อย่างถูกต้องครบถ้วนทุกครั้ง

บทความยกคำกล่าวของ Leonardo de Moura ผู้สร้าง Lean ว่า “การทดสอบช่วยสร้างความมั่นใจ ส่วนการพิสูจน์ให้หลักประกัน”

ในบทความอีกชิ้นที่เผยแพร่เมื่อวันที่ 29 ตุลาคม 2026 Sergey อธิบายกลไกของการตรวจสอบโปรแกรม โดยเริ่มจากบทความของ Alan Turing ในปี 1949 เรื่อง “Checking a Large Routine” ซึ่งเสนอให้โปรแกรมเมอร์แนบข้อความยืนยันที่ชัดเจนไปกับโค้ด เพื่อให้เครื่องมือตรวจสอบยืนยันแต่ละข้อได้ บทความกล่าวถึงข้อกำหนด อินวาเรียนต์ของลูป และการพิสูจน์ที่ตรวจสอบด้วย Lean พร้อมระบุว่าเป้าหมายของ &Truth คือช่วยให้นักพัฒนาได้รับหลักฐานที่ตรวจสอบได้โดยอิสระ เช่น การพิสูจน์อย่างเป็นทางการใน Lean ด้วยต้นทุนที่ทำให้การตรวจสอบเป็นส่วนหนึ่งของกระบวนการพัฒนาตามปกติ

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