&Truth huy động 70 triệu USD ở vòng hạt giống để xây dựng cỗ máy kiểm chứng phổ quát cho mã nguồn

&Truth, một công ty vì lợi ích công cộng phát triển công nghệ chứng minh bằng toán học rằng phần mềm an toàn, đã rời khỏi chế độ hoạt động bí mật vào ngày 29 tháng 10 năm 2026, công bố khoản vốn hạt giống 70 triệu USD và kế hoạch xây dựng thứ mà công ty gọi là cỗ máy kiểm chứng phổ quát cho mã nguồn.

Trong thông báo ra mắt, công ty cho biết được thành lập vào đầu năm 2026 và nhận 70 triệu USD vốn hạt giống từ một nhóm mà công ty mô tả là gồm những nhà lãnh đạo có vai trò định hình trong lĩnh vực an toàn AI và đầu tư mạo hiểm. Công ty cho biết cỗ máy kiểm chứng đang được xây dựng để đọc mã nguồn bằng bất kỳ ngôn ngữ lập trình nào và chứng minh bằng toán học rằng mã nguồn đó an toàn, bảo mật và chính xác, với các chứng minh mà bất kỳ ai cũng có thể kiểm tra độc lập.

Tự động hóa chứng minh dựa trên Lean

Theo thông báo, kiểm chứng hình thức đã tồn tại trong nhiều thập kỷ nhưng trước đây khó tiếp cận và tốn kém, bởi các chuyên gia phải xây dựng chứng minh thủ công, khiến phương pháp này chỉ được áp dụng cho một số ít hệ thống trọng yếu. Công ty cho biết AI hiện giúp đẩy nhanh công việc chứng minh hình thức lên 100 lần hoặc hơn, còn công nghệ tự động hóa chứng minh của công ty tăng tốc quy trình thêm 100 lần nữa, rút ngắn thời gian tạo chứng minh từ nhiều năm hoặc nhiều tháng xuống còn vài giờ hoặc vài phút.

Công ty cũng giới thiệu công nghệ mà họ gọi là “nhà máy đặc tả”, cho biết công nghệ này giúp doanh nghiệp và nhà phát triển chuyển ý định của con người cùng các yêu cầu kinh doanh thành những đặc tả hình thức chính xác trên quy mô lớn, tạo ra các bảo đảm có thể được kiểm tra độc lập thay vì chỉ dựa vào kết quả kiểm thử hoặc tuyên bố của nhà cung cấp.

&Truth đang xây dựng trên Lean, một hệ thống chứng minh mã nguồn mở, và Mathlib, một thư viện gồm hơn hai triệu dòng định nghĩa và định lý toán học, cùng với các công nghệ mã nguồn mở như CSLib. Theo công ty, mục tiêu là xây dựng một ngôn ngữ hình thức phổ quát cho phần mềm, bao gồm các mô hình toán học về ngôn ngữ lập trình và hệ thống, kỹ thuật chứng minh, cùng các đặc tả chính xác cho phép tự động kiểm chứng trên nhiều ngôn ngữ. &Truth cho biết công ty hợp tác với Lean Focused Research Organization và dự định phát hành các thư viện nền tảng dưới dạng mã nguồn mở.

Nhà đồng sáng lập kiêm đồng CEO Clark Barrett cho biết Lean và Mathlib đã cung cấp cho AI một ngôn ngữ chính xác để lập luận trong toán học, còn phần mềm thì chưa có nền tảng tương đương. Nhà đồng sáng lập kiêm Giám đốc Khoa học Ilya Sergey cho rằng niềm tin vào phần mềm nên dựa trên các chứng minh có thể kiểm tra độc lập, chứ không phải lời cam kết của bất kỳ công ty nào.

Các nhà sáng lập và hai trụ sở chính

Barrett là Giáo sư Corbel ngành Khoa học Máy tính tại Stanford University, đồng giám đốc sáng lập Stanford Center for AI Safety, giám đốc Stanford Center for Automated Reasoning, đồng sáng tạo CSLib và trưởng dự án phát triển công cụ lập luận tự động cvc5. Sergey thành lập VERSE Lab tại National University of Singapore và đồng sáng tạo các công cụ kiểm chứng mã nguồn mở Veil và Velvet. Nhà đồng sáng lập, đồng CEO kiêm Chủ tịch điều hành Chris Hsu là thành viên Ban Cố vấn Chiến lược Lean FRO và chủ tịch Infinitude Foundation; trước đây ông từng là CEO của Kilometre Capital và giám đốc điều hành tại Citadel Investment Group.

Thông báo cũng nêu tên Gregory Malecha, người trước đây lãnh đạo mảng phương pháp hình thức tại BlueRock Security và là kiến trúc sư chủ chốt của khung kiểm chứng BRiCk; Sebastian Ullrich, đồng kiến trúc sư của Lean 4 và đồng sáng lập Lean Focused Research Organization; Linus Lee, cựu đối tác điều hành tại Kilometre Capital; và Drew Harman, cựu giám đốc thương mại tại Fastino Labs, đồng thời là đối tác điều hành tại Insight Partners và Shasta Ventures. &Truth cho biết công ty kế thừa nhiều thập kỷ nghiên cứu về kiểm chứng hình thức và lập luận tự động tại Stanford University và National University of Singapore.

Trụ sở tại Mỹ của &Truth đặt ở Palo Alto, còn trụ sở quốc tế đặt tại Singapore. Công ty cho biết văn phòng tại đây sẽ mở rộng đáng kể các hoạt động nghiên cứu, kỹ thuật, phát triển sản phẩm và tiếp cận thị trường. Trong thông báo, Low Jin Yong, Phó chủ tịch cấp cao kiêm Đồng trưởng bộ phận Công nghiệp số Singapore, cho biết trụ sở này sẽ tăng cường năng lực về niềm tin và an toàn tại Singapore, đồng thời củng cố vị thế của quốc gia này như một cứ điểm cho các công ty phát triển AI đáng tin cậy.

Trang web của công ty cũng có buổi thảo luận bàn tròn với Leonardo de Moura, người phát minh ra Lean, đồng thời là Phó chủ tịch kiêm Nhà khoa học xuất sắc tại AWS, và Simone Severini, thành viên Ban Cố vấn Chiến lược Lean FRO kiêm Kỹ sư xuất sắc tại Google.

Các bài luận đi kèm trình bày chi tiết lý do thành lập công ty

Trong bài luận đi kèm đề ngày 29 tháng 10 năm 2026, Hsu phân tích những xu hướng mà công ty cho là khiến việc kiểm chứng trở nên cấp thiết. Ông dẫn lời CEO Google Sundar Pichai, theo đó 75% mã nguồn mới tại Google hiện do AI tạo ra và được các kỹ sư phê duyệt; ông cũng dẫn kết quả kiểm thử năm 2026 của Veracode, cho thấy các mô hình AI thất bại ở gần một nửa số tác vụ lập trình có yêu cầu bảo mật. Bài luận còn đề cập một chiến dịch vào tháng 9 năm 2026, trong đó kẻ tấn công triển khai hàng trăm tác nhân AI để xâm nhập 395 tổ chức tại 48 quốc gia thông qua các lỗ hổng trong phần mềm quản lý in ấn được sử dụng rộng rãi, cùng kỷ lục 14.959 lỗ hổng phần mềm được công bố trong tháng 9 năm 2026 — con số mà bài luận mô tả là gấp 3,5 lần số lỗ hổng được công bố một năm trước đó.

Bài luận điểm lại những cột mốc trước đây trong lĩnh vực kiểm chứng hình thức: để hoàn thành chứng minh ban đầu cho vi nhân seL4, các chuyên gia đã bỏ ra khoảng 20 người-năm công sức cho khoảng 8.700 dòng mã; năm 2015, trong khuôn khổ chương trình HACMS của DARPA, seL4 được tích hợp vào trực thăng Unmanned Little Bird của Boeing, nhưng một đội đỏ chuyên nghiệp dù được tiếp cận trong nhiều tuần vẫn không thể xâm nhập hệ thống điều khiển bay của trực thăng; và vào tháng 9 năm 2026, một mô hình AI do Anthropic phát triển đã hình thức hóa toàn bộ chứng minh Định lý cuối cùng của Fermat bằng Lean trong 11 ngày. Bài luận cũng lưu ý rằng trước đó trong năm 2026, Kim Morrison, kỹ sư phần mềm nghiên cứu cấp cao tại Lean FRO, đã dùng Claude của Anthropic với sự hướng dẫn tối thiểu của con người để xây dựng phiên bản thư viện nén zlib bằng Lean và chứng minh rằng thư viện này luôn khôi phục chính xác dữ liệu mà nó đã nén.

Bài luận trích lời Leonardo de Moura, người tạo ra Lean: “Kiểm thử mang lại sự tin cậy. Chứng minh mang lại sự bảo đảm.”

Trong bài luận thứ hai, được xuất bản ngày 29 tháng 10 năm 2026, Sergey giải thích cơ chế kiểm chứng chương trình, bắt đầu với bài báo năm 1949 của Alan Turing, “Kiểm tra một chương trình con lớn”, trong đó đề xuất rằng lập trình viên nên kèm theo mã của mình những khẳng định chính xác để một bộ kiểm tra có thể xác minh từng khẳng định. Bài luận mô tả các đặc tả, bất biến vòng lặp và các chứng minh được kiểm tra bằng Lean, đồng thời nêu rõ mục tiêu của &Truth là giúp nhà phát triển có được bằng chứng có thể kiểm tra độc lập, chẳng hạn như một chứng minh hình thức bằng Lean, với chi phí đủ thấp để việc kiểm chứng trở thành một phần thường xuyên trong quá trình phát triển.

&Truth mô tả tầm nhìn dài hạn của mình là chuyển từ “lập trình theo cảm tính” sang “lập trình có thể kiểm chứng”, trong đó mã do AI tạo ra được xác minh bằng toán học trước khi triển khai, các tác nhân AI hoạt động trong những môi trường có phạm vi giới hạn được chứng minh, phần mềm cũ được hiện đại hóa một cách an toàn và cơ sở hạ tầng trọng yếu được bảo vệ bằng những bảo đảm toán học có thể kiểm tra độc lập.