스탠퍼드 연구자 추위에 선(Chuyue Sun)과 동료들이 개발한 AI 도구는 엔지니어링 프로젝트를 500달러 미만의 비용으로 반나절도 안 돼 끝냈다. 숙련된 전문가 3명이 같은 작업을 수작업으로 하는 데는 5개월이 걸렸다. 선이 최근 논문에서 보고한 이 결과는 코드가 의도대로 작동하는지 수학적으로 확인하는 형식 검증(formal verification)에 관심이 커지는 배경 중 하나다.

개발자들은 수십 년 동안 수학으로 소프트웨어에 버그가 없음을 증명하는 방법을 구상해왔다. 소프트웨어의 목표를 정밀한 명세로 작성하고 코드를 검증 가능한 수식으로 바꿔야 해 시간과 노력이 많이 든다. 기업들은 이미 여러 테스트로 결함을 찾지만, 더 예측하기 어려운 동작까지 잡아낼 수 있는 형식 검증에는 비용을 들이는 경우가 드물다.

최근 스타트업들은 생성형 AI가 형식 검증을 실용적이고 필수적인 도구로 만들 수 있다고 보고 있다. 선이 8월 합류한 &Truth는 목요일 공개 출범했다. 선의 연구는 메시징 앱 Signal의 대화 암호화 코드 일부를 AI로 검증해 기술의 가능성을 보였다. &Truth의 최고과학책임자 일리야 세르게이(Ilya Sergey)는 형식 검증에 필요한 수학적 추론 기술은 이미 있었지만 규모를 키우기 어려웠다고 말했다. &Truth는 투자금 7,000만 달러를 유치했으며, 장기적으로 모든 프로그래밍 언어를 검증하는 것을 목표로 한다.

경쟁사 Harmonic은 이번 주 수학 중심 AI 에이전트 Aristotle이 C로 작성한 소프트웨어와 Verilog 하드웨어 설계를 검증할 수 있다고 발표했다. 로빈후드 최고경영자 블라드 테네프(Vlad Tenev)가 공동 창업한 Harmonic은 2억9,500만 달러를 투자받았다. 이 회사는 잠재 고객인 칩 제조사 Tensordyne과 엔비디아를 대상으로 기술을 평가하고 있다. 엔비디아의 벤처 투자 부문도 투자자다.

앤스로픽과 검증 스타트업 Theorem은 지난주 AI를 활용해 수조 번의 테스트에서도 발견하지 못한 오픈소스 소프트웨어 버그를 찾았다고 발표했다. 두 회사는 다른 개발자의 검증 작업을 돕는 Claude용 추가 기능도 공개했다. 초기 프로젝트 비용은 공개하지 않았다.

형식 검증이 널리 쓰이면 소프트웨어의 신뢰성을 높이고 보안 문제를 줄일 수 있다는 기대가 있다. 그러나 AI가 NASA나 애플 같은 조직의 핵심 시스템을 넘어 일반적인 소프트웨어 개발에도 형식 검증을 확산시킬 수 있을지는 아직 불확실하다. 기술은 시제품 단계이며, 수요는 높지만 고객이 얼마를 지불할지, 어떤 방식으로 도입하려 할지는 분명하지 않다. 검증은 컴퓨터와 사람이 소프트웨어를 사용하는 방식에 대한 가정에 의존하기 때문에, 사용자 실수나 하드웨어 고장에서 비롯된 버그를 잡는 데 한계가 있다는 전문가들의 회의론도 있다.

버그 탐지 AI 스타트업 Antithesis를 이끄는 윌 윌슨(Will Wilson)은 형식 검증을 수학 애호가에게 ‘골칫거리’라고 부른다. Antithesis는 사이버 보안 방어 기능 일부를 형식 검증하는 데 수백만 달러를 썼지만, 자체 도구를 이용해 추가 오류를 발견했다. Antithesis는 고객들이 형식 검증을 마친 소프트웨어에서도 버그를 찾아냈다. 윌슨은 형식 검증이 어느 정도 확신을 줄 수는 있지만, 그 확신이 옳음을 증명하려면 철저하고 포괄적인 테스트가 필요하다고 말했다.

이더리움 암호화폐를 만든 엔지니어 비탈릭 부테린(Vitalik Buterin)도 올해 초 블로그 글에서 형식 검증은 만능이 아니라고 썼다. 다만 부테린을 비롯한 지지자들은 AI 시스템이 사이버 공격을 벌이거나 큰 혼란을 일으키는 일을 막는 데 형식 검증이 중요한 방어 수단이 될 수 있다고 본다.

기업 공개 자료에 따르면 보잉 항공기와 아마존 서버, 애플의 활성 기기 25억 대 이상에는 형식 검증을 거친 소프트웨어가 일부 포함돼 있다. 해당 코드는 대체로 보안과 관련돼 있으며, 취약점이 악용되면 심각한 피해를 낳을 수 있다. 아마존웹서비스의 부사장이자 저명 과학자인 바이런 쿡(Byron Cook)은 형식 검증이 고객의 클라우드 보안 우려를 덜고, 큰 버그를 초기에 제거해 내부 팀의 작업 속도를 높이는 데 도움이 됐다고 말했다.

반면 중견 기술 기업들은 제품의 핵심 기능 하나만 검증했거나, 아예 검증하지 않은 경우가 많다고 WIRED에 전했다. 검증 엔지니어 부족과 비용 대비 위험, 검증에 몇 주를 기다리느라 혁신이 늦어질 수 있다는 우려가 이유로 꼽혔다. 애플 보안팀은 올해 초 암호화에 쓰이는 ‘corecrypto’ 라이브러리에서 형식 검증으로 찾아낸 문제 가운데 일부는 다른 방법으로 발견할 수 없었을 것이라고 밝혔다. 동시에 검토 속도를 맞추기 위해 corecrypto에 새 코드를 추가할 때는 신중해야 한다고 덧붙였다.

코드 형식 검증을 한 번도 하지 않은 대기업 두 곳의 사이버 보안 임원은 자동화가 투자할 가치가 있는지 확신하지 못한다고 말했다. 다만 AI 연구소가 ‘검증된’ AI 생성 코드를 제공한다면 비용을 지불할 수도 있다고 봤다. 오픈소스 프로젝트 개발자들도 AI 보조 검증을 시험하고 있다. 비영리 단체 Beneficial AI Foundation은 앤스로픽의 지원금을 받아 선의 스탠퍼드 연구에서 검증한 것과 같은 암호화 코드를 올해 검증했다. 라이브러리 curve25519-dalek의 관리자인 마이클 로젠버그(Michael Rosenberg)는 지속적인 검증을 뒷받침할 안정적인 재원이 마련되길 바라지만, AI 기업의 선의에 의존해서는 안 된다고 말했다.

스타트업들은 프로그램의 동작 방식을 정의하는 작업 상당 부분을 AI로 자동화하려 한다. 예를 들어 데이터 표는 정렬 전후에 항목은 같고 순서만 달라야 한다는 명세를 둘 수 있다. 이후 AI를 쓰지 않는 자동화 과정이 코드를 Lean, Rocq, Isabelle 같은 수학 도구가 확인할 수 있는 형식으로 바꾼다.

마이크로소프트 리서치에서 20년 넘게 일한 뒤 스타트업 Truidic을 세운 마단 무수바티(Madan Musuvathi)는 Hugging Face를 겨냥한 OpenAI 해킹 사건 등을 계기로 자신의 연구를 상용화할 필요가 시급하다고 느꼈다. 그는 공격자가 AI를 활용하면 큰 위협이 될 수 있지만, 검증이 모두를 위한 AI 안전과 보안을 뒷받침할 수 있다고 말했다.

전통적인 형식 검증 서비스를 오래 제공해온 Proofcraft는 잠재 고객의 문의가 크게 늘었다고 밝혔다. 최고경영자 준 앤드로닉(June Andronick)과 최고과학자 게르빈 클라인(Gerwin Klein)은 관심이 자사와 경쟁사들이 제공할 수 있는 수준을 크게 웃돈다고 말했다. 그러나 두 사람은 AI가 만든 명세가 결과에 대한 ‘정당하지 않은 신뢰’를 낳을 수 있다고 우려한다. 클라인은 검증 작업을 퍼즐 게임처럼 중독성 있는 일이라고 표현했다.