&Truth, 코드용 범용 검증 기계 구축 위해 시드 투자 7,000만 달러 유치

소프트웨어가 안전하다는 사실을 수학적으로 증명하는 기술을 개발하는 공익법인 &Truth가 2026년 10월 29일 비공개 개발 단계에서 벗어나 시드 투자금 7,000만 달러를 공개하고, 자사가 ‘코드용 범용 검증 기계’라고 부르는 기술을 구축할 계획을 밝혔다.

출범 발표에서 회사는 2026년 초에 설립됐으며, AI 안전과 벤처캐피털 분야를 이끄는 선구자들이라고 설명한 투자자 그룹으로부터 시드 자금 7,000만 달러를 조달했다고 밝혔다. 또한 이 검증 기계는 어떤 프로그래밍 언어로 작성된 코드든 읽고, 해당 코드가 안전하고 보안성이 있으며 정확하다는 사실을 수학적으로 증명하도록 개발 중이며, 그 증명은 누구나 독립적으로 확인할 수 있다고 설명했다.

Lean을 기반으로 한 증명 자동화

발표에 따르면 형식 검증은 수십 년 전부터 존재했지만, 전문가가 증명을 수작업으로 작성해야 했기 때문에 접근하기 어렵고 비용도 많이 들었으며, 그 결과 소수의 핵심 시스템에만 적용됐다. 회사는 이제 AI가 형식 증명 작업을 100배 이상 빠르게 하고, 자체 증명 자동화 기술이 여기에 다시 100배의 속도 향상을 더해 증명 생성에 걸리는 시간을 수년 또는 수개월에서 몇 시간 또는 몇 분으로 줄인다고 밝혔다.

회사는 또한 ‘명세 공장’ 기술을 소개했다. 이 기술은 기업과 개발자가 인간의 의도와 비즈니스 요구사항을 정밀한 형식 명세로 대규모 변환할 수 있게 해 준다. 이를 통해 테스트나 공급업체의 주장에 의존하는 대신, 누구나 독립적으로 확인할 수 있는 보장을 제공한다는 설명이다.

&Truth는 오픈소스 증명 시스템인 Lean과 수학적 정의 및 정리를 200만 줄 넘게 담은 라이브러리 Mathlib, 그리고 CSLib를 포함한 오픈소스 기술을 기반으로 개발하고 있다. 회사가 지향하는 목표는 소프트웨어를 위한 범용 형식 언어다. 여기에는 프로그래밍 언어와 시스템의 수학적 모델, 증명 기법, 언어를 넘나드는 자동 검증을 가능하게 하는 정밀한 명세가 포함된다. &Truth는 Lean Focused Research Organization과 협력하고 있으며, 기반 라이브러리를 오픈소스로 공개할 계획이라고 밝혔다.

공동 창업자 겸 공동 CEO인 Clark Barrett은 Lean과 Mathlib이 AI에 수학적 추론을 위한 정밀한 언어를 제공했지만, 소프트웨어에는 이에 상응하는 토대가 없었다고 말했다. 공동 창업자 겸 최고과학책임자인 Ilya Sergey는 소프트웨어에 대한 신뢰는 어떤 기업의 말이 아니라 독립적으로 확인할 수 있는 증명에 기반해야 한다고 말했다.

창업자와 두 곳의 본사

Barrett은 Stanford University의 코벨 컴퓨터과학 석좌교수이자 Stanford Center for AI Safety의 창립 공동 소장, Stanford Center for Automated Reasoning의 소장, CSLib의 공동 제작자이며, 자동 추론 엔진 cvc5의 프로젝트 책임자다. Sergey는 National University of Singapore에 VERSE Lab을 설립했으며, 오픈소스 검증기 Veil과 Velvet을 공동 제작했다. 공동 창업자 겸 공동 CEO이자 이사회 의장인 Chris Hsu는 Lean FRO 전략자문위원회 위원이자 Infinitude Foundation의 대표이며, 이전에는 Kilometre Capital의 CEO와 Citadel Investment Group의 매니징 디렉터를 역임했다.

발표에는 BlueRock Security에서 형식 기법을 이끌었으며 BRiCk 검증 프레임워크의 핵심 설계자였던 Gregory Malecha, Lean 4의 공동 설계자이자 Lean Focused Research Organization의 공동 창업자인 Sebastian Ullrich, Kilometre Capital의 전 매니징 파트너인 Linus Lee, Fastino Labs의 전 최고영업책임자이자 Insight Partners와 Shasta Ventures의 운영 파트너인 Drew Harman도 이름을 올렸다. &Truth는 Stanford University와 National University of Singapore에서 수십 년간 축적된 형식 검증 및 자동 추론 연구를 바탕으로 사업을 추진한다고 밝혔다.

&Truth의 미국 본사는 Palo Alto에, 국제 본사는 Singapore에 있다. 회사는 연구, 엔지니어링, 제품 및 시장 진출 업무 전반에 걸쳐 Singapore 사무소를 크게 확장할 계획이라고 밝혔다. Low Jin Yong 싱가포르 디지털 산업 담당 수석 부사장 겸 공동 책임자는 발표에서 본사가 Singapore의 신뢰 및 안전 역량을 심화하고, 신뢰할 수 있는 AI를 개발하는 기업들의 거점으로서 국가의 위상을 강화할 것이라고 말했다.

회사 웹사이트에는 Lean의 발명가이자 AWS 부사장 겸 특별연구원인 Leonardo de Moura와 Lean FRO 전략자문위원회 위원이자 Google의 특별 엔지니어인 Simone Severini가 참여한 원탁 토론도 소개돼 있다.

회사의 사업 배경을 설명하는 동반 에세이

2026년 10월 29일자 동반 에세이에서 Hsu는 회사가 검증을 시급한 과제로 보는 배경이 된 흐름을 자세히 설명했다. 그는 Google CEO Sundar Pichai의 발언을 인용해 현재 Google에서 새로 작성되는 코드의 75%를 AI가 생성하고 엔지니어가 승인한다고 전했다. 또한 AI 모델이 보안이 중요한 코딩 작업의 거의 절반에서 실패한 것으로 나타난 Veracode의 2026년 테스트 결과도 언급했다. 에세이는 널리 사용되는 인쇄물 관리 소프트웨어의 취약점을 통해 공격자가 AI 에이전트 수백 개를 동원해 48개국 395개 조직에 침투한 2026년 9월의 캠페인과, 2026년 9월에 공개된 소프트웨어 취약점이 사상 최대인 14,959건에 달했다는 사실도 인용했다. 에세이는 이 수치가 1년 전 공개된 건수의 3.5배라고 설명했다.

이 글은 형식 검증의 주요 성과를 되짚는다. seL4 마이크로커널의 최초 증명에는 약 8,700줄의 코드를 대상으로 전문가의 작업 약 20인년이 들었다. 2015년에는 DARPA의 HACMS 프로그램에 따라 seL4가 Boeing의 무인 헬리콥터 Unmanned Little Bird에 탑재됐다. 전문 레드팀은 몇 주 동안 접근 권한을 부여받았지만 헬리콥터의 비행 제어 시스템을 뚫지 못했다. 2026년 9월에는 Anthropic이 개발한 AI 모델이 Lean에서 페르마의 마지막 정리에 대한 완전한 증명을 11일 만에 형식화했다. 또한 2026년 초에는 Lean FRO의 선임 연구 소프트웨어 엔지니어인 Kim Morrison이 Anthropic의 Claude를 활용해 사람의 안내를 최소한으로만 받고 Lean으로 zlib 압축 라이브러리를 구현했으며, 이 라이브러리가 압축한 데이터를 항상 정확히 복원한다는 점을 증명했다고 전한다.

이 글은 Lean의 창시자 Leonardo de Moura의 말을 인용한다. “테스트는 확신을 줍니다. 증명은 보증을 제공합니다.”

2026년 10월 29일에 발표된 두 번째 글에서 Sergey는 프로그램 검증의 작동 원리를 설명하며, 프로그래머가 검사기가 개별적으로 검증할 수 있는 정확한 주장을 코드와 함께 제시해야 한다고 제안한 Alan Turing의 1949년 논문 「Checking a Large Routine」에서 이야기를 시작한다. 이 글은 명세, 루프 불변식, Lean으로 검사하는 증명을 설명하고, 개발자가 Lean의 형식 증명과 같이 독립적으로 검증할 수 있는 근거를 검증이 개발 과정의 일상적인 일부가 될 수 있는 비용으로 얻도록 하는 것이 &Truth의 목표라고 밝힌다.

&Truth는 장기적인 비전을 “바이브 코딩”에서 “검증 코딩”으로의 전환으로 설명한다. 이 전환은 AI가 생성한 코드를 배포 전에 수학적으로 검증하고, AI 에이전트가 작동 범위를 증명할 수 있는 환경 안에서 활동하며, 레거시 소프트웨어를 안전하게 현대화하고, 독립적으로 검증할 수 있는 수학적 보증으로 핵심 인프라를 보호하는 것을 뜻한다.