Anthropic은 Theorem Labs와 함께 Claude를 기계어 수준까지 섬세한 소프트웨어 취약점 대소탕에 밀어 넣었다. 이들은 Claude를 가장 하위 계층까지 내려보내 RISC-V 어셈블리 명령을 대상으로 다수의 프로덕션급 오픈소스 코드베이스에 대해 형식적 검증을 수행하게 했다—단 몇 주 만에 123개 오픈소스 코드베이스, 239개 테스트 진입점을 처리하고 검증을 통과한 1.8억 줄의 Rocq 수학적 증명 코드를 산출했다.
정말 등골이 서늘해지는 것은 그것이 찾아낸 내용이다. 퍼징(fuzzing)을 수조 번 돌려도 발견하지 못한 숨겨진 취약점, 십여 년 넘게 잠복해 온 고위험 논리적 사각지대, 나아가 x86 프로세서 수준의 하드웨어 결함과 공식 문서 속 오류까지 Claude가 단번에 잡아냈다. 기존의 무작위 테스트는 모래로 취약점을 반복해서 걸러내는 것과 같아 항상 빠뜨리는 것이 있었다. 이 방식의 강점은 테스트 진입점을 수학적 명제로 직접 변환하여 전체 경로, 전체 입력에 대한 포괄적 증명을 수행한다는 점이다—증명이 어딘가에서 "막혀" 더 이상 진행되지 못하면, 그곳이 대개 취약점의 은신처인데, Claude는 아울러 패치를 수정하고 다시 검증을 이어갈 수 있어 누락률이 크게 낮아진다.
비용의 척도에 놓고 보면 이 일의 의미가 더욱 분명해진다. 기계어 수준까지 내려가는 형식적 검증은 예로부터 공학량이 많기로 악명 높은 고된 작업이었으나, 이제 대규모 모델의 능력을 빌려 검증 효율이 약 두 달마다 두 배가 되는 속도로 급증하고 있으며, 작성된 증명은 프로젝트 간 재사용도 가능하다. 현재 추세로 추산하면 약 1.34억 달러를 투입하면 2027년 말까지 Nix 생태계 기계어의 95% 검증을 완료할 수 있을 것으로 보인다. 현재 첫 번째 관련 증명들이 이미 공개되어 있다. 사이버 보안 상황이 날로 긴밀해지는 가운데, 이러한 "AI로 코드의 정확성을 수학적 정리로 만드는" 경로는 업계에 전혀 새로운 방어선을 제공한다.