AI 코딩 루프를 위한 형식 검증 게이트 (Formal Verification Gates)

가장 심각한 소프트웨어 버그 중 일부는 가장 지루한 것들입니다. 사용자가 다른 테넌트(tenant)의 데이터를 읽을 수 있어서는 안 됩니다. 이에 반대하는 사람은 아무도 없으며, 설계 검토(design review)에서 Alice가 Bob의 기록을 읽는 것을 옹호하며 일어서는 사람도 없습니다. 그럼에도 불구하고 깨진 접근 제어(broken access control)는 여전히 OWASP Top 10의 1위 카테고리로 남아 있습니다.

이러한 버그들이 배포되는 이유는 규칙이 시스템의 잘못된 부분에 배치되었기 때문입니다. 규칙은 프롬프트(prompt)에, 리뷰 체크리스트(review checklist)에, 혹은 미래의 모든 엔지니어와 이제는 미래의 모든 모델 호출(model invocation)이 불변량(invariant)을 기억하고 이를 올바르게 재적용할 것이라는 공유된 기대 속에 존재합니다.

그 가정은 이미 취약했으며, AI가 대부분의 코드를 생성함에 따라 완전히 실패하고 있습니다. CLAUDE.md에 규칙을 넣거나, 신중한 시스템 프롬프트(system prompt)를 작성하고, 에이전트(agent) 지침에 "권한 부여(authorization)는 매우 중요합니다"를 추가하는 등 명백한 조치들을 모두 취할 수 있으며, 실제로 그렇게 해야 합니다. 하지만 모델이 16,000줄의 코드를 작성한 후에도 진짜 질문은 여전히 남아 있습니다: 코드가 당신이 원하는 대로 작동한다는 것을 어떻게 알 수 있습니까? 테스트(test)가 도움이 되지만, 테스트는 경험적(empirical)입니다. 테스트는 당신과 모델이 작성하기로 기억한 케이스들을 확인하며, 다음 주에 누군가가 추가할 핸들러(handler)에 대해서는 말해줄 수 없습니다.

저는 다른 레버를 당기고 싶습니다. 솔직하게 말씀드리는 저의 베팅은 이것입니다: 광범위한 범주의 프로덕션 소프트웨어(production software)에 있어, 구조적 백프레셔(structural backpressure)는 에이전트 지능의 점진적인 개선보다 더 효과적입니다. 기존 모델들은 이미 당신의 코드 거의 전부를 작성할 수 있습니다. 제한 요소는 그들이 당신이 원하는 대로 수행했는지 당신이 알 수 있느냐 하는 것이며, 그 지식은 더 똑똑한 모델을 기다리는 것이 아니라 그들이 작성하는 기질(substrate)로부터 나옵니다.

Shen-Backpressure는 그 베팅을 탐구하기 위해 제가 구축한 도구이자 방법론입니다. 실행 중인 데모를 통해 그것이 무엇을 하는지 보여드린 후, 동일한 루프를 당신의 프로젝트에 연결하는 방법을 보여드리겠습니다.

행동 게이트(Behavioral Gates) 및 구조적 게이트(Structural Gates)

대부분의 프롬프트 수준 제약 조건은 *행동 게이트 (behavioral gates)*입니다. 우리는 모델에게 "인증을 건너뛰지 마세요", "입력을 검증하세요", "공유된 헬퍼 (helper)를 사용하세요"라고 지시합니다. 모델은 유용할 정도로 충분히 자주 이 지침을 따르기도 하지만, 전체 구조를 불안정하게 만들 정도로 충분히 자주 실패하기도 합니다. 행동 게이트는 모델이 규칙을 기억하고, 그것이 적용되는 위치를 인식하며, 국소적 문맥 (local context)의 중력적 인력에 저항하는 능력, 그리고 인간 검토자가 전체 코드베이스에 걸쳐 동일한 불변량 (invariant)을 유지하는 능력에 의존합니다.

*구조적 게이트 (Structural gates)*는 다릅니다. 컴파일러 (compiler), 타입 체커 (type checker), 테스트 러너 (test runner), 린터 (linter), 증명 검사기 (proof checker) 등이 이에 해당합니다. 각각은 눈앞에 있는 산출물 (artifact)에 대해 구체적인 답을 내놓습니다. 그 답이 완벽하지는 않더라도 실재하며, 자신의 범위 내에서 코드가 틀렸을 경우 거부합니다.

그 거부야말로 핵심입니다. 이를 통해 우리는 작업을 모델의 지시 공간 (instruction space)에서 모델이 구축하고 있는 기질 (substrate)로 옮길 수 있습니다. 모델에게 불변량을 기억해 달라고 애원하며 토큰을 소비하는 대신, 실수로 불변량을 위반하기 어렵도록 코드를 구성하는 것입니다. 즉, 가장 중요하게 생각하는 속성을 가져와 기계가 검사할 수 있는 형태로 표현하고, 이를 구현 단계에 투영하며, 창발적인 산출물이 이를 만족할 때까지 루프가 해당 검사 단계에서 튕겨져 나오게(bounce off) 만드는 것입니다.

이것이 바로 Geoff Huntley의 Ralph 및 에세이 'Don’t Waste Your Backpressure'에서 사용된 의미에서의 백프레셔 (backpressure)를 강력하게 만드는 요소입니다. 이전의 오류가 다음 반복 (iteration)으로 전달될 때, 결정론적인 게이트 (deterministic gate)는 루프가 단순한 느낌 (vibes)보다 더 확고한 무언가를 바탕으로 밀어붙일 수 있게 해줍니다. 이제 이 루프는 더 이상 틈새 아이디어가 아닙니다. Codex CLI는 이제 Ralph 루프에 대한 OpenAI만의 해석인 /goal 기능을 탑업하여 제공하며, 목표가 달성될 때까지 멈추기를 거부하고 턴 (turn) 전반에 걸쳐 목표를 유지합니다.

기질로의 이동 (The Substrate Move)

강제할 가치가 있는 불변량들은 대개 정확하게 기술하기 쉽습니다. "사용자는 인증되었고, 테넌트 (tenant)의 구성원이며, 해당 리소스가 그 테넌트에 속해 있는 경우에만 리소스에 접근할 수 있다." 이것은 완전하고 경계가 명확한 규칙입니다. 영어는 단지 이를 *강제 (enforce)*하기에 적절하지 않은 매체일 뿐입니다.

Shen-Backpressure는 시퀀트 계산 (sequent-calculus) 타입 시스템을 갖춘 작고 정적 타입이 지정된 Lisp인 Shen을 사용하여, 기계가 기질 (substrate)로 투영할 수 있는 형태, 즉 모델이 작성해야 하는 대상 언어의 타입 (types), 생성자 (constructors), 그리고 게이트 명령 (gate commands)의 형태로 그러한 규칙을 작성합니다. 사양 (spec)을 한 번 작성하면, 코드 생성기 (shengen)가 이를 대상 언어의 가드 타입 (guard types)으로 낮춥니다 (lowers). Go나 TypeScript를 작성하는 모델은 Shen의 존재를 알 필요가 없습니다. 모델에게 필요한 것은 코드가 컴파일되고 게이트를 통과하는 것뿐입니다.

멀티 테넌트 인증을 위한 증명 체인 (A Proof Chain For Multi-Tenant Auth)

다음은 멀티 테넌트 API 데모의 핵심인 specs/core.shen의 발췌본입니다:

(datatype jwt-token X : string; (not (= X "")) : verified; ============================ X : jwt-token;)
(datatype tenant-access Principal : authenticated-principal; Tenant : tenant-id; IsMember : boolean; (= IsMember true) : verified; ================================ [Principal Tenant IsMember] : tenant-access;)
(datatype resource-access Access : tenant-access; Resource : resource-id; IsOwned : boolean; (= IsOwned true) : verified; ================================ [Access Resource IsOwned] : resource-access;)

가로선이 핵심적인 역할을 수행합니다. 선 아래의 결론 (conclusion)이 구성되기 전에 선 위의 전제 (premises)들이 반드시 충족되어야 합니다. resource-access를 얻으려면 tenant-access가 필요하고 해당 리소스가 소유되었음을 증명해야 하며, tenant-access를 얻으려면 인증된 주체 (authenticated principal)와 멤버십 증명이 필요합니다. 전체 체인은 jwt-token → authenticated-user → tenant-access → resource-access로 실행됩니다. 중간 규칙들에 대한 전체 사양을 참조하십시오.

이러한 타입들은 증인 (witnesses)입니다. 이들 중 하나의 값을 구성하려면 해당 규칙에 선언된 전제들을 해소 (discharging)해야 합니다.

사양에서 가드 타입으로 (From Spec To Guard Types)

shengen은 각 규칙을 대상 언어의 가드 타입 (guard type)으로 낮춥니다. Go의 경우, 필드들은 외부로 노출되지 않으며 (unexported), 생성된 생성자 (constructor)가 이를 채울 수 있는 유일한 방법입니다:

type TenantAccess struct { principal AuthenticatedPrincipal tenant TenantId isMember bool}
func NewTenantAccess(principal AuthenticatedPrincipal, tenant TenantId, isMember bool) (TenantAccess, error) { if !(isMember == true) { return TenantAccess{}, fmt.Errorf("isMember must equal true") } return TenantAccess{principal: principal, tenant: tenant, isMember: isMember}, nil}

여기에 특별한 기교는 없으며, 일반적인 Go의 가시성 (visibility) 규칙일 뿐입니다. 패키지 외부의 코드는 필드들이 소문자로 시작하기 때문에 TenantAccess{isMember: true}와 같이 작성할 수 없습니다. 생성자 (constructor)가 값이 채워진 객체로 가는 유일한 경로이며, 이 생성자는 isMember == false인 경우를 거부합니다.

authenticated-principal과 같은 합 타입 (Sum types) 도 동일한 방식으로 봉인된 인터페이스 (sealed interface)를 갖게 됩니다. 생성된 가드 (guards)를 확인해 보세요.

이 포스트 전반에 걸쳐 Go를 예시로 사용하고 있지만, 개념과 도구는 Go에 국한되지 않습니다. 현재 Go와 TypeScript가 프로덕션 대상이며, Python과 Rust를 위한 참조 에미터 (reference emitters)도 제공됩니다. 대상 언어는 실제적인 트레이드오프 (tradeoffs)가 존재하는 선택 사항입니다. 봉인 (seal)의 강도는 해당 언어가 제공하는 캡슐화 (encapsulation)만큼 강력하며, 에이전트 (agents) 또한 언어 중립적이지 않습니다.

스마트 생성자 (Smart constructors)는 오래된 개념입니다. 타입 래퍼 (Type wrappers)도 오래되었습니다. 코드 생성 (Codegen) 역시 오래되었습니다. 유용한 움직임은 이들을 루프 (loop) 안에 배치하여, 생성되는 강제 코드 (enforcement code)보다 더 짧고 검토하기 쉬운 명세 (spec)로부터 파생된 단일 거부 표면 (refusal surface)으로 만드는 것입니다.

수동 작성된 체크 없는 권한 부여 (Authorization)

멀티 테넌트 (multi-tenant) 핸들러를 작성하는 일반적인 방법은 모든 엔드포인트 (endpoint)에 if 문을 넣는 것입니다:

if !user.IsMemberOf(tenantID) { http.Error(w, "forbidden", http.StatusForbidden) return}

이 패턴은 합리적이며, 바로 그러한 합리적인 방식 때문에 일곱 번째 핸들러나 세 번째 리팩터링 (refactor) 과정에서 잊히곤 합니다. Shen-Backpressure 버전에서도 멤버십 체크 (membership check)는 여전히 존재합니다. 여전히 데이터베이스 쿼리가 존재하지만, 이는 관습적으로 핸들러 곳곳에 흩어져 있는 대신 TenantAccess의 생성 경계 (construction boundary)에 집중되어 있습니다.

isMember := exists > 0access, err := shenguard.NewTenantAccess(principal, tenantID, isMember)if err != nil { return shenguard.TenantAccess{}, fmt.Errorf("tenant access denied: %s is not a member of %s", userID, tenantID.Val())}

그 후 핸들러는 이미 탐색된 체인을 나타내는 (represents the already-traversed chain) 값을 바탕으로 동작합니다. 증명(proof)이 값과 함께 이동합니다. 실행 중인 데모에서 Acme의 멤버인 Alice는 Acme의 리소스를 나열할 수 있지만, Globex의 리소스 요청은 거부됩니다:

=== Alice requests Globex resources (NOT member - should fail) ===tenant access denied: user u-alice is not a member of tenant t-globex

만약 에이전트가 체인을 건너뛰고 가공되지 않은 값(raw value)을 전달하려고 시도하면, 바이너리가 생성되기 전에 빌드가 실패합니다:

cannot use tenantID (variable of type string) as shenguard.TenantId value in argument to CheckTenantAccess: string does not implement shenguard.TenantId (missing method Val)

이 짧고 기계적인 "안 돼(no)"라는 응답이 바로 백프레셔 (backpressure)입니다. 저는 프롬프트에 들어가는 긴 문단보다, 이런 응답이 더 많아지기를 바랍니다.

시도해보기

데모는 처음부터 끝까지 읽을 수 있도록 설계되었습니다. 리포지토리 (repo)를 클론하고 examples/multi-tenant-api/를 여세요.

: 여기에는 명세 (spec), 생성된 가드 (guards), 이를 구축한 Ralph 루프 (cmd/ralph/), 그리고 demo.md에 포함된 curl 트랜스크립트 (transcript)가 들어 있습니다.

자신의 프로젝트에 연결하려면 sb CLI를 설치하고 다음을 실행하세요:

sb init # scaffold specs/core.shen + the gate scripts, # install /sb:* commands into .claude/sb loop # run the Ralph loop with gate-driven backpressure

sb init은 시작용 명세와 가드 스크립트를 스캐폴딩 (scaffold)하며, -config 옵션을 사용하면 sb.toml 매니페스트 (manifest)도 함께 스캐폴딩합니다. 루프의 매 반복은 sb.toml에 선언된 고정된 가드 세트를 실행합니다:

가드 (Gate)	명령 (Command)	포착 내용 (Catches)
shengen	sb gen	Shen 명세와 생성된 가드 사이의 드리프트 (Drift)
...

이 다섯 가지가 기본 세트입니다. sb에는 선택 사항이며 아직 실험적인 여섯 번째 가드 (shen-derive)도 있습니다.

, (사양-동등성 테스트 (spec-equivalence testing)를 위한) 명시적으로 설정된 경우에만 실행됩니다. 게이트 (gate)가 실패하면, 그 실패 결과가 구체적인 컨텍스트 (context)로서 다음 프롬프트 (prompt)로 전달됩니다. 이것이 바로 백프레셔 (backpressure)입니다. 루프를 수동으로 제어하고 싶다면 반복 (iteration) 사이에 직접 sb gates를 실행할 수 있습니다. 하네스 (harness)는 교체 가능합니다. Claude Code (cla -p)가 기본값이며, Cursor, Codex 등은 RALPH_HARNESS를 설정하여 사용할 수 있습니다. 게이트 4를 위해서는 Shen 런타임 (runtime)이 필요합니다: brew tap Shen-Language/homebrew-shen && brew install shen-sbcl. sb init -lang ts는 단순히 코드 생성 (codegen)뿐만 아니라 TypeScript를 위한 전체 게이트 루프 (gate loop)를 연결합니다. 이는 Go와 함께 완전한 타겟 (target)입니다. 또한 /sb:* 명령은 sb init 시 .claclaude/에 설치되며, 여기에는 새로운 타겟 언어를 위한 shengen 에미터 (emitter)를 생성하기 위한 완전한 프롬프트인 /sb:create-shengen이 포함되어 있습니다.

비용 및 한계

사양 (spec)을 작성하는 것은 공짜가 아닙니다. 어떤 불변량 (invariants)을 인코딩할 가치가 있는지 결정하고, 읽기 쉬우면서도 투영 가능한 (projectable) 표기법으로 이를 표현하며, 생성기 (generator)와 감사 (audit) 스크립트를 유지 관리해야 합니다. 생성된 가드 (guard) 코드는 신성합니다. 이를 수동으로 편집하면 감사 게이트 (audit gate)가 이를 거부합니다. 이제 당신의 신뢰 컴퓨팅 기반 (trusted computing base)에는 Shen 타입 체커 (type checker), 생성기, 그리고 타겟 컴파일러 (target compiler)가 포함됩니다.

그리고 이것이 우회 (bypasses)를 불가능하게 만드는 것은 아닙니다. 바로 이 지점에서 타겟 언어의 트레이드오프 (tradeoffs)가 명확하게 드러납니다. Go에서는 가드 패키지 (guard package) 내부의 코드가 값을 위조할 수 있습니다. 리플렉션 (reflection)과 제로 값 (zero values)이 이론적으로 탈출구 (escape hatches)로서 존재하기 때문입니다. 부주의한 SQL 쿼리는 생성자 (constructor)에 true를 전달할 수 있습니다.

그렇게 해서는 안 됩니다. 저의 주장은 의도적으로 좁은 범위를 설정하고 있습니다. shengen을 사용하여 명세 증명 (spec proofs)을 대상 언어로 낮추는 것은, 지정된 불변량 (invariants)을 실수로 우회하는 것을 실질적으로 불가능하게 만드는 것이지, 우회하는 것 자체가 범주적으로 불가능하게 만드는 것이 아닙니다. 형식 방법론 (formal-methods)을 다루는 청중에게는 평범하고 상당히 약한 주장일 수 있습니다. 하지만 LLM이 생성한 코드를 배포하는 실무자에게 이것은 매우 강력한 레버리지 (leverage)를 가진 도구입니다. 이제 잊혀진 체크, 유출된 테넌트 ID (tenant ID), 그리고 복사되었지만 불완전한 핸들러 (handler) 등은 모두 실수로 도입하기에 구조적으로 어렵고 비용이 많이 드는 작업이 됩니다.

명세 (spec) 자체가 틀릴 수도 있고, 생성기 (generator)가 표류할 수도 있으며, 테스트는 여전히 케이스를 놓칠 수 있습니다. 이러한 한계들을 명시하는 것은 도구를 이해하고, 도구가 제공하는 것을 절제된 방식으로 활용하기 위해 중요합니다.

이러한 게이트 (gates)를 설치하는 비용 자체도 낮아지고 있습니다. 명세를 작성하고, 에미터 (emitter)를 만들고, 감사 스크립트 (audit script)를 작성하는 것은 모델들이 계속해서 더 잘해내고 있는 바로 그 작업입니다. 더 나은 모델이 나온다고 해서 기질 (substrate)이 불필요해지는 것이 아니라, 그것을 건너뛰는 것을 정당화하기 더 어렵게 만듭니다.

논지 (The Thesis)