먼저, 결론부터 말씀드리겠습니다.

형식 증명(Formal Proof)은 「프로그램의 버그를 모두 없애는 마법」이 아닙니다. 인간이 「무엇을 보장하고 싶은가」를 사양(Specification)으로서 작성하고, 그 사양에 대해 프로그램이 올바른지를 수학적으로 검증하는 기술입니다. 그렇기에,

사양을 스스로 직접 작성해야 하는 곳── 암호 라이브러리, OS 커널, 컴파일러, 인가 엔진(Authorization Engine)과 같은 「기반(Infrastructure)」 ── 에서 특히 가치를 가집니다.

일본의 일반적인 Web 개발에서는 갑자기 필수적이 되는 기술은 아닙니다. 그 점은 숨기지 않고 말씀드리겠습니다. 하지만,

AI 에이전트나 Physical AI에 「무엇을 해도 되는지」를 정하는 사양 계층에서는 향후 중요성이 커질 가능성이 있습니다. 그리고 학습을 시작한다면 ──

명제 논리(Propositional Logic)·술어 논리(Predicate Logic)·자연 연역(Natural Deduction)까지 왔다면, 이제 Lean 4를 만져봐도 좋다, 라는 것이 본 기사의 답입니다.

「프로그램에 버그가 없다는 것을, 테스트가 아니라 수학으로 증명한다」

그런 기술이 있다고 들었다면, 어떻게 생각하시겠습니까?

꿈 같은 이야기처럼 들릴지도 모릅니다.

하지만 그것은 현실에 존재하며, 항공기나 로켓, 암호나 금융 시스템과 같이 실수가 허용되지 않는 곳에서 조용히 사용되고 있습니다.

그 기술을 담당하는 것이 Lean, Rocq(구 Coq), Agda, Idris, Isabelle와 같은

언어입니다.

더 정확히 말하자면, 본 기사에서 주인공으로 다루는 것은 **수학적인 증명을 인간이 구성하고, 컴퓨터가 그 올바름을 검증하는 「대화형 증명 보조 도구(Interactive Theorem Prover)」**라고 불리는 계통의 도구입니다.

최근에는 수학자가 난제의 증명을 기계로 검증하거나, AI가 생성한 답의 올바름을 보장하는 도구로서도 갑작스럽게 주목을 받고 있습니다.

그렇다고는 해도, 막상 배우려고 하면 벽이 가로막습니다.

일본어 서적은 거의 없고, 실무에서 사용할 기회도 제한적이며, 애초에 어디서부터 손을 대야 할지 이정표가 없습니다.

「재미있어 보이지만, 자신과는 인연이 없는 세계겠지」라며 많은 분이 입구 앞에서 발길을 돌려버립니다.

이 기사는 그 입구에 하나의 길을 내는 것을 목적으로 하고 있습니다.

고교 수학을 많이 잊어버린, Python으로 머신러닝을 작성하고 있는 엔지니어 분

── 그러한 독자를 염두에 두고, 이 기술이 무엇에 도움이 되는지, 커리어로 이어지는지, 그리고 무엇을 어떤 순서로 배워야 하는지를 차례대로 말씀드리겠습니다.

예비 지식은 필요 없습니다.

부디 가벼운 마음으로 함께해 주십시오.

이 기사는 다음과 같은 흐름으로 진행됩니다.

첫째, 「프로그램의 올바름을 수학적으로 확인하는 기술」은 두 가지 질문에 의해 세 가지로 나뉩니다.

질문은, 「증명하고 싶은 성질을 스스로 직접 작성해야 하는가」와 「그 증명을 기계가 스스로 찾아낼 수 있는가」 입니다.

증명하고 싶은 성질이 미리 결정되어 있음 (배열의 범위를 벗어나 읽지 않는지 증명하고 싶다, 잘못된 상태에 빠지지 않는지 증명하고 싶다)

버튼 하나로 기계가 조사해 줍니다. **정적 분석(Static Analysis)**이나 **모델 검사(Model Checking)**가 이것입니다.

성질은 직접 작성하지만, 증명은 기계가 찾아줌 ── Dafny나 F*가 이것입니다.

성질도 증명도 사람이 작성함 ── Lean, Rocq, Agda, Isabelle. 이 기사의 주제입니다.

둘째, 비용의 근원은 「성질을 스스로 직접 작성해야 하는가 여부」에 있습니다.

「배열의 범위를 벗어나 읽지 않는다」라면 툴에 이미 내장되어 있습니다. 하지만 「이 함수는 수학적으로 정의된 AES 암호와 어떤 입력에 대해서도 엄격하게 일치한다」라는 성질은, 매번 수학의 언어로 직접 작성할 수밖에 없습니다.

셋째, 그러한 작성이 필요해진 곳은 「기반(Infrastructure)」을 만드는 현장이었습니다.

암호 라이브러리, OS 커널, C 컴파일러, 클라우드의 인가 엔진. 모두 그 위에 무수한 소프트웨어가 올라가는 토대입니다. 토대이기 때문에 「어떤 입력이 올지」를 한정할 수 없습니다. 그래서 「모든 입력에 대해 사양대로이다」라고 증명할 필요가 생겼습니다.

그리고 그중 증명이 너무 깊어 기계가 스스로 찾아낼 수 없었던 것 ── OS 커널, 컴파일러, 인가 엔진 ── 에서 사람이 증명을 조립하는 도구가 사용되었습니다. 미국과 유럽이 이 영역에 발을 들여놓았습니다.

넷째, 그렇다면 일본은 동일한 문제를 방대한 테스트로 극복해 온 것일까요?

그렇지 않다는 것이 본 기사의 견해입니다.

일본의 고보증 산업이 강한 이유는 자동차의 전자 제어나 철도의 진로 제어와 같이 입력 범위가 물리적으로 정해져 있는 영역이기 때문입니다.

그래서 요구되는 성질은, 툴에 미리 내장되어 있는 종류의 것이었습니다.

즉, 성질을 스스로 직접 작성해야 하는 상황에 애초에 직면할 기회가 적었던 것입니다.

"툴에 내장되어 있는 성질"과 "스스로 직접 작성해야 하는 성질"이란 무엇일까요? 구체적인 예를 들어 설명하겠습니다.

툴에 미리 내장되어 있는 성질이란 다음과 같은 것입니다.

• 배열의 범위를 벗어난 읽기/쓰기를 하지 않는다
• 0으로 나누지 않는다
• 수치 오버플로 (Overflow)가 발생하지 않는다
• 시스템이 정지된 채 움직이지 않는 상태에 빠지지 않는다

이것들은 어떤 프로그램에도 공통적으로 요구되는 사항입니다. 그렇기에 검증 툴 측에서 미리 "이러한 결함을 찾아라"라는 형태로 가지고 있습니다.

사용자는 성질을 쓸 필요가 없습니다.

프로그램을 불러와서 버튼을 누르기만 하면, 기계가 조사해 줍니다.

반면, 스스로 직접 작성해야 하는 성질이란 다음과 같은 것입니다.

• 이 함수는 AES 암호의 수학적 정의와 일치하며, 어떤 입력에 대해서도 동일한 결과를 반환한다
• 이 컴파일러는 어떤 소스 코드에 대해서도 변환 전후의 동작이 바뀌지 않는다
• 이 인가 엔진 (Authorization Engine)은 어떤 규칙의 조합에 대해서도 정해진 대로 허가 또는 거부를 반환한다

이것들은 프로그램 일반에 공통되는 이야기가 아닙니다. "AES 암호란 무엇인가"를 수학적인 언어로 기술하지 않으면, 애초에 비교할 대상이 없는 것입니다.

그렇기에,

사용자가 스스로 그 성질을 기술하는 것부터 시작해야 합니다.

그리고 이 "기술하는 (writing down)" 작업이야말로 증명 보조 시스템 (Proof Assistant)의 학습 비용이 발생하는 근원입니다. 성질을 기술하기 위해서는 논리학과 타입 이론 (Type Theory)의 소양이 필요합니다.

일본이 강점을 가진 제어 계통의 현장에서 요구되어 온 것은, 대부분 전자인

이미 툴이 가지고 있는 종류의 성질이었습니다. "센서 값이 이상하더라도 제어가 파탄 나지 않는다", "위험한 상태에 이르지 않는다"와 같은 질문은 툴에 내장할 수 있는 형태를 띠고 있습니다.

후자를 필요로 하는 상황에 놓이지 않는다면, 증명 보조 시스템을 도입할 이유도 생기지 않습니다. 이것이 바로 이 절에서 말하고자 하는 바입니다.

다섯째, 그 지도를 지금 AI가 새로 그리고 있습니다.

AI의 출력이 올바르다는 것을 기계적으로 보장하는 것.

이것은 "어떤 입력이 들어올지 모르는" 새로운 기반층 (Foundation Layer)의 문제입니다.

그리고 이 영역에서는, 아직 어느 국가도 타국보다 앞서 있다는 입지를 확고히 하지 못했습니다.

여섯째, Physical AI와 AI 에이전트에서는 시스템의 계층에 따라 필요한 기법이 다릅니다.

로봇이나 자율 주행의 지각·제어 그 자체를 검증하는 것은 성질이 미리 정해져 있는 기법입니다.

"위험 영역에 들어가지 않는다", "입력이 조금 변해도 출력이 파탄 나지 않는다"

── 타입 (Type)이 정해져 있기 때문입니다.

반면, 에이전트에게 무엇을 해도 좋은가라는 규칙의 계층에서는, 성질을 사람이 직접 작성할 수밖에 없습니다.

"이 거래는 규제에 부합하는가", "이 대출은 신용 기준을 초과하지 않았는가"

등은 그때마다 직접 작성할 수밖에 없기 때문입니다.

이 "기술하는" 작업이야말로 증명 보조 시스템 학습을 통해 얻을 수 있는 힘입니다.

그 위에서, 증명을 기계가 자동으로 찾을 수 있는 범위라면 기계에 맡기고, 미치지 못한다면 사람이 조립하는

── 실무에서는 두 가지 방식이 모두 사용되고 있습니다.

그리고 이 두 가지를 잇는 "자연어 규칙을 형식적인 사양 (Formal Specification)으로 번역하는" 계층이, 현재 최대의 미해결 과제이자 최전선입니다.

머신러닝 (Machine Learning)의 소양과 증명 보조 시스템의 소양이 모두 필요한 곳입니다.

"그것도 똑똑한 AI 에이전트에게 맡기면 되지 않을까?"라는 의문은 당연합니다. 실제로 AI에게 사양을 쓰게 하는 연구는 진행되고 있습니다.

하지만,

전적으로 맡길 수는 없습니다.

이유는 "AI가 거짓말을 하기 때문"이 아닙니다.

증명에 대한 거짓말이라면 검증기 (Verifier)가 걸러냅니다. 문제는 다른 곳에 있습니다.

"그 사양이 인간의 진정한 의도를 나타내고 있는가"만은 기계가 확인할 방법이 없기 때문입니다.

대조해야 할 대상 ── 의도 ── 가 형식적인 세계에 존재하지 않기 때문입니다. 게다가 사양과 증명을 모두 AI에게 맡기면,

증명하기 쉬운 약한 사양을 작성함으로써 목표를 달성해 버리는 유인 (Incentive)이 발생합니다. 실제로 자연어로부터 코드와 사양을 생성하는 연구에서는,

자명한 사양으로 검증기를 만족시켜 버리는 "공허한 검증 (Vacuous Verification)"에 대한 대처가 필요했다고 보고되었습니다. 또 하나,

형식 검증 (Formal Verification)의 가치는 "아마 맞을 것이다"가 아니라 "증명되었다"라고 말할 수 있는 데 있습니다. 사양 생성을 확률적인 메커니즘에 맡겨버리면, 사슬의 첫 번째 고리가 확률적이 되어

전체가 "아마 맞을 것이다"로 떨어지게 됩니다. 사용하는 이유 그 자체가 훼손되는 것입니다.

AI가 사양(Specification)을 초안 작성하는 것과, 확인하는 인간을 불필요하게 만드는 것은 별개의 문제입니다. 이 논점은 제5부에서 다시 자세히 다루겠습니다.

일곱 번째로, 여기에 일본이 지금까지와는 다른 형태로 참여할 수 있는 가능성이 있습니다.

일본은 Physical AI의 현장

── 로봇, 자동차, 공장

── 를 세계 유수의 규모로 보유하고 있습니다.

검증해야 할 대상을 가지고 있다는 것 자체가, 이 분야에서는 희귀한 자산입니다.

이상을 바탕으로 한 실무적인 결론은 다음과 같습니다.

이 언어들은 결코 마이너하지 않습니다. 수학의 최전선과 산업의 기반층에서 지금 실제로 사용되고 있습니다.

다만, 일본의 일반적인 Web 개발 현장에서는 도입 장벽이 높다는 것도 사실입니다. 이 점은 숨기지 않고 말씀드리겠습니다.

배운다면, 우선 Lean 4부터. 브라우저에서 즐길 수 있는 입문 과정이 있고, 커뮤니티가 가장 활발하며, 막혔을 때 물어볼 수 있는 곳이 있습니다.

**향후 니즈가 늘어날 것으로 보이는 직역은 해외·기반 산업·그리고 「AI × 증명 지원계」**입니다. 특히 마지막은 머신러닝 (Machine Learning) 소양을 가진 분들에게 유리한, 이제 막 태동한 영역입니다.

• 다만,
  「AI 시대의 도래로 수요가 급증하고 있다」는 표현은 현시점에서는 다소 과합니다. 실무를 움직이는 양은 아직 자동화 기법 쪽이 더 많습니다. 증명 지원계의 수요는 이제 막 시작된 단계입니다. 이 견해의 근거는 기사 안에서 서술하겠습니다.

학습을 시작하는 기준은 명확합니다. 명제 논리(Propositional Logic)·술어 논리(Predicate Logic)·자연 연역(Natural Deduction)까지 왔다면, 이제 Lean 4를 만져봐도 좋습니다. 논리학을 체계적으로 마스터한 뒤에 시작해야 한다는 순서는 필요하지 않습니다. 오히려 그것을 하려다가 힘이 다 빠져버리는 경우가 더 많습니다.

이 기사는 다음과 같은 분들을 위해 작성되었습니다.

• 고교 수학은 상당히 잊어버렸다

• Python으로 머신러닝 (Machine Learning) 업무를 하고 있다 (타입 힌트(Type Hint)는 쓰지만, 타입 시스템(Type System)을 깊게 배운 적은 없다)

• 논리학, 정리 증명(Theorem Proving), 형식 증명(Formal Proof), 함수형 프로그래밍(Functional Programming), 대학 수준의 수학 ── 이 중 어느 것도 체계적으로 배운 경험은 없다

• 하지만 「증명을 컴퓨터로 검증한다」는 세계에 왠지 모르게 끌리고 있다

예비 지식은 필요 없습니다. 이 기사는 거기서부터 시작할 수 있도록 작성되었습니다.

"Lean이나 Coq이 궁금하지만, 어디서부터 손을 대야 할지 모르겠다"

이 기사는 여러분이 그러한 상태에서 벗어나 졸업하는 것을 돕는 것이 목적입니다.

구체적으로는 다음 질문들에 순서대로 답하겠습니다.

• 이 언어들은 마이너한가요?

• 실무에서 사용할 수 있는 직장은 어느 업계의 어느 직종인가요?

• 기계가 자동으로 조사해 주는 도구가 있는데, 왜 인간이 증명을 써야 하나요?

• 서구권에서는 그 「인간이 증명을 써야만 하는 상황」이 구체적으로 무엇이었나요?

• 일본에서는 왜 그 수요가 적은가요? 방대한 테스트로 버텨온 것인가요?

• 배우는 데 시간과 에너지가 많이 들 것 같은데, 커리어로 이어질까요?

• 논리학 학습이 어느 정도 진행되어야 정리 증명·형식 검증을 무리 없이 배울 준비가 될까요?

• 수많은 정리 증명 언어·형식 증명 언어 중에서 어떤 언어를 어떤 경로로 배우면 좋을까요?

본론에 들어가기에 앞서, 기술의 전체상을 한 장의 지도로서 보여드리겠습니다.

세부 사항은 나중에 자세히 설명할 것이므로, 여기서는 "그런 지도가 있구나"라고 바라보는 것만으로 충분합니다.

「프로그램이나 시스템의 올바름을 수학적으로 확인하는」 기술은 통칭하여 **형식 기법 (Formal Methods)**이라 불립니다.

다만, 이 용어가 가리키는 내용은 하나가 아닙니다.

성격이 완전히 다른 기술들이 같은 「형식 기법」이라는 이름 아래 여러 개 포함되어 있습니다.

이 부분을 혼동하면 배우는 길을 잘못 들게 됩니다.

따라서 본 기사에서는 학습 경로를 생각하기 위해, 형식 기법을 편의상 4가지 계통으로 나눕니다.

이는 학술적으로 확립된 분류가 아니라, 본 기사의 설명을 위해 설정한 구분입니다. 실제로는 이들이 서로 겹치기도 합니다.

예를 들어

TLA+는 모델 검사(Model Checking)뿐만 아니라 TLAPS라는 정리 증명 기구도 가지고 있습니다.

Dafny도 내부적으로 여러 기법을 조합하여 사용합니다. 그럼에도 불구하고,

「누가 사양을 쓰고, 누가 증명을 만드는가」라는 축으로 나누어 두면 학습 방법을 고민하는 데 도움이 됩니다. 그 목적을 위한 구분이라고 생각해주시기 바랍니다.

이 지도에서 **가장 중요한 것은 「인간이 어디까지 관여하는가」**입니다.

그리고 그것은 두 가지 질문으로 결정됩니다.

질문 1: 증명하고 싶은 성질을 스스로 직접 써 내려가야 하는가.

질문 2: 그 증명을 기계가 스스로 찾아낼 수 있는가.

③④ 타입은, 성립 여부를 증명하고 싶은 성질이 도구에 내장되어 있으며, 증명 또한 기계가 찾습니다. 말하자면 「버튼을 누르면 기계가 조사해 주는」 편리함이 있습니다. 다만, 확인할 수 있는 것에는 한계가 있습니다.

② 타입은, 증명하고 싶은 성질은 사람이 쓰지만, 증명은 기계가 찾습니다.

**① 타입 (이 기사의 주제)**은, 증명하고 싶은 성질을 사람이 쓰고, 증명의 경로도 사람이 설계합니다. 훈련이 필요하지만, 그만큼 직접 써 내려간 사양(Specification)에 대해 매우 강력한 보증을 얻을 수 있습니다.

본 기사가 다루는 것은 ① 대화형 증명 지원계 ── 특히 Lean, Rocq, Agda, Idris, Isabelle입니다.

왜 편리한 ③④만으로는 부족하며, 수고스러운 ①이 굳이 필요한 것일까요?

그 이유는 제2부에서 자세히 해설하겠습니다. 이 기사의 핵심에 해당하는 부분입니다.

우선은, **「형식 기법(Formal Methods)에는 여러 종류가 있으며, 이 기사는 그중 『사람이 사양을 쓰고, 증명의 경로도 설계하는』 계통을 주제로 한다」**라고만 머릿속 한구석에 두시기 바랍니다.

표에 열거한 ①~④는 모두 생소한 용어였을지도 모릅니다.

여기서 각각의 내용을 간결하게 소개하겠습니다.

지금은 전체적인 상을 어렴풋이 파악하는 것만으로도 충분합니다.

여기서 소개하는 ①~④는 모두, 「수많은 테스트 케이스를 자동으로 만들어 하나씩 전부 시도하는 것」이 아닙니다.

테스트는 말하자면 「입력을 몇 가지 시도해 보고, 우연히 동작하니까 괜찮을 것이다」라고 확인하는 방법입니다.

입력이 무수히 많다면 전부 시도할 수 없습니다.

시도한 입력에서는 동작하더라도, 시도하지 않은 입력에서 버그가 숨어 있을지도 모릅니다.

이것이 테스트의 한계입니다.

앞서 표로 나타낸 ①~④는 모두 이 한계를 각자의 방식으로 극복하려고 합니다.

문제는, 하나씩 실제로 동작시켜 확인하는 방식을 취하는 한, 입력이 무수히 많다면 어떻게 해도 테스트를 다 할 수 없다는 어려움입니다.

이것은 원리적인 한계입니다.

그렇다면 이 한계를 넘으려면 무엇을 어떻게 바꿔야 할까요?

열쇠는 개별 입력에 대해 실제로 실행하고 그 결과를 확인한다는 방식을 버리는 것입니다.

왜냐하면 이 방법을 채택하는 한, 확인할 수 있는 것은 실제로 테스트를 수행할 때 실행한 유한한 개수의 입력에 대한 결과로 한정되기 때문입니다.

입력이 무수히 많다면, 아무리 실행을 거듭해도 아직 테스트를 실시하지 못한, 미검증 입력 케이스가 남게 됩니다.

한계는 바로 여기서 발생합니다.

그렇다면, 실제로 테스트 케이스를 실행해 봄으로써 실시한 입력에 대한 결과를 확인한다는 방식 이외의 방법에서 활로를 찾을 수밖에 없습니다.

하지만 어떻게 하여 「아직 실행하지 않은 입력에 대해서도 올바른 결과를 얻을 수 있음」을 보여줄 수 있을까요?

표에 열거한 4가지 계통은 여기서 서로 다른 접근 방식을 선택하게 됩니다.

그 접근 방식은 크게 세 가지로 나뉩니다.

수학적 논리로 이끌어내는 접근 방식

입력을 개별적으로(하나하나) 실행해 나가는 것이 아니라, 「모든 경우에 대해 성립한다」는 것을 수학적 논법(귀납법 등)을 통해 이끌어내는 접근 방식입니다.

테스트를 단 한 번도 실행하지 않고도, 무수히 많은 입력 사례에 대해 발생할 수 있는 결과를 증명합니다.

이것이 ①의 증명 보조 시스템 (Proof Assistant)입니다.

범위를 구분하여 그 안을 망라하는 접근 방식

대상을 상태가 유한해지는 모델로 잘라낸 뒤, 그 범위 안에서는 상태를 하나도 빠짐없이 조사하는 접근 방식입니다.

②나 ③의 모델 검사 (Model Checking)가 이에 해당합니다.

값 그 자체가 아니라, 값의 성질을 쫓는 접근 방식

개별 값을 하나씩 확인하는 대신, 그 변수에 들어가는 값이 어떤 성질을 갖는지를 추적합니다.

예를 들어, 변수 $x$에 $3$이 들어가는 경우, $7$이 들어가는 경우, $11$이 들어가는 경우... 와 같이 하나씩 조사하는 것이 아니라, "$x$에 들어가는 것은 양수뿐이다"라고 파악한 상태에서 그대로 해석을 진행합니다.

이렇게 하면 $x$가 가질 수 있는 값이 아무리 많아도 단 한 번의 해석으로 끝납니다.

다만, 해석 도구가 $x$에 대해 파악하고 있는 것은 "양수이다"라는 점뿐입니다.

따라서 $x$가 $0$이 되지 않는다는 것은 확실히 말할 수 있으므로 "$0$으로 나눌 위험은 없다"라고 판정할 수 있지만, $x$가 $100$ 미만인지까지는 판정할 수 없습니다.

판단이 서지 않는 부분은 안전을 위해 "위험할지도 모른다"라고 경고합니다.

그 결과, 진짜 위험을 놓치는 일은 없지만, 실제로는 문제가 없는 부분까지 경고해 버리는 경우가 있습니다. ③의 정적 분석 (Static Analysis)이 이 접근 방식을 채택합니다.

참고로, 엄밀한 학술 용어로는 이처럼 값을 성질로 묶어서 다루는 조작을 추상화 (Abstraction), 그 사고방식에 기반한 기법 전체를 **추상 해석 (Abstract Interpretation)**이라고 부릅니다.

즉, "모든 경우를 하나씩 골라서 확인하는" 것이 아닙니다.

수학적인 논법으로 이끌어내거나, 범위를 구분하여 그 안을 망라하거나, 값의 성질로 묶어서 안전한 쪽으로 판정하거나.

어떠한 접근 방식에도 "어떤 입력을 조사할지 선택하는" 단계가 없습니다.

이 점이 테스트와의 결정적인 차이입니다.

테스트에서는 무수히 많은 입력 중에서 시험할 것을 골라야만 합니다. 시간은 유한하기 때문입니다.

그렇기에, 선택하지 않은 입력이 반드시 남게 됩니다.

반면, 세 가지 접근 방식은 모두 선택하지 않습니다.

수학적 논법은 모든 경우를 묶어서 다루고,

모델 검사는 잘라낸 범위를 하나도 빠짐없이 다하며,

정적 분석은 개별 값을 구별하지 않고 계산합니다.

선택에서 누락되는 것이 애초에 발생하지 않는 것입니다.

그렇기에 테스트로는 도달할 수 없는 범위까지 정당성을 주장할 수 있는 것입니다.

다음 두 가지는 무엇이 다를까요?

범위를 구분하여 그 안을 망라하는가

값의 성질로 묶어서 안전한 쪽으로 판정하는가

차이는 **상태를 일일이 세어 올리는가 (Enumeration)**에 있습니다.

모델 검사 (두 번째)는 상태를 세어 올립니다.

대상을 유한한 개수의 상태로 기술한 뒤, 그 상태를 하나도 빠짐없이 따라갑니다. "변수 $x$는 $0$부터 $100$까지"라고 정하면, 그 $101$가지 경우를 모두 조사하는 것입니다. 망라적으로 탐색하는 (Exhaustive Search) 방식입니다.

그에 반해, 정적 분석 (세 번째)은 상태를 세어 올리지 않습니다.

대신에, 변수가 가질 수 있는 값을 미리 정해둔 유한한 개수의 기호로 대체합니다.

예를 들어, "양수", "영", "음수"의 세 가지를 준비하여 $3$도 $7$도 $11$도, 모두 "양수"라는 기호 하나에 할당합니다.

그리고, 이 기호들끼리 연산을 진행합니다.

"양수 $ imes$ 양수 $=$ 양수", "양수 $+$ 양수 $=$ 양수"와 같은 식입니다.

$x$가 "양수"이고 $y$가 "양수"라는 것을 알고 있다면, $x imes y$를 실제로 계산하지 않고도 결과가 "양수"임을 이끌어낼 수 있습니다.

$3 imes 7$인지 $11 imes 5$인지를 일일이 확인할 필요가 없어지는 것입니다.

이렇게 값을 기호로 대체한 채로, 프로그램의 시작부터 끝까지 계산을 통과시키는 것입니다.

한쪽은 "모든 상태를 본다", 다른 한쪽은 "기호로 대체하여 계산한다".

이상이 두 가지를 가르는 결정적인 차이입니다.

이하, 네 가지 계통을 하나씩 살펴보며 풀어가겠습니다.

인간이 수학적 증명을 한 단계씩 써 내려가면, 기계가 그 증명에 빈틈이 없는지 엄격하게 체크한다.

그런 도구입니다.

Lean, Rocq (구 Coq), Agda, Idris, Isabelle이 이에 해당합니다.

학교 수학에서 "증명하시오"라는 문제를 풀었던 것을 떠올려 보세요.

그것을 기계를 상대로, 기계가 절대 놓치지 않는 엄격함으로 수행한다는 이미지입니다.

테스트와의 차이는 결정적입니다.

이것은 입력을 시험하는 것이 아니라, 수학적으로 증명합니다.

예를 들어, "모든 입력에 대해 이 성질이 성립한다"는 것을 수학적 귀납법 (Mathematical Induction) 등을 사용하여, 무한히 존재하는 경우를 한꺼번에 묶어서 증명하는 것입니다.

그렇기 때문에, 증명된 성질에 대해서는 테스트하지 않은 입력에서도 성립함이 보장됩니다.

수고는 들지만, 작성한 사양 (Specification)에 대해 매우 강력한 보장을 얻을 수 있습니다.

"최강의 수법"은 아닙니다. 보장의 강도는

무엇을 사양으로 작성했는지, 어떤 논리 체계 (Logical System)를 사용했는지, 그리고 컴파일러나 하드웨어를 어디까지 신뢰하는지에 따라 달라집니다. 증명 지원 시스템이 보장하는 것은 어디까지나 작성된 사양에 대한 올바름입니다.

강점은 "보장의 절대적인 강도"가 아니라, "보장하고 싶은 성질을 자유롭게 작성할 수 있다는 것"에 있습니다. 그 대신 사양과 증명을 구축하는 비용이 높다 ── 이것이 트레이드오프 (Trade-off)입니다.

여기서 중요한 유보 사항을 하나 말씀드립니다. 형식 증명 (Formal Proof)은 "버그가 절대 없다"는 것을 마법처럼 보장하는 것이 아닙니다.

정확하게는, **"명확하게 정의된 사양에 대해 프로그램이 그 사양을 만족함"**을 증명합니다.

즉,

사양을 쓰는 방식 자체가 틀렸다면, 그 오류까지 포함하여 증명해 버리는 것입니다. "사양이 인간의 실제 의도와 일치하는가"를 확인하는 것은 어디까지나 인간의 몫으로 남습니다.

인간이 "이렇게 동작해야 한다"라는 사양을 쓰고, 그 증명을 기계가 스스로 찾는 도구입니다.

①과의 차이는, 증명을 사람이 조립하느냐 아니냐에 있습니다. ①에서는 사람이 증명을 쓰지만, 여기서는 쓰지 않습니다. 사양만 작성하면 나머지는 기계가 찾습니다.

대표적인 것이 두 종류 있습니다.

Dafny, F* (에프스타) ── 코드에 사전 조건 (Pre-condition), 사후 조건 (Post-condition), 불변 조건 (Invariant)을 주석으로 작성하면, 내장된 **SMT 솔버 (SMT Solver)**라는 자동 증명 엔진이 증명을 찾습니다. 찾으면 그것으로 끝입니다.

TLA+ ── 프로그램 코드가 아니라, **그 전 단계인 "설계도"**의 올바름을 확인하는 데 적합합니다. Amazon이 자사의 거대한 클라우드 서비스 설계 체크에 사용하고 있습니다. 설계가 취할 수 있는 상태를 기계가 빠짐없이 조사하여, "어떤 순서로 처리가 일어나도 좋지 않은 상태에는 결코 도달하지 않는다"는 것을 확인합니다.

이 계통은 ①과 ③의 중간에 위치합니다. 성질은 스스로 작성하지만 (①과 동일), 증명은 기계가 찾습니다 (③, ④와 동일).

이 위치 설정이 제2부에서 중요해집니다.

작성한 프로그램을 실제로 실행하지 않고 기계가 자동으로 조사하여, "여기서 에러가 발생할 수 있다", "위험한 곳이 있다"라고 알려주는 도구입니다.

Astrée나 Frama-C는 항공기 등의 C 언어 프로그램을 해석하는 데 사용되어 왔습니다.

인간은 증명을 쓰지 않고, 버튼을 누르면 기계가 답을 내는 것이 특징입니다.

이 부분은 오해하기 쉬운 곳이므로 조금 자세히 설명하겠습니다.

이 계통도 테스트처럼 입력을 여러 개 시도하는 것이 아닙니다. 방법은 크게 두 가지가 있습니다.

모델 검사 (Model Checking)

검사하고 싶은 시스템을 취할 수 있는 상태가 유한해지도록 "모델 (Model)"로 표현한 후, 그 모델이 취할 수 있는 상태를 기계가 체계적으로 조사하는 수법입니다.

테스트가 "입력을 표본으로서 시도"하는 것에 반해, 모델 검사는 그 모델의 범위 내에서는 빠짐없이 조사한다는 점이 다릅니다.

정적 분석 (Static Analysis) (특히 추상 해석 (Abstract Interpretation)이라는 수법)

개별 값을 하나씩 조사하는 대신, "이 변수는 양수다"와 같이 값의 성질로 묶어서 분석합니다.

이 방식은 안전한 쪽으로 치우치도록 (Conservative) 만들어져 있습니다.

즉, 정말로 위험한 곳을 놓치는 일은 없지만, "위험할지도 모른다"며 실제로는 문제가 없는 곳까지 경고를 보내는 (오경보/False Positive가 발생하는) 경우가 있습니다.

**"놓치는 것은 제로, 단 헛스윙은 있음"**이라고 생각하십시오.

"결국 모든 패턴을 체크하는 것인가, 아닌가?"

이 질문에 대한 답은, "만든 모델의 범위 내에서는 모든 패턴을 조사한다. 다만, 그 모델은 현실의 시스템을 단순화한 것이다"가 답변입니다.

이것은 무슨 뜻일까요.

예를 들어, "변수 $x$는 0~100의 정수"라고 정하여 모델을 만들면, 그 101가지 경우를 하나도 빠짐없이 조사합니다. 하지만 현실의 프로그램에서는 $x$가 64비트 정수일 수도 있습니다.

거기까지 포함하면 상태 수(state number)가 천문학적으로 늘어나서 전부 조사할 수 없습니다(이를 상태 폭발 (state explosion)이라고 부릅니다). 그래서 검사할 수 있는 크기로 모델을 간략화한 다음, 그 범위 내에서 모든 패턴을 조사하는 것입니다. 실무에서는 이러한 상태 폭발을 피하기 위해, 상태를 영리하게 묶어서 다루는 기법 (심볼릭 모델 검사 (symbolic model checking))이나, 탐색 범위를 미리 제한하는 기법 (유계 모델 검사 (bounded model checking)) 등 다양한 방안이 사용됩니다.

결론적으로,

"테스트처럼 일부만 시도하는 것"은 아니지만, "현실 시스템의 모든 가능성을 완전히 조사하는 것"도 아닙니다. "잘라낸 모델 안에서는 전수 조사하되, 모델 밖은 보증하지 않는다"

이것이 모델 검사 (model checking)의 실체이자 한계입니다.

**모델 검사 (model checking)**와 **정적 분석 (static analysis)**은, **"실행한 입력에 대해서만 올바름을 확인할 수 있는" 테스트와 달리, "미리 정해둔 범위에 대해 망라적으로 올바름을 보증하는 것"**을 목표로 합니다.

다만, 복잡한 수학적 성질을 자동으로 확인하는 데에는 한계가 있습니다.

그 영역은 ①의 **증명 보조 도구 (proof assistant)**가 담당합니다.

이것은 성격이 완전히 다릅니다.

소프트웨어가 아니라, 반도체 칩의 회로가 올바르게 설계되었는지를 검증하는 분야입니다.