AI 코딩 루프를 위한 형식 검증 게이트

AI 에이전트가 수천 줄의 코드를 생성할 때 보안 불변 조건(invariant)을 실제로 지켰는지 확인하기 어렵다. 프롬프트에 "권한 검증은 매우 중요합니다"라고 강조해도 모델은 잊거나 건너뛸 수 있고, 테스트는 경험적이라 작성된 케이스만 검사한다.

Shen-Backpressure는 이 문제를 구조적 제약으로 해결한다. 핵심 아이디어는 행동 게이트(behavioral gate, 프롬프트로 모델에게 "~하지 말라"고 지시)가 아닌 **구조 게이트(structural gate, 컴파일러·타입 체커·증명 검사기)**를 사용하는 것이다.

작동 방식:

• Shen 언어로 불변 조건을 형식 명세로 작성 (예: "사용자는 인증되고, 테넌트 멤버이며, 리소스가 해당 테넌트 소유일 때만 접근 가능")
• shengen 코드 생성기가 이를 타겟 언어(Go, TypeScript 등)의 가드 타입(guard type)으로 변환
• 생성된 타입은 봉인되어 있어 올바른 증명 없이 생성 불가 (Go의 경우 unexported field + 스마트 생성자)
• AI 에이전트가 증명 체인을 건너뛰면 빌드 실패

5개 게이트로 구성된 검증 루프:

1. shengen: Shen 명세와 생성 코드 간 동기화 검사
2. test: 런타임 불변 조건 및 회귀 테스트
3. build: 타입 불일치, 잘못된 증명 체인 사용 검출
4. shen tc+: Shen 명세 내부 일관성 검사
5. tcb audit: 생성된 가드 코드 수동 편집 검출

게이트 실패는 다음 프롬프트에 구체적 컨텍스트로 피드백되어 Ralph 루프 스타일의 **백프레셔(backpressure)**를 형성한다. Claude Code, Cursor, Codex 등과 통합 가능하며 sb init로 프로젝트에 설치할 수 있다.

멀티 테넌트 API 데모에서는 권한 검증 로직을 각 핸들러에 if 문으로 반복하는 대신, TenantAccess 타입 생성 시점에 집중시켰다. 에이전트가 이를 우회하려 하면 컴파일 에러가 발생한다.

한계도 명확하다. 명세 작성 비용이 들고, 생성된 가드 코드를 수동 편집할 수 없으며, 타겟 언어의 캡슐화 강도에 의존한다. Go의 경우 리플렉션이나 패키지 내부 코드로 우회가 이론적으로는 가능하다. 하지만 실수로 인한 우회를 구조적으로 어렵게 만드는 것만으로도 AI 생성 코드 환경에서는 높은 레버리지를 제공한다는 것이 저자의 주장이다.