Theorem, AI가 쓴 코드 검증해 버그 막는다… 600만 달러 유치

AI가 코드를 쓰는 시대, 신뢰가 새 병목이다

개요

투자와 시장 타이밍: 형식 검증 수요가 온다

샌프란시스코의 Y 콤비네이터 2025 스프링 배치 출신 스타트업 Theorem이 600만 달러 시드 투자를 유치했다. 라운드는 Khosla Ventures가 주도했고, Y 콤비네이터, e14, SAIF, Halcyon과 함께 Recursion 공동창업자 블레이크 보르게슨, 테조스 공동창업자 아서 브라이트먼 등 엔젤이 참여했다. GitHub, 아마존, 구글의 코딩 어시스턴트가 매년 수십억 줄의 코드를 만들어내는 가운데, 창업자들은 이를 검증할 인력·도구가 따라가지 못하는 ‘감독 격차’가 금융 시스템부터 전력망까지 위협한다고 지적한다. 공동창업자 제이슨 그로스는 “AI가 만든 6만 줄 코드를 사람이 검토하라면 방법이 없다”고 말했다.

왜 검증이 병목이 되었나

AI+형식 검증으로 검증 비용을 낮추다

Theorem의 핵심은 소프트웨어가 명세대로 동작함을 수학적으로 보이는 형식 검증에 AI를 결합해, 증명을 자동 생성·검사하는 것이다. 과거에는 코드 한 줄당 평균 8줄의 수학적 증명이 필요해 비용이 너무 컸고, 항공전자·원자로 제어·암호 프로토콜 등 임무임계 영역에만 쓰였다. MIT에서 HTTPS를 지탱하는 검증 암호 코드를 만들던 그로스는 해당 프로젝트에만 약 15 인년이 들었다며, “이제는 AI가 그 증명을 쓴다”고 설명했다.

기술과 성과

‘분수형 증명 분해’: 테스트가 놓치는 버그 잡기

Theorem은 코드 구성요소의 중요도에 비례해 검증 자원을 배분하는 ‘분수형 증명 분해’로, 복잡 소프트웨어의 전경로를 기계적으로 다 때려보지 않고도 핵심 동작의 정확성을 보장한다. 이 접근은 AI 안전 기업 Anthropic의 테스트를 통과했던 버그를 찾아내기도 했다. 그로스는 “큰 연산 없이도 지금 당장 버그를 잡게 해준다”고 말했다.

SFBench: Rocq→Lean 1,276문제 동등성 증명

최근 데모인 SFBench에서 Theorem은 Rocq의 1,276개 문제를 Lean으로 자동 변환한 뒤, 원본과의 동등성을 자동으로 증명했다. 사람이 했다면 약 2.7 인년이 걸렸을 작업이다. 또한 문맥 창 제약으로 상호 의존 코드에 약한 기존 AI 에이전트와 달리, 이 아키텍처는 병렬뿐 아니라 순차 실행을 통해 수십 개 파일에 걸친 누적 의존성을 다룬다.

실제 적용

1500쪽 사양에서 1만6천 줄 코드로: 현장 적용

한 고객은 1500쪽 PDF 사양과 메모리 누수·크래시 등 난해한 버그에 시달리던 레거시 구현을 들고 왔다. 과제는 오류 없이 처리속도를 10Mbps에서 1Gbps로 100배 끌어올리는 것. Theorem은 방대한 문서를 수백 줄의 실행 가능 사양으로 일반화하고, 동등성 체크 하네스를 붙여 새 구현이 의도한 동작과 일치함을 검증했다. 그렇게 생성된 1만6천 줄의 생산 코드는 사람의 수작업 리뷰 없이 배포됐고, 고객은 “파싱 중 정보 손실이 없다”는 확신과 함께 1Gbps급 프로덕션 파서를 손에 넣었다.

보안·정책

임계 인프라 보안·규제: 형식 검증의 의무화 논쟁

금융시장, 의료기기, 교통망, 전력망 등은 이미 소프트웨어로 움직이고, AI는 그 진화를 가속한다. 취약점 발굴·악용 비용이 AI로 급락하는 만큼, 방어는 자원 투입이 선형으로 늘지 않아도 버티는 ‘비대칭 방어’가 필요하다. 그로스는 “지속 가능한 소프트웨어 보안의 유일한 해법은 검증”이라며, 임계 시스템의 AI 생성 코드에 대해 규제가 형식 검증을 요구해야 하느냐는 질문에 “이제 형식 검증이 충분히 저렴해졌다면, 이를 쓰지 않는 것이 ‘중대한 과실’로 간주될 수 있다”고 답했다.

차별화와 팀

경쟁 구도와 팀: 형식 검증을 현업에 맞추다

AI와 형식 검증의 접점을 노리는 경쟁자가 많지만, Theorem은 수학 등 타 도메인이 아닌 소프트웨어 감독 스케일링에만 초점을 맞춘다. ‘하드웨어에 가까운’ 시스템 엔지니어링 팀이 변경을 머지하기 전 정확성 보증을 요구하는 사용 시나리오에 최적화했다. 공동창업자 그로스는 PL 이론과 대규모 프로덕션 배포 경험을, 라자슈리 아그라왈은 검증 파이프라인을 구동하는 ML 모델 학습을 이끈다. 그는 “평균 개발자 수준의 AI를 감독하는 것을 넘어, ‘리누스 토르발즈급’ AI의 역량을 제대로 끌어쓰도록 공식적 프로그램 추론을 만들고 있다”고 말했다.

전망

향후 계획: 로보틱스·재생에너지 등으로 확장

조달 자금은 인력 확충과 검증 모델 학습을 위한 컴퓨트 증설, 로보틱스·재생에너지·암호화폐·신약 합성 등 산업 확장에 쓰인다. 현재 팀은 4명 규모다. 기업 IT 리더들에게는 ‘더 많은 코드’보다 ‘속도가 안전을 갉아먹지 않는다는 수학적 증거’가 핵심 기준으로 부상하고 있다. 그로스는 AI 시스템의 기하급수적 개선을 전제로, 인간을 넘어서는 소프트웨어 공학이 불가피하다고 본다. “감독의 경제학을 근본적으로 바꾸지 못하면, 통제하지 못하는 시스템을 배포하게 될 것”이라는 경고가 Theorem의 문제의식을 요약한다.