Theorem Blog의 연구진은 모델의 소프트웨어 검증 능력이 두 달마다 두 배로 향상된다는 가정 아래, 2027년 말까지 nixpkgs에 포함된 기계어의 95%를 검증하는 데 약 1억 3,400만 달러가 들 것으로 추산했다. 이 추산은 nixpkgs의 의존성 정보를 이용해, 프로그램을 실행하는 바이너리 수준에서 검증을 순차적·병렬적으로 진행하는 방식을 바탕으로 한다.

연구진은 각 바이너리에 검증 작업을 하나씩 배정하고, 실행에 필요한 의존 라이브러리의 검증이 끝나면 그 결과를 재사용하도록 설계했다. 예를 들어 OpenSSL은 약 1만 6,000개 패키지의 실행 의존성에 포함된다. 오늘날의 검증 비용으로 OpenSSL을 한 번 증명하는 데 약 22만 달러가 들지만, 이를 재사용하면 패키지당 비용은 약 14달러가 된다는 계산이다. 의존성을 공유하지 않고 각 패키지가 필요한 실행 환경 전체를 따로 검증하면 비용은 약 1,900억 달러로, 공유할 때의 약 64억 달러보다 크게 늘어난다고 추산했다.

모델의 검증 속도와 향상 추세는 연구진이 진행한 평가에서 가져왔다. 평가에서는 기계어 크기가 0.5~2.5KB인 C 프로그램 36개를 검증하도록 했다. 2026년 5~9월에 출시된 앤스로픽과 오픈AI의 모델 7개를 비교한 결과, 통과한 시도만 집계한 검증 속도는 약 두 달마다 두 배가 됐다. Opus 4.8의 시간당 약 0.12KB에서 9월 모델의 시간당 0.6~0.9KB로 높아졌다. 다만 GPT-6 Luna는 108번의 시도 중 8번 미만만 통과해 비교에서 제외했다.

연구진은 시작 검증 속도를 시간당 0.5KB, 비용을 KB당 40달러로 놓고, 측정된 추세가 계속돼 능력이 두 달마다 두 배로 향상된다고 가정했다. 이는 언어 모델 전반에 대해 Epoch AI가 추산한 8개월 주기보다 네 배 빠른 향상 속도다. 이런 가정에서 연간 1억 달러를 투입하면 2027년 말까지 기계어의 95%를 검증하고, 마지막 패키지는 작업 시작 약 1년 반 뒤에 검증을 마쳐 총비용은 약 1억 3,400만 달러가 된다고 계산했다. 이는 예측이지 실제 검증을 완료한 결과는 아니다.

분석 대상은 2026년 9월 16일의 nixpkgs nixos-26.05 스냅샷이다. 중복을 제거하고 x86 바이너리만 남긴 결과 2만 8,650개 패키지에 걸친 바이너리 12만 3,471개, 기계어 153.7GB를 분석했다. 바이너리 크기는 .text 섹션 기준이며, 패키지 간 연결은 실행 시 참조하는 의존성만 포함했다. 비용과 시간은 바이너리 크기에 비례한다고 가정했으며, 연구진은 이 가정이 시험한 작은 바이너리에서 성립하고 의존성을 제외한 바이너리의 90% 이상이 2MB 미만이라고 밝혔다.

연구진은 실제 운영 소프트웨어를 바이너리 수준에서 검증하면 여러 언어와 도구 체인으로 만들어진 프로그램을 다룰 수 있고, 증명 과정에서 발견한 버그가 모델링 방식의 부산물이 아니라 실제 프로그램의 버그가 될 수 있다고 설명한다. 다만 전체 소프트웨어 검증이라는 목표와 비용·일정은 모델 능력의 향상 추세가 계속된다는 가정에 달려 있다. 연구진은 소프트웨어를 만드는 이들에게 검증하고 싶은 속성을 제안하고, 프런티어 모델 개발자에게는 형식 검증 능력 향상을 지원하며, 칩·독점 플랫폼 제작자에게는 소프트웨어가 의존하는 동작의 완전한 사양을 공개해 달라고 요청했다.

연구의 추정 자료와 언어 모델의 알고리즘 발전 추정, 검증 속도 평가 그래프, 원문을 참고할 수 있다.