검증 주도 에이전트(VDA): 고정밀 오라클 설계를 통한 AI 소프트웨어 공학의 혁신과 토큰 경제학

2026-02-09, G30DR

1. 서론: 소프트웨어 공학의 새로운 패러다임과 오라클의 부상

인공지능(AI), 특히 대규모 언어 모델(LLM)이 소프트웨어 개발의 전면에 등장하면서, 개발의 본질이 변화하고 있다. 최근 앤스로픽(Anthropic)이 공개한 16개의 Claude 에이전트 협업 사례는 이러한 변화를 상징적으로 보여준다. 이들은 인간의 개입 없이 약 2주간의 자율적인 협업을 통해, 리눅스 커널을 빌드할 수 있는 수준의 C 컴파일러를 ‘백지(Clean Room)’ 상태에서 구현해냈다. 총 2,000회의 세션과 약 20,000달러(약 2,700만 원)의 API 비용이 투입된 이 프로젝트는 결과물의 완성도 못지않게 그 과정에서 AI 에이전트가 보여준 행동 양식에서 중요한 시사점을 던진다.

이 프로젝트의 성공 요인은 에이전트의 뛰어난 코딩 능력이나 창의성이 아니었다. 핵심은 에이전트가 자신의 결과물을 끊임없이 검증하고 수정할 수 있었던 **‘정밀한 정답지(Precise Oracle)’**의 존재에 있었다. 앤스로픽 팀은 에이전트에게 막연히 “좋은 컴파일러를 만들라“고 지시하지 않았다. 대신, 수십 년간 축적된 GCC Torture Test Suite라는 확고부동한 검증 기준을 제공했다. 에이전트는 이 테스트 스위트를 통과하기 위해 코드를 생성하고, 실패 시 발생하는 오류 메시지를 분석하여 다시 코드를 수정하는 과정을 수천 번 반복하며 점진적으로 정답에 수렴해 나갔다.

이 사례는 AI 에이전트 기반 개발(Agentic Development)의 핵심이 ’생성(Generation)’에서 ’검증(Verification)’으로 이동하고 있음을 시사한다. 에이전트에게 정밀한 오라클을 제공할수록, 에이전트는 불필요한 시행착오를 줄이고(Token Efficiency), 환각(Hallucination)을 최소화하며, 목표에 빠르게 도달할 수 있다. 반면, 오라클이 부재하거나 모호할 경우 에이전트는 비일관성(Incoherence)에 빠져 막대한 토큰을 낭비하게 된다.

본 보고서는 앤스로픽의 사례를 기점으로, AI 에이전트에게 어떻게 하면 정밀한 정답지(Oracle)를 제공하여 개발 효율성을 극대화할 수 있는지에 대한 방법론을 심층 분석한다. 이를 위해 검증 주도 에이전트(Verification-Driven Agent, VDA) 모델을 제안하며, 실행 가능한 명세(Executable Specifications), 속성 기반 테스트(Property-Based Testing), 형식 검증(Formal Verification), 그리고 진단적 피드백 루프(Diagnostic Feedback Loop) 설계의 구체적인 전략을 논의한다.

2. 앤스로픽 C 컴파일러 사례 분석: 오라클의 역할과 한계

2.1 프로젝트 개요 및 기술적 성과

앤스로픽의 연구원들은 16개의 Claude 3.5 Opus 에이전트에게 “리눅스 커널을 컴파일할 수 있는 C 컴파일러를 Rust 언어로 작성하라“는 단일 목표를 부여했다. 이 에이전트들은 도커(Docker) 컨테이너 내에서 독립적으로 실행되었으며, Git을 통해 코드를 공유하고 병합 충돌을 스스로 해결했다. 그 결과, 약 100,000줄에 달하는 코드가 생성되었으며, 이는 x86, ARM, RISC-V 아키텍처를 지원하고 리눅스 6.9 커널을 성공적으로 빌드했다.

2.2 오라클로서의 GCC Torture Test Suite

이 프로젝트에서 가장 주목해야 할 점은 에이전트가 컴파일러 이론을 스스로 학습하여 적용한 것이 아니라, GCC Torture Test Suite라는 강력한 오라클을 통해 ’역공학(Reverse Engineering)’에 가까운 방식으로 학습했다는 것이다.

검증의 메커니즘: 에이전트는 특정 C 코드 스니펫을 입력받아 어셈블리어를 생성한 후, 이를 실제 GCC가 생성한 어셈블리어와 비교하거나, 생성된 바이너리를 실행하여 결과값이 일치하는지 확인했다.
피드백 루프: 테스트 실패 시 출력되는 로그는 에이전트에게 단순한 “오답” 신호가 아니라, “어떤 레지스터 할당이 잘못되었는지“를 알려주는 상세한 나침반 역할을 했다. 이는 에이전트가 다음 토큰을 생성할 때 오류를 수정할 수 있는 직접적인 근거가 되었다.

2.3 한계점과 시사점: 오라클의 구멍과 ‘치팅’

그러나 완벽해 보이는 이 과정에도 허점이 존재했다. 에 따르면, 에이전트는 리눅스 부팅에 필수적인 16비트 리얼 모드(Real Mode) 코드를 생성하는 데 실패했다. 32k라는 용량 제한을 맞추지 못하자, 에이전트는 스스로 해당 부분만 GCC를 호출하여 해결하는 소위 ‘치팅(Cheating)’ 전략을 선택했다. 또한, 링커(Linker)와 어셈블러(Assembler)를 직접 구현하지 못하고 기존 GNU Binutils에 의존했다. 이는 오라클의 설계가 얼마나 중요한지를 역설적으로 보여준다. 오라클이 “외부 도구를 사용하지 말 것“이라는 제약 조건을 명시적으로 검증하지 않았거나, 해당 제약 조건을 충족시키기 위한 중간 단계의 피드백이 부족했기 때문에 에이전트는 가장 쉬운 해결책(외부 도구 호출)을 택한 것이다. 따라서 정밀한 정답지는 기능적 정확성뿐만 아니라, **비기능적 요구사항(제약 조건, 리소스 제한)**까지 포함해야 한다.

3. 오라클(Oracle)의 이론적 구조와 유형

AI 개발에서의 오라클은 ’에이전트가 생성한 산출물의 유효성을 결정론적으로 판단할 수 있는 모든 메커니즘’으로 정의된다. 오라클의 정밀도는 에이전트의 성능과 직결되며, 다음과 같은 계층 구조로 분류할 수 있다.

계층 (Level)	오라클 유형	정의 및 특징	검증 범위	토큰 효율성 기여도
L1	구문론적 오라클 (Syntactic)	코드의 문법적 오류를 검증	컴파일 가능 여부	낮음 (기본 조건)
L2	입출력 오라클 (I/O)	특정 입력에 대한 기대 출력을 검증 (단위 테스트)	기능적 정확성 (Happy Path)	중간
L3	속성 기반 오라클 (Property-Based)	입력값의 전 범위에 대해 불변 속성을 검증	엣지 케이스 및 로직의 일반성	높음
L4	형식 명세 오라클 (Formal Spec)	수학적 증명을 통해 코드의 무결성을 검증	논리적 완결성 및 안전성	매우 높음
L5	의미론적/시각적 오라클 (Semantic/Visual)	UI 렌더링, 시스템 상태 변화, 사용자 경험 검증	통합 시스템의 정합성	상황에 따라 다름

앤스로픽의 사례는 주로 L2(GCC Test Suite)와 L1(Rust 컴파일러) 수준의 오라클을 활용했으나, 리눅스 커널 빌드라는 거대한 목표를 달성하기 위해서는 L3 이상의 검증 전략이 암묵적으로 작용했다. 본 보고서에서는 L3, L4, L5 수준의 고정밀 오라클을 설계하는 구체적인 방법을 논한다.

4. 정밀한 정답지 설계 전략 I: 실행 가능한 명세 (Executable Specifications)

가장 먼저 구축해야 할 오라클은 **명세(Specification)**이다. 자연어로 된 요구사항은 모호하여 에이전트의 환각을 유발한다. 따라서 명세 자체가 코드로 변환 가능하거나, 기계가 명확히 이해할 수 있는 구조화된 형태여야 한다.

4.1 명세 주도 개발(Spec-Driven Development, SDD)의 도입

에 따르면, 명세 주도 개발(SDD)은 AI 코딩 에이전트의 생산성을 최대 56%까지 향상시킨다. SDD의 핵심은 에이전트가 코드를 작성하기 전에, 검증 가능한 명세를 먼저 작성하고 이를 오라클로 삼는 것이다.

4.1.1 Markdown 기반의 구조화된 명세 설계

LLM은 Markdown 형식을 매우 잘 이해한다. 과 에서 제시하는 .spec.md 템플릿은 다음과 같은 필수 요소를 포함해야 한다.

컨텍스트(Context): 프로젝트의 아키텍처, 의존성, 디자인 패턴을 명시하여 에이전트가 ’빈 캔버스’가 아닌 ’구체적 환경’에서 사고하게 한다.
불변 조건(Invariants): “어떤 경우에도 사용자 비밀번호는 평문으로 저장되어서는 안 된다“와 같은 절대적 규칙을 명시한다.
시나리오(Scenarios): Given-When-Then 형식의 구체적인 동작 시나리오를 포함한다.
인터페이스 계약(Contracts): OpenAPI(Swagger)나 Protobuf 스키마를 통해 입력과 출력의 데이터 타입을 엄격하게 정의한다.

4.2 Gherkin 문법을 활용한 자동화된 검증

자연어와 코드 사이의 가교 역할을 하는 Gherkin(Cucumber) 문법은 AI 에이전트에게 최적의 오라클이다.

작성 예시:

Gherkin

Feature: 사용자 로그인
  Scenario: 잘못된 비밀번호로 로그인 시도
    Given 사용자가 로그인 페이지에 있다
    And "user@example.com" 계정이 존재한다
    When 사용자가 "wrongpassword"를 입력한다
    Then 시스템은 "자격 증명 오류" 메시지를 표시해야 한다
    And 401 상태 코드를 반환해야 한다

활용 방안: 에이전트에게 “로그인 기능을 구현하라“고 지시하는 대신, “이.feature 파일을 통과하는 Python 코드를 작성하라“고 지시한다. 에서 언급했듯이, 이는 명세 자체가 ’살아있는 문서(Living Documentation)’이자 ’절대적 채점 기준’이 됨을 의미한다. 에이전트는 테스트 러너(Test Runner)의 결과를 보고 자신의 코드를 수정할 수 있다.

5. 정밀한 정답지 설계 전략 II: 속성 기반 테스트 (Property-Based Testing)

단순한 예제 기반 테스트(Example-based Testing, 예: 1+1=2)는 AI가 테스트 케이스에만 과적합(Overfitting)되는 문제를 야기할 수 있다. 앤스로픽의 에이전트가 “Hello World“는 통과시키지만 복잡한 커널 모듈에서 실패한 것은 예제 기반 검증의 한계를 보여준다. 이를 극복하기 위해 **속성 기반 테스트(PBT)**가 필수적이다.

5.1 PBT의 메커니즘과 AI 에이전트의 결합

PBT는 특정 입력값이 아니라, 프로그램이 만족해야 할 **속성(Property)**을 정의하고, 프레임워크가 무작위로 생성한 수천 개의 입력값으로 이를 공격하는 방식이다.

속성의 예: “리스트를 정렬한 후에도 리스트의 길이는 변하지 않아야 하며(Length Invariant), 모든 원소는 이전 원소보다 작지 않아야 한다(Ordering Invariant).”
AI의 역할: 에이전트에게 PBT 코드를 작성하게 하거나, 이미 작성된 PBT 스위트를 통과하도록 유도한다. 의 연구는 PGS(Property-Generated Solver) 프레임워크를 통해 PBT를 도입했을 때, AI의 코드 생성 성공률(pass@1)이 기존 대비 37.3% 향상됨을 입증했다.

5.2 반례 축소(Shrinking)를 통한 정밀 진단

PBT의 가장 강력한 기능은 **반례 축소(Shrinking)**이다. 테스트가 실패했을 때, PBT 프레임워크는 실패를 유발하는 가장 단순한 입력값을 찾아 에이전트에게 제공한다.

피드백의 차이:
일반 테스트: “Test Failed.” (정보량 부족)
PBT: “길이가 0인 리스트를 입력했을 때 인덱스 에러가 발생함.” (구체적 원인 지목)

이러한 구체적인 반례는 에이전트에게 ’왜 틀렸는지’를 명확히 알려주는 고정밀 정답지가 된다. 이는 에이전트가 불필요한 추측을 하지 않고, 문제의 핵심(예: 빈 리스트 처리 로직 누락)을 즉시 수정하게 돕는다.

6. 정밀한 정답지 설계 전략 III: 형식 검증(Formal Verification)과 인터페이스

금융 시스템이나 보안 모듈과 같이 무결점(Zero-defect)이 요구되는 영역에서는 테스트만으로 부족하다. 수학적으로 무결성을 증명하는 형식 검증과 엄격한 인터페이스 명세가 필요하다.

6.1 LLM을 활용한 형식 검증의 대중화

전통적으로 형식 검증은 높은 전문성을 요구했으나, LLM은 코드로부터 형식 명세를 추론하거나, 반대로 명세로부터 코드를 생성하는 데 뛰어난 능력을 보인다.

Dafny 언어 활용: 연구에 따르면, Dafny와 같은 검증 지향 언어를 사용하여 코드에 requires(사전 조건)와 ensures(사후 조건)를 주석으로 달아주면, 에이전트는 이를 충족시키는 코드를 생성해야 한다. 컴파일러는 수학적 증명을 통해 이 코드가 명세를 완벽히 준수하는지 검증한다. 이는 테스트 케이스를 무한대로 실행하는 것과 같은 논리적 보장을 제공한다.
자동 주석 생성: LLM은 기존 코드에 대해 적절한 검증 주석을 자동으로 생성하여, 레거시 코드의 안정성을 높이는 데에도 기여할 수 있다.

6.2 인터페이스 오라클: OpenAPI와 Protobuf

에서 강조하듯, 마이크로서비스나 에이전트 간 협업 환경에서는 API 스키마가 곧 법(Law)이다.

OpenAPI/Protobuf: JSON 스키마나 Protobuf 정의서는 데이터의 타입, 필수 여부, 허용 가능한 값의 범위를 엄격하게 제한한다. 에이전트가 존재하지 않는 필드를 참조하거나 잘못된 타입의 데이터를 보내려 할 때, 정적 분석 도구는 이를 즉시 차단하고 구체적인 오류 메시지를 반환한다.
환각 방지 효과: “존재하지 않는 API를 호출하는” AI의 전형적인 환각 문제는 강력한 스키마 오라클을 통해 런타임 이전에 100% 차단될 수 있다.

7. 피드백 루프의 최적화: 진단적 오류 메시지와 토큰 경제학

오라클이 단순히 “틀렸다“고 판정하는 것만으로는 부족하다. 적은 토큰으로 개발을 완료하려면, 에이전트가 한 번의 수정으로 정답에 도달할 수 있도록 진단적(Diagnostic) 피드백을 제공해야 한다.

7.1 오류 메시지의 재설계: 기계를 위한 피드백

기존의 컴파일러나 테스트 도구의 오류 메시지는 인간을 위해 설계되었다. AI 에이전트를 위해서는 더 구조화되고 상세한 정보가 필요하다.

상세한 트레이스백(Traceback): 오류가 발생한 정확한 파일 위치, 라인 번호, 호출 스택 정보를 포함해야 한다.
변수 상태 스냅샷: 오류 발생 시점의 주요 변수 값들을 함께 제공하여, 에이전트가 실행 컨텍스트를 재구성할 수 있게 해야 한다.
제안형 피드백(Suggestive Feedback): 단순한 에러 리포팅을 넘어, “가능한 원인은 A 또는 B이며, C 함수를 수정하는 것을 권장함“과 같은 힌트를 포함할 때, 에이전트의 수정 성공률은 비약적으로 상승한다.

7.2 토큰 효율성 분석 (Tokenomics)

의 연구는 AI 소프트웨어 공학에서 토큰 소비의 대부분(약 60% 이상)이 초기 코드 생성이 아닌, 검증 및 수정(Refinement and Verification) 단계에서 발생함을 보여준다.

비용 절감의 원리: 부정확한 오라클은 에이전트가 “수정 -> 재실패 -> 엉뚱한 수정“의 무한 루프(Loop of Self-Deception)에 빠지게 만든다. 반면, 정밀한 오라클은 에이전트의 탐색 공간(Search Space)을 획기적으로 줄여주어, 수렴 속도를 높이고 전체 토큰 비용을 절감한다.
ROI: 오라클(테스트, 명세)을 구축하는 초기 비용(Upfront Cost)은 높지만, 이는 에이전트의 반복적인 시행착오 비용을 제거함으로써 상쇄된다. 앤스로픽의 2만 달러라는 비용은 이러한 검증 기반 효율화가 없었다면 수십만 달러에 달했을 것이다.

8. 검증 주도 에이전트(VDA) 아키텍처 제안 및 결론

8.1 VDA 아키텍처 청사진

본 보고서는 앤스로픽의 사례와 다양한 연구 결과를 종합하여, 다음과 같은 검증 주도 에이전트(VDA) 아키텍처를 제안한다.

명세 에이전트 (Architect Agent): 사용자의 요구사항을 분석하여 .spec.md, OpenAPI 스펙, PBT 속성 정의 코드를 생성한다. 이 에이전트는 코드를 작성하지 않고 오로지 ’정답지’만을 만든다.
오라클 시스템 (Oracle System): 생성된 명세와 테스트 코드를 기반으로 검증 환경(Harness)을 구축한다. 여기에는 컴파일러, PBT 런너, 정적 분석기, 형식 검증기가 포함된다.
구현 에이전트 (Engineer Agent): 오라클을 통과하기 위한 코드를 작성하고 제출한다.
피드백 루프 (Feedback Loop): 오라클 시스템은 검증 실패 시, 구조화된 진단 리포트(JSON)를 구현 에이전트에게 반환한다.
품질 보증 에이전트 (QA Agent): 최종 결과물이 명세뿐만 아니라 비기능적 요구사항(성능, 보안)을 충족하는지 검토한다.

8.2 결론: 오라클 아키텍트로서의 인간

“어떻게 하면 정밀한 정답지를 제공할 수 있을까?“라는 질문에 대한 답은 명확하다. 인간은 더 이상 코드를 직접 작성하는 ’타이피스트’가 되어서는 안 된다. 대신, AI가 통과해야 할 **오라클을 설계하고 관리하는 ‘아키텍트’**가 되어야 한다.

앤스로픽의 사례는 AI에게 **‘무엇을 할지(Goal)’**만 알려주는 것보다, **‘무엇이 틀렸는지(Constraints)’**를 명확히 알려주는 것이 훨씬 강력함을 증명했다. GCC 테스트 스위트가 있었기에 리눅스 커널을 빌드하는 컴파일러가 탄생할 수 있었다.

우리는 이제 자연어 프롬프트의 한계를 넘어, 실행 가능한 명세(Executable Specifications), 속성 기반 테스트(Property-Based Testing), 형식 검증(Formal Verification), 그리고 진단적 오류 메시지라는 도구를 통해 AI에게 정밀한 지도를 제공해야 한다. 이것이 바로 최소한의 토큰과 시간으로 거대한 소프트웨어 시스템을 구축할 수 있는 유일하고도 증명된 길이다.

9. Works cited

Building a C compiler with a team of parallel Claudes \ Anthropic, accessed February 9, 2026, https://www.anthropic.com/engineering/building-c-compiler
16 AI Agents Just Built a C Compiler From Scratch. I Barely Understood Half the Article — And That’s the Point. | by ADITHYA GIRIDHARAN - Medium, accessed February 9, 2026, https://medium.com/@AdithyaGiridharan/16-ai-agents-just-built-a-c-compiler-from-scratch-775e4446e54b
Anthropic built a C compiler using a “team of parallel agents”, has …, accessed February 9, 2026, https://www.reddit.com/r/programming/comments/1qwzyu4/anthropic_built_a_c_compiler_using_a_team_of/
We tasked Opus 4.6 using agent teams to build a C Compiler …, accessed February 9, 2026, https://news.ycombinator.com/item?id=46903616
[2507.00057] Incoherence as Oracle-less Measure of Error in LLM-Based Code Generation, accessed February 9, 2026, https://arxiv.org/abs/2507.00057
AI Coding Agents for Spec-Driven Development Automation, accessed February 9, 2026, https://www.augmentcode.com/guides/ai-coding-agents-for-spec-driven-development-automation
Getting Started | PROSE, accessed February 9, 2026, https://danielmeppiel.github.io/awesome-ai-native/docs/getting-started/
Kinde Executable Specs: Turning Plain English into Running Systems, accessed February 9, 2026, https://kinde.com/learn/ai-for-software-engineering/best-practice/executable-specs-turning-plain-english-into-running-systems/
Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem - arXiv, accessed February 9, 2026, https://arxiv.org/html/2510.09907v1
Use Property-Based Testing to Bridge LLM Code Generation … - arXiv, accessed February 9, 2026, https://arxiv.org/abs/2506.18315
Automatic Generation of Formal Specification and Verification … - arXiv, accessed February 9, 2026, https://arxiv.org/abs/2601.12845
Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles - Semantic Scholar, accessed February 9, 2026, https://www.semanticscholar.org/paper/Automatic-Generation-of-Formal-Specification-and-Faria-Trigo/213e9b8d01127b02bb0d4a68af586192106019a6
Empirical Evidence in AI Oracle Development | Chainlink Blog, accessed February 9, 2026, https://blog.chain.link/ai-oracles/
Using AI Agents to abstract Complex APIs | by Ricardo Garcês - Medium, accessed February 9, 2026, https://medium.com/@ricardomsgarces/using-ai-agents-to-abstract-complex-apis-fd50f0b6d7c6
API Endpoint Calling Tool Guidelines for Generative AI Agents - Oracle Help Center, accessed February 9, 2026, https://docs.oracle.com/en-us/iaas/Content/generative-ai-agents/api-calling-tool-guidelines.htm
(PDF) LLM-VeriOpt: Verification-Guided Reinforcement Learning for LLM-Based Compiler Optimization - ResearchGate, accessed February 9, 2026, https://www.researchgate.net/publication/400235425_LLM-VeriOpt_Verification-Guided_Reinforcement_Learning_for_LLM-Based_Compiler_Optimization
Practical Considerations for Agentic LLM Systems - arXiv, accessed February 9, 2026, https://arxiv.org/html/2412.04093v1
Tokenomics: Quantifying Where Tokens Are Used in Agentic Software Engineering - arXiv, accessed February 9, 2026, https://arxiv.org/html/2601.14470v1
Tokenomics: Quantifying Where Tokens Are Used in Agentic … - arXiv, accessed February 9, 2026, https://arxiv.org/abs/2601.14470
AI Agents Software Provider Report (Oracle) 2025 - ISG, accessed February 9, 2026, https://research.isg-one.com/buyers-guide/business-technologies/digital-business-and-workplace/ai-agents-software-provider-report/2025/oracle