AI 주도 개발을 뒷받침하는 부품으로서의 계약 (Contract)

이 기사에서 말하고자 하는 것은, 결국 이 한 마디로 요약된다.

TL;DR

• 계약 프로그래밍 (Design by Contract)은 50년 전의 오래된 기법을 재게시하는 것이 아니다.
  AI 코드 생성 시대에 「의도의 격차 (Intent Gap)」를 메우는 부품으로서 재해석할 수 있다 - 계약 프로그래밍은 「테스트」와 「형식 검증 (Formal Verification)」의 중간에 위치하며, 비용과 보증 사이의 균형을 맞춘 선택지이다.
• GitHub Spec Kit, AWS Kiro 등 2026년의 SDD 도구들은
  스펙 자체를 「계약」이라고 부르고 있다. 이론과 실무가 이미 합류하고 있다.
• 계약은 함수 내의 assert가 아니라,
  인간 ↔ AI 에이전트 ↔ 검증 도구 사이의 책임 분계 프로토콜로서 재정의하면, 부품으로서 통합하기 쉬워진다.

서론: 왜 지금, 계약 프로그래밍인가

AI 주도 개발의 부품 중 하나로서의 계약 (Contract). 이 기사에서 말하고자 하는 것은, 결국 이 한 마디로 요약된다.

「AI에게 구현하게 했더니, 동작은 하지만, 우리의 의도와는 미묘하게 다른 것이 돌아왔다」.

AI 주도 개발을 하고 있다면 한 번쯤 부딪히는 상황이라고 생각한다. 코드는 작성되어 있다. 테스트도 통과했다. 하지만 우리가 정말로 원했던 것과는 어딘가 어긋나 있다.

이 어긋남의 정체를 언어화하는 개념으로서, 최근 다시 주목받고 있는 것이 **계약 프로그래밍 (Design by Contract)**이다. 1986년 Bertrand Meyer가 Eiffel 언어로 제창한, 결코 새롭지 않은 기법이다. 하지만 AI가 코드를 대량으로 생성하는 시대가 되면서, 이 고전적인 사고방식이 다른 의미를 갖기 시작했다.

본고에서는 계약 프로그래밍의 이론을 간단히 복습한 후, 왜 지금 이 기법이 AI 주도 개발의 문맥에서 재평가되고 있는지 정리하고, 마지막으로 「부품」으로서 실무에 통합하는 구체적인 패턴을 제시한다.

1. 계약 프로그래밍이란 무엇인가 (복습)

계약 프로그래밍의 발상은 법률상의 계약과 같다. 계약에는 당사자 쌍방의 의무와 권리가 명시된다. 소프트웨어의 계약도 마찬가지로, 호출하는 측 (클라이언트, Client)과 호출되는 측 (서플라이어, Supplier) 사이에서 다음의 3가지를 명시한다.

이론적인 뿌리는 더욱 오래되어, Hoare 논리 (사전 조건 P와 사후 조건 Q로 {P} S {Q}라고 나타내는 검증 수법)나 Floyd의 연구까지 거슬러 올라간다. 일반적인 유효성 검사 (Validation)와 다른 점은, 「호출하는 측의 책임」과 「호출되는 측의 책임」을 명확하게 구분한다는 점이다. 사전 조건이 충족되어 있다면, 서플라이어 측은 방어적인 체크를 중복해서 작성할 필요가 없다는 설계 사상이 배경에 깔려 있다.

언어별 지원 상황도 대략 파악해 두자.

• Eiffel: 언어 네이티브로 DbC를 지원 (발상 언어)
• Python: 언어 네이티브 기능은 없지만, 서드파티 라이브러리를 사용함으로써 계약을 실현할 수 있음
• Rust: 타입 시스템을 통해 사전 조건의 일부를 정적으로 보증할 수 있음
• 검증 대응 언어 (verification-aware languages): Dafny, F*, Verus. 계약을 증명 가능한 형식 명세 (Formal Specification) 수준까지 승화시켜, 컴파일 시점에 수학적인 정확성의 증명을 요구함

여기까지는 전제 지식이다. 본론은 이 기법이 왜 지금 AI의 문맥에서 재부상하고 있는가에 있다.

2. Intent Gap: AI가 증폭시키는 「의도와 구현의 어긋남」

Microsoft Research의 Shuvendu Lahiri가 2026년에 발표한 논문 『Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents』가 이 문제를 명쾌하게 정식화하고 있다.

논문의 주장은 심플하다. 자연어로 된 모호한 요구와 프로그램의 정확한 동작 사이의 괴리, 이른바 intent gap은 예전부터 소프트웨어 공학을 괴롭혀온 문제였지만, AI 생성 코드는 이를 전례 없는 규모로 증폭시킨다는 지적이다. 서두의 에피소드와 같은 「동작은 하지만 미묘하게 어긋나 있는」 느낌은 이러한 구조적인 갭의 발현이라고 할 수 있다.

이 논문이 제시하는 「의도 형식화의 트레이드오프 스펙트럼 (trade-off spectrum)」이 계약 프로그래밍을 위치시키는 데 있어 매우 유용한 축이 된다.

중요한 점은 이러한 단계들이 대안적인 관계가 아니라 상호 보완적인 관계에 있다는 것이다. 테스트가 사후 조건(postcondition)을 검증하고, 사후 조건이 불변 조건(invariant)의 발견을 유도하며, 불변 조건이 본격적인 증명을 뒷받침하는 연쇄 구조를 이룬다. 계약(Contract)은 이 스펙트럼의 정확히 중간, 즉 "테스트만큼 느슨하지는 않지만, 형식 검증(formal verification)만큼 무겁지도 않은" 실무적으로 딱 적당한 위치를 차지한다.

또한 이 논문은 「오토 포멀라이제이션 (Auto-formalization, 자연어의 완전한 사양을 형식 논리에 변환하는 것)」과 「의도 형식화 (intent formalization)」를 명확히 구분하고 있다. 의도 형식화는 원문에 대한 완전한 충실성을 목표로 하는 것이 아니라, 모호함이 발생할 수 있는 부분에만 비용을 집중하여 형식화하는 현실적인 접근 방식이다. 이는 후술할 "어디까지 계약을 작성할 것인가"라는 실무적 판단과 직결된다.

3. 사양 주도 개발(SDD)이라는 실무 트렌드와의 합류

이론적인 이야기만이 아니다. 2025년 하반기부터 2026년에 걸쳐 GitHub Spec Kit, AWS Kiro, Claude Code Skills, Cursor, OpenSpec, BMAD-METHOD, Tessl과 같은 주요 AI 코딩 도구들이 앞다투어 "사양(spec)을 중심으로 하는 개발"을 구현했다.

GitHub 자체의 설명이 상징적이다. 그들은 사양을 코드가 어떻게 동작해야 하는지에 대한 계약이자, AI 에이전트가 코드를 생성, 테스트, 검증할 때 사용하는 신뢰할 수 있는 정보원으로 정의하고 있다.

여기서 흥미로운 점은, SDD가 "문서를 먼저 작성한다"는 고전적인 발상의 재탕이 아니라, "vibe coding"(Karpathy가 명명한, AI에게 모든 것을 맡기고 코드의 내부를 의식하지 않는 개발 스타일)에 대한 직접적인 반작용으로 등장했다는 점이다. SDD 도구들이 다수 채택하는 표기법(EARS: Easy Approach to Requirements Syntax)은 "시스템은 ~해야 한다"라는 단일하고 테스트 가능한 주장으로 요구사항을 압축한다. 이는 계약의 사전 조건(precondition) 및 사후 조건과 실질적으로 맥을 같이 한다.

구체적인 워크플로우의 이미지는 다음과 같다. 인간이 자연어로 모호하게 요구사항을 전달한다 $\rightarrow$ 에이전트가 이를 받아 기능 단위로 spec.md를 생성한다 $\rightarrow$ 인간이 리뷰하고 승인한다 $\rightarrow$ 구현에 들어간다. 여기서 인간의 역할은 구현의 세부 사항을 리뷰하는 것이 아니라, spec.md라는 계약서의 타당성을 승인하는 것으로 좁혀진다. 사양 자체가 비즈니스적으로 올바른지를 판단할 수 있는 최종적인 오라클(Oracle, 판정자)은, 아무리 기계적인 검증을 거듭하더라도 인간 이외에는 존재하지 않는다는 점이 Lahiri의 논문과도 일치하는 지적이다.

다만, SDD에는 실무적인 한계도 존재한다. 사양이 커질수록 AI가 전체를 올바르게 파악하며 동작한다는 보장이 없어진다. 이를 피하기 위해서는 spec.md를 산문(prose) 형태로 작성하는 것이 아니라, 계약의 3요소(사전 조건, 사후 조건, 불변 조건)에 해당하는 구조를 명시적인 포맷으로 갖추는 것이 유효하다고 판단된다.

## 기능: 주문 취소
### 사전 조건
- 주문 상태가 `shipped` 이전일 것
...

이렇게 해두면 인간의 리뷰는 "비즈니스 규칙으로서 올바른가"에만 집중할 수 있으며, 구현으로의 번역과 테스트 생성은 이 구조화된 spec.md로부터 기계적으로 도출할 수 있다.

반도체 RTL 설계 분야의 연구이지만, 시사적인 사례로 VERI-SURE라는 멀티 에이전트 프레임워크가 있다. 여러 AI 에이전트의 의도를 일치시키기 위한 "설계 계약"을 먼저 확립하고, 그 계약을 축으로 구현 에이전트와 검증 에이전트의 역할을 분리하는 구성을 취하고 있다. 계약을 "에이전트 간의 인터페이스 사양"으로 사용한다는 발상은 다음 장의 부품화 패턴으로 그대로 이어진다.

4. 계약을 "부품"으로 다루는 6가지 패턴

여기가 본론이다. 계약 프로그래밍을 단일한 기법이 아니라, AI 주도 개발 파이프라인 내의 교체 가능한 부품으로 재정의한다.

패턴 1: Contract as Interface Boundary (경계의 명시화)

함수 및 모듈의 경계에 계약을 작성함으로써 AI 에이전트에게 부여하는 태스크의 경계를 명확히 한다. "이 함수를 구현해줘"라는 모호한 요청이 아니라, "이 사전 조건과 사후 조건을 만족하는 구현을 생성해줘"라는 구체적인 발주서가 된다. GitHub Spec Kit의 /plan 명령은 이 발상을 그대로 체현하고 있다. spec.md가 "무엇을", "왜" 실현하는지를 기록하는 인간용 계약서라면, /plan이 생성하는 contracts/...

디렉토리는 인터페이스 정의 그 자체이며, 말하자면 "기계용 계약서"다. 양자는 동일한 커맨드 체인(/specify → /plan)의 출력으로서 연결되어 있기 때문에, 한쪽만 업데이트되어 동기화가 깨지는 상황이 구조적으로 발생하기 어렵게 만든다.

패턴 2: Contract as Machine-Readable Spec (기계 가독형 사양으로의 승격)

GitHub Spec Kit이 좋은 예시다. /plan 커맨드를 실행하면, Phase 1의 출력으로서 contracts/ (인터페이스 정의)나 data-model.md (데이터 모델)와 같은 구조화된 결과물이 생성된다. AI 에이전트에게 "이 기능을 구현해줘"라고 요청할 때, Prose의 spec.md뿐만 아니라 이러한 구조화된 파일들을 함께 전달하면, 사전 조건(Pre-condition)·사후 조건(Post-condition)이 구현 에이전트에 대한 입력으로서 일관된 형태로 전달된다. 즉, 계약 = 구현 에이전트에 대한 입력 스키마(Schema)로 치환될 수 있다.

패턴 3: Contract as Test Oracle (계약으로부터 테스트 자동 생성)

GitHub Spec Kit은 워크플로우 자체에 TDD (테스트 주도 개발) 사고방식을 통합하고 있다. /tasks 커맨드를 실행하면, 테스트와 관련된 태스크가 자동으로 구현 태스크보다 앞선 순서로 배치되며, "무엇을 약속했는가(spec)"와 "무엇이 구현되었는가"를 추적할 수 있도록 테스트가 요구사항에 직접 연결된다. 인간은 계약(spec.md)에서 무엇을 보장해야 하는지만 작성하고, 구현은 AI가 생성하며, 테스트는 계약에서 유래한 태스크로서 워크플로우 내에서 도출되는 삼자 분업이 성립한다. 이를 통해 "AI가 작성한 테스트가 AI가 작성한 구현의 끼워 맞추기만 하고 있다"라는, AI 주도 개발에서 흔히 발생하는 품질 보증 실패 패턴을 구조적으로 회피할 수 있다. 테스트의 출처가 구현과는 독립된 계약이기 때문이다.

패턴 4: Contract as Verification Gate (CI에서의 자동 검증 게이트)

GitHub Spec Kit의 /analyze 커맨드는 품질 게이트(Quality Gate)로서 기능한다. 사양(spec.md)·기술 계획(plan.md)·태스크 분해(tasks.md)가 프로젝트의 "헌법"에 해당하는 constitution.md와 일치하는지를 검증하여, 구현으로 넘어가기 전에 불일치를 감지하는 메커니즘이다. AI 생성 코드를 머지(Merge)하기 전에 이 정합성 체크를 CI (지속적 통합) 단계에 삽입하면, 인간의 리뷰를 기다리지 않고도 기계적으로 결함을 감지할 수 있다. Dafny/F*/Verus와 같은 검증 대응 언어에서는 증명이 통과되지 않으면 빌드가 통과되지 않는 형태로 이것이 더욱 강력하게 나타난다.

패턴 5: Contract as Agent-to-Agent Protocol (에이전트 간의 책임 분계)

구현 에이전트와 검증 에이전트를 분리하고, 양자 사이에 계약을 배치한다. VERI-SURE의 발상 그 자체다. 구현 에이전트의 생성물과 검증 에이전트의 합격/불합격 판정이 계약이라는 공통 언어를 통해 느슨한 결합(Loosely Coupled) 상태가 되므로, 에이전트를 교체하더라도 계약만 충족하면 된다는 교환 가능성이 생긴다. 계약이 변하지 않는 한, 구현의 세부 사항 변경이 다른 에이전트나 다른 모듈에 영향을 주지 않는다고 기계적으로 주장할 수 있다.

패턴 6: Contract as Audit Trail (감사 추적으로서의 계약 위반 로그)

계약 위반(사전 조건·사후 조건의 위반)을 단순한 예외로 치부하여 묵인하는 것이 아니라, "AI가 어디에서 의도와 어긋났는가"에 대한 기록으로서 구조화된 로그로 남긴다. 2030년대를 내다본다면, AI 에이전트의 자율성이 높아질수록 "에이전트가 어떤 권한으로 무엇을 했는가"에 대한 추적 가능성(Traceability)이 요구될 것이다. 계약 위반 로그는 그 최소 단위의 감사 추적(Audit Trail)이 될 수 있다.

구현 예시: 사양 생성과 구현을 분리하는 2모델 구성

패턴 1(경계의 명시화)과 패턴 5(에이전트 간 프로토콜)를 결합하여 실제로 적용하기 쉬운 구성을 하나 들겠다. 사양을 쓰는 데 능숙한 모델과 구현을 쓰는 데 능숙한 모델을 의도적으로 분리하고, 그 사이에 인간의 승인을 배치하는 형태다.

역할 분담의 포인트는 다음과 같다.

• 사양 생성 담당 (예: GPT-5.6): 모호한 요구사항을 받아 섹션 3에서 보여준 것과 같은 구조화된 포맷(사전 조건/사후 조건/불변 조건)으로 spec.md를 작성한다. 여기서 모델의 특기 분야는 '요구사항의 언어화 및 모호성 제거 (disambiguate)'이며, 구현이 아니다. -
• Human in the Loop: 리뷰의 초점은 코드의 세부 사항이 아니라, spec.md라는 계약서가 비즈니스적으로 올바른가라는 단 한 점에 집중한다. 이곳이 유일한 오라클 (Oracle, 판정자)이며, 승인될 때까지 구현 단계로 진행하지 않는다. -
• 구현 담당 (예: Fable 5): 승인된 spec.md만을 입력으로 받아 구현에 전념한다. 사양 생성 측의 대화 이력이나 프롬프트의 변동성을 가져오지 않기 때문에, 패턴 5에서 언급한 '계약이라는 공통 언어를 통한 느슨한 결합 (loose coupling)'을 그대로 실현할 수 있다.

이 워크플로의 장점은 사양 생성 모델과 구현 모델을 교체 가능하게 만들 수 있다는 점이다. 계약(spec.md)이라는 인터페이스만 지켜진다면, 어떤 모델이 사양을 쓰고 어떤 모델이 구현할지는 교체 가능한 부품이 된다. 역으로 말하면, 사양 생성 모델의 출력을 리뷰 없이 구현 모델로 직결해 버리면, 의도 격차 (intent gap)가 '인간이 알아차리지 못한 채' 구현 측으로 전파될 리스크가 있으므로, Human in the Loop의 승인 게이트를 생략하지 않는 것이 핵심이다.

5. 도입을 위한 단계적 로드맵

의도 형식화 (intent formalization) 스펙트럼에 따라 단계적으로 도입하는 것이 현실적이다.

• Step 0 (현상태): docstring의 Args/Returns/Raises만 존재. 계약은 자연어로 되어 있으며, AI 에이전트로의 전달은 인간의 리뷰에 의존함. -
• Step 1: 중요한 공개 함수 및 기능 (외부 API 경계, 금액 계산, 상태 전이 등)에 대해 GitHub Spec Kit으로 spec.md를 작성하여 사전 조건과 사후 조건을 명시한다. AI에게 코드를 생성하게 할 때, 이 spec.md를 계약으로서 프롬프트에 포함한다. -
• Step 2: /tasks 명령어로 테스트 관련 태스크를 구현 태스크보다 앞서 자동으로 배치하게 하고, 계약 기반의 테스트를 CI에 통합한다. AI 생성 코드는 계약 기반의 테스트를 통과하지 않는 한 머지(merge)할 수 없도록 한다. -
• Step 3: /analyze 명령어로 사양·계획·태스크가 constitution.md와 일치하는지 CI에서 검증하고, 계약 위반(불일치)을 기계적으로 탐지한다. -
• Step 4 (선택적): 정말로 크리티컬한 부분 (결제 로직, 권한 판정 등)에 대해서만 Dafny/Verus 등 검증 인식 (verification-aware) 언어로 이중 구현하여 수학적 증명까지 나아간다.

이 로드맵의 핵심은 리스크가 높은 부품에만 중량급 기법을 투입하며, 모든 것을 Step 4까지 진행할 필요는 없다는 점이다. 마찬가지로 spec.md의 입도(granularity)도 일률적으로 맞출 필요는 없다. 외부 API, 금전 처리, 권한 판정과 같은 경계에만 무거운 스펙을 요구하고, 그 외에는 타입 힌트(type hint)와 docstring 정도의 경량 계약으로 끝내는 가변 입도 운용이 현실적이다.

요약

계약은 '쓰는 양을 늘리는 것'이 아니라, AI에게 무엇을 맡겨도 되는지의 경계선을 긋는 것이라고 파악하면 도입 장벽은 크게 낮아진다. 우선 Step 1 (중요한 공개 함수에 대한 사전 조건·사후 조건 추가)부터 시작하여, 리스크가 높은 부분에만 단계적으로 기법을 쌓아가는 것이 현실적인 첫걸음이다.

참고 문헌·정보원

참고 문헌·정보원

• Lahiri, S. K. (2026).
  Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents. https://arxiv.org/abs/2603.17150 - GitHub Blog:
  Spec-driven development with AI: Get started with a new open source toolkit. https://github.blog/ai-and-ml/generative-ai/spec-driven-development-with-ai-get-started-with-a-new-open-source-toolkit/ - GitHub Spec Kit 리포지토리: https://github.com/github/spec-kit
• Veri-Sure:
  A Contract-Aware Multi-Agent Framework ... for Correct RTL Code Generation. https://arxiv.org/pdf/2601.19747

본 게시물은 개인의 견해에 기반한 것이며, 소속 조직을 대표하지 않습니다.

논의