결제 한도가 초과되지 않아야 하는 기능, 권한이 없는 사용자가 데이터를 읽을 수 없어야 하는 기능, 장비가 위험한 상태로 전환되면 안 되는 제어 기능이 있다. 이런 기능은 테스트를 많이 돌려도 “모든 경우에 규칙을 지켰다”는 답을 얻기 어렵다.
LLM은 이 간극을 줄일 가능성을 보여주고 있다. 최근에는 LLM을 활용해 100개가 넘는 공개 소프트웨어 라이브러리의 RISC-V 실행 코드에 대해 특정 안전 속성을 증명하려는 대규모 시도가 공개됐다. 다만 그 결과는 모든 환경과 모든 버그에 대한 보장이 아니다. 단일 스레드 정적 바이너리, 정해진 메모리 예산, 특정 CPU와 운영체제 모델, 입력 크기 등의 전제가 붙는다.
CTO와 개발 리드는 여기서 “형식 검증을 전사적으로 도입할 것인가”보다 더 좁은 질문을 먼저 다루는 편이 낫다.
우리 제품에서 실패 비용이 크고, 지켜야 할 규칙을 명확히 쓸 수 있으며, 검증 범위를 통제할 수 있는 기능은 무엇인가.
답은 대개 제품 전체가 아니라 몇 개의 경계 기능에 있다.
형식 검증이 답할 수 있는 질문부터 분리해야 한다
형식 검증은 코드나 설계 모델이 정해진 수학적 조건을 항상 만족하는지 확인하려는 방법이다. 예를 들어 다음과 같은 문장은 검증 목표로 비교적 구체화하기 쉽다.
- 승인되지 않은 역할은 관리자 작업을 수행할 수 없다.
- 계좌·포인트·재고 수량은 정의한 조건 아래 음수가 되지 않는다.
- 한 요청은 동일한 거래를 중복 확정하지 않는다.
- 장비 제어 상태는 허용되지 않은 순서로 바뀌지 않는다.
- 입력 길이와 메모리 조건이 주어진 범위 안에서 실행이 중단되거나 메모리 안전 오류를 내지 않는다.
반대로 “사용자가 불편하지 않아야 한다”, “추천 결과가 적절해야 한다”, “공격에 안전해야 한다”는 문장만으로는 증명 대상이 정해지지 않는다. 보안은 특히 어려운 편이다. 권한 우회, 정보 노출, 시간 차이에서 발생하는 부채널처럼 무엇을 막아야 하는지부터 모델로 표현해야 하기 때문이다.
따라서 형식 검증의 첫 산출물은 증명 코드가 아니라 검증할 속성의 문장이어야 한다. 그 문장을 제품 책임자, 도메인 담당자, 보안 담당자, 개발자가 함께 읽고 같은 의미로 해석할 수 없다면 LLM에게 증명을 맡겨도 범위가 흔들린다.
우선순위는 코드 복잡도보다 오류 비용과 명세 가능성으로 정한다
형식 검증 후보를 고를 때 “가장 복잡한 서비스”부터 집는 경우가 많다. 그러나 복잡한 기능이 항상 좋은 출발점은 아니다. 외부 시스템, 비정형 사용자 입력, 빈번한 정책 변경이 많으면 모델 경계와 요구사항 자체가 계속 바뀔 수 있다.
초기 후보는 아래 두 축으로 나누어 보는 편이 낫다.
| 조건 | 형식 검증 우선순위 | 적합한 접근 |
|---|---|---|
| 오류 발생 시 금전·안전·권한 피해가 크고 규칙을 명확히 쓸 수 있음 | 높음 | 핵심 불변조건을 정해 증명과 테스트를 함께 적용 |
| 오류 비용은 크지만 정책과 예외가 자주 바뀜 | 중간 | 상태 모델과 정책 명세부터 정비하고 좁은 규칙만 검증 |
| 규칙은 단순하지만 오류 비용이 낮음 | 낮음 | 단위 테스트, 정적 분석, 코드 리뷰 중심 |
| 사용자 경험·콘텐츠 품질처럼 정답을 수식으로 정의하기 어려움 | 낮음 | 실험, 관찰, 샘플 검토, 회귀 테스트 중심 |
예를 들어 주문 화면 전체의 동작을 한 번에 증명하려 하기보다, 주문 확정 뒤 재고 차감과 결제 확정이 어떤 순서와 조건에서 일관돼야 하는지부터 좁힐 수 있다. 인증 시스템도 화면 흐름 전체보다 토큰 검증, 권한 전이, 관리자 작업 승인 같은 보안 경계를 먼저 고르는 편이 검증 대상을 관리하기 쉽다.
이 기준은 규제 산업에만 해당하지 않는다. 장애가 나면 수작업 정정이 어렵거나, 고객 간 데이터가 섞이면 안 되거나, 한번 실행된 명령을 되돌리기 어려운 기능도 같은 방식으로 평가할 수 있다.
LLM은 증명 담당자가 아니라 검증 작업의 가속 장치로 써야 한다
형식 검증은 전통적으로 전문 인력과 긴 작업 시간을 요구했다. LLM은 명세 초안 작성, 증명 도구의 문법 처리, 실패한 증명 조건의 탐색, 반복적인 증명 코드 보완에서 도움을 줄 수 있다. 이 변화는 검증 대상을 넓힐 수 있는 이유다.
하지만 LLM이 만든 증명 문서가 그 자체로 신뢰의 근거는 아니다. 확인해야 할 것은 다음 세 가지다.
-
검증기가 증명을 독립적으로 확인하는가
LLM의 설명이나 생성 로그가 아니라, 선택한 검증 도구가 증명과 모델을 기계적으로 검사해야 한다. -
증명한 속성이 제품 요구사항과 같은가
“예외가 발생하지 않는다”는 결과가 “권한 우회가 없다”는 뜻은 아니다. 개발팀은 증명 속성과 실제 위험 시나리오를 항목별로 대응시켜야 한다. -
전제 조건이 운영 환경에서도 유지되는가
단일 스레드, 입력 크기 제한, 특정 라이브러리 버전, 고정된 메모리 조건에서 성립한 증명은 그 조건 밖에서 자동으로 이어지지 않는다. 배포 설정, 동시성, 외부 API, 하드웨어, 운영체제 차이가 모델 밖에 남을 수 있다.
LLM이 형식 검증의 비용을 낮춘다는 말은 “사람의 판단이 사라진다”는 뜻이 아니다. 오히려 사람은 무엇을 증명할지, 어떤 가정을 허용할지, 증명 밖의 위험을 어떻게 다룰지에 더 집중해야 한다.
테스트·정적 분석·리뷰를 대체하지 말고 빈틈을 나눈다
각 방법은 다른 질문에 강하다. 이 구분 없이 형식 검증을 도입하면, 증명 범위 밖의 문제를 놓치거나 검증 비용만 커질 수 있다.
- 형식 검증은 정의한 규칙이 가능한 모든 모델 상태에서 지켜지는지 확인하는 데 맞는다. 상태 전이, 접근 제어, 금액·수량 불변조건, 저수준 메모리 안전 속성이 대표적이다.
- 정적 분석은 코드 패턴, 타입 불일치, 위험한 API 사용, 일부 취약한 구현 관행을 넓게 찾는 데 유용하다. 빠르게 많은 변경을 훑을 수 있지만 제품 고유의 업무 규칙을 모두 이해하지는 못한다.
- 테스트는 실제 통합 환경에서 API, 데이터베이스, 외부 서비스, 사용자 흐름이 기대대로 연결되는지 확인한다. 모델과 운영 환경의 차이를 발견하는 역할도 맡는다.
- 사람의 검토는 요구사항의 누락, 정책 해석의 오류, 위협 모델의 빈칸을 찾는다. 무엇을 증명할지 정하는 단계에서는 특히 대체하기 어렵다.
임베디드 소프트웨어 분야에서도 형식 검증과 모델 기반 테스트를 결합한 사례가 보고된 바 있다. 이 조합이 중요한 이유는 간단하다. 검증은 모델 안의 규칙을 확인하고, 테스트는 모델과 구현·환경이 만나는 지점을 살핀다. 둘 중 하나만으로 충분하다고 두기보다, 어느 위험을 어느 수단이 맡는지 문서로 나누는 편이 낫다.
도입은 한 기능의 불변조건을 CI에 넣는 데서 시작한다
탐색 단계에서는 대규모 플랫폼 전환보다 작은 검증 루프를 만드는 것이 적합하다.
먼저 제품·보안·개발 담당자가 한 기능을 고른다. 그다음 “허용하면 안 되는 상태”를 두세 문장으로 작성한다. 예를 들어 “취소된 주문은 출고 상태로 전환될 수 없다”, “테넌트 식별자가 다른 데이터는 조회 결과에 포함될 수 없다”처럼 쓴다.
이후에는 다음 순서로 범위를 줄여 확인할 수 있다.
- 규칙마다 입력, 상태, 예외, 외부 의존성을 적는다.
- 실제 코드와 분리된 작은 모델 또는 핵심 모듈에서 규칙을 표현한다.
- LLM은 명세·증명 초안·실패 분석을 돕되, 검증 도구의 결과로만 통과 여부를 판정한다.
- 증명한 규칙에는 회귀 테스트와 통합 테스트를 연결한다.
- 배포 환경이 증명의 가정을 깨는 변경을 했는지 코드 리뷰와 CI에서 확인한다.
초기 실험이 실패하는 조기 신호도 분명하다. 팀이 증명하려는 속성을 합의하지 못하거나, 예외 규칙이 회의마다 바뀌거나, 모델을 만들기 위해 실제 동작을 지나치게 단순화해야 한다면 대상 범위가 너무 넓거나 요구사항이 아직 덜 정리된 상태일 수 있다. 이때는 증명 도구나 모델을 바꾸기 전에 정책과 상태 전이를 다시 정리하는 쪽이 낫다.
다음 기술 검토 회의에서는 “LLM으로 무엇을 증명할 수 있는가”보다 이 질문을 먼저 올려보면 좋다.
우리 서비스에서 잘못되었을 때 가장 비싸고, 한 문장으로 금지 상태를 정의할 수 있으며, 운영 조건까지 통제 가능한 기능은 무엇인가.
그 기능 하나가 형식 검증의 첫 범위가 될 수 있다. 그 뒤에야 LLM, 증명 도구, 테스트 자동화에 투자할 이유와 경계가 함께 선명해진다.
