MoonBit 0.9: 일급 형식 검증 소개

코드 생성이 가속화되면서, 소프트웨어 공학의 핵심 문제는 더 이상 외면하기 어려워졌습니다. AI가 대량의 코드를 생성하는 동안에도, 그 코드가 신뢰할 수 있고 반드시 만족해야 하는 성질에 의해 제약되도록 하려면 어떻게 해야 할까요?

최근 기술 매체들은 겉보기에는 완성된 것처럼 보였지만 인증, 접근 제어, 데이터베이스 권한에 심각한 결함이 포함된 AI 생성 호스팅 애플리케이션을 보도했습니다. 그 결과 수만 건의 사용자 기록에 영향을 미치는 유출이 발생했습니다.

관련 보고서: The Register coverage

이 사례가 드러낸 핵심 문제는, 애플리케이션이 겉으로는 작동하는 것처럼 보여도 시스템이 신뢰할 만한지를 실제로 결정하는 제약 조건은 명확하게 표현되지도 않고 체계적으로 검증되지도 않을 수 있다는 점입니다.

테스트와 퍼징은 여전히 중요하지만, 둘 다 표본과 커버리지에 의존합니다. 이들은 더 강한 질문, 즉 프로그램이 중요한 성질을 항상 만족하는가에 답하는 데에는 적합하지 않습니다. 이것만으로는 이런 종류의 문제를 근본적으로 제거하기에 여전히 충분하지 않습니다.

형식적 증명은 더 분명한 앞으로의 길을 제시합니다. 반복적인 테스트를 통해 정확성을 근사하는 대신, 우리는 프로그램이 반드시 만족해야 하는 성질을 직접 기술하고 구현이 실제로 그것을 만족하는지 자동으로 검사할 수 있습니다. 더 중요한 점은, 기저 가정이 타당하기만 하다면 증명 과정 자체도 AI에 의해 대규모로 생성될 수 있다는 것입니다.

MoonBit 0.9의 핵심 진전 가운데 하나는 AI 협업을 위해 구축된 완전한 형식 증명 기능 집합입니다. 이는 AI가 비자명한 증명을 자동으로 구성하고, 명세를 생성하며, 구현이 그 명세를 만족하는지 검증하도록 도와주어, 대규모 고품질 검증 가능 코드 생성을 위한 기반을 제공합니다. 이는 이 분야에서 나온 최초의 이런 종류의 돌파구이기도 합니다.

고전적인 예로 이진 탐색을 생각해 봅시다. 이진 탐색은 단순해 보이지만, 악명 높을 정도로 구현을 잘못하기 쉽습니다. 2006년 Joshua Bloch는 Java 표준 라이브러리의 이진 탐색 구현에 있던 정수 오버플로 버그에 대해 썼는데, 이 결함은 발견되기 전까지 거의 10년 동안 실제 환경에 남아 있었습니다.

위 그림은 MoonBit에서 이진 탐색을 완전히 검증한 예를 보여줍니다. 왼쪽에는 계약과 루프 불변식이 주석처럼 달린 함수 구현이 있고, 오른쪽에는 술어 정의 파일이 있습니다. 아래쪽 터미널 출력은 검증이 완전히 성공했음을 보여줍니다.

계약: 함수가 하는 수학적 약속​

함수 시작 부분의 proof_requires(sorted(xs))와 proof_ensures(binary_search_ok(xs, key, result))는 함수와 외부 세계 사이의 계약을 이룹니다. 호출자는 입력 배열이 정렬되어 있음을 약속합니다. 함수는 반환값이 올바름을 약속합니다. 결과를 찾았다면 그 결과는 실제로 목표 원소이고, 아무것도 반환하지 않았다면 목표값은 진짜로 배열에 존재하지 않습니다. 이것들은 주석이나 문서가 아닙니다. 기계가 엄격하게 검사하는 제약 조건입니다.

술어: 수학으로 모호함 제거하기​

오른쪽의 .mbtp 파일은 계약에 등장하는 모든 개념에 대해 정확한 정의를 제공합니다. 예를 들어, “sorted”는 다음과 같이 정의됩니다. 유효한 임의의 인덱스 i <= j에 대해 xs[i] <= xs[j]입니다. “이진 탐색의 정확성”은 다음과 같이 정의됩니다. 함수가 Some(i)를 반환하면 xs[i]는 목표값과 같고, None을 반환하면 배열의 어떤 원소도 목표값과 같지 않습니다. 모든 개념은 한정자와 논리 연결사로 표현되어, 자연어가 숨길 수 있는 모호함을 남기지 않습니다.

루프 불변식: 코드와 증명을 잇는 다리​

where 블록의 proof_invariant 항목들은 루프의 모든 반복에서 참으로 유지되어야 하는 성질을 설명합니다. 탐색 구간 [i, j)는 항상 유효하게 유지되고, 구간 왼쪽의 모든 원소는 목표값보다 작으며, 구간 오른쪽의 모든 원소는 목표값보다 큽니다. 이러한 불변식이 평범한 루프를 단계별로 추론할 수 있는 대상으로 바꿔 줍니다.

검증이 작동하는 방식​

개발자가 moon prove를 실행하면, MoonBit 도구 체인은 프로그램 논리와 술어 정의를 제약 해결 문제로 변환하고 이를 Z3 같은 SMT 솔버에 넘겨 자동 검증을 수행합니다. 솔버는 루프 불변식이 초기 상태에서 성립하는지, 각 반복 이후에도 보존되는지, 루프가 종료될 때 사후조건이 따라오는지를 하나씩 검사합니다. 여기서 검증되는 것은 프로그램이 몇몇 입력에 대해 우연히 올바른 답을 반환한다는 사실이 아니라, 가능한 모든 입력을 포괄하는 수학적 증명입니다. 다시 말해, 어떤 길이의 어떤 정렬된 배열과 어떤 목표값에 대해서도, 이 이진 탐색 구현은 자신의 계약을 만족합니다.

MoonBit는 AI를 사용해 AVL 트리 검증도 도울 수 있습니다: moonbit-community/verified/tree/main/avl

여기서 더 중요한 질문이 생깁니다. 형식 검증 자체가 너무 어렵다면, 그것이 어떻게 널리 채택될 수 있을까요?

형식 검증에서 가장 위압적으로 느껴지는 부분은 증명 자체를 작성하는 일입니다. 루프 불변식은 매우 신중하게 선택되어야 합니다. 사후조건을 함의할 만큼 충분히 강해야 하면서도, 모든 반복 이후에 참으로 남을 만큼 충분히 안정적이어야 합니다.

MoonBit의 핵심 연구 방향 가운데 하나는 AI를 사용해 그 장벽을 낮추는 것입니다. 실제로 위에서 언급한 이진 탐색과 AVL 트리 검증의 상당 부분은 루프 불변식, 술어 정의, 그리고 유도 역할을 하는 proof_assert 문들의 연쇄를 포함해 AI 에이전트의 도움으로 생성되었습니다. 개발자는 구현과 의도한 계약을 제공하고, AI는 후보 불변식과 중간 단언을 제안한 다음, 정리 증명기가 그것들을 기계적 엄밀성으로 검사합니다.

이는 우아한 협업 모델을 만들어 냅니다. AI는 추측하고, 증명기는 검사합니다. AI는 틀릴 수 있습니다. 너무 약한 불변식이나 필요한 단계를 빠뜨린 중간 단언을 제안할 수도 있습니다. 그러나 잘못된 추측은 증명기의 검토를 통과할 수 없습니다. 증명기는 각 추론 단계가 유효함을 확인하거나, 어떤 목표가 증명될 수 없는지 정확히 지적하여 AI가 수정하고 다시 시도할 수 있게 합니다. 최종 결과는 AI 환각 때문에 그럴듯하게 들리는 것이 아니라, 언제나 수학적으로 검증된 것입니다.

관련 저장소: moonbit-community/verified

오늘날 형식 검증 접근법은 대체로 두 범주로 나뉩니다.

기존 언어에 검증 지원을 추가하는 방식, 예를 들어 C용 Frama-C, Java용 OpenJML, Rust용 Creusot 같은 것들입니다.

이들 시스템의 장점은 실제 제품 코드를 직접 검증할 수 있다는 점입니다. 하지만 구조적인 문제가 있습니다. 검증은 언어 자체와 분리되어 있습니다. 계약과 명세는 주석이나 매크로를 통해 주입되며, 사실상 언어가 진정으로 볼 수 없는 외부 부가물처럼 작동합니다. 그 결과 IDE는 검증 주석을 네이티브하게 이해할 수 없어서 자동 완성, 탐색, 진단에 추가 플러그인 지원이 필요합니다. 빌드 시스템은 검증의 존재를 알지 못하므로 개발자는 별도의 도구 체인을 수동으로 유지해야 합니다. 그리고 언어가 발전하면 검증 도구는 종종 몇 달, 심지어 몇 년씩 뒤처집니다.

검증을 위해 특별히 설계된 언어, 예를 들어 Microsoft의 Dafny, Rocq(구 Coq), Lean 같은 것들입니다.

이들 시스템은 더 강력한 검증 기능과 언어와 증명 사이의 더 자연스러운 통합을 제공합니다. 그러나 일반 목적 프로그래밍 언어가 갖는 생태계 기반은 대체로 부족합니다. 성숙한 패키지 관리도 없고, 폭넓은 서드파티 라이브러리 생태계도 없으며, 큰 산업 사용자 기반도 없습니다. Rocq와 Lean은 표현력이 매우 높지만, C나 Java 같은 기존 언어를 검증하려면 증명기 내부에 대상 언어의 의미론을 다시 구축해야 하며, 이는 비용이 많이 들고 유지보수도 어렵습니다. Ada/SPARK는 산업 수준의 검증 강도와 실제 배포 이력을 모두 갖춘 몇 안 되는 접근법 중 하나이지만, Ada 생태계에 묶여 있고 현대적인 클라우드 네이티브 및 웹 개발과의 접점은 매우 적습니다.

MoonBit는 수직 통합을 통해 다른 길을 택합니다. 계약, 술어, 루프 불변식, 그리고 proof_assert는 모두 주석이나 매크로 안에 숨겨진 이류 구성물이 아니라 언어 문법의 일급 요소입니다. 컴파일러가 이를 직접 이해합니다. 이는 IDE가 일반 코드와 같은 방식으로 검증 주석에 대해 문법 강조, 자동 완성, 타입 검사, 오류 위치 표시를 제공할 수 있음을 뜻합니다. moon prove는 도구 체인에 내장된 명령으로, moon build, moon test와 나란히 존재하므로 개발자는 별도의 도구 체인을 구성하거나 작업 흐름을 전환할 필요가 없습니다. 코드를 작성하는 것에서부터 증명을 작성하고 검증을 실행하는 것까지, 모든 것이 같은 언어, 같은 IDE, 같은 명령줄에서 이루어집니다.

AI가 증명 작성 비용을 더욱 낮추면서, MoonBit는 역사적 문제 두 가지를 동시에 해결하려고 합니다. 형식 검증은 사용하기에도 너무 어려웠고, 배우기에도 너무 어려웠습니다. 목표는 검증을 더 강력하게 만드는 것만이 아니라, 일반 개발자에게 진정으로 사용할 수 있는 것으로 만드는 것입니다.

이런 맥락에서 형식 검증의 의미도 바뀌고 있습니다. 그것은 더 이상 극소수의 안전 필수 시스템을 위해 남겨진 전문 기법에만 머물지 않습니다. 더 신뢰할 수 있는 소프트웨어로 가는 실용적인 경로가 되어 가고 있습니다. 언어 설계, AI 보조, 도구 체인 통합을 통해 MoonBit는 검증의 장벽을 계속 낮추고, 제약을 표현하고 증명을 생성하며 결과를 검사하는 일이 일상적인 개발 워크플로의 일부가 되도록 더 자연스럽게 만들고자 합니다. 우리는 이 능력이 성숙해짐에 따라 “코드가 올바름을 증명하기”가 테스트를 작성하고 빌드를 실행하는 것만큼 일상적인 일이 되기를 바랍니다.

형식 검증을 넘어, 0.9 릴리스에는 그 밖에도 여러 중요한 업데이트가 포함되어 있습니다. 전체 릴리스 노트는 MoonBit v0.9 Release에서 확인하세요.