본 기사는 Hashnode에 공개한 The Rising Sea of Software Engineering — Rebuilding the Discipline on Algebraic Geometry의 일본어판입니다.

AI가 코드를 작성하는 속도는 인간이 리뷰할 수 있는 속도를 넘어서고 있습니다. 이는 예측이 아니라, 많은 개발 현장에서 느끼는 실감이라고 생각합니다.

그리고 또 하나의 실감이 있습니다. 테스트와 CI/CD를 아무리 잘 정비해도, E2E 장애는 발생합니다. 유닛 테스트(Unit Test)는 모두 통과했습니다. 통합 테스트(Integration Test)도 통과했습니다. CI는 green입니다. 그런데도 운영 환경에서 망가집니다.

저는 이 문제를 테스트의 양이나 CI의 속도 문제가 아니라, 소프트웨어 공학 자체가 따라가지 못하고 있는 문제라고 생각합니다. 이 기사는 그 진단에서 시작되는 하나의 등반 기록입니다. 하나의 정상(SAGA 정리)에 도달한 것. 그 정상에서 저 멀리 보였던 풍경. 그리고 앞으로 오를 산.

처음 접하시는 분들을 위해, 이 기사에 등장하는 것들을 미리 정리해 둡니다.

이름	내용
AAT (Algebraic Architecture Theory)	소프트웨어 아키텍처의 대수기하학적 이론. Atom을 공리로 하는 순수 수학
Atom	AAT의 공리적인 최소 단위. 코드나 언어, 라이브러리로부터 추상화된 아키텍처의 구성 요소
SAGA 정리	AAT의 중심 정리 (SAGA Grounding Theorem). 아키텍처 의미론 측의 $H^1$과 Atom이 생성하는 site 상의 실제 Čech $H^1$이 일치한다는 비교 정리. Lean 4로 증명 완료. 이름은 Serre의 GAGA에 대한 오마주
ArchSig	AAT에 기반한 Rust 제작 계측 도구. 아키텍처의 관측 데이터로부터 붙임 장애 (obstruction)를 검출함
SFT (Software Field Theory)	소프트웨어의 시간 발전을 기술하는 동역학 이론. AAT가 정역학이라면 SFT는 동역학
Lean	정리 증명 지원 시스템 (Theorem Prover). AAT / SFT의 정리는 여기서 형식 검증됨

SAGA 정리에 대해서는 이쪽으로

미리 말씀드리자면, 이 기사에는 '증명된 것', '구상', '미증명인 것'의 세 종류가 등장합니다. 이 세 가지를 섞지 않고 작성하겠습니다. 증명되지 않은 것을 증명된 것처럼 말하지 않는 것이 이 프로젝트의 방식이기 때문입니다.

기슭 — E2E 장애에는 수학적인 이름이 있다

먼저 진단부터 하겠습니다.

테스트와 CI가 보증하는 것은 **국소적인 정당성 (local correctness)**입니다. 유닛 테스트는 하나의 모듈의 단면을 검증합니다. 통합 테스트도 결국 선택된 유한한 경로를 검증하고 있습니다.

하지만 E2E 장애는 각 부분이 모두 올바른데 전체가 망가지는 형태로 발생합니다. 국소적으로는 정합적인 파편들이 대역적(globally)으로는 붙지 않는 것입니다.

수학, 특히 층 (sheaf) 이론에는 이 상황을 가리키는 정확한 용어가 있습니다. 국소 단면 (local section)이 모두 존재함에도 불구하고, 대역 단면 (global section)이 존재하지 않는다. 그리고 그 '붙임 장애'를 세는 도구가 코호몰로지 (cohomology) — 우선적으로 $H^1$입니다.

'테스트는 모두 통과했는데 운영에서 망가지는' 현상은 integration hell이라 불리며 경험칙으로 다뤄져 왔지만, 사실 정확한 수학적 이름을 가지고 있습니다. 중요한 것은 이 장애가 각 부분의 성질이 아니라, 부분과 부분의 겹침 위에 존재한다는 점입니다. 인터페이스의 암묵적인 전제, 상태의 공유, 시간적인 순서 — 이 모든 것은 단일 모듈 안에는 존재하지 않습니다. 그렇기에 테스트 커버리지(Test Coverage)를 100%로 만들어도 사라지지 않습니다. 측정하는 대상이 국소적인 한, 원리적으로 도달할 수 없습니다.

기존의 소프트웨어 공학은 '부품의 품질을 높이면 전체의 품질이 올라간다'는 암묵적인 합성 원리 위에 세워져 있습니다. 하지만 붙임 문제는 바로 그 합성이 자명하지 않다는 것을 말해줍니다. 국소의 총합은 대역이 아닙니다.

AI 주도 개발이 이 문제를 악화시키는 이유

AI 주도 개발에서 이 문제가 급격히 악화되는 것은 우연이 아닙니다.

AI는 국소적 생성에 비정상적으로 능숙하며, 게다가 각 파편은 개별적으로는 올바릅니다. 생성 속도가 올라갈수록 겹침 위의 불일치가 축적되어 갑니다.

여기서 깨달아야 할 점이 있습니다. 인간의 리뷰가 담당해 온 것은 사실 코드의 정확성을 확인하는 것이 아니었습니다. 바로 머릿속에서 붙여넣기(patching)를 검산하는 것이었습니다. "이 변경 사항이 저쪽 모듈의 전제 조건과 맞아떨어지는가?" — 리뷰어가 무의식적으로 수행하던 것이 바로 이것이었으며, 그것이 따라가지 못하게 된 것이 현장의 실체라고 생각합니다.

이 격차를 메우는 방법은 원리적으로 두 가지뿐입니다.

• 리뷰하는 측도 AI로 만든다
• 리뷰를 **판정 가능한 수학 (mathematics)**으로 만든다

전자에는 "누가 감시자를 감시할 것인가"라는 무한 소급의 문제가 뒤따릅니다. 생성물이 생성물을 검사하는 세계에서는 어떤 에이전트의 판단도 다른 에이전트의 판단 이상의 권위를 가질 수 없습니다. 저는 후자를 선택했습니다.

Rising Sea — 수위를 높여 껍질을 열다

방법에 대해 이야기하겠습니다.

Grothendieck는 대수기하학(algebraic geometry)에서 난제를 못과 망치로 억지로 열어젖히는 대신, 추상화의 수위를 높여 어느 순간 깨달으면 껍질이 자연스럽게 열려 있게 만드는 방식을 취했습니다. 그 자신의 표현을 빌리자면 la mer qui monte — 상승하는 바다입니다.

소프트웨어 공학의 역사는 망치의 역사였습니다. E2E가 깨지면 테스트를 늘립니다. 통합(integration)이 깨지면 CI를 빠르게 합니다. 경계(boundary)가 깨지면 계약 테스트(contract test)를 작성합니다. 개별 도구들은 올바른데도 문제가 사라지지 않는 이유는 도구가 나빠서가 아니라, 문제가 정식화된 추상화 수준이 너무 낮기 때문입니다. 국소(local)와 대역(global)의 관계라는 문제를 국소적인 도구로 계속 두들겨 왔던 것입니다.

저의 연구 프로그램인 AAT가 하고 있는 것은 바로 이 수위를 높이는 작업입니다. 코드나 모듈이라는 수면 아래의 바위를 직접 다루는 것을 그만두고, Atom, 층(sheaf), 피복(covering), 붙여넣기(gluing)라는 수준까지 올라갑니다. 그러면 "테스트는 통과하는데 운영 환경에서 깨진다"라는 공학적 난제는 싸워야 할 적이 아니라, H^1이라는 좌표를 가진 당연한 대상이 됩니다.

이 수위 높이기는 실무적인 부수 효과도 있습니다. Atom은 코드로부터 추상화된 단위이므로, 이론도 측정도 특정 언어·프레임워크·라이브러리에 의존하지 않습니다. Rust의 마이크로서비스든, 레거시 Java 모놀리스든 관측 데이터만 주어진다면 동일한 정리로 동일한 장애를 설명할 수 있습니다. lint나 아키텍처 테스트처럼 에코시스템마다 도구를 새로 만들 필요가 없으며, 기술 스택이 바뀌어도 이론은 낡지 않습니다. 추상화란 이런 의미에서 이식성(portability)이기도 합니다.

문제는 사라지지 않습니다. 하지만 수수께끼는 아니게 됩니다. 수수께끼가 아니게 된 것은 측정할 수 있습니다. 측정할 수 있는 것은 도구가 할 일이 됩니다.

올바른 일반성(generality)의 수준으로 끌어올리면, 난제는 '풀리는' 것이 아니라 자명(trivial)해집니다. 이것이 rising sea의 핵심이며, 이 프로젝트의 방법론입니다.

한 가지, Grothendieck의 바다와 다른 점이 있습니다. 그의 바다는 EGA/SGA라는 수천 페이지의 산문에 퇴적되어 후세대가 그 수위를 유지하는 데 고생했습니다. 저의 바다는 Lean이 수위를 보장합니다. 정리가 형식 검증(formal verification)되어 있는 한, 물은 빠지지 않습니다. 이 바다의 중심에 있는 정리를 SAGA 정리라고 명명한 것은, Serre의 GAGA — 대수기하학(algebraic geometry)과 해석기하학(analytic geometry)이라는 두 세계의 대응을 확립한 기념비적인 작업 — 에 대한 오마주입니다. GAGA가 두 기하학을 연결했듯이, SAGA 정리는 아키텍처 의미론(architecture semantics)과 대수기하학을 연결하는 비교 정리입니다. 거기에 기계 검증(machine verification)이라는 한 층을 더했습니다.

또 하나, 잊어서는 안 될 것이 있습니다. rising sea는 도피로서의 추상화가 아니었습니다. Grothendieck는 항상 구체적인 문제(Weil 추측)를 침수시켜야 할 대상으로 중심에 두었습니다. 이 프로젝트도 같은 형태를 띠고 있습니다. E2E의 파탄이라는 현장의 구체적인 고통이, 침수시켜야 할 껍질로서 처음부터 중심에 있습니다. 추상화는 현실에서 멀어지기 위해서가 아니라, 현실을 자명하게 만들기 위해 수행하는 것입니다.

여기까지가 방법에 대한 이야기입니다. 방법은 바다 — 추상화의 수위를 높여 문제를 가라앉히는 것입니다. 하지만 연구의 과정 자체는 바다보다는 등산에 가깝습니다. 어떤 봉우리에 올랐는지, 정상에서 무엇이 보였는지, 다음은 어느 봉우리인지. 여기서부터는 그 등반의 기록입니다.

등정 — SAGA 정리라는 정상 (증명 완료)

이 부분은 경계를 엄격히 지켜서 작성하겠습니다. 다음은 이미 성립되어 있습니다.

• AAT 수학 본문 (AAT 数学本文) — Atom을 공리로 하는 순수 수학 이론으로서의 AAT 본문입니다. 도구나 형식화(formalization)에 대한 변명은 일절 배제하며, 수학이 자신의 언어로만 이야기하는 형식을 취합니다. -
• SAGA 정리 (SAGA 定理) — 아키텍처 의미론(architecture semantics) 측면에서 육성한 $H^1$과, Atom으로부터 생성된 site 상의 실제 Čech $H^1$이 일치한다는 비교 정리입니다. Lean 4로 증명 완료되었습니다. 이 등반에는 AI 에이전트의 자동 연구 루프(automatic research loop)가 352 사이클 소요되었으며, 그중 347 사이클은 "이 어휘로는 등반할 수 없다"라는 불가능성 정리(impossibility theorem)의 벽에 부딪히는 작업이었습니다. 마지막 5 사이클, "law(아키텍처의 법)는 술어가 아니라 방정식이다"라는 어휘의 전환이 암반을 뚫어냈습니다. -
• Lean 형식화의 탑 (Lean 形式化の塔) — "말할 수 있는 명제만을 형식화한다"라는 규율 아래, 정의(definition)·정리(theorem)·예시(example)를 sorry 없이 쌓아 올리고 있습니다. -
• ArchSig — Rust로 제작된 계측기입니다. 아키텍처 관측 데이터 (ArchMap), 지켜야 할 법 (LawPolicy), 증거의 계약 (evidence contract)을 입력으로 받아 $H^1$ 장애 검출을 수행합니다. 중요한 설계 원칙이 하나 있습니다. 주어진 contract로부터 말할 수 있는 것만을 말하고, 말할 수 없는 것에는 침묵한다. 입력을 보완하거나 추측하지 않습니다. -
• SFT — 소프트웨어의 시간적 발전을 기술하는 동역학(dynamics) 측면입니다. AAT가 정역학(특정 시점의 정합성)이라면, SFT는 변경 사항이 어떻게 전파되는지에 대한 이론이며, 이 또한 정리를 만들어내기 시작했습니다. -
• 개발 체제 자체가 실증 실험 — 이 리포지토리는 AI 에이전트가 고속으로 구현하고, 적대적 리뷰(adversarial review)와 Lean 게이트가 정합성을 판정하며, 인간은 질문의 설정과 수락만을 담당하는 체제로 운영됩니다. 즉, AAT/ArchSig가 지키고자 하는 개발 양식으로 AAT/ArchSig 자체가 개발되고 있는 것입니다. 이러한 자기 적용성(self-applicability)은 이론이 실제 개발을 견뎌낼 수 있다는 첫 번째 증거라고 생각합니다.

산 정상에서의 전망 1 — 고요한 미래

여기서부터는 구상입니다. SAGA의 정상에서 저 멀리 보였던 풍경 두 가지를 남겨둡니다.

첫 번째는 이렇습니다.

어느 엔지니어가 업무를 시작합니다. 완성된 코드를 "ArchSig로 분석해줘"라고 말합니다. 몇 가지 obstruction(장애/방해 요소)이 검지됩니다. 그는 코드를 수정합니다. E2E 장애는 미연에 방지되었습니다.

이 광경에서 주목해야 할 점은 그 고요함입니다. 그곳에는 범주(category)도 층(sheaf)도 코호몰로지(cohomology)도 등장하지 않습니다. 엔지니어는 "분석해줘"라고 말하고, obstruction이라는 단어만을 받아들여 수정하고 앞으로 나아갑니다. 동작 측면에서는 lint를 돌리는 것과 구분이 되지 않습니다.

엔지니어는 대수기하학을 습득할 필요가 없습니다 — 이것은 이 프로젝트가 처음부터 정해둔 추상화 원칙이며, 이 광경의 설계도입니다. 이론이 완성에 가까워질수록 이론은 보이지 않게 됩니다. 수위가 충분히 높아진 바다는 수면만을 보여주기 때문입니다.

이 광경에는 더 깊은 변화가 숨어 있습니다. "E2E 장애는 미연에 방지되었다"라는 문장은 **반사실적 가정 (counterfactual)**입니다. 일어나지 않은 장애는 관측할 수 없습니다. 오늘날의 소프트웨어 공학에는 방지된 장애에 대해 이야기할 어휘가 원리적으로 존재하지 않습니다. 그렇기에 테스트는 사후에만 가치를 증명할 수 있고, 아키텍처의 좋고 나쁨은 사고가 발생하기 전까지 공중에 떠 있습니다.

obstruction이 정리에 접지(grounding)되었을 때 비로소, "이 수정이 없었다면 붙이기(pasting)는 실패했을 것이다"라는 말이 경험칙이 아닌 **귀결 (consequence)**로서 말해질 수 있게 됩니다. 그 고요한 광경은 반사실적 가정이 수학이 된 세계입니다.

산 정상에서의 전망 2 — 에이전트 사회의 부동점

더 극단적인 미래도 있습니다.

엔지니어는 밖에서 지켜보기만 합니다. 여러 AI 에이전트가 역동적으로 협력하여 소프트웨어를 초고속으로 만듭니다. 도중에 ArchSig의 알람이 울립니다 — 배포 게이트(deploy gate)에 ArchSig가 배치되어 있기 때문입니다. 에이전트는 ArchSig의 출력을 읽고 코드를 수정합니다.

이 미래에는 코드도, 테스트도, 리뷰도, 수정도, 모든 것이 AI의 생성물이 됩니다. 모든 것이 동일한 지반 위에서 흔들리는 세상에서, 유일하게 흔들리지 않는 것은 정리에 기반한 게이트(gate)입니다. 그 판정은 누군가의 의견이 아니라, 형식 검증(formal verification)된 정리의, 선택된 contract 상에서의 귀결이기 때문입니다. 맹렬한 속도로 회전하는 생성의 소용돌이 속에, 단 한 점 움직이지 않는 바위가 있는 것입니다. 배포 게이트(deploy gate)에 두어야 할 것은 바로 그러한 성질을 가진 것뿐입니다. ArchSig는 인간의 도구에서, **에이전트 사회의 부동점(fixed point)**이 됩니다.

이 미래에는 "말할 수 없는 것에 침묵한다"라는 설계 원칙이 사치품에서 안전장치로 변합니다. 인간을 상대할 때는 모호한 경고라도 행간을 읽어줄 수 있지만, 에이전트는 출력을 문자 그대로 읽고 문자 그대로 행동합니다. "왠지 수상하다"를 출력하는 검사기는 에이전트의 루프(loop)를 발산시킵니다. 침묵의 규율은 멀티 에이전트 시대의 interface 사양입니다.

그렇다면 인간은 어디로 가는 것일까요. "밖에서 지켜보기만 한다"는 것은, 정확히 말하면 입법부로 이동한다는 것을 의미한다고 생각합니다. LawPolicy를 쓰는 것은 누구인가. 어떤 어휘로 말하는 것을 허용하고, 무엇을 SAFE라고 정의할 것인가를 정하는 것은 누구인가. 에이전트는 행정부이고, 검사기는 사법부이며, 인간은 법을 씁니다. 코드를 쓰는 손은 놓더라도, "무엇이 보호되어야 하는가"에 대한 결정은 놓지 않습니다. 오히려 그 부분만이 인간의 업무로서 순화되는 것입니다.

엔지니어가 밖에서 지켜보기만 하는 미래는 인간이 퇴장한 미래가 아닙니다. 인간이 신뢰의 근거를 만들어낸 미래입니다.

경제적인 순풍도 하나 있습니다. 검증은 생성보다 몇 자릿수나 더 저렴합니다. ArchSig는 결정적인 계산을 수행하므로, LLM의 추론 비용과 비교하면 실질적으로 거의 공짜에 가깝습니다. Lean 또한 한 번 증명이 세워지면 재검증은 가볍습니다. 계산 자원이 긴박해지는 세상일수록, "LLM이 LLM을 리뷰하는" 사치스러운 구성은 수지타산이 맞지 않게 되며, 저렴하고 결정적인 게이트로 생성의 낭비를 조기에 차단하는 구성이 경제적으로 승리합니다. 메모리가 희소했던 시대에 타입 시스템(type system)이 효율적이었던 것과 마찬가지로, 자원 제약은 항상 "실행 전에 오류를 걸러내는" 기술의 가치를 끌어올립니다. 초고속 생성의 시대에 가장 비용이 많이 드는 것은, 잘못된 코드를 생성한 뒤에야 그것을 깨닫는 것입니다.

하강로 — 다음 정리의 이름은 descent(미증명)

등산에서는 "정상은 절반일 뿐이다. 무사히 내려와야 비로소 등산이 완성된다"라고 말합니다. SAGA의 등정에도 아직 하강로가 남아 있습니다. 그리고 아주 절묘하게도, 그 하강로의 첫 번째 정리는 말 그대로 descent(하강) 정리라고 불리는 것입니다.

망망을 성과처럼 말하지 않기 위해, 미증명된 것들을 명시합니다.

descent 정리(본진) — "어떤 조건 하에서라면, 국소적인 정당성으로부터 대역적인 정당성이 따르는가". 소프트웨어 공학이 암묵적으로 믿어왔지만 한 번도 증명한 적 없는 합성 원리에, 처음으로 성립 조건을 부여하는 정리입니다. 검출 측(대역적 복구가 존재한다면 장애는 사라져 있다)은 쌓여가고 있지만, 본진인 역방향(장애가 사라져 있다면 대역적 복구가 실재한다)은 아직 open 상태입니다.
H^2 이상 — 고차의 장애 구조를 설명할 언어는 아직 없습니다. 유도적인 확장은 의도적으로 보류하고 있습니다.
관측층의 충실성 — ArchSig 판정의 신뢰성은 ArchMap이 현실의 코드를 어디까지 충실하게 투영하느냐를 넘어설 수 없습니다. 이 지점이 이론이 아닌 공학의 급소이며, 관측의 순화(판정의 주관을 배제하고 관측을 생데이터로 남기는 것)를 방어선으로서 공고히 하고 있습니다.
실제 코드베이스에서의 실증 — H^1의 장애 검출이 실제 프로젝트에서 "인간이 간과했던 결합의 실패"를 먼저 찾아내는 것. 이론의 진위와는 별개로, 도구로서의 가치는 여기서 결정됩니다.

descent가 증명되면 무엇이 바뀔까요. ArchSig는 그것을 검사 항목으로 삼을 수 있습니다. "이 아키텍처는 descent의 가정을 만족하므로, 국소 테스트의 합격이 대역적 정합성을 함의한다"라고 말입니다. 반대로 가정이 깨져 있는 곳이야말로 E2E 테스트를 집중시켜야 할 곳이라고, 이론이 지시하게 되는 것입니다. 정상에서의 전망은 이 하강로를 무사히 내려와야 비로소 현실의 계곡에 닿습니다.

말할 수 있는 것만을 말한다

마지막으로, 이 도구가 무엇을 말하지 않는지를 분명히 해둡니다.

ArchSig가 말할 수 있는 것은 "이 변경은 주어진 어휘와 법의 테두리 안에서 안전하다"는 것까지입니다. "이 변경은 좋은 설계다"라고는 말하지 않습니다. 말할 수 없기 때문입니다. 안전성 판정과 설계의 좋고 나쁨 사이에는 의도적으로 그어진 침묵의 경계가 있습니다.

이것은 약점이 아니라, 신뢰의 조건이라고 생각합니다. 판정할 수 없는 것까지 판정하려는 도구는 언젠가 반드시 거짓을 말하게 됩니다. 판정할 수 있는 것만을 판정하는 도구는, 그 범위 내에서는 절대로 거짓을 말하지 않습니다. AI가 무엇이든 말하고 싶어 하는 시대에, 말할 수 있는 것만을 말하는 도구는 희귀합니다. 배포 게이트 (Deploy Gate)에 두어도 되는 것은 후자뿐입니다.

이 글 또한 그 규율에 따라 작성했습니다. 증명된 절 (Proven section), 구상의 절 (Conception section), 미증명된 절 (Unproven section). 이 세 가지를 섞지 않는 것.

결론

소프트웨어 공학이 따라가지 못하고 있는 것이 아닙니다. 필요한 수학이 아직 공학으로 수입되지 않았던 것입니다. 이 연구 프로그램은 그 수입 작업이며, 심지어 밀수가 아니라 Lean을 통해 통관 절차를 마친 정식 수입입니다.

과제는 아직 많이 남아 있습니다. descent (하강), 고차 장애 (Higher-order obstructions), 관측층 (Observation layer)의 충실성, 실제 코드베이스에서의 실증 — 어느 것 하나 가볍지 않습니다. 하지만 오를 수 없는 산과 오를 수 있는 산의 차이는 해발 고도가 아니라, 경로를 그릴 수 있느냐의 여부라고 생각합니다.

수위는 차오르기 시작했습니다. 그리고 바다는 차오르기 시작한 이후부터가 빠릅니다.

해낼 수 없는 일은 아닙니다. 그리고 오를 수 없는 산도 아닙니다.

참고

• 리포지토리 (Repository): AlgebraicArchitectureTheoryV2 (MIT 라이선스)
• 웹사이트 (Website): AAT/SFT Research Notes

Discussion