---
id: P-REINFORCE-AI-FORMAL-VERIFICATION
category: "10_Wiki/💡 Topics/AI"
confidence_score: 0.92
tags: [SoftwareEngineering, FormalVerification, Math, Security]
last_reinforced: 2026-04-20
---

# [[Formal-Verification-of-Software|Formal-Verification-of-Software]] (소프트웨어 정식 검증)

## 📌 한 줄 통찰 (The Karpathy Summary)
> "테스트가 99.9%를 보장한다면, 정식 검증은 수학적 증명으로 100%를 보장한다." 코드의 동작이 수학적 모델에 부합하는지 논리적으로 증명하여, 치명적인 버그가 없음을 절대적으로 확신하는 최고수준의 보안/신뢰성 기술이다.

## 📖 구조화된 지식 (Synthesized Content)
- **Mechanism**:
    - **Model Checking**: 시스템이 가질 수 있는 모든 상태를 전수 조사하여 결함이 없는지 확인.
    - **Theorem Proving**: 코드를 수식으로 변환하여 공리(Axioms)로부터 정답임을 유도함.
- **Use Cases**: 원자력 제어 시스템, 항공기 항법 장치, 스마트 컨트랙트(블록체인), OS 커널 보안.
- **Benefit**: 인간이 결코 상상할 수 없는 아주 희귀한 상황(Edge Cases)에서의 에러도 100% 발견 및 방지.

## ⚠️ 모순 및 업데이트 (RL Update)
- 정식 검증은 고도의 수학적 지식이 필요하며, 대규모 소스 코드에 적용하기에 연산 비용이 어마어마하다(State Explosion). 최근에는 AI가 복잡한 증명 과정을 대신 생성해주거나 코드를 읽고 정식 모델을 자동 추출하는 연구가 진행되어, 일반 상용 소프트웨어 영역으로 문턱을 낮추고 있다.

## 🔗 지식 연결 (Graph)
- Related: [[SAST (Static Application Security Testing)|SAST (Static Application Security Testing)]] , Cyber-Security
- Concept: Logic-And-Mathematics