&Truth Menggalang Pendanaan Awal $70 Juta untuk Membangun Mesin Verifikasi Universal bagi Kode

&Truth, perusahaan manfaat publik yang mengembangkan teknologi untuk membuktikan secara matematis bahwa perangkat lunak aman, mengumumkan keberadaannya setelah beroperasi secara tertutup pada 29 Oktober 2026. Perusahaan ini mengungkapkan telah memperoleh pendanaan awal sebesar $70 juta dan berencana membangun sesuatu yang disebutnya mesin verifikasi universal bagi kode.

Dalam pengumuman peluncurannya, perusahaan itu menyatakan didirikan pada awal 2026 dan menerima pendanaan awal sebesar $70 juta dari sejumlah pemimpin di bidang keselamatan AI dan modal ventura yang disebutnya berperan penting. Perusahaan itu mengatakan mesin verifikasinya sedang dikembangkan agar dapat membaca kode dalam bahasa pemrograman apa pun dan membuktikan secara matematis bahwa kode tersebut aman, terlindungi, dan benar, dengan bukti yang dapat diperiksa secara mandiri oleh siapa pun.

Otomasi Pembuktian Berlandaskan Lean

Menurut pengumuman tersebut, verifikasi formal telah ada selama puluhan tahun, tetapi sebelumnya sulit diakses dan mahal karena para ahli harus merumuskan bukti secara manual. Akibatnya, penerapannya terbatas pada segelintir sistem penting. Perusahaan itu mengatakan AI kini mempercepat pekerjaan pembuktian formal hingga 100 kali lipat atau lebih, sementara teknologi otomasi pembuktiannya mempercepat proses tersebut 100 kali lipat lagi, sehingga waktu untuk menghasilkan bukti berkurang dari hitungan tahun atau bulan menjadi hitungan jam atau menit.

Perusahaan itu juga menjelaskan teknologi yang disebutnya “pabrik spesifikasi”, yang menurutnya memungkinkan perusahaan dan pengembang menerjemahkan maksud manusia dan persyaratan bisnis menjadi spesifikasi formal yang tepat dalam skala besar. Hasilnya adalah jaminan yang dapat diperiksa secara mandiri, bukan jaminan yang hanya mengandalkan pengujian atau klaim vendor.

&Truth mengembangkan teknologinya dengan berlandaskan Lean, sistem pembuktian sumber terbuka, dan Mathlib, pustaka yang memuat lebih dari dua juta baris definisi dan teorema matematika, serta teknologi sumber terbuka lainnya, termasuk CSLib. Menurut perusahaan itu, tujuannya adalah membangun kosakata formal universal untuk perangkat lunak: model matematika bahasa pemrograman dan sistem, teknik pembuktian, serta spesifikasi tepat yang memungkinkan verifikasi otomatis lintas bahasa. &Truth mengatakan pihaknya bekerja sama dengan Lean Focused Research Organization dan berniat merilis pustaka dasarnya sebagai sumber terbuka.

Salah satu pendiri sekaligus CEO bersama, Clark Barrett, mengatakan Lean dan Mathlib memberi AI bahasa yang tepat untuk bernalar dalam matematika, sedangkan perangkat lunak belum memiliki landasan yang setara. Salah satu pendiri sekaligus Kepala Ilmuwan Ilya Sergey mengatakan kepercayaan terhadap perangkat lunak seharusnya didasarkan pada bukti yang dapat diperiksa secara mandiri, bukan pada perkataan perusahaan mana pun.

Para Pendiri dan Kantor Pusat di Dua Lokasi

Barrett adalah Profesor Corbel bidang Ilmu Komputer di Stanford University, salah satu direktur pendiri Stanford Center for AI Safety, direktur Stanford Center for Automated Reasoning, salah satu pencipta CSLib, dan pemimpin proyek mesin penalaran otomatis cvc5. Sergey mendirikan VERSE Lab di National University of Singapore dan turut menciptakan perangkat verifikasi sumber terbuka Veil dan Velvet. Salah satu pendiri, CEO bersama, sekaligus Ketua Eksekutif Chris Hsu merupakan anggota Lean FRO Strategic Advisory Board dan presiden Infinitude Foundation. Sebelumnya, ia menjabat CEO Kilometre Capital dan direktur pelaksana Citadel Investment Group.

Pengumuman itu juga menyebut Gregory Malecha, yang sebelumnya memimpin bidang metode formal di BlueRock Security dan menjadi arsitek utama kerangka kerja verifikasi BRiCk; Sebastian Ullrich, salah satu arsitek Lean 4 dan salah satu pendiri Lean Focused Research Organization; Linus Lee, mantan mitra pengelola di Kilometre Capital; serta Drew Harman, mantan kepala pejabat komersial di Fastino Labs dan mitra operasional di Insight Partners dan Shasta Ventures. &Truth mengatakan pengembangannya berpijak pada penelitian selama puluhan tahun di bidang verifikasi formal dan penalaran otomatis di Stanford University dan National University of Singapore.

Kantor pusat &Truth di AS berada di Palo Alto, sedangkan kantor pusat internasionalnya berada di Singapura. Perusahaan itu mengatakan kantornya di Singapura akan berkembang pesat di bidang penelitian, rekayasa, produk, serta pemasaran dan pengembangan pasar. Dalam pengumuman tersebut, Low Jin Yong, Wakil Presiden Senior sekaligus Kepala Bersama Digital Industry Singapore, mengatakan bahwa kantor pusat itu akan memperdalam kapabilitas kepercayaan dan keselamatan di Singapura serta memperkuat posisi negara tersebut sebagai basis bagi perusahaan yang mengembangkan AI tepercaya.

Situs web perusahaan itu juga menampilkan diskusi meja bundar bersama Leonardo de Moura, pencipta Lean sekaligus Wakil Presiden dan Ilmuwan Terhormat di AWS, serta Simone Severini, anggota Lean FRO Strategic Advisory Board sekaligus Insinyur Terhormat di Google.

Esai Pendamping Menguraikan Alasan di Balik Perusahaan

Dalam esai pendamping bertanggal 29 Oktober 2026, Hsu menguraikan tren yang menurut perusahaan membuat verifikasi mendesak. Ia mengutip pernyataan CEO Google Sundar Pichai bahwa 75% kode baru di Google kini dihasilkan oleh AI dan disetujui oleh para insinyur, serta pengujian Veracode pada 2026 yang menemukan bahwa model AI gagal mengerjakan hampir separuh tugas pemrograman yang mengutamakan keamanan. Esai tersebut juga mengutip kampanye pada September 2026, ketika seorang penyerang mengerahkan ratusan agen AI untuk membobol 395 organisasi di 48 negara melalui kelemahan dalam perangkat lunak manajemen cetak yang banyak digunakan, serta rekor 14.959 kerentanan perangkat lunak yang dipublikasikan pada September 2026, angka yang disebutnya 3,5 kali jumlah yang dipublikasikan setahun sebelumnya.

Esai tersebut mengisahkan tonggak-tonggak awal verifikasi formal: pembuktian awal untuk mikrokernel seL4 membutuhkan sekitar 20 tahun-orang upaya para ahli untuk kira-kira 8.700 baris kode; pada 2015, dalam program HACMS DARPA, seL4 dipasang pada helikopter Unmanned Little Bird milik Boeing, yang sistem kendali penerbangannya tidak dapat ditembus oleh tim merah profesional meski mereka diberi akses selama berminggu-minggu; dan pada September 2026, sebuah model AI yang dikembangkan Anthropic memformalkan bukti lengkap Teorema Terakhir Fermat dalam Lean hanya dalam 11 hari. Esai itu juga mencatat bahwa pada awal 2026, Kim Morrison, insinyur perangkat lunak riset senior di Lean FRO, menggunakan Claude dari Anthropic dengan panduan manusia yang minimal untuk membuat versi pustaka kompresi zlib dalam Lean dan membuktikan bahwa pustaka itu selalu memulihkan data yang persis sama dengan yang dikompresinya.

Esai tersebut mengutip pencipta Lean, Leonardo de Moura: “Pengujian memberi keyakinan. Pembuktian memberi jaminan.”

Dalam esai kedua yang diterbitkan pada 29 Oktober 2026, Sergey menjelaskan mekanisme verifikasi program, dimulai dengan makalah Alan Turing tahun 1949, “Checking a Large Routine,” yang mengusulkan agar pemrogram menyertakan klaim-klaim terperinci pada kode mereka, yang dapat diperiksa satu per satu oleh sebuah pemeriksa. Esai tersebut menguraikan spesifikasi, invarian perulangan, dan pembuktian yang diperiksa dalam Lean, serta menyatakan bahwa tujuan &Truth adalah memungkinkan pengembang memperoleh bukti yang dapat diperiksa secara independen—seperti pembuktian formal dalam Lean—dengan biaya yang membuat verifikasi menjadi bagian rutin dari proses pengembangan.

&Truth menggambarkan visi jangka panjangnya sebagai peralihan dari “pemrograman berbasis intuisi” ke “pemrograman terverifikasi”, ketika kode yang dihasilkan AI diverifikasi secara matematis sebelum diterapkan, agen AI beroperasi dalam lingkungan yang pembatasannya dapat dibuktikan, perangkat lunak lama dimodernisasi dengan aman, dan infrastruktur kritis dilindungi oleh jaminan matematis yang dapat diperiksa secara independen.