정식 검증(형식 검증)

정식 검증은 프로그램이나 회로가 명세대로 동작한다는 사실을 테스트가 아니라 수학적 증명으로 보이는 방법이에요. 테스트는 찾은 경우에만 확인할 수 있지만, 증명은 가능한 모든 입력에 대해 성립한다는 것을 논리로 보장하려고 해요. 그래서 오류 비용이 큰 분야에서 주로 써 왔어요.

정식 검증은 오래전부터 연구된 방법이지만, 증명을 사람이 한 단계씩 써야 해서 비용이 매우 컸어요. 그래서 보안 프로토콜처럼 중요도가 높은 일부 코드에만 제한적으로 쓰였어요. 최근에는 AI가 증명 코드를 대신 작성하면서 적용 범위를 넓힐 가능성이 열리고 있어요.

정식 검증은 먼저 프로그램이 지켜야 할 성질을 수학 명세로 적어요. 예를 들어 과거 대화는 나중에 키가 노출되어도 읽히지 않아야 한다는 조건을 논리식으로 바꾸는 식이에요. 그다음 증명 도구가 코드의 모든 실행 경로가 이 명세를 만족하는지 단계별로 확인해요.

증명 도구는 보통 Lean 같은 증명 보조 언어로 작성되고, 각 단계가 논리 규칙을 따르는지 기계가 검사해요. 한 번 확인된 증명 파일은 다시 실행해도 같은 결과가 나와서 신뢰를 쌓을 수 있어요.

메신저 암호 프로토콜처럼 설계가 복잡하고 실패할 때 피해가 큰 코드에 적합해요. 다만 보안 목표를 수학 사양으로 옮기는 일은 여전히 사람 전문가가 맡아야 하며, 그 정의가 잘못되면 증명도 의미가 없어져요.

항공 제어, 반도체 회로 설계, 금융 거래 엔진처럼 오류 비용이 큰 분야에서도 일부 적용돼요. 적용 조건은 명세를 명확히 쓸 수 있고, 검증할 범위를 좁힐 수 있어야 한다는 점이에요.

정식 검증이 끝난 코드도 명세에 빠진 위험은 막지 못해요. 증명은 약속한 성질이 맞는지만 보장하고, 약속 자체가 충분한지는 따로 판단해야 해요. 이 점을 모르고 완벽하게 안전하다고 오해하기 쉬워요.

증명 비용은 여전히 크고 대규모 시스템 전체에 적용하기는 어려워요. AI가 증명을 생성하더라도 증명 도구나 명세가 틀리면 결과도 틀릴 수 있어서 독립적인 검토가 계속 필요해요.

시험 문제를 몇 개 풀어 보고 합격이라 하는 것이 테스트라면, 모든 경우를 공식으로 증명해 답이 항상 맞다고 보이는 것이 정식 검증이에요. 계산기가 어떤 숫자를 넣어도 덧셈 규칙을 지킨다는 것을 증명하는 셈이에요.

정식 검증을 알면 앱 보안 발표를 볼 때 말로만 안전하다는 주장과 수학으로 확인된 주장을 구분할 수 있어요. 메신저나 금융 인증처럼 일상에서 쓰는 기술이 실제로 무엇을 보장하는지 판단하는 데 도움이 돼요.