테스트 말고 증명 — 버그가 없음을 수학으로 보장하는 언어 F* 이야기

'테스트는 버그가 있다는 것은 보여줄 수 있어도, 없다는 것은 증명할 수 없다.' 컴퓨터과학자 다익스트라의 유명한 말인데요. 테스트 케이스를 아무리 많이 짜도 결국 우리가 생각해낸 입력만 검사할 뿐, 생각하지 못한 입력에서 터지는 버그는 못 잡아요. 그런데 접근을 아예 뒤집어서, 코드가 명세대로 동작한다는 사실 자체를 수학적으로 증명해버리는 분야가 있어요. 형식 검증(formal verification)이라고 하는데요. 오늘 소개할 F*(에프스타)는 마이크로소프트 리서치와 프랑스 국립연구소 Inria가 만든, 이 분야의 대표적인 '증명 지향 프로그래밍 언어'예요. 이름만 들으면 상아탑 연구용 같지만, 사실 여러분이 오늘 쓴 소프트웨어 안에 이 언어로 증명된 코드가 이미 들어 있을 가능성이 높거든요.

'증명 지향'이 뭐냐면

일반적인 언어의 타입은 int, string 정도의 정보만 담아요. F*는 여기에 조건을 붙일 수 있어요. 이걸 정제 타입(refinement type)이라고 하는데요, 예를 들어 나눗셈 함수의 분모를 그냥 int가 아니라 x:int{x <> 0}, 즉 '0이 아닌 정수'라는 타입으로 선언할 수 있어요. 그러면 0이 들어갈 가능성이 조금이라도 있는 코드는 아예 컴파일이 안 돼요. 런타임에 if로 검사해서 예외를 던지는 게 아니라, 그런 상황이 존재할 수 없음을 컴파일 시점에 수학적으로 확정하는 거예요. 여기에 값에 따라 타입이 달라지는 의존 타입(dependent type)이라는 개념까지 더해지면 '이 함수는 입력받은 리스트와 길이가 같은, 정렬된 리스트를 반환한다' 같은 성질도 전부 타입으로 표현할 수 있어요. 타입이 곧 명세가 되는 거죠.

증명은 누가 하느냐: 자동화가 강점이에요

'그런 걸 다 증명하려면 얼마나 힘든데'라고 생각하실 텐데, 맞아요. 이 분야의 전통적인 도구인 Coq(지금은 Rocq로 개명)나 Lean은 사람이 증명을 한 단계씩 직접 써 내려가는 비중이 커요. F의 강점은 증명의 상당 부분을 Z3라는 SMT 솔버에게 자동으로 맡긴다는 거예요. SMT 솔버가 뭐냐면, 논리식을 주면 그게 참인지 거짓인지 기계적으로 판별해주는 프로그램이거든요. 덕분에 개발자가 타입에 조건을 잘 써놓으면 많은 증명이 별도 작업 없이 자동으로 통과해요. 물론 복잡한 성질은 보조 정리(lemma)를 직접 작성해야 하지만, 순수 증명 도구들보다 진입 장벽이 확실히 낮아요. 그리고 검증이 끝난 코드는 OCaml이나 F#으로 추출해서 쓸 수 있고, Low라는 저수준 부분집합으로 작성하면 C 코드로 뽑아내서 성능이 중요한 실제 제품에 넣을 수도 있어요.

장난감이 아니에요, 이미 여러분도 쓰고 있어요

F가 흥미로운 건 실전 배치 실적이에요. 대표작이 HACL라는 검증된 암호 라이브러리인데요, 암호 알고리즘 구현이 수학적 정의와 정확히 일치하고, 버퍼 오버플로 같은 메모리 오류가 없고, 실행 시간이 비밀값에 따라 달라지지 않는다(타이밍 공격 방어)는 것까지 증명된 코드예요. 이 코드가 Firefox의 암호 모듈에 들어갔고, 리눅스 커널에도 검증된 타원곡선 암호 코드가 채택됐고, 파이썬은 3.12부터 hashlib의 SHA 구현을 HACL 기반으로 교체했어요. 그러니까 파이썬으로 해시 한 번 돌려봤다면 이미 F로 증명된 코드를 쓴 셈이에요. 네트워크 패킷 파서를 검증하는 EverParse는 마이크로소프트 Hyper-V의 네트워크 스택에 들어가 있고요. 이것들은 HTTPS 스택 전체를 검증하겠다는 'Project Everest'라는 장기 프로젝트의 산물이에요. 암호와 파서는 버그 하나가 곧 보안 취약점이 되는 영역이라, 형식 검증의 비용을 치를 가치가 가장 확실한 곳이거든요.

업계 지형에서 보면

형식 검증 도구들은 저마다 영역이 갈려요. Lean은 수학 정리 라이브러리 mathlib와 AI 증명 연구 쪽에서 주목받고 있고, Rocq는 검증된 C 컴파일러 CompCert 같은 굵직한 실적이 있고, Dafny는 AWS가 인증 관련 핵심 서비스 검증에 쓰고 있어요. Rust와 비교하자면, Rust의 소유권 시스템은 메모리 안전을 보장하지만 '로직이 명세대로 동작한다'는 것까지 증명해주지는 않아요. 형식 검증은 그보다 한 층 위의 보장인 거죠. 큰 흐름을 보면, AI가 코드를 대량으로 찍어내는 시대가 되면서 '이 코드가 정말 맞는지 기계적으로 확인하는 기술'의 가치가 오히려 커지고 있어요. 사람이 리뷰할 수 없는 속도로 코드가 생산된다면, 정확성을 보장하는 수단도 자동화되어야 하니까요.

한국 개발자에게

내일부터 웹 서비스를 F로 짜자는 얘기는 당연히 아니에요. 하지만 가져갈 게 셋 있어요. 첫째, 결제나 인증, 외부 입력 파싱처럼 버그 비용이 유난히 큰 모듈이 우리 시스템 어디인지 생각해보는 계기가 돼요. 둘째, '검증된 값'과 '아직 검증 안 된 값'을 타입으로 구분하는 정제 타입의 사고방식은 TypeScript의 브랜디드 타입이나 Rust의 newtype 패턴으로 오늘부터 흉내 낼 수 있어요. 검증 함수를 통과한 문자열만 Email 타입이 되게 만들면, 검증을 빼먹은 코드 경로를 컴파일러가 잡아주거든요. 셋째, 공식 사이트에 'Proof-Oriented Programming in F'라는 무료 튜토리얼 북이 공개되어 있어서 주말 학습거리로 좋아요.

마무리

한 줄로 정리하면, F*는 '테스트 대신 증명'이라는 아이디어를 연구실 밖으로 끌고 나와 Firefox와 리눅스, 파이썬 안에까지 밀어 넣은 언어예요. 여러분은 테스트로 도저히 못 잡아서 고생했던 버그, '이건 증명 수준의 보장이 필요했는데' 싶었던 순간이 있으신가요?