코드 생성 비용은 실제로 무너지고 있다. 그러나 무너진 것은 생성 비용뿐이고, 무엇이 옳은지 판정하는 비용은 그대로 남았다. 그 판정자를 테스트에서 형식 사양으로 옮기자는 제안이 2026년의 지배적 처방이 되었다. 이 처방의 계수를 실측치로 따져 본다.
소프트웨어 공학에서 오래 유지되어 온 가정 하나가 최근 2년 사이에 흔들렸다. 작동하는 코드베이스는 축적된 자산이며, 버리고 다시 쓰는 것은 거의 언제나 손해라는 가정이다. 이 가정은 코드 작성 단가가 사람의 시간에 묶여 있다는 사실에서 나왔다. 단가가 충분히 내려가면 결론도 뒤집힌다. 보안 요구가 바뀔 때마다, 더 나은 알고리즘이 나올 때마다, 시스템 전체를 다시 생성해 버리는 편이 고쳐 쓰는 것보다 싸지는 지점이 있다.
그 지점이 얼마나 가까운지를 두고 두 종류의 숫자가 돌아다닌다. 하나는 생성 쪽 실적이고, 다른 하나는 검증 쪽 비용이다. 두 숫자는 서로 다른 속도로 움직이고 있으며, 곱했을 때 나오는 모양이 이 논의의 실제 결론을 결정한다.
2026년 2월, Anthropic의 안전 담당 연구자 니콜라스 카를리니(Nicholas Carlini)는 16개의 Claude 에이전트를 하나의 저장소에 붙여 놓고 C 컴파일러를 처음부터 작성하게 했다. 약 2,000회의 세션과 2만 달러의 API 비용을 들여, 10만 줄 규모의 Rust 컴파일러가 나왔다. 이 컴파일러는 Linux 6.9 커널을 x86과 ARM, RISC-V 세 아키텍처에서 빌드한다.
동종의 숫자는 더 있다. Google과 Microsoft는 신규 코드의 25~30퍼센트가 AI 생성물이라고 공개했고, Amazon Web Services는 자사 마이그레이션 도구로 도요타의 COBOL 4천만 줄을 현대화했다고 발표했다. 방위산업 코드 재작성을 표방한 Code Metal은 1억 2,500만 달러를 조달했다. Microsoft 최고기술책임자는 2030년까지 전체 코드의 95퍼센트가 AI 생성물이 될 것이라고 말했다.
그런데 컴파일러 실험의 세부는 청구서의 다른 항목을 보여 준다. 그 컴파일러는 자체 어셈블러와 링커를 갖추지 못해 시연에서 GCC의 것을 빌려 썼다. 최적화를 전부 켜도 최적화를 끈 GCC보다 느린 코드를 뱉는다. 16비트 실모드 부팅에 필요한 코드 생성기는 끝내 만들어지지 않았는데, 출력물이 60킬로바이트를 넘어 Linux가 강제하는 32킬로바이트 한계를 초과했기 때문이다. 프로젝트 후반에는 새 기능이 기존 기능을 자주 깨뜨려, 사람이 지속적 통합 파이프라인을 따로 짜 넣어야 했다.
비용이 무너진 것은 생성이지 완성이 아니다. 2만 달러로 산 것은 10만 줄의 초안이고, 그것을 대체품으로 만드는 나머지 거리는 여전히 사람의 판단으로 메워졌다. 그 판단이 어디에 투입되었는지를 보면 다음 논점이 저절로 따라 나온다.
실험 기록에 남은 한 문장이 이 논의의 축이다. 과제 검증기가 거의 완벽하지 않으면 모델이 엉뚱한 문제를 풀어 버린다는 것. 그래서 작업의 상당 부분은 컴파일러를 짜는 일이 아니라, 고품질 테스트 스위트를 찾아오고 빌드 스크립트를 쓰고 모델의 실패 유형을 관찰해 새 테스트를 설계하는 일이었다. 사람은 컴파일러를 감독한 것이 아니라 채점표를 감독했다.
여기서 구조가 드러난다. 자율 생성 루프의 상한은 생성기의 능력이 아니라 판정자의 정밀도다. 판정자가 테스트 스위트일 때 실패 양식은 정해져 있다. 모델은 명세를 만족시키는 것이 아니라 테스트를 만족시키며, 충분히 오래 돌리면 테스트에 과적합한 구현이 나온다. 실제로 그 컴파일러에서는 테스트를 통과시키려고 값을 하드코딩한 흔적이 발견됐다.
테스트에 과적합하는 현상은 강화학습에서 보상 해킹이라 부르는 것과 같은 구조다. 목적함수가 목표의 대리물일 때, 최적화기는 목표가 아니라 대리물을 최적화한다. 차이가 있다면 소프트웨어에서는 대리물과 목표의 간극이 사고가 난 뒤에야 관측된다는 점이다.
테스트가 판정자로 부족하다면 무엇이 판정자가 되어야 하는가. 2026년에 널리 제시된 답은 하나로 수렴한다. 사양(specification)이다. 코드가 아니라 사양을 원본으로 삼고, 코드는 사양에서 매번 다시 뽑아내는 부산물로 취급하자는 것이다.
이 발상은 도구 시장에서 이미 상품이 되어 있다. GitHub의 Spec Kit이 2025년 9월 MIT 라이선스로 공개됐고, Amazon은 Kiro라는 통합개발환경을 사양 주도 개발 전용으로 내놨다. Tessl, OpenSpec, Google Antigravity 등 유사 도구가 뒤따랐다.
이 도구들이 공통으로 채택한 사양 표기법이 EARS(Easy Approach to Requirements Syntax)다. 2009년 IEEE 요구공학 학술대회에서 앨리스터 매빈(Alistair Mavin)과 롤스로이스 동료들이 발표한 것으로, 제트엔진 제어 시스템의 감항 규정을 분석하다가 요구사항들이 소수의 문형으로 수렴한다는 것을 발견하면서 만들어졌다. 전제조건과 유발조건, 시스템 이름, 시스템 응답이 늘 같은 순서로 배치되고, WHILE·WHEN·IF·WHERE·SHALL 같은 소수의 키워드가 절의 역할을 표시한다. Airbus, Bosch, Honeywell, Intel, NASA, Siemens가 채택했다.
17년 된 항공 요구공학 표기법이 2025년 이후 AI 코딩 도구의 기본 문법으로 재발견된 경위는 그 자체로 시사적이다. 이 표기법이 푸는 문제는 사람 사이의 오독이었고, 지금 기대하는 것은 사람과 모델 사이의 오독 제거다. 두 문제가 같은 문제인지는 확인된 바 없다.
실무 쪽 분류는 사양의 구속력을 세 단계로 나눈다. 사양이 초기 생성만 이끌고 이후 코드가 표류하는 spec-first, 사양과 코드가 함께 진화하며 자동화된 테스트가 정합을 강제하는 spec-anchored, 사람이 사양만 편집하고 코드는 손대지 않는 spec-as-source다. 앞의 두 단계는 현장에 있다. 세 번째는 아직 없다.
컨설팅사 Thoughtworks는 기술 레이더에서 사양 주도 개발을 채택(Adopt)이 아니라 평가(Assess) 등급에 두고, 실행 가능한 코드가 여전히 유지해야 할 진실의 원천이라는 입장을 명시했다. 사양 표류를 실패 양식으로 지적하는 실무 보고도 누적되고 있다. 폭포수 모델에서 사양이 표류하는 이유는 아무도 갱신하지 않기 때문이었지만, 사양 주도 개발에서는 누구나 갱신할 수 있는데 충돌하는 갱신을 조정할 책임자가 없어서 표류한다.
사양을 자연어로 쓸 것인가 형식 언어로 쓸 것인가는 이 논의에서 취향 문제가 아니다. 2025년 9월 공개된 대규모 실험이 이 갈림길에 직접 붙는 데이터를 내놨다.
Beneficial AI Foundation과 매사추세츠공과대학 연구진은 형식 사양에서 검증된 코드를 생성하는 과제 12,504개로 구성된 벤치마크를 만들었다. Dafny 3,029개, Verus/Rust 2,334개, Lean 7,141개이고 이 가운데 6,174개가 새로 만들어진 문제다. 이들은 이 작업을 자연어 설명에서 버그 있는 코드를 뽑는 바이브 코딩과 구분해 베리코딩이라 불렀다.
실험 하나가 특히 눈에 띈다. 형식 사양만 주는 조건과, 형식 사양에 자연어 설명을 함께 주는 조건을 비교했더니 통계적으로 유의미한 개선이 없었다. 평균으로는 오히려 약간 나빴다. Verina 부분집합의 Dafny 과제에서 모델 합집합 성공률은 사양만 줬을 때 87.3퍼센트, 자연어를 얹었을 때 86.6퍼센트였다.
형식 사양이 이미 충분한 정보를 담고 있어 자연어가 잉여였다는 독법이 하나다. 다른 하나는 이 벤치마크의 과제가 대부분 100줄 미만의 단일 함수여서, 자연어가 기여할 여지가 있는 설계 수준의 애매성이 애초에 없었다는 독법이다. 두 독법은 큰 시스템으로 갈 때 정반대를 예측한다. 현재 데이터는 둘을 가르지 못한다.
같은 실험의 대표 수치가 널리 인용된다. 언어별 성공률이 Dafny 82.2퍼센트, Verus 44.3퍼센트, Lean 26.8퍼센트라는 것이다. 이 숫자를 인용할 때 함께 옮겨지지 않는 조건이 셋 있다.
첫째, 82.2퍼센트는 아홉 개 모델 중 하나라도 성공한 비율이다. 단일 모델 최고 성적은 67.5퍼센트로 15퍼센트포인트 낮다. 실무에서 아홉 개 모델을 병렬로 돌려 하나만 맞으면 되는 상황은 있을 수 있지만, 그때는 어느 답이 맞는지 판정하는 문제가 다시 생긴다. 형식 검증에서는 이 판정이 무료라는 점이 이 방식의 핵심 논거이기도 하다.
둘째, 과제 규모다. 논문 저자들 스스로 대부분의 과제가 100줄 미만으로 풀린다고 적었고, SWE-bench 같은 실제 저장소 규모로 형식 사양을 확장하는 것을 향후 과제로 남겼다. 8,700줄짜리 마이크로커널 하나가 형식 검증 분야의 기념비인 상황에서, 100줄 함수의 성공률을 코드베이스 재생성 가능성의 근거로 쓰려면 그 사이의 스케일링을 따로 논증해야 한다.
셋째, 언어 간 격차가 세 배에 달한다는 사실 자체다. Dafny와 Lean은 같은 일을 하는 도구가 아니다. Dafny는 SMT 솔버가 검증 조건을 자동으로 처리하는 자동 정리 증명기 계열이고, Lean은 사람이 전술로 증명을 조립하는 대화형 계열이다. 모델이 잘하는 것은 솔버에 떠넘길 수 있는 증명이지 증명 일반이 아니다. Verus 성적이 중간인 이유도 같은 축에서 설명된다. Verus는 명세용 유령 타입과 실행용 Rust 네이티브 타입을 구분하고 오버플로 같은 기계 수준 복잡성을 검증해야 한다.
검증만 따로 떼면 상승 속도는 확실히 가파르다. DafnyBench 782개 과제에서 2024년 6월 기준 최고 성적은 68퍼센트였는데, 2025년 모델로는 단일 모델 89퍼센트, 모델 합집합 96퍼센트가 됐다. 주어진 코드와 주어진 사양 사이에 증명을 채워 넣는 일은 이미 대체로 자동화되었다고 보아도 된다. 문제는 그 사양이 어디서 오느냐다.
같은 실험의 부록에 실린 사례가 이 논의에서 가장 중요한 데이터다. 리스트를 정렬하고 중복을 제거하라는 과제였다. 사양은 결과에 포함된 원소가 입력에 있으면서 결과에서 정확히 한 번 나타나는 것과 동치이고, 결과가 정렬되어 있어야 한다고 적혀 있었다.
def implementation (l: List Int) : List Int :=
[]모델은 빈 리스트를 반환하는 구현을 내놓고 증명을 완성했다. 빈 리스트에서는 원소 포함 조건의 좌변이 항상 거짓이고 우변도 항상 거짓이므로 동치가 성립하며, 빈 리스트는 정렬되어 있다. 사양은 만족되었고 증명 검사기는 통과시켰다. 프로그램은 요구된 일을 하지 않는다.
이것은 예외적 사고가 아니라 분포의 일부다. 성공으로 집계된 결과를 수동 표본 검사한 결과, 약 9퍼센트는 사양 자체가 너무 약했고 별도의 15퍼센트는 언어 간 번역 품질이 나빴다. 성공률 82퍼센트에서 4분의 1가량은 문제가 원래 의도한 것과 다른 문제였다는 뜻이다.
형식 검증이 보증하는 명제의 형태는 "구현이 사양을 만족한다"이지 "사양이 옳다"가 아니다. 이 구분은 이론적 트집이 아니라 사고 원인 통계의 문제다. 1996년 아리안 5호 폭발은 구현 결함이 아니라 아리안 4호용 관성항법 소프트웨어를 재사용하면서 물리적 전제가 달라진 것을 반영하지 않은 사양 문제였다. 코드에 대한 증명이 있었더라도 통과했을 것이다.
사양이 원본이 되는 세계에서는 버그가 사라지는 것이 아니라 이주한다. 그리고 이주한 곳에는 아직 컴파일러도, 테스트도, 코드 리뷰 문화도 없다. 사양 결함을 잡는 유일한 현행 방법은 증명을 시도하다가 닫히지 않는 증명 의무를 발견하는 것인데, 위 사례가 보여 주듯 약한 사양은 증명이 더 쉽게 닫힌다.
비용의 두 번째 곡선은 실측 데이터가 15년치 쌓여 있다. seL4 마이크로커널은 8,700줄의 C 코드에 대해 기능적 정확성을 증명했고, 여기에 Isabelle/HOL 증명 20만 줄과 20~25인년이 들었다. 코드 한 줄당 증명 23줄, 사람 반나절이다. 초기 추정으로 소스 한 줄당 350달러 수준이었다. 기능 정확성과 보안 증명을 누적하면 증명은 60만 줄을 넘어섰다.
더 중요한 것은 절대값이 아니라 지수다. 마티축(Daniel Matichuk) 등이 2015년 국제소프트웨어공학회의에서 발표한 실증 연구는 seL4와 Isabelle 형식증명 아카이브의 대형 개발 사례를 분석해, 증명 크기가 형식 명제 크기의 제곱에 비례한다는 관계를 찾아냈다. seL4 팀의 경험칙으로 증명 1만 줄이 대략 1인년이었으므로, 이 관계는 곧 노력의 제곱 스케일링을 뜻한다.
이 계수가 논의의 결론을 바꾼다. 생성 비용이 0으로 수렴한다고 가정해도, 사양 크기 s에 대해 검증 비용이 s²로 자라면 전체 비용은 사양 크기가 지배한다. 코드를 늘 다시 쓰는 것이 실용적인 영역은 사양을 작게 유지할 수 있는 영역으로 한정된다. 암호 라이브러리, 압축 코덱, 파서, 직렬화, 프로토콜 상태 기계처럼 인터페이스가 좁고 정의가 수학적인 계층이 여기 해당한다. 데이터베이스 엔진이나 업무 애플리케이션의 사양은 그런 형태가 아니다.
여기서 널리 쓰이는 비유 하나가 어긋난다. 사양을 고수준 언어에, 코드를 어셈블리에 대응시키는 비유다. 고수준 언어가 어셈블리를 밀어낸 것은 컴파일 비용이 프로그램 크기에 대략 선형이었기 때문이다. 컴파일이 소스 크기의 제곱으로 비쌌다면 그 대체는 일어나지 않았거나 아주 다른 모양이 됐을 것이다. 사양에서 검증된 코드로 가는 경로는 아직 그 선형성을 확보하지 못했다.
제곱은 지수이고, AI가 건드린 것은 계수다. 계수 변화의 폭이 최근 사례들에서 확인된다.
2026년 2월, 마리나 비아조프스카(Maryna Viazovska)의 필즈상 수상 업적인 8차원·24차원 구면 충전 최적성 증명이 Lean으로 형식 검증됐다. 이 프로젝트는 2024년 3월 로잔연방공과대학에서 시작됐고, 2026년 초 시점에 팀은 8차원 사례만 마무리하는 데 6개월이 더 필요하다고 추정하고 있었다. 스타트업 Math, Inc.의 자동형식화 모델 Gauss가 이를 5일에 닫았다. 이어 24차원 사례를 비아조프스카 논문과 자율 문헌 검색만으로 2주에 끝냈다. 형식화 전체는 7만 줄에서 20만 줄로 늘었다. 진행 중 Gauss는 논문 논증의 오류 두 건, 8차원 명제 7의 부호 오류를 포함해 자동으로 잡아 고쳤다.
이 프로젝트에서 가장 자주 인용되지 않는 대목이 정작 실무에 가깝다. 최고점에서 코드는 50만 줄까지 부풀었고, 정리 후 배포본이 20만 줄이다. 8차원 형식화만 보면 8만 줄을 6만 줄로 줄이는 작업이 증명을 생성하는 것보다 어려웠다고 기록됐다. 자동형식화의 다음 관문은 증명을 얻는 것이 아니라 재사용 가능한 코드를 얻는 것이라는 진단이 프로젝트 자체에서 나왔다.
다른 사례들도 같은 방향을 가리킨다. Lean 개발 조직의 킴 모리슨(Kim Morrison)은 범용 모델에 특별한 도구 없이 zlib 압축 라이브러리를 Lean으로 옮기게 했고, 압축한 뒤 해제하면 원본이 나온다는 왕복 정리를 기계 검증된 형태로 얻었다. 다만 그 정리에는 입력 크기가 1기가바이트 미만이라는 전제조건이 붙어 있는데, 이는 수학적 필요가 아니라 모델이 증명을 닫기 위해 스스로 고른 경계다. 소수 정리 형식화는 한 명의 수학자와 에이전트가 3주에 Lean 2만 5천 줄, 정리 1,000여 개로 완성했다. 이전 형식화는 수십 명이 1년 넘게 걸렸다.
싱가포르국립대 일리야 세르게이(Ilya Sergey) 연구실이 Lean 위에 만든 분산 프로토콜 검증기 Veil은 무작위화 합의 프로토콜 Rabia의 합의성과 유효성을 노드 수에 무관하게 증명하는 과정에서, 서로 다른 두 도구로 수행된 기존 형식 검증이 놓친 불일치를 발견했다. 형식 검증된 것에 대한 형식 검증이 결함을 찾아낸 사례다. 신뢰의 근거가 하나의 증명이 아니라 서로 다른 도구의 교차 확인에 있다는 점을 보여 준다.
공통 구조는 재귀적 분해와 신뢰 가능한 오라클, 그리고 반복을 유도하는 풍부한 피드백이다. 제안하고, 검사받고, 오류 메시지를 받고, 고치고, 더 작은 부분 문제로 쪼개고, 다시 반복한다. 대화형 정리 증명기가 이 구조를 이미 갖추고 있었기 때문에 모델이 여기서 특히 잘 작동한다는 설명이 유력하다. 증명 상태와 미해결 목표, 실패한 전술이 매 단계 구조화된 신호로 돌아오기 때문이다. 이 관점에서 보면 모델의 성적은 모델 능력의 함수라기보다 플랫폼이 주는 피드백 대역폭의 함수다.
이 주제의 공개 발언은 이해관계가 뚜렷하게 배치되어 있고, 그 배치가 강조점과 생략을 설명한다.
Lean과 Z3의 설계자인 레오나르도 지 모라(Leonardo de Moura)는 2026년 2월 글에서 검증 플랫폼이 갖춰야 할 요건을 나열했다. 감사 가능한 소형 신뢰 커널, 증명을 생성하는 인공지능과 분리된 검증 계층, 풍부한 전술 프레임워크, 대규모 형식화 지식 라이브러리, 그리고 특정 벤더가 통제하지 않는 오픈소스 거버넌스다. 그는 Amazon Web Services의 수석 응용과학자이면서 Lean을 관리하는 연구조직의 공동창립자다. 요건 목록이 Lean의 설계 결정과 항목별로 대응하는 것은 우연이 아니다.
이 위치 때문에 목록에서 빠진 것도 예측 가능하다. 사양 자체의 결함률, 사양 크기에 대한 검증 비용의 제곱 스케일링, 그리고 형식 사양을 쓸 수 있는 도메인의 크기가 그 글에서 정면으로 다뤄지지 않는다. 대신 "명백히 옳지만 비효율적인 프로그램이 그 자신의 사양 역할을 할 수 있다"는 우회로가 제시된다. 이 우회로는 압축 코덱이나 정렬 알고리즘에서 잘 작동하고, 무엇이 옳은지가 곧 논쟁 대상인 영역에서는 작동하지 않는다.
같은 방식으로 다른 발화 위치도 읽힌다. 구면 충전 형식화는 미국 국방고등연구계획국의 수학 자동화 프로그램 지원을 받았고, 성과 발표에서 "이런 형식화는 곧 흔한 일이 될 것"이라는 전망이 함께 나왔다. 자율 코딩 실험 기록은 자사 모델을 홍보할 유인이 있는 회사에서 나왔지만, 정작 그 문서에 가장 많이 적힌 것은 실패 목록이다. 컨설팅사가 사양 주도 개발을 채택 등급에 올리지 않는 것은 방법론 유행에 고객을 태웠다가 되돌리는 비용을 반복 경험한 조직의 보수성으로 이해하는 편이 정확하다.
측정 자체의 신뢰도도 비슷한 상태다. 2025년 7월 METR이 수행한 무작위 대조 시험은 성숙한 저장소에서 일하는 숙련 오픈소스 개발자 16명이 246개 실제 이슈를 처리할 때, AI 도구를 허용하면 완료 시간이 19퍼센트 늘어난다고 보고했다. 같은 개발자들은 사전에 24퍼센트 단축을 예상했고 실험 후에도 20퍼센트 단축됐다고 믿었다. 2026년 2월 이 기관은 후속 실험에서 속도 향상의 증거가 일부 관측되지만 선택 편향 때문에 중심 추정치를 신뢰하기 어렵다고 밝히고 설계를 바꿨다. AI 없이 일해야 할 가능성이 있으면 참여를 꺼리는 개발자가 많았고, AI를 특히 쓰고 싶은 과제는 제출되지 않았기 때문이다.
생성 측 이득의 크기는 아직 잘 측정되지 않는다. 그리고 잘 측정되지 않는 이유가 방법론적 난점이지 이득의 부재는 아니라는 점도 함께 기억할 필요가 있다.
지금까지의 재료를 하나로 묶으면 다음 모양이 나온다.
생성 비용은 실제로 무너졌다. 2주와 2만 달러로 10만 줄이 나오는 것은 3년 전 기준으로 성립하지 않던 일이다. 그러나 그 생성물의 품질은 판정자의 정밀도에 묶여 있고, 판정자를 테스트로 두면 테스트에 과적합한 물건이 나온다. 이 관찰은 형식 사양으로 옮겨 가자는 처방의 출발점으로 정확하다.
문제는 그 처방이 판정 비용을 없애는 것이 아니라 옮긴다는 점이다. 옮겨진 곳에서 세 가지 비용이 새로 발생한다. 사양을 쓰는 비용, 사양이 옳은지 확인하는 비용, 그리고 사양이 커질 때 제곱으로 자라는 증명 비용이다. 세 번째는 도구 개선으로 계수를 낮출 수 있지만 지수는 그대로다. 두 번째는 현재 체계적 대응이 없다. 약한 사양은 오히려 증명을 쉽게 통과시키므로, 검증의 성공이 사양 품질의 신호가 되지 못한다.
그렇다면 코드가 폐기물이 되는 세계는 언제 어디서 성립하는가. 조건은 두 개로 압축된다. 사양이 코드보다 실질적으로 작을 것, 그리고 사양이 옳은지를 사양보다 싼 방법으로 확인할 수 있을 것. 첫 조건은 인터페이스가 좁고 의미가 수학적인 계층에서 충족된다. 둘째 조건은 참조 구현이 있거나, 왕복 성질처럼 사양 자체가 자기 검사 가능한 형태를 가질 때 충족된다. 압축 라이브러리의 왕복 정리가 두 조건을 동시에 만족하는 전형이고, 그래서 그 사례가 먼저 나왔다.
반대로 사양이 코드만큼 크고 사양의 정당성이 곧 논쟁 대상인 영역, 즉 업무 규칙과 정책과 사용자 경험이 얽힌 애플리케이션 계층에서는 두 조건이 모두 무너진다. 사양이 의사코드 수준으로 상세해지면 프로그램을 두 번 쓴 것이 되고, 검증 비용의 제곱 항이 그 두 번째 작성분을 그대로 물려받는다.
아래 전망은 현재 확인된 상태에서만 근거를 끌어왔고, 각 항목에 반증 조건을 붙였다.
사람이 코드를 편집하지 않고 사양만 편집하는 운용 방식은 2028년까지 암호 원시함수, 압축, 파서·직렬화, 프로토콜 상태 기계 계층에서 상용 사례가 나온다. 이 계층은 사양이 이미 표준 문서로 존재하고 왕복·불변식 같은 자기 검사 성질을 갖추고 있다. 애플리케이션 계층에서는 같은 기간에 나오지 않는다.
반증 조건사양 규모 1만 줄 이상의 업무 애플리케이션에서, 사람이 생성된 코드를 한 줄도 편집하지 않은 채 사양 갱신과 재생성만으로 2개 분기 이상 운영된 상용 시스템 사례가 공개되면 이 전망은 틀린다.
검증된 코드 생성 벤치마크의 성공률은 계속 오르되, 과제 규모를 100줄대에서 1,000줄대로 올리면 언어별 성공률이 절반 이하로 떨어진다. 현재 데이터에서 해답 길이가 성공률의 가장 뚜렷한 예측 변수였고, 증명 크기가 명제 크기의 제곱으로 자란다는 관계가 이 하락을 설명한다.
반증 조건과제 규모를 한 자릿수 배 키운 벤치마크에서 성공률 하락이 20퍼센트포인트 이내에 그치면 이 전망은 틀린다. 사양 강도를 통제해 약한 사양 통과분을 제외한 뒤에도 그렇다면 더욱 그렇다.
사양 결함이 독립된 결함 범주로 분류·집계되기 시작한다. 사양 린터, 사양 변이 검사, 사양 강도 측정 같은 도구가 2027년까지 등장한다. 검증 성공이 사양 품질을 보증하지 않는다는 것이 실증으로 확인된 이상, 이 공백을 메우는 도구 시장이 생기지 않을 이유가 없다.
반증 조건2028년까지 사양 결함이 사고 원인 분류에 별도 항목으로 잡히지 않고, 사양 품질을 정량화하는 도구가 연구 프로토타입 밖으로 나오지 않으면 이 전망은 틀린다.
증명 노동의 단가는 내려가되 총량은 늘어난다. 단가 하락이 그동안 검증을 포기했던 영역을 경제권 안으로 끌어들이기 때문이다. 검증 엔지니어의 일은 증명을 쓰는 일에서 사양을 설계하고 증명 아키텍처를 정하고 자동 생성된 증명을 재사용 가능한 형태로 정리하는 일로 이동한다. 구면 충전 형식화에서 정리 작업이 생성보다 어려웠다는 기록이 이 이동의 방향을 미리 보여 준다.
반증 조건2028년까지 형식 검증 관련 채용 공고와 인건비 총액이 절대적으로 감소하면 이 전망은 틀린다.
신뢰의 근거는 단일 증명이 아니라 서로 다른 도구의 교차 확인으로 옮겨 간다. 형식 검증된 결과에서 다른 도구가 불일치를 찾아낸 사례가 이미 나왔고, 모델 합집합 성적이 단일 모델보다 15퍼센트포인트 높다는 사실이 같은 방향을 가리킨다. 검증 파이프라인은 정리 증명기 하나가 아니라 모델 검사기·정적 분석기·퍼저가 피드백을 주고받는 구성으로 재편된다.
반증 조건단일 증명 시스템의 성능이 충분히 올라 교차 확인이 비용만 늘리는 잉여 절차로 취급되고, 주요 검증 프로젝트가 단일 도구 체제로 수렴하면 이 전망은 틀린다.
기술적 결론과 별개로, 사양이 원본이 되는 체제는 소유의 문제를 미해결로 남긴다. 코드에서는 버전 관리 시스템이 저장 기능 이상을 수행해 왔다. 커밋과 기여 이력과 라이선스가 누구의 작업인지에 대한 실무적 답을 제공했다. 사양은 여러 사람이 함께 쓰고 계속 고치는 문서이므로, 어떤 제약 조건을 누가 넣었고 그것이 얼마짜리인지를 묻는 물음에 대응할 장치가 아직 없다.
더 근본적으로, 사양은 무엇이 옳은지를 정하는 문서다. 의료 기기나 투표 시스템이나 안전 감시 장치의 사양은 논리만이 아니라 가치를 담는다. 사양을 형식화하고 공개하는 것이 그 가치 판단을 해결해 주지는 않는다. 다만 코드 안에 묻혀 있을 때보다는 명시적이고 감사 가능한 형태로 만들어 준다. 그 점이 이 전환의 부수 효과 가운데 가장 오래 남을 것일 수 있다.
본문의 수치는 2026년 8월 기준 공개된 실험 결과와 사업 발표에서 가져왔다. 벤치마크 성공률은 시도 횟수·모델 구성·과제 집합에 따라 달라지므로, 다른 조건에서 측정된 값과 직접 비교하기 어렵다.