비즈니스 결정에 형식 검증이 필요한 이유

가격 규칙 40개는 한 번에 만들어지지 않습니다. 신규 가입 프로모션 하나, 등급별 적립 보너스 하나, 지금 가격 체계보다 계약이 먼저 있었던 엔터프라이즈 고객 한 곳에만 걸리는 예외 하나. 요청이 올 때마다 한 줄씩 붙었습니다. 전부 리뷰를 거쳤고, 전부 테스트가 있었고, 1년 동안 사고 없이 프로덕션에서 돌았습니다.

그러다 문의가 하나 들어옵니다. STANDARD 등급 고객이 소액 장바구니로 결제했는데 할인이 하나도 붙지 않았고, 의도한 동작인지 아무도 답하지 못합니다. 누군가 40개를 순서대로 다 읽고 나서야 답이 나옵니다. 그 조합을 덮는 규칙이 없습니다. 누가 잘못 짠 코드가 아니라, 하나하나는 맞게 짜인 규칙 사이에 뚫린 구멍입니다.

실패한 테스트는 없습니다. 그 조합을 확인해 본 테스트가 애초에 없었으니까요. 알림도 울리지 않습니다. 오류가 난 게 아니니까요. 시스템은 규칙이 시킨 대로 정확히 동작했습니다. 규칙이 그 경우를 두고 아무 말도 하지 않았을 뿐입니다.

이 글은 그 침묵 안에 있는 결함, 테스트와 시뮬레이션이 구조적으로 거기에 닿지 못하는 이유, 그리고 둘이 답하지 못하는 질문에 답하려면 무엇이 필요한지를 다룹니다. 무슨 일이 일어났는가가 아니라, 무슨 일이 일어날 수 있는가입니다.

통과한 테스트가 증명하지 못하는 것

테스트는 예시입니다. 입력 공간에서 점 하나를 골라 그 자리의 출력을 확인합니다. 테스트 100개는 점 100개입니다.

규칙 집합의 입력 공간은 점 100개가 아닙니다. 등급 하나, 음수가 없는 실수인 장바구니 금액 하나, 국가 코드 하나, 가입 후 경과일 하나. fact 네 개만으로도 조합은 세는 게 의미 없는 크기가 됩니다. 테스트 스위트는 작성자가 생각하고 있던 자리를 표본으로 찍습니다. 같은 사람이 같은 시간에 같은 머릿속 그림으로 규칙과 테스트를 함께 썼기 때문입니다. 결함은 아무도 생각하지 않은 자리에 남고, 그 자리에는 당연히 테스트도 없습니다.

일반 코드에도 같은 간극이 있습니다. 규칙 집합에서 더 나빠지는 이유는 구조에 있습니다. 규칙 집합은 쌓여서 커집니다. 37번 규칙은 6번 규칙과 다른 사람이, 다른 분기에, 다른 마감을 앞두고 붙인 것입니다. 리뷰는 그 규칙 자체의 의도만 봅니다. 나머지 39개와의 관계까지 보려면 조합을 전부 훑어야 하는데 사람은 그 작업을 잘 못 합니다. 상호작용의 면적은 제곱으로 늘어나고 사람의 주의력은 선형으로 늘어납니다.

그래서 규칙 집합은 흔하지만 잘 눈에 띄지 않는 상태에 도달합니다. 규칙은 하나하나 다 맞는데 집합은 틀린 상태입니다.

조용히 어긋나는 세 가지

규칙 집합은 시간이 지나면 스스로 세 가지 결함을 만듭니다. 셋 다 자기를 드러내지 않습니다.

도달 불가능한 규칙: 절대 발동하지 않는 규칙입니다. LexQ에서 priority는 버전 안에서 1부터 N까지 자동으로 매겨지고, 해소 방식이 EXCLUSIVE인 mutex group은 구성원 중 하나만 이기게 합니다. 그 그룹의 priority 6 자리에 조건이 비어 있는 catch-all을 하나 넣으면 7번부터 12번까지는 죽은 코드가 됩니다. 그런데도 콘솔에는 그대로 보이고, 그게 돌아간다고 믿는 사람이 계속 손을 댑니다. 조건 자체가 원인일 때도 있습니다. tier = 'GOLD'와 tier = 'SILVER'를 동시에 요구하는 조건은 트래픽이 어떻게 들어오든 만족될 수 없습니다.

충돌: 조건이 동시에 참이 될 수 있는데 액션이 서로 어긋나는 두 규칙입니다. 같은 fact에 값을 쓰는 SET_FACT 두 개, 할인 규칙과 BLOCK이 함께 매칭되는 경우. 의도한 겹침이라면 mutex group이 해소합니다. 문제는 아무도 겹침을 알아채지 못한 경우입니다. 그때 결과를 정하는 건 먼저 매겨진 priority이고, 그건 서로 관계없는 두 사람이 티켓을 올린 순서입니다.

공백: 어떤 규칙도 덮지 않는 입력 영역입니다. 앞에서 본 문의가 여기서 나옵니다. 오류도 로그도 남지 않습니다. 아무것도 적용되지 않은 결정으로 돌아오는데, 원래 아무것도 적용되지 않아야 하는 결정과 구분되지 않습니다.

셋 다 트래픽과 무관한 규칙 집합 자체의 성질입니다. 해당 영역으로 요청이 한 번도 들어오지 않아도 그대로 참입니다. 런타임 관측으로 찾을 수 없는 이유가 여기에 있습니다.

시뮬레이션이 답하는 것과 답하지 못하는 것

실제 트래픽을 다시 흘려보는 것은 지금 팀이 가진 가장 강한 도구입니다. LexQ의 변경 영향 시뮬레이션(Impact Simulation)은 새 규칙 버전을 과거 실행 기록에 대고 돌려서 무엇이 달라졌는지 보여줍니다. 매칭률, 지표 변화량, 규칙별 통계. Decision Replay는 결정 하나를 놓고 이전 결과와 새 결과를 나란히 놓습니다. 모든 결정에는 어떤 규칙이 어떤 입력으로 어느 버전에서 발동했는지가 trace로 남고, 그 기록은 불변 감사 원장에 쌓입니다. 배포 전에 규칙 변경의 영향을 보는 일이 왜 LexQ를 만든 출발점이었는지와 지난 결정의 근거를 나중에 어떻게 대는지는 따로 한 편씩 썼습니다.

둘은 같은 모양의 답입니다. 존재하는 입력을 덮습니다. 시뮬레이션은 이미 받은 트래픽을 다시 돌리고, 감사 기록은 이미 내려진 결정을 설명합니다. 아직 아무도 보내지 않은 조합을 두고는 둘 다 아무 말도 하지 않습니다.

앞에서 본 공백은 여기에 걸리지 않습니다. 재생 구간에 STANDARD 등급의 소액 장바구니 결제가 한 건도 없었다면 시뮬레이션은 그 영역을 두고 침묵합니다. "문제 없음"이 아니라 관측 자체가 없는 것인데, 화면에는 똑같이 보입니다. 도달 불가능한 규칙은 더 나쁩니다. 시뮬레이션에서 매칭 0건으로 나오는데, 드물게 들어오는 고객군을 담당하는 정상 규칙도 똑같이 0건으로 나옵니다. 화면만 보고 둘을 구분하실 수 있을까요?

여기서 선을 하나 긋겠습니다. 독자가 먼저 찾아내게 두는 것보다 제가 직접 긋는 편이 낫습니다. LexQ는 오늘 앞의 일은 하고 뒤의 일은 하지 않습니다. 변경 영향 시뮬레이션, Decision Replay, 규칙별 latency 프로파일러, 버전 관리와 즉시 롤백, decision trace, 불변 감사 원장. 여기까지는 지금 프로덕션에서 돌아갑니다. 규칙 집합의 형식 검증(formal verification)은 LexQ에 없습니다. 열어볼 검증기가 없습니다. 이 선 아래로 이어지는 내용은 문제 정의와 설계 방향이지, 지금 쓸 수 있는 기능이 아닙니다.

형식 검증은 무엇을 다르게 하는가

핵심은 입력 공간을 표본으로 찍는 대신 통째로 기술하는 것입니다.

규칙 조건은 이미 논리식입니다. tier = 'GOLD' AND cartTotal > 5000은 제약 두 개의 논리곱이고, 하나는 문자열 도메인 위에, 하나는 수 도메인 위에 있습니다. 규칙 집합은 그런 논리식의 모음에 승자를 정하는 의미론이 얹힌 것입니다. priority 순서, mutex group, 그리고 조건이 비어 있어 무엇에나 매칭되는 catch-all.

조건을 코드 경로가 아니라 논리식으로 보기 시작하면 앞의 세 결함은 만족 가능성(satisfiability) 문제가 됩니다. 그리고 만족 가능성은 연구 커뮤니티가 40년 동안 실용 수준까지 끌어내린 문제입니다. Z3 같은 SMT solver는 1차 논리 포뮬러를 받아 둘 중 하나를 합니다. 그 식을 만족하는 값을 찾아내거나, 그런 값이 존재하지 않음을 증명합니다.

• 도달 불가능한 규칙: 그 규칙의 조건에, 먼저 가로챌 수 있는 상위 priority 조건 전부의 부정을 논리곱으로 붙인 식을 만들어 solver에 넘깁니다. UNSAT이면 어떤 입력으로도 발동하지 않는다는 뜻입니다.
• 충돌: 액션이 어긋나면서 mutex로 갈라지지도 않은 두 규칙의 조건이 동시에 만족될 수 있는지 solver에 넘깁니다. SAT이면 solver가 둘을 함께 발동시키는 입력을 하나 돌려줍니다.
• 공백: 전체 조건의 논리합을 부정한 식을 solver에 넘깁니다. SAT이면 덮이지 않은 영역이 있고, solver가 그 안의 점 하나를 짚어 줍니다.

여기서 답의 성격을 정확히 보셔야 합니다. 테스트 결과와의 차이가 이 글의 논지 전부입니다. 통과한 테스트 스위트가 말해 주는 것은 "확인한 경우는 잘 돌았다"까지입니다. UNSAT은 그런 경우가 존재하지 않음을 말합니다. 하나는 표본을 두고 하는 보고이고, 다른 하나는 입력 공간 전체에서 성립합니다. 3년 뒤에나 처음 들어올 입력까지 포함해서요.

제가 이 문제에 붙이려는 이름은 LexQ Verify입니다. 출력이 어떤 모양이면 좋겠다고 생각하는지는 이렇습니다.

✅ No unreachable rules
⚠️  2 potential conflicts:
   "vip-discount" ∧ "loyalty-bonus"
   → Resolved by mutex group "promo-exclusive"
❌ 1 gap:
   tier=STANDARD, cartTotal < 5000 is uncovered

이 블록은 출력의 스케치이지 스크린샷이 아닙니다. 뒤에 구현을 두지 않은 채로 이름과 모양을 먼저 공개해 둡니다. 어느 회사가 결국 이걸 만들든 아니든, 이 문제에는 부를 이름이 필요하기 때문입니다. "이 규칙 집합에 도달 불가능한 분기가 없음이 증명됐다"를 가리키는 업계 공용 표현이 지금 없고, 그 부재도 같은 결함이 계속 배포되는 이유의 일부입니다.

왜 아무도 비즈니스 규칙에는 만들지 않았나

SMT를 실제로 다뤄 본 엔지니어가 드뭅니다. 그 능력은 컴파일러와 검증 연구 쪽에 모여 있고, 룰 엔진을 만드는 사람들과 거의 겹치지 않습니다.

규칙 조건 DSL을 SMT 포뮬러로 내리는 컴파일러는 학술 수준의 설계 작업입니다. fact는 타입이 있고 종류가 섞여 있습니다. 유한 도메인 문자열, 범위가 열려 있는 수치, boolean, 포함 여부를 확인하는 배열. 이걸 그대로 모델링하는 쪽은 그나마 작은 일입니다. 큰 일은 규칙 집합의 의미론이 조건만으로 끝나지 않는다는 데 있습니다. priority 순서, mutex 해소, 평가 도중에 fact를 바꾸는 MUTATE_FACT까지 전부 어떤 규칙이 결정을 내리는지에 관여합니다. 순서를 무시한 검증기는 아무도 돌리고 있지 않은 시스템을 놓고 참인 명제를 증명합니다.

그리고 규칙 집합의 형식 검증을 제품으로 내놓은 상용 룰 엔진의 수는 0입니다. 말 그대로 하나도 없습니다. 직접 운영하는 엔진과 관리형 서비스가 운영에서 어디서 갈리는지를 정리하면서 살펴본 엔진은 전부 작성, 실행, 그리고 어떤 형태의 테스트에서 멈춥니다.

여기서 포장하지 않고 말씀드릴 부분이 있습니다. 이미 먼저, 그리고 잘 해낸 곳이 있습니다. Amazon의 Cedar는 authorization 영역에서 formal verification을 제품으로 내놨습니다. Lean과 automated reasoning 위에 올렸고, 출시됐고, 문서도 공개돼 있습니다. 기법 자체를 놓고 보면 LexQ는 follower입니다. 아닌 척하는 것은 이 블로그가 할 수 있는 주장이 아닙니다.

비어 있는 곳은 다른 영역입니다.

"Cedar verifies who can access what. LexQ verifies what decision will be made."

Cedar가 검증하는 것은 누가 무엇에 접근할 수 있느냐이고, LexQ가 검증하려는 것은 어떤 결정이 내려지느냐입니다. 두 문제는 실질적으로 다릅니다. 의사결정 운영 플랫폼은 authorization이 아니라고 썼을 때 갈랐던 것은 다루는 범위였습니다. 형식화 층으로 내려오면 구분이 기술적으로 갈립니다. authorization 결정은 대체로 엔티티 그래프 위의 boolean입니다. principal, action, resource, 그리고 허용이냐 거부냐. 비즈니스 결정은 값을 만들어 냅니다. 할인 금액, 중간에 바뀐 누적 합계, 막힌 이체, 여러 종류의 산술이 섞인 일할 계산. "이 principal이 이 문서를 읽어도 되는지"와 "서로 모순되는 할인 두 개를 동시에 발동시키는 장바구니가 존재하는지"는 서로 다른 이론 위에 놓인 서로 다른 논리식입니다. 선행 사례는 기법에서는 앞선 출발점이지만 도메인에서는 거의 도움이 되지 않습니다. 이 비교는 Cedar가 무엇을 증명하고 결정 규칙이 왜 더 어려운 대상인지에서 따로 자세히 다뤘습니다.

이게 필요 없는 경우, 그리고 LexQ가 필요 없는 경우

규칙 집합의 형식 검증은 공짜가 아닙니다. 반대편 논리는 짧고 분명합니다.

규칙 집합이 작고 움직이지 않습니다: 2년째 그대로인 규칙 5개는 한 사람 머릿속에 다 들어갑니다. 그냥 읽으시면 됩니다. solver가 오후 한나절의 정독보다 더 알려줄 게 없습니다.

규칙이 설계상 겹치지 않습니다: 필드 하나를 키로 잡고 값마다 행 하나씩 두는 조회표라면 충돌도 도달 불가능도 구조상 생기지 않습니다. 증명할 게 없습니다.

틀린 결정의 비용이 작습니다: 공백이 만드는 최악의 결과가 고객이 정가를 내고 문의를 보내는 정도라면 손실은 한정돼 있습니다. 증명은 틀린 답이 비쌀 때 사는 것이고, 그렇지 않은 자리에서는 값을 못 합니다.

그리고 검증에서 한 걸음 물러나 LexQ 자체를 놓고 보면 더 넓은 경우가 있습니다. 규칙이 아직 서비스 안의 if-else 분기이고 하나 바꾸려면 PR과 배포가 필요한 상태라면, 도달 불가능한 분기는 아직 문제가 아닙니다. 결정을 릴리스 주기 밖으로 꺼내는 일이 먼저입니다. 그리고 결정이 거의 바뀌지 않는다면 의사결정 운영 플랫폼도 필요 없습니다. 코드베이스 안의 조건문이 맞는 도구이고, 아니라고 말하는 벤더가 있다면 그건 돕는 게 아니라 파는 것입니다.

LexQ는 엔지니어링 팀을 위한 의사결정 운영 플랫폼이고, "이 규칙 변경이 무슨 일을 하는가"라는 질문에 오늘 내놓는 답은 실제 트래픽에 대고 돌리는 변경 영향 시뮬레이션입니다. 가지고 있는 입력을 놓고 하는 답입니다. 규칙 집합이 앞으로 받을 수 있는 모든 입력에서 어떻게 동작하는지는 다른 질문이고, 그 질문에는 이미 알려진 수학적 형태가 있습니다. 그리고 아직 어떤 상용 룰 엔진도 답하지 않았습니다. LexQ Verify는 그 질문에 붙인 이름입니다.

→ 지금 돌아가는 것부터 확인해보세요. lexq.io에서 무료로 시작하기