Formal Verification Gates for AI Coding Loops

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

Related Papers

• Show HN: ctx – Search the coding agent history already on your machine

  Claude Code, Cursor, Codex 등 코딩 에이전트가 이전 세션의 논의·결정·실패 시도를 잊지 않도록 SQLite로 인덱싱해 재사용할 수 있게 해주는 오픈소스 CLI 도구다.

• Micro-Agent: Beat Frontier Models with Collaboration Inside Model API

  vLLM 팀이 단일 모델 API 호출 뒤에서 여러 모델이 협업하는 'Micro-Agent' 개념을 공개했습니다. 별도의 에이전트 코드 없이 라우터 레이어에서 모델 조합을 실행해 GPT-4급 결과를 더 저렴하게 낼 수 있다는 아이디어입니다.

• Ornith-1.0: self-improving open-source models for agentic coding

  Gemma 4와 Qwen 3.5를 기반으로 파인튜닝한 코딩 특화 오픈소스 모델로, RL(강화학습)을 통해 스캐폴드(에이전트 실행 구조)까지 함께 최적화하는 방식을 주장하지만, 커뮤니티에서는 벤치마크 과최적화에 불과하다는 의심을 받고 있다.

• Entity Binding Failures in Tool-Augmented Agents

  AI 에이전트가 올바른 도구를 선택해도 잘못된 대상에 실행하는 'Entity Binding 실패' 문제를 정의하고, 이를 막는 실행 정책을 평가한 논문.

• Herdr: Agent multiplexer that lives in your terminal

  여러 AI 코딩 에이전트(Claude, Codex 등)를 하나의 터미널에서 동시에 실행·관리할 수 있는 Rust 기반 오픈소스 툴로, tmux처럼 세션이 유지되고 SSH로 원격 접속도 가능해 멀티 에이전트 워크플로우를 크게 단순화해준다.

• Ornith-1.0: Self-scaffolding LLMs for agentic coding

  모델이 문제 풀이 전략(scaffold)을 직접 생성하고 개선하는 자기강화 학습 프레임워크를 적용한 오픈소스 코딩 특화 LLM으로, 9B 소형 모델부터 397B 대형 모델까지 라인업을 갖추고 SWE-Bench 등 주요 벤치마크에서 Claude Opus 4.7을 능가하는 성능을 보여줬다.

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