AI는 왜 같은 버그를 고치고 또 생각할까? — 바이브 코딩의 무한 Loop를 끊는 방법

Bug Fix Loop·Reasoning Loop의 차이부터 Anthropic의 수학적 검증 연구, Claude Code·Codex에서 반복 작업을 줄이는 방법까지

2026년 10월 28일 기준

AI로 프로그램을 만드는 속도는 정말 빨라졌다.

예전에는 며칠씩 걸리던 기능도 이제는 Codex나 Claude Code에 요구사항을 설명하면 금방 구현된다. 파일을 만들고, 코드를 수정하고, 테스트까지 진행한다.

처음에는 놀라울 정도로 잘된다.

그런데 프로젝트가 커지고 여러 기능이 연결되기 시작하면 조금씩 다른 문제가 나타난다.

어제 해결한 로그인 오류가 다시 발생한다. 네트워크 재시도 기능을 수정했더니 취소 기능이 제대로 동작하지 않는다. 이 문제를 고치면 이번에는 이전 요청의 응답이 새로운 화면에 표시된다.

AI에게 다시 수정을 요청한다.

처음에는 파일 몇 개를 조사하더니, 점점 더 많은 코드를 읽기 시작한다. 이미 확인한 함수를 다시 분석하고, 다른 가능성을 찾다가 원래 수정하려던 범위를 벗어나기도 한다.

한참 생각한 뒤 코드를 수정한다.

그런데 빌드를 실행하면 또 다른 문제가 발견된다.

버그 발견
    ↓
AI가 원인 분석
    ↓
코드 수정
    ↓
테스트 실패
    ↓
다른 코드 수정
    ↓
이전 버그 재발
    ↓
다시 원인 분석
    ↺

끝나지 않는 반복 작업이다.

이런 현상을 크게 두 가지로 구분할 수 있다.

Bug Fix Loop는 버그를 수정했지만 다른 문제가 생기거나 이전 오류가 재발해 같은 작업을 반복하는 상황이다.

Reasoning Loop는 AI가 해결 방향을 결정하지 못하고 비슷한 가설과 코드 분석을 반복하면서 시간과 토큰을 소비하는 상황이다.

둘은 서로 다른 문제지만 실제 개발에서는 함께 나타날 수 있다.

특히 동시성, 상태 관리, 재시도, 취소 같은 기능이 복잡하게 얽혀 있을 때 그렇다.

그렇다면 해결책은 테스트 코드를 더 많이 작성하는 것일까?

테스트는 중요하지만 그것만으로 모든 상황을 확인하기는 어렵다.

여기서 최근 주목받는 기술이 있다.

바로 **정형 검증(Formal Verification)**이다.

2026년 10월 22일, Anthropic은 Theorem과 함께 AI를 이용해 실제 오픈소스 프로그램을 수학적으로 검증한 연구를 공개했다.

123개 오픈소스 라이브러리의 239개 진입점에 대해 특정 안전성 조건을 증명했고, 기존 테스트에서 오랫동안 발견되지 않았던 버그도 찾아냈다.

그렇다고 정형 검증이 AI의 생각을 무조건 빠르게 만들거나 모든 버그를 없애는 기술은 아니다.

오히려 검증에 더 많은 시간과 토큰을 사용할 수 있다.

하지만 복잡한 문제에서 추측과 수정을 반복하는 대신, 어떤 규칙이 깨지는지 확인하고 수정 범위를 좁히는 방법으로 활용할 수 있다.

이번 글에서는 두 가지 Loop가 왜 발생하는지, 정형 검증이 어느 부분에 도움이 되는지, 그리고 Claude Code와 Codex에서 실제로 적용할 수 있는 방법까지 살펴본다.

1. 바이브 코딩에서 발생하는 두 가지 Loop

먼저 Bug Fix Loop와 Reasoning Loop를 구분할 필요가 있다.

두 용어 모두 이 글에서 반복적인 개발 문제를 설명하기 위해 사용하는 표현이다. 특히 Reasoning Loop는 특정 모델의 공식 오류 분류명이라기보다, 분석이 불필요하게 반복되는 사용 경험을 설명하는 말에 가깝다.

Bug Fix Loop — 고치면 다른 곳이 깨진다

예를 들어 앱에 다음 기능이 있다고 생각해보자.

네트워크 요청

자동 재시도

작업 취소

백그라운드 복구

화면 상태 업데이트

각 기능은 정상적으로 동작한다.

그런데 네트워크 재시도를 수정하면서 취소된 작업이 다시 실행되는 문제가 발생했다.

이 문제를 고쳤더니 이번에는 새로운 요청이 이전 요청의 응답으로 덮어써진다.

재시도 버그 수정
       ↓
취소 기능 오류
       ↓
취소 버그 수정
       ↓
상태 업데이트 오류
       ↓
상태 업데이트 수정
       ↓
재시도 문제 재발

이런 반복이 Bug Fix Loop다.

원인은 단순히 테스트 코드가 부족해서만은 아니다.

변경한 코드가 여러 기능의 공통 상태나 제약 조건에 영향을 주기 때문이다.

Reasoning Loop — 생각은 길어지는데 해결 방향이 좁혀지지 않는다

이번에는 AI가 코드를 수정하기 전에 계속 분석하는 상황이다.

버그 분석 시작
       ↓
원인 A 추정
       ↓
관련 파일 조사
       ↓
원인 B 가능성 발견
       ↓
다른 파일 조사
       ↓
원인 C 검토
       ↓
처음 파일 재조사
       ↓
새로운 가설 제시
       ↺

모델이 깊게 분석하는 것 자체가 문제는 아니다.

실제로 복잡한 문제에서는 충분한 탐색이 필요하다.

문제는 추가 분석이 실제로 새로운 근거를 확보하거나 해결 방향을 좁히지 못하는 경우다.

같은 파일을 여러 번 읽고, 검증하지 않은 가설을 계속 바꾸고, 비슷한 수정안을 반복해서 제시한다면 생산성이 떨어진다.

정리하면 다음과 같다.

구분	Bug Fix Loop	Reasoning Loop
주요 현상	수정 후 오류 재발	분석·추론 반복
발생 단계	구현·테스트·재수정	원인 분석·계획
주요 문제	기존 규칙이 깨짐	원인을 좁히지 못함
발생 결과	재작업 증가	시간·토큰 사용 증가
우선 대응	회귀 테스트와 영향 범위 확인	가설 정리·증거 확보·탐색 제한
정형 검증의 역할	불변식 위반 탐색	검증 가능한 질문으로 분석 범위 축소

두 문제가 반드시 동시에 발생하는 것은 아니다.

또 Reasoning Loop가 모두 정형 검증으로 해결되는 것도 아니다.

이 차이를 이해하는 것이 중요하다.

2. AI는 왜 같은 코드를 계속 분석할까?

AI 코딩 에이전트는 일반적으로 사용자의 요청을 바탕으로 관련 파일을 탐색한다.

예를 들어 다음과 같이 요청했다고 생각해보자.

작업 취소 후에도
이전 응답이 화면에 반영되는 문제를 수정해줘.

AI는 취소 로직과 네트워크 코드를 조사한다.

문제의 원인이 명확하면 비교적 빠르게 수정할 수 있다.

하지만 여러 비동기 작업이 연결돼 있다면 이야기가 달라진다.

SearchViewModel
      ↓
SearchRepository
      ↓
NetworkService
      ↓
RetryHandler
      ↓
RequestQueue
      ↓
ResponseHandler

AI는 어느 부분에서 문제가 발생하는지 알아내야 한다.

이 과정에서 필요한 컨텍스트가 부족하거나 실행 흐름을 확인할 수 없다면 여러 가설을 세우게 된다.

예를 들어 다음과 같은 추측이 가능하다.

취소가 정상적으로 전달되지 않았을까?

Task가 취소됐지만 결과를 처리했을까?

이전 요청과 새 요청을 구분하지 않았을까?

재시도 로직에서 새로운 요청을 만들었을까?

화면 상태를 갱신하는 순서가 잘못됐을까?

문제는 이런 가설을 하나씩 검증하지 않고 계속 확장하는 경우다.

모델이 오래 생각하는 것처럼 보여도 실제로는 같은 불확실성을 반복해서 다루고 있을 수 있다.

하지만 여기서 주의할 부분이 있다.

AI의 내부 추론이 길다고 해서 모두 Reasoning Loop라고 볼 수는 없다. 사용자에게 보이는 Tool 호출 기록만으로 모델 내부의 모든 사고 과정을 정확히 알 수도 없다.

따라서 문제를 판단할 때는 추론 시간 자체보다 다음 항목을 확인하는 편이 좋다.

• 새로운 정보가 실제로 발견됐는가?
• 원인 후보가 줄어들고 있는가?
• 같은 파일이나 명령을 불필요하게 반복하는가?
• 검증 가능한 가설이 만들어졌는가?
• 수정 범위가 요청보다 계속 커지는가?

좋은 분석은 오래 생각하는 분석이 아니라, 불확실성을 줄이는 분석이다.

3. 정형 검증이 Reasoning Loop에 도움이 될 수 있는 이유

정형 검증은 AI의 추론 속도를 높이는 기술이 아니다.

그렇다면 왜 Reasoning Loop에 도움이 될 수 있을까?

핵심은 문제를 다루는 방식이 달라지기 때문이다.

일반적인 버그 수정에서는 AI가 원인을 추측하고 관련 코드를 조사한다.

버그 발생
    ↓
원인 추측
    ↓
코드 조사
    ↓
수정 시도
    ↓
테스트

반면 정형 검증을 활용하면 먼저 프로그램이 반드시 지켜야 하는 규칙을 정의할 수 있다.

예를 들어 다음과 같다.

취소된 작업의 응답은 현재 화면 상태를 변경할 수 없다.

이제 질문이 구체적으로 바뀐다.

기존 질문은 다음과 같았다.

왜 검색 결과가 잘못 표시될까?

검증할 질문은 다음처럼 바꿀 수 있다.

어떤 작업 실행 순서에서
취소된 요청의 응답이
현재 화면 상태를 변경할 수 있는가?

이렇게 하면 가능한 실행 순서를 상태 모델로 표현하고, 규칙이 깨지는 반례를 찾을 수 있다.

문제 정의
    ↓
불변식 작성
    ↓
상태 모델 구성
    ↓
모델 검사
    ↓
반례 확인
    ↓
실제 코드에서 재현
    ↓
수정

여기서 중요한 것은 모델 검사기가 실제로 실행되고, 의미 있는 반례가 발견됐을 때다.

그 경우 AI는 막연한 추측 대신 구체적인 실패 순서를 바탕으로 문제를 분석할 수 있다.

따라서 Reasoning Loop를 줄일 가능성이 생긴다.

다만 반례가 발견되지 않았다고 해서 문제가 없다는 결론이 자동으로 나오지는 않는다.

모델 자체가 잘못됐거나 중요한 상황을 제외했을 수 있기 때문이다.

정형 검증은 AI에게 정답을 알려주는 기술이 아니라, 확인할 수 있는 근거를 만드는 방법에 가깝다.

4. 테스트 코드가 많아져도 Loop가 끝나지 않는 이유

회귀 버그를 줄이는 가장 기본적인 방법은 자동화 테스트다.

AI 코딩 도구에서도 테스트 작성은 중요한 작업이다.

기능을 수정할 때 테스트를 추가하고, 기존 테스트가 통과하는지 확인한다.

그런데 테스트가 많아진다고 해서 모든 상황이 검증되는 것은 아니다.

특히 문제가 되는 것은 실행 순서다.

예를 들어 서버 요청을 취소하는 테스트를 만들었다고 생각해보자.

요청 시작
    ↓
취소
    ↓
응답 처리 중단
    ↓
테스트 성공

이 테스트는 정상적으로 통과할 수 있다.

하지만 실제 환경에서는 다음과 같은 순서도 가능하다.

요청 A 시작
    ↓
요청 A 취소
    ↓
요청 B 시작
    ↓
요청 B 완료
    ↓
요청 A의 늦은 응답 도착
    ↓
현재 상태 변경

두 번째 상황을 테스트하지 않았다면 오류를 발견하지 못할 수 있다.

이런 문제가 복잡해지는 이유는 가능한 순서가 많기 때문이다.

10개의 독립적인 사건을 모두 다른 순서로 배치할 수 있다고 가정하면 가능한 순열은 다음과 같다.

\[ 10! = 3,628,800 \]

물론 실제 프로그램에는 실행 순서에 대한 제약이 있으므로 모든 순열이 가능한 것은 아니다.

하지만 취소와 재시도, 타임아웃, 동시 실행이 결합하면 검토해야 할 상태가 빠르게 증가한다.

기존 테스트는 여전히 중요하다.

다만 테스트를 무작정 늘리는 것보다 어떤 규칙을 검증해야 하는지 먼저 정하는 것이 더 효과적일 수 있다.

예를 들어 테스트가 1,000개 있어도 모두 정상적인 요청 흐름만 확인한다면 취소 후 늦은 응답이라는 문제를 놓칠 수 있다.

반대로 단 하나의 잘 설계된 상태 모델이 해당 문제를 발생시키는 실행 순서를 찾아낼 수도 있다.

그렇다고 정형 검증이 테스트보다 언제나 우수한 것은 아니다.

일반적인 기능 검증은 테스트가 더 간단하고 빠를 수 있다.

중요한 것은 두 방법의 역할이 다르다는 점이다.

5. Anthropic은 10월 22일 무엇을 실제로 증명했을까?

2026년 10월 22일 Anthropic은 Theorem과 공동으로 진행한 정형 검증 연구를 공개했다.

연구팀은 Claude를 사용해 실제 오픈소스 프로그램의 안전성을 수학적으로 증명했다.

결과는 상당히 인상적이다.

123

오픈소스 라이브러리

239

검증한 진입점

1.8억

Rocq 증명 코드 줄 수

다만 239는 발견한 버그 수가 아니라 검증한 테스트 진입점의 개수다.

이번 연구에서 특히 흥미로운 부분은 소스 코드가 아니라 컴파일된 RISC-V 기계어를 검증했다는 사실이다.

일반적인 프로그램은 컴파일 과정을 거쳐 CPU가 실행할 수 있는 기계어로 변환된다.

Anthropic과 Theorem은 이 기계어의 동작을 수학적으로 표현하고, Claude가 증명을 작성하도록 했다.

이후 Rocq이라는 증명 검사기가 결과를 확인했다.

오픈소스 라이브러리
       ↓
RISC-V 바이너리 생성
       ↓
기계어 동작 모델링
       ↓
Claude가 증명 작성
       ↓
Rocq 증명 검사
       ↓
특정 안전성 조건 확인

이 구조에서 중요한 것은 AI가 안전하다고 주장하는 것과 독립적인 증명 검사기가 확인하는 것이 다르다는 점이다.

Claude는 증명을 작성한다.

Rocq은 해당 증명이 명시한 규칙과 가정 아래에서 올바른지 확인한다.

연구 과정에서는 기존 퍼징 테스트로도 발견하기 어려웠던 오래된 오류가 발견됐다.

일부는 매우 드문 입력 조건에서만 발생하는 메모리 안전성 문제였다.

연구팀은 이런 버그를 수정하고 다시 증명을 시도했다.

하지만 이 연구가 모든 프로그램의 버그를 없앴다는 의미는 아니다.

6. 정형 검증을 통과하면 버그가 없는 프로그램일까?

아니다.

이번 Anthropic 연구에는 명확한 검증 조건이 있다.

항목	연구의 주요 조건
CPU	RISC-V
운영체제 모델	Linux
실행 파일	정적 링크된 바이너리
실행 구조	단일 스레드
입력 범위	64MB 미만
메모리	고정된 예산
검증 내용	특정 메모리 안전성 오류와 크래시 방지

따라서 이번 연구가 Swift 동시성 문제나 분산 결제 시스템 전체의 정확성을 증명했다고 설명하면 안 된다.

예를 들어 메모리 안전성 검증을 통과한 프로그램이 잘못된 결제 금액을 계산할 수도 있다.

프로그램 정상 실행
       ↓
크래시 없음
       ↓
결제 금액 계산
       ↓
잘못된 금액 반환

프로그램이 크래시를 일으키지 않는다는 것과 비즈니스 로직이 올바르다는 것은 다른 문제다.

또 증명이 성립하는 범위는 모델에서 정한 조건에 따라 달라진다.

이 점은 Reasoning Loop에도 중요하다.

AI가 아무리 오래 분석하고 증명을 작성하더라도, 검증할 규칙 자체가 잘못됐다면 실제 문제를 해결하지 못할 수 있다.

정형 검증에서 중요한 것은 증명의 길이가 아니라 무엇을 증명했는지다.

7. 테스트와 정형 검증은 어떻게 다를까?

일반적인 테스트는 프로그램을 실행해 결과를 확인한다.

입력
  ↓
프로그램 실행
  ↓
결과
  ↓
예상 결과와 비교

정형 검증은 프로그램의 상태와 동작을 수학적으로 표현하고, 특정 규칙이 유지되는지 확인한다.

하지만 정형 검증도 하나의 기술만을 뜻하는 것은 아니다.

방법	주요 역할	주의할 점
단위 테스트	개별 함수의 동작 확인	실행하지 않은 입력
통합 테스트	기능 간 연동 확인	테스트 시나리오 범위
퍼징 테스트	다양한 입력으로 오류 탐색	모든 입력을 검사하지 않음
속성 기반 테스트	공통 규칙 확인	생성한 입력에 의존
모델 검사	상태 변화와 실행 순서 탐색	모델 크기와 가정
정리 증명	수학적 속성 증명	명세와 실제 구현의 일치

여기서 TLA+와 Lean, Rocq은 서로 다른 역할을 한다.

TLA+의 TLC는 모델에서 도달 가능한 상태를 탐색해 규칙 위반을 찾을 수 있다.

Lean과 Rocq은 명시한 명제를 수학적으로 증명하는 데 사용한다.

Swift 코드에 이러한 도구를 연결한다고 해서 모든 상태가 자동으로 검증되는 것은 아니다.

개발자가 먼저 검증할 중요한 규칙과 모델의 범위를 정해야 한다.

이 부분이 실제 도입에서 가장 어렵지만 중요한 작업이다.

8. Loop를 줄이려면 '원인 추측'보다 '불변식'부터 정의하자

티켓이 한 장 남은 콘서트 예매 시스템을 생각해보자.

두 사용자가 동시에 구매를 시도한다.

그런데 개발자가 버그를 해결하기 위해 다음과 같이 요청한다면 어떨까?

동시에 결제할 때 오류가 발생하니까
원인을 찾아서 수정해줘.

AI는 데이터베이스, 결제 API, 요청 큐, 재시도 로직 등 여러 부분을 조사할 수 있다.

그 과정에서 Reasoning Loop처럼 보이는 반복적인 분석이 발생할 수도 있다.

반면 중요한 규칙을 먼저 정의하면 검증할 대상이 명확해진다.

규칙 1

예약 중인 좌석 수 + 판매 확정 좌석 수는
전체 좌석 수를 초과할 수 없다.

규칙 2

하나의 좌석을 두 사용자에게
동시에 판매 확정할 수 없다.

규칙 3

동일한 결제 요청을 여러 번 처리해도
실제 결제는 중복 발생하지 않아야 한다.

이런 규칙을 불변식(Invariant)이라고 부른다.

이제 AI에게 요청할 수 있다.

이 시스템의 예약·결제 상태를 모델링해줘.

앞에서 정의한 세 가지 불변식이
깨질 수 있는 실행 순서가 있는지 검사해줘.

문제가 발견되면 반례를 보여주고,
실제 코드에서 같은 상황을 재현해줘.

이렇게 하면 분석의 방향이 달라진다.

단순히 버그가 있을 만한 파일을 계속 탐색하는 대신, 정해진 규칙을 깨뜨리는 상태 변화가 있는지 확인하도록 작업을 좁힐 수 있다.

물론 모델을 설계하는 데 시간이 필요하고, 큰 상태 공간에서는 검사가 오래 걸릴 수도 있다.

그래도 반복되는 추측보다 구체적인 실패 조건이 필요한 상황에서는 도움이 될 수 있다.

9. Swift의 actor를 사용해도 Bug Fix Loop가 발생하는 이유

iOS 개발에서는 Swift Concurrency가 좋은 사례다.

Swift 6에서는 actor, Sendable, @MainActor 등을 통해 동시성 안전성을 강화할 수 있다.

하지만 actor를 사용했다고 해서 모든 상태 관리 문제가 해결되는 것은 아니다.

다음 예제를 살펴보자.

actor TicketStore {
    private var available = 1

    func purchase() async -> Bool {
        guard available > 0 else {
            return false
        }

        let approved = await authorizePayment()

        guard approved else {
            return false
        }

        available -= 1
        return true
    }

    private func authorizePayment() async -> Bool {
        true
    }
}

이 코드는 설명을 위한 단순한 예제다.

문제는 재고를 확인한 뒤 await를 호출하는 부분이다.

guard available > 0 else {
    return false
}

let approved = await authorizePayment()

Swift의 Actor Reentrancy 때문에 await에서 실행이 중단되는 동안 다른 작업이 actor의 상태를 변경할 수 있다.

예를 들어 다음과 같은 순서가 가능하다.

초기 재고: 1

Task A
재고 확인 → 1

Task A
결제 승인 대기

Task B
재고 확인 → 1

Task B
결제 승인 완료

Task B
재고 감소 → 0

Task A
결제 승인 완료

Task A
재고 감소 → -1

actor를 사용했는데도 재고가 음수가 됐다.

이는 actor 격리 자체가 실패했다는 의미가 아니다.

재고 확인과 감소가 하나의 중단 없는 작업으로 처리되지 않았기 때문이다.

AI에게 단순히 actor를 적용하라고 요청하는 것만으로는 해결되지 않는다.

재고 예약과 결제 승인, 예약 만료 같은 상태 전이를 함께 설계해야 한다.

정형 검증을 활용한다면 다음 규칙을 확인할 수 있다.

어떤 실행 순서에서도
available은 0보다 작아질 수 없다.

이처럼 기술적인 동시성 안전성과 비즈니스 규칙의 정확성은 구분해야 한다.

10. 취소했는데 이전 응답이 돌아온다 — 가장 흔한 상태 Loop

이번에는 네트워크 검색 기능을 생각해보자.

사용자가 검색어를 입력한다.

Swift

검색 요청 A가 시작된다.

잠시 뒤 사용자가 검색어를 변경한다.

SwiftUI

앱은 A를 취소하고 B를 시작한다.

하지만 이전 요청의 응답이나 후처리가 늦게 완료될 수 있다.

요청 A 시작
    ↓
요청 A 취소
    ↓
요청 B 시작
    ↓
요청 B 완료
    ↓
SwiftUI 결과 표시
    ↓
요청 A의 늦은 처리 결과
    ↓
Swift 결과로 덮어쓰기

이 문제를 반복해서 수정하는 대신 먼저 규칙을 정의하자.

현재 요청과 식별자가 다른 응답은 화면 상태를 수정할 수 없다.

Swift에서는 요청마다 식별자를 부여해 이를 구현할 수 있다.

import Foundation

@MainActor
final class SearchViewModel {
    private var currentRequestID: UUID?
    private var searchTask: Task<Void, Never>?

    private(set) var results: [String] = []

    func search(_ query: String) {
        searchTask?.cancel()

        let requestID = UUID()
        currentRequestID = requestID

        searchTask = Task {
            do {
                let newResults = try await fetchResults(query)

                guard !Task.isCancelled else {
                    return
                }

                guard currentRequestID == requestID else {
                    return
                }

                results = newResults
            } catch {
                // 실제 앱에서는 오류 상태 처리 필요
            }
        }
    }

    private func fetchResults(
        _ query: String
    ) async throws -> [String] {
        [query]
    }
}

이 예제에서 핵심은 다음 조건이다.

guard currentRequestID == requestID else {
    return
}

이전 요청의 결과가 늦게 도착하더라도 현재 요청과 식별자가 다르면 화면을 변경하지 않는다.

실제 서비스에서는 취소 전파, 오류 처리, 검색 요청의 중복 실행, ViewModel 생명주기 등을 추가로 검토해야 한다.

정형 검증에서는 다음 상황을 모델링할 수 있다.

• A가 먼저 완료
• B가 먼저 완료
• A 취소 후 응답 도착
• B 시작 중 A 응답 도착
• 여러 요청이 연속으로 생성

이렇게 검증하면 막연하게 코드 전체를 반복 분석하는 대신 상태가 깨지는 실행 순서를 확인하는 데 집중할 수 있다.

11. Claude Code와 Codex에서 사용할 수 있는 정형 검증 스킬

이제 실제 도구를 살펴보자.

Anthropic과 Theorem이 사용한 연구용 검증 시스템을 누구나 일반적인 앱에 바로 적용할 수 있는 것은 아니다.

하지만 Claude Code와 Codex에서 사용할 수 있는 오픈소스 정형 검증 스킬은 공개돼 있다.

대표적인 프로젝트는 두 가지다.

프로젝트	주요 기능	지원 환경
proof-skills	TLA+·Lean 기반 모델 검사와 증명, 버그 재현	Claude Code
agent-formal-verify	TLA+·Lean·Kani를 활용한 선택적 검증	Claude Code·Codex·Pi

둘 다 일반적인 코드 수정과 다른 접근을 사용한다.

문제 코드 분석
      ↓
검증할 규칙 정의
      ↓
상태 모델 작성
      ↓
검증 도구 실행
      ↓
반례 발견
      ↓
실제 코드 재현
      ↓
수정
      ↓
재검증

이 과정에서 중요한 것은 AI가 스스로 안전하다고 판단하는 것이 아니라 실제 검증 도구를 실행한다는 점이다.

다만 모델과 실제 코드가 정확히 대응하는지 확인하는 과정은 여전히 필요하다.

Claude Code — proof-skills 설치

proof-skills는 Opum AI가 공개한 커뮤니티 플러그인이다.

현재 공식 저장소에서 안내하는 설치 명령은 다음과 같다.

/plugin marketplace add opum-ai/opum-marketplace

/plugin install proof-skills@opum

설치하면 formal-verify, tlaplus-model, lean-model, proof-simplify 등의 스킬을 사용할 수 있다.

하지만 플러그인을 설치했다고 해서 검증에 필요한 모든 실행 환경이 준비된 것은 아니다.

TLA+와 Lean의 도구 체인이 필요할 수 있으며, 공식 저장소는 관련 설정 스크립트를 제공한다.

특히 이 스킬은 검증 결과를 보고서로 남기고, 발견한 반례를 실제 코드에서 재현하는 과정을 중요하게 다룬다.

Codex — agent-formal-verify 설치

Codex에서는 agent-formal-verify 프로젝트를 사용할 수 있다.

공식 저장소에서 안내하는 설치 명령은 다음과 같다.

codex plugin marketplace add michael-denyer/agent-formal-verify

codex plugin add agent-formal-verify@agent-formal-verify

설치 후 해당 프로젝트의 setup 스킬을 이용해 필요한 도구를 준비한다.

프로젝트에서 제공하는 주요 검증 방법은 다음과 같다.

도구	주요 역할
TLA+ / TLC	동시 실행, 작업 종료, 자원 소유권
Lean 4	수학적 속성, 경계 조건, 순차 상태 전이
Kani	제한된 범위의 Rust 코드 검증

Kani가 지원된다고 해서 Swift 코드를 직접 검증할 수 있다는 의미는 아니다.

Swift 프로젝트에서는 중요한 상태와 실행 규칙을 TLA+ 등으로 모델링하는 접근이 더 현실적이다.

또 이 프로젝트는 커뮤니티 플러그인이므로 설치 전에 코드와 실행 권한을 확인하는 것이 좋다.

12. 실제로 Reasoning Loop를 줄이려면 어떻게 요청해야 할까?

스킬을 설치한 것보다 중요한 것은 요청 방법이다.

AI에게 다음과 같이만 요청하면 분석 범위가 계속 커질 수 있다.

이 코드의 동시성 문제를
전부 찾아서 수정해줘.

프로젝트가 크다면 상당히 많은 파일을 조사할 수 있다.

또 어떤 상태가 올바른 상태인지 판단하기 어려울 수 있다.

이럴 때는 검증할 대상을 좁히는 편이 좋다.

예를 들어 다음과 같다.

현재 SearchViewModel의
작업 취소와 재시작 로직만 검증해줘.

다음 불변식을 확인해.

1. 취소된 요청은 현재 결과를 변경할 수 없다.

2. 현재 요청과 ID가 다른 응답은 무시해야 한다.

3. 같은 요청 결과가 중복 적용되면 안 된다.

검증 범위는 SearchViewModel과
관련 NetworkService로 제한해줘.

먼저 상태 모델을 작성하고
반례가 있는지 확인해줘.

반례가 발견되면
실제 코드에서 재현해줘.

수정 전에 영향받는 파일을 알려줘.

검증이 끝나면 사용한 도구,
검증 범위, 제외한 조건을 보고해줘.

이런 지시의 장점은 질문이 명확하다는 점이다.

AI가 프로젝트 전체를 무작정 탐색하기보다 특정 규칙을 중심으로 조사하도록 유도할 수 있다.

하지만 모든 문제에 정형 검증을 적용하는 것은 아니다.

예를 들어 빌드 오류가 단순한 타입 불일치라면 컴파일러 오류를 확인하는 편이 훨씬 빠르다.

또 문제가 발생한 로그가 충분하다면 일반적인 디버깅만으로 해결할 수 있다.

Reasoning Loop를 줄이는 첫 번째 방법은 스킬을 추가하는 것이 아니라, 문제의 범위와 종료 조건을 명확하게 만드는 것이다.

정형 검증은 그다음 선택지다.

13. 정말 효과가 있을까? 54%에서 98%로 올라간 검증 평가

proof-skills 개발팀은 다섯 가지 버그 사례를 대상으로 스킬 사용 전후를 비교했다.

검증한 사례에는 Python 비동기 웹훅, TypeScript 작업 큐, Go DAG 실행기, Python 주문 서비스, Rust 연결 풀 등이 포함됐다.

개발팀의 자체 평가 결과는 다음과 같다.

스킬 미사용

54%

평가 항목 평균 충족률

스킬 사용

98%

평가 항목 평균 충족률

차이가 상당히 크다.

하지만 여기서 주의할 점이 있다.

이 수치는 버그 탐지율이나 모든 경우의 수를 검증한 비율이 아니다.

개발팀이 구성한 다섯 가지 예제에서 정해진 평가 항목을 얼마나 충족했는지 측정한 것이다.

스킬을 사용하지 않은 경우에도 심어 놓은 버그를 찾아 수정했다.

차이는 검증 결과를 얼마나 엄밀하게 확인하고 기록했는지에 있었다.

스킬을 사용한 경우에는 검증 범위와 가정을 명시하고, 모델에서 발견한 반례를 실제 코드로 재현하고, 검증 로그를 남기는 과정이 강화됐다.

대신 비용이 늘었다.

개발팀은 스킬 사용 시 시간과 토큰이 대략 두 배 정도 필요했다고 설명한다.

이 사실이 중요하다.

정형 검증 스킬을 사용하면 AI가 무조건 더 빠르게 작업하는 것이 아니다.

오히려 검증 절차 때문에 한 번의 작업은 더 오래 걸릴 수 있다.

그렇다면 왜 사용할까?

반복되는 복잡한 버그를 여러 차례 수정하는 것보다, 처음에 검증 비용을 들여 중요한 규칙을 확인하는 편이 유리할 수 있기 때문이다.

예를 들어 다음과 같은 두 상황을 생각해보자.

일반적인 수정

원인 분석
    ↓
코드 수정
    ↓
오류 재발
    ↓
다시 분석
    ↓
추가 수정
    ↓
다른 오류 발생

정형 검증 활용

불변식 정의
    ↓
상태 모델 작성
    ↓
반례 확인
    ↓
실제 코드 재현
    ↓
수정
    ↓
검증

두 번째 과정이 항상 빠르지는 않다.

하지만 특정 종류의 버그에서는 수정의 근거를 명확하게 만들 수 있다.

따라서 한 번의 검증 비용과 장기적인 재작업 비용을 비교해야 한다.

현재 공개된 다섯 가지 예제만으로 일반 프로젝트 전체의 장기 비용 절감 효과가 입증됐다고 볼 수는 없다.

14. 정형 검증을 사용했는데도 Loop가 끝나지 않을 수 있다

정형 검증 역시 잘못 사용하면 또 다른 반복 작업이 될 수 있다.

가장 큰 문제는 검증 모델 자체가 틀린 경우다.

예를 들어 중복 결제를 막는 규칙을 검증한다고 생각해보자.

동일한 결제 요청은
한 번만 처리돼야 한다.

그런데 AI가 만든 상태 모델에서 재시도 기능을 아예 제외했다면 어떻게 될까?

결제 요청
    ↓
결제 성공
    ↓
종료

이 모델에서는 중복 결제가 발생하지 않는다.

하지만 실제 프로그램에는 네트워크 지연과 재시도가 존재한다.

검증을 통과했다고 해도 실제 시스템의 문제가 해결되지 않는다.

또 AI가 검증을 통과시키기 위해 불변식을 약화하는 상황도 조심해야 한다.

처음에는 다음 규칙을 검증하려고 했다.

중복 결제는 절대 발생하면 안 된다.

그런데 모델을 수정하는 과정에서 다음과 같이 바뀌었다면 문제가 된다.

정상적인 요청에서는
중복 결제가 발생하지 않는다.

이미 검증하려는 범위가 달라졌다.

따라서 검증할 조건을 먼저 확정하고, 수정 과정에서 그 조건이 달라지지 않도록 관리해야 한다.

Lean이나 Rocq을 사용할 때도 미완성 증명이나 추가 가정에 의존하는지 확인해야 한다.

정형 검증에서 가장 위험한 결과는 검증 실패가 아니라, 잘못된 조건을 검증하고 안전하다고 믿는 것이다.

이런 문제를 막으려면 실제 코드와 모델의 관계, 검증 범위, 제외 조건을 함께 확인해야 한다.

15. 모든 작업에 정형 검증을 실행하는 것은 낭비일 수 있다

정형 검증이 중요하다고 해서 모든 코드 변경에 적용할 필요는 없다.

예를 들어 다음과 같은 작업을 생각해보자.

버튼 색상 변경

텍스트 수정

SwiftUI Padding 변경

아이콘 교체

이런 작업은 일반적인 빌드와 UI 테스트로 충분한 경우가 많다.

정형 검증까지 수행하면 불필요하게 시간과 토큰을 사용할 수 있다.

반면 다음과 같은 작업에서는 검토할 가치가 있다.

작업 취소와 재시작

네트워크 자동 재시도

중복 요청 처리

작업 큐 종료

공유 상태 변경

결제·예약·재고 관리

자원 소유권

실무에서는 다음 기준으로 시작할 수 있다.

작업	우선 검토할 방법
UI 문구·색상 변경	UI 확인, 기존 테스트
단순 함수 수정	단위 테스트
입력 처리	속성 기반 테스트
취소·재시도	상태 전이 테스트
동시성·중복 요청	모델 검사 검토
결제·예약·재고	불변식과 정형 검증 검토
자원 풀·작업 큐	동시성 모델 검사 검토
반복되는 원인 불명 버그	검증 범위 축소 후 정형 검증 검토

정형 검증을 적용할지는 작업의 복잡도와 실패 비용에 따라 결정해야 한다.

중요한 것은 검증할 필요가 없는 작업까지 무조건 검증하지 않는 것이다.

16. CLAUDE.md와 AGENTS.md에 Loop 방지 지침 추가하기

이제 실제 프로젝트에 적용할 방법을 정리해보자.

Claude Code는 CLAUDE.md, Codex는 AGENTS.md를 통해 프로젝트 지침을 전달할 수 있다.

여기에 반복적인 분석과 버그 수정, 선택적 정형 검증에 대한 규칙을 추가할 수 있다.

다만 지침 파일만으로 AI의 모든 행동이 강제되는 것은 아니다.

또 정형 검증 스킬이 자동으로 설치되거나 실행되는 것도 아니다.

실제 설치된 도구와 실행 결과를 확인해야 한다.

Claude Code·Codex 공통 지침 예제

# AI 코딩 작업 및 검증 정책

## 1. 기본 원칙

요청한 변경 범위를 최소화한다.

기존 기능과 Public API를 유지한다.

관련 없는 파일은 수정하지 않는다.

일반적인 수정에는 기존 테스트를 우선한다.

## 2. 반복 분석 방지

같은 원인을 반복해서 조사하지 않는다.

분석 과정에서 확인한 사실과
검증되지 않은 가설을 구분한다.

같은 실패가 반복되면
새로운 가설과 검증 방법을 먼저 정리한다.

새로운 근거 없이 같은 명령이나
파일 탐색을 반복하지 않는다.

추가 분석이 해결 가능성을 높이지 못하면
현재까지 확인한 사실과 막힌 원인을 보고한다.

## 3. Bug Fix Loop 방지

기존 버그를 수정하기 전에
재현 조건을 확인한다.

가능하면 실패하는 테스트를 먼저 작성한다.

수정 후에는 관련 회귀 테스트를 실행한다.

새로운 오류가 발생하면
수정 범위를 무작정 확대하지 않는다.

## 4. 정형 검증 검토 조건

다음 상황에서는 정형 검증 필요성을 검토한다.

- 공유 상태와 동시성
- 취소와 재시작
- 네트워크 재시도
- 중복 요청과 멱등성
- 작업 큐와 자원 소유권
- 결제·예약·재고 상태 전이
- 특정 순서에서 반복 발생하는 오류

## 5. 정형 검증 절차

1. 검증할 불변식을 정의한다.
2. 상태와 실행 범위를 명시한다.
3. 실제 설치된 검증 도구를 확인한다.
4. 필요한 경우 상태 모델을 작성한다.
5. 모델 검사 또는 증명 도구를 실행한다.
6. 발견한 반례를 실제 코드에서 재현한다.
7. 최소 범위로 수정한다.
8. 기존 테스트와 검증을 다시 실행한다.

## 6. 검증 비용 관리

단순 UI 수정에는 정형 검증을 실행하지 않는다.

검증 예상 비용과 범위를 먼저 판단한다.

검증이 과도하게 길어지면
현재 진행 상황과 남은 문제를 보고한다.

## 7. 금지 사항

검증을 통과시키기 위해
불변식을 약화하지 않는다.

검증하지 않은 부분을
검증 완료라고 보고하지 않는다.

원인을 모른 채 반복적으로 코드를 수정하지 않는다.

## 8. 결과 보고

다음 항목을 정리한다.

- 실제 수정한 내용
- 확인한 원인
- 실행한 테스트
- 정형 검증 여부
- 검증한 불변식
- 발견한 반례
- 검증하지 못한 항목

이 지침은 두 가지 문제를 동시에 고려한다.

첫 번째는 Reasoning Loop다.

같은 파일과 가설을 반복해서 조사하는 상황에서 새로운 근거가 있는지 확인하도록 한다.

두 번째는 Bug Fix Loop다.

실패 조건을 재현하고 테스트와 검증을 남겨 같은 버그가 다시 발생하지 않도록 돕는다.

정형 검증은 모든 작업에 적용하는 것이 아니라 특정 위험 조건에서 선택적으로 사용하도록 설정했다.

이 점이 중요하다.

검증 도구를 많이 사용하는 것보다 필요한 곳에서 제대로 사용하는 편이 더 효율적일 수 있다.

17. 정형 검증과 함께 필요한 것은 컨텍스트 엔지니어링이다

Reasoning Loop와 Bug Fix Loop를 줄이기 위해 정형 검증만 사용할 필요는 없다.

오히려 먼저 확인해야 할 부분이 있다.

AI가 기존 프로젝트의 중요한 정보를 제대로 이해하고 있는지다.

예를 들어 다음과 같은 규칙이 있다고 생각해보자.

취소된 작업은 다시 실행하지 않는다.

작업 ID가 다른 응답은 무시한다.

기존 Public API는 변경하지 않는다.

네트워크 재시도는 중복 요청을 만들면 안 된다.

이런 규칙을 AI에게 전달하지 않으면 코드를 수정하는 과정에서 놓칠 수 있다.

따라서 프로젝트 지침과 아키텍처 문서, 관련 테스트를 통해 중요한 정보를 제공해야 한다.

이를 컨텍스트 엔지니어링이라고 부른다.

또 AI가 어떤 순서로 작업을 수행하는지도 중요하다.

요구사항 확인
      ↓
영향 범위 분석
      ↓
검증할 규칙 확인
      ↓
작은 범위로 수정
      ↓
빌드 및 테스트
      ↓
필요 시 정형 검증
      ↓
결과 보고

이런 실행 절차를 관리하는 구조를 흔히 Harness라고 부른다.

같은 AI 모델이라도 파일 탐색 방식, 도구 호출, 테스트 실행, 컨텍스트 관리에 따라 결과가 달라질 수 있다.

그래서 바이브 코딩의 반복 문제를 줄이려면 다음 세 가지가 함께 필요하다.

컨텍스트 엔지니어링
         +
테스트와 실행 절차
         +
선택적 정형 검증

컨텍스트 엔지니어링은 AI가 기존 구조를 이해하도록 돕는다.

테스트는 실제 코드가 기대한 대로 동작하는지 확인한다.

정형 검증은 복잡한 상태와 실행 순서에서 특정 규칙이 유지되는지 더 엄밀하게 확인한다.

어느 하나가 나머지를 완전히 대체하지는 않는다.

마치며 — AI가 오래 생각하는 것보다 중요한 것은 문제를 좁히는 능력이다

바이브 코딩으로 프로그램을 만드는 속도는 계속 빨라지고 있다.

하지만 프로젝트가 커질수록 다른 문제가 나타난다.

버그를 수정했는데 또 다른 오류가 생기고, AI는 다시 코드를 분석한다.

분석이 길어지면 더 많은 시간과 토큰이 소비된다.

이 과정이 반복되면 개발 속도는 처음보다 훨씬 느려질 수 있다.

여기서 중요한 것은 두 가지 Loop를 구분하는 것이다.

Bug Fix Loop는 기존 규칙을 깨뜨리는 코드 변경과 재작업의 문제다.

Reasoning Loop는 원인을 충분히 좁히지 못한 채 분석이 반복되는 문제다.

정형 검증은 특히 첫 번째 문제에서 도움이 될 수 있다.

중요한 불변식을 정의하고, 이를 깨뜨리는 실행 순서를 찾고, 실제 코드에서 반례를 재현할 수 있기 때문이다.

이런 근거가 확보되면 두 번째 문제에서도 추측을 줄이고 분석 방향을 좁히는 효과를 기대할 수 있다.

하지만 정형 검증이 AI의 추론 속도를 직접 높여주는 것은 아니다.

오히려 검증 과정에는 추가적인 시간과 토큰이 필요하다.

따라서 모든 작업에서 사용하는 것은 비효율적일 수 있다.

이번 Anthropic과 Theorem의 연구는 AI를 활용한 정형 검증의 가능성을 보여줬다.

Claude Code와 Codex에서 사용할 수 있는 커뮤니티 스킬도 등장했다.

그러나 이를 도입할 때 가장 먼저 해야 할 일은 새로운 스킬을 설치하는 것이 아니다.

프로그램에서 절대로 깨지면 안 되는 규칙이 무엇인지 정의하는 것이다.

그리고 AI가 반복해서 추측하고 수정하는 대신 검증 가능한 문제로 바꿔 접근하도록 만드는 것이다.

결국 AI 코딩의 생산성은 얼마나 많은 코드를 작성했느냐만으로 결정되지 않는다.

얼마나 적은 재작업으로, 기존 기능을 유지하면서, 안정적인 결과를 완성할 수 있는지가 중요하다.

AI에게 필요한 것은 무조건 더 오래 생각하는 능력이 아니라, 언제 충분히 생각했고 무엇을 검증해야 하는지 판단하는 능력일지도 모른다.

참고자료

Anthropic — AI를 활용한 대규모 정형 검증 연구

2026년 10월 22일 발표. 123개 라이브러리의 239개 진입점에 대한 검증, 기계어 수준 안전성 증명, 기존 테스트에서 놓친 버그 발견 사례를 설명한다.

LLMs are making formal software verification feasible at a much larger scale

Theorem — OSS Verify 공개 증명

공개된 정형 검증 결과와 검증 범위, RISC-V 및 운영체제 모델을 확인할 수 있다.

OSS Verify Proofs

Theorem — 오픈소스 검증 신청

오픈소스 프로젝트 유지관리자를 위한 검증 신청 경로.

Theorem 공식 안내

Opum AI — proof-skills

Claude Code용 TLA+·Lean 정형 검증 스킬. 버그 재현, 모델 검사, 평가 결과와 실행 비용을 설명한다.

proof-skills GitHub

Michael Denyer — agent-formal-verify

Claude Code·Codex·Pi에서 사용하는 정형 검증 플러그인. TLA+·Lean·Kani 도구와 설치 방법을 설명한다.

agent-formal-verify GitHub

Swift Evolution — Actors

Swift Actor Reentrancy와 await 전후의 상태 변경 문제를 설명한다.

Swift Evolution SE-0306

TLA+ — TLC 모델 검사

상태 전이와 실행 순서를 모델링하고 TLC로 검증하는 기본 개념을 설명한다.

TLA+ By Example

Lean — 증명 검증 가이드

미완성 증명과 추가 가정, 검증 결과를 확인하는 방법을 설명한다.

Validating a Lean Proof