AI 코딩 루프에 Formal Verification Gate 적용하기

Who Should Read

AI 코딩 에이전트를 프로덕션에 활용하고 싶은데, 생성된 코드의 보안 규칙 준수 여부를 검증하기 어려워 고민 중인 백엔드/풀스택 개발자.

Core Mechanics

• OWASP Top 10 1위인 '잘못된 접근 제어' 같은 심각한 버그는 규칙을 잘못된 위치(프롬프트, 리뷰 체크리스트)에 두기 때문에 발생한다. AI가 대부분의 코드를 생성하는 지금, 이 문제는 더 심각해졌다.
• 프롬프트에 'authorization IS VERY IMPORTANT'처럼 지시하는 방식은 '행동 게이트(behavioral gate)'로, 모델이 규칙을 기억하고, 적용 시점을 인식하고, 로컬 컨텍스트의 유혹을 이겨내야 한다. 모델은 이걸 자주 까먹는다.
• 컴파일러, 타입 체커, proof checker 같은 '구조적 게이트(structural gate)'는 아티팩트 자체를 검사해 pass/fail을 명확하게 돌려준다. 모델이 기억할 필요 없이 코드가 틀리면 그냥 컴파일이 안 된다.
• 핵심 아이디어는 'substrate move'다. 지키고 싶은 불변식을 기계가 검사할 수 있는 형태(타입, guard 타입)로 표현해서 모델이 작성하는 코드의 기반에 심어두면, 에이전트 루프가 그 체크에 부딪혀 스스로 고치게 된다.
• 저자가 만든 도구 Shen-Backpressure는 Shen이라는 정적 타입 Lisp으로 불변식 스펙을 작성하면, shengen이라는 코드 제너레이터가 Go나 TypeScript 같은 실제 타겟 언어의 guard 타입으로 변환해준다. 모델은 Shen을 몰라도 된다.
• 멀티테넌트 API 예제에서는 'jwt-token', 'tenant-access' 같은 타입을 Shen으로 정의하고, 이 타입이 컴파일되려면 인증·테넌트 멤버십·리소스 소속을 모두 충족해야 한다. 조건 하나라도 빠지면 컴파일 자체가 안 된다.
• 이 접근법은 Geoff Huntley의 'backpressure' 개념(이전 에러를 다음 반복에 피드백하는 루프)을 활용한다. OpenAI Codex CLI의 /goal 기능도 같은 원리로, 목표가 달성될 때까지 루프를 유지한다.
• 저자의 핵심 주장: 더 똑똑한 모델을 기다리는 것보다, 모델이 작성하는 기반(substrate)을 잘 만드는 게 더 빠른 해결책이다. 기존 모델도 코드는 잘 쓴다. 문제는 '원하는 대로 썼는지 아는 것'이다.

Evidence

• DevOps 실무자의 경험 공유: LLM 도입 단계가 '많이 시키기 → 멀티 에이전트 → 에이전트가 도구 빌드 → 결정론적 도구 + 인간도 사용 가능한 도구'로 수렴했다고 한다. 결정론적 도구는 바이너리 결과를 주고 반복 가능하며, LLM이 2~3분 걸리던 작업을 스크립트로 30초 안에 처리할 수 있었다는 경험담.
• 가장 날카로운 기술적 반론은 JWT 예제의 허점을 지적한 댓글이다. 제시된 스펙에서 jwt-token 검증이 '문자열이 비어있지 않다'만 확인할 뿐, 실제 파싱·만료 검사·신뢰된 키 서명 확인은 없다는 것. AI가 생성자(constructor)를 직접 호출할 수 있으면 `(tenant-access user-id tenant-id true)`처럼 멋대로 '증명'을 만들 수 있어 보안 의미가 퇴색한다는 지적.
• 위 반론에 대한 종합적 평가도 올라왔다. '타입에 규칙을 넣는 방식은 프롬프트 규칙이 컨텍스트 윈도우 밖으로 밀려나는 순간 사라지는 것과 달리 영속적이고 리뷰 가능하다'는 장점은 인정하면서도, '컴파일러는 네가 인코딩한 것을 강제하지 네가 의도한 것을 강제하지 않는다'는 한계도 솔직하게 짚었다. 결론적으로 어려운 판단이 사라지는 게 아니라 '타입 정의 시점'으로 주소가 바뀌는 것이라는 평가.
• SQL 위에 타입 시스템을 올려서 에이전트 문제를 해결한 실무 경험도 공유됐다. 타입 도구가 에이전트 게이트 역할도 하지만, 에이전트가 복잡한 데이터 인프라를 더 적은 토큰으로 이해하는 추상화 도구로도 쓸 수 있다는 이중 효용을 언급.
• Rust 사용자로부터 'Rust의 private field, newtype, constructor로 이미 쉽게 구현 가능한데 이 도구가 무엇을 더 주냐'는 질문이 있었다. 비슷하게 Liquid Haskell(refinement type)이나 Lean(dependent type)을 쓰면 사이드카 없이 바로 프로그램에 불변식을 넣을 수 있다는 대안도 제시됐다.

How to Apply

• 멀티테넌트 SaaS를 개발 중이고 AI 에이전트가 인증/인가 코드를 많이 생성한다면, 테넌트 접근 조건(인증됨 + 멤버 여부 + 리소스 소속)을 guard 타입으로 정의하고 해당 타입 없이는 API 핸들러가 컴파일되지 않도록 구조를 잡아라. CLAUDE.md에 규칙을 적는 것보다 훨씬 강력하게 에이전트를 제약할 수 있다.
• Shen-Backpressure(github.com/pyrex41/Shen-Backpressure) 대신 이미 쓰고 있는 언어의 타입 기능을 활용하는 것도 동일한 효과다. Rust라면 newtype + private field + 검증 로직이 담긴 생성자, TypeScript라면 branded type으로 동일한 구조적 게이트를 만들 수 있다.
• AI 에이전트 루프를 구성할 때, 에이전트가 생성한 코드를 `cargo build` 또는 `tsc --noEmit` 같은 컴파일/타입 체크 결과와 함께 다음 반복에 피드백하는 구조를 만들어라. Codex CLI의 /goal처럼 컴파일이 성공할 때까지 루프를 유지하면, 에이전트가 구조적 제약을 스스로 맞춰나간다.
• 결정론적 검증 도구(컴파일러, 린터, 타입 체커)를 에이전트가 직접 호출할 수 있는 MCP 도구 또는 스크립트로 노출시켜라. 에이전트가 2~3분 고민해서 '아마도 맞을' 코드를 내놓는 대신, 30초짜리 검증 스크립트를 반복 실행하며 확정적 피드백을 받게 할 수 있다.

Code Example

-- specs/core.shen 예시 (Shen-Backpressure 스펙 파일)

-- jwt-token 타입: 비어있지 않은 문자열만 허용
(datatype jwt-token
  X : string;
  (not (= X "")) : verified;
  ============================
  X : jwt-token;)

-- tenant-access 타입: 인증된 principal + tenant-id + 실제 멤버 여부가 true일 때만 타입 성립
(datatype tenant-access
  Principal : authenticated-principal;
  Tenant : tenant-id;
  IsMember : boolean;
  (= IsMember true) : verified;
  ================================
  [Principal Tenant IsMember] : tenant-access;)

-- shengen으로 타겟 언어(Go/TypeScript)의 guard 타입으로 코드 생성
-- 모델은 Shen을 몰라도 되고, 생성된 타입이 컴파일되게만 작성하면 됨

Terminology

관련 논문

• AI로 Rust 코드 100K 라인 작성하며 얻은 교훈 (2025)

  Azure RSL(분산 합의 라이브러리)을 Rust로 재구현하면서 AI 코딩 에이전트를 활용해 4주 만에 100K 라인을 작성한 경험담으로, Code Contracts와 Spec-Driven Development를 AI와 조합하는 실전 워크플로우를 공유한다.

• Forge – Guardrails로 8B 모델 성능을 53%에서 99%로 끌어올리기

  작은 로컬 LLM(8B)에 guardrails(구조적 안전망)를 씌워 멀티스텝 에이전트 작업 성공률을 53%에서 99%까지 올린 Python 프레임워크 Forge 공개. 모델 자체는 건드리지 않고 실행 환경을 강화하는 접근법이라 주목받고 있음.

• Mini Shai-Hulud 재등장: npm 패키지 314개 동시 감염 사건 분석

  2026년 5월 19일, npm 계정 하나가 탈취되어 22분 만에 637개 악성 버전이 배포됐고, echarts-for-react·size-sensor 등 월 수백만 다운로드 패키지들이 감염되어 AWS 자격증명·SSH 키·AI 코딩 에이전트까지 탈취하는 정교한 공급망 공격이 발생했다.

• Semble – AI 에이전트용 코드 검색 도구, grep 대비 토큰 98% 절감

  AI 에이전트가 코드베이스를 탐색할 때 grep+파일 읽기 대신 자연어로 관련 코드 스니펫만 뽑아주는 검색 라이브러리로, 토큰 사용량을 약 98% 줄여준다.

• Zerostack – 순수 Rust로 작성된 Unix 철학 기반 코딩 에이전트

  Claude Code나 OpenCode처럼 메모리를 수 GB씩 잡아먹는 코딩 에이전트 대신, Rust로 만든 초경량(~8MB RAM) 코딩 에이전트 Zerostack이 공개됐다. 저사양 환경에서도 쓸 수 있고, 직접 만든 유사 프로젝트들과 비교 토론이 활발하게 이뤄지고 있다.

• Δ-Mem: LLM을 위한 효율적인 온라인 메모리 메커니즘

  LLM의 컨텍스트 윈도우를 늘리지 않고도 과거 정보를 효율적으로 기억할 수 있는 경량 메모리 모듈 δ-mem을 제안한 논문. 모델 자체를 바꾸거나 파인튜닝 없이 기존 LLM에 붙여서 장기 기억 성능을 높일 수 있어 에이전트 시스템 개발자에게 관심을 끌고 있다.

Related Resources

• https://reubenbrooks.dev/blog/structural-backpressure-beats-smarter-agents/
• https://github.com/pyrex41/Shen-Backpressure
• https://spawn-queue.acm.org/doi/10.1145/3194653.3197520