# 형식 증명 (Formal Proof)

형식 증명(Formal Proof)은 수학에서 용어의 의미에 전혀 의존하지 않는 증명입니다. 각 고유한 용어는 명제의 진실성에 영향을 미치지 않고 임의의 고유한 기호로 대체될 수 있습니다. 형식 증명은 정해진 공리에서 출발해 추론 규칙만으로 한 줄씩 결론을 이끌어 내는 기호의 나열이므로, 그 논리 구조는 기계적 검증에 적합합니다. 비형식 증명과 반대됩니다.

## 형식 증명의 본질

- **기호 치환:** 형식 증명에서 각 용어는 고유한 기호로 표현됩니다. 기호를 다른 고유한 기호로 바꾸어도 명제의 참거짓은 달라지지 않으며, 증명은 추론 규칙에 따른 기호 조작만으로 이루어집니다.
- **기계적 검증:** 형식 증명은 구조가 엄격하므로 Coq, Lean, Isabelle 같은 증명 보조기(proof assistant)로 각 단계를 확인할 수 있습니다. 이로써 증명 과정의 인적 오류를 크게 줄일 수 있지만, 검증 도구와 명세가 올바르다는 전제는 여전히 남습니다.

다음과 같이 비교해 볼 수 있습니다.

- **비형식 증명:** 수학 논문의 증명처럼 자연어와 수식을 섞어 쓰고, 독자가 당연하다고 받아들일 단계는 생략합니다.
- **형식 증명:** 생략 없이 모든 단계를 공리와 추론 규칙으로 정당화하므로, 의미를 이해하지 못하는 프로그램도 그 정확성을 확인할 수 있습니다.

## 암호학과 블록체인에서 구별할 개념

암호학과 블록체인 분야에서는 비슷한 이름의 세 가지 개념을 구별해야 합니다.

1. **형식 증명(논리):** 위에서 설명한, 추론 규칙만으로 구성되어 기계로 확인할 수 있는 증명 자체입니다.
2. **증명 가능한 안전성(provable security):** 암호 방식이 명시된 가정(예: 특정 수학 문제가 어렵다는 가정) 아래에서 안전하다는 것을 환원(reduction) 논증으로 보이는 방법입니다. 대부분 비형식적인 수학 증명으로 작성되며, 일부는 증명 보조기로 형식화되기도 합니다.
3. **형식 검증(formal verification):** 프로그램이나 프로토콜이 명세를 만족함을 형식적 방법으로 확인하는 일입니다. 스마트 컨트랙트에서는 취약점이 곧 금전적 손실로 이어지므로, 핵심 컨트랙트의 코드가 명세대로 동작하는지 형식 검증 도구로 확인하기도 합니다.

영지식 증명(ZKP)의 “증명”은 증명자가 검증자에게 비밀을 드러내지 않고 어떤 명제가 참임을 납득시키는 암호 프로토콜을 뜻하며, 형식 증명과는 다른 개념입니다. 다만 영지식 증명 시스템의 건전성·영지식성 같은 성질은 수학적으로 증명되며, 그 증명이나 회로 구현을 형식 검증하는 연구도 진행되고 있습니다.

## 형식 증명이 중요한 이유

암호 시스템은 민감한 정보와 자산을 다루므로 직감이나 모호한 보증에 의존하는 것만으로는 충분하지 않습니다. 형식 증명과 형식 검증은 명시된 가정과 명세 아래에서 시스템이 의도한 성질을 만족함을 확인해 줍니다. 다만 가정이 현실과 다르거나 명세에 빠진 부분이 있으면 증명된 시스템도 공격받을 수 있습니다.

## 장점

- **엄격성:** 형식 증명은 모호성을 제거하고 엄격한 논리적 추론에 의존하므로 높은 수준의 확실성을 제공합니다.
- **검증 가능성:** 구조화된 특성으로 인해 형식 증명은 기계적으로 정확성을 확인할 수 있어 오류 가능성을 줄입니다.
- **기반:** 일관성과 신뢰성을 보장하면서 많은 수학적 및 논리적 시스템의 기반을 형성합니다.

## 단점

- **복잡성:** 비교적 간단한 명제조차도 형식 증명을 구성하는 데 매우 복잡하고 시간이 오래 걸릴 수 있습니다.
- **접근성:** 형식 증명은 논리와 수학에 대한 강력한 배경 지식이 없는 사람들에게는 이해하기 어려울 수 있습니다.

## 응용 분야

수학과 논리학에서 널리 사용되지만 형식 증명의 개념은 다른 영역으로 확장됩니다.

1. **컴퓨터 과학:** 특히 중요한 시스템에서 알고리즘과 소프트웨어의 정확성을 검증합니다.
2. **암호화:** 암호화 프로토콜의 안전성 증명을 증명 보조기로 확인하거나, 프로토콜 설계와 구현을 형식 검증합니다.
3. **인공 지능:** 자동화된 추론 및 정리 증명이 가능한 시스템을 개발합니다.

---
출처: https://achivx.kr/glossary/formal-proof-%ED%98%95%EC%8B%9D-%EC%A6%9D%EB%AA%85/ · ACHIVX 용어 사전 · 수정일 2026-10-20