배포하는 그 빌드에 결합된 증명.Proofs bound to the build you ship.

어떻게 동작하나How it works

LLM이 만든 것은 모두 검사할 후보입니다. 통과 판정은 고정된 검사기만 내립니다. Everything an LLM produces is a candidate to be checked. Only a pinned, independent checker issues a verdict.

1. 대상과 요구를 고정Pin the target and the requirementstrusted

   요구사항 ID, 위협 모델, 바이너리 해시, 툴체인, 전제조건을 등록합니다. 증명은 이 해시에 묶이고, 배포 파일이 바뀌면 자동으로 만료됩니다.Register requirement IDs, threat model, binary hash, toolchain and preconditions. Proofs are bound to that hash and expire automatically when the shipped file changes.

2. 명세 추출과 1차 검토Extract and review the specificationcandidate

   바이너리에서 동작 명세를 뽑고, LLM이 요구와의 차이를 1차 검토합니다. 정책과 전제는 사람이 정하고, 그 뒤에 정리 문장을 잠급니다.Derive a behavioural specification from the binary and let an LLM flag gaps against the requirements. People decide policy and assumptions; only then is the theorem statement locked.

3. 증명 작성Write the proofcandidate

   이전 증명 재사용, 엔진의 증명 골격, 결정적 자동화를 먼저 쓰고, 남은 지역 의무만 LLM 에이전트에 맡깁니다. 증명 보조기는 Rocq, 대상 ISA는 AArch64입니다.Reuse prior proofs, engine proof skeletons and deterministic automation first; hand only the remaining local obligations to LLM agents. The proof assistant is Rocq; the target ISA is AArch64.

4. 독립 재검사Independent re-checktrusted

   고정된 검사기가 등록한 정리 문장, 허용 공리, 생략 여부를 다시 확인합니다. 정리를 약화하거나 증명을 생략하면 실패입니다.A pinned checker re-verifies the registered statement, the allowed axioms and the absence of skipped steps. A weakened theorem or an admitted proof is a failure.

5. 릴리스마다 새 증거Fresh evidence for every releasetrusted

   새 빌드에서는 영향을 받은 의무만 다시 증명하고, 무엇을 다시 확인했는지 증거에 남깁니다.On a new build, only the affected obligations are re-proved, and the evidence records exactly what was re-checked.

받게 되는 것What you receive

무엇이 보장되는지, 왜 보장되는지, 어떤 조건에 의존하는지 추적할 수 있는 증거입니다.Evidence that lets you trace what is guaranteed, why, and under which conditions.

• 증명 완료proved
• 반례 확인refuted
• 예산 초과budget exceeded
• 미지원unsupported
• 명세 보류spec on hold

모든 명제는 이 다섯 상태 중 하나로만 기록합니다. 예산 초과를 안전으로 보지 않고, 분모는 착수 전에 등록한 정리 목록입니다. Every proposition ends in exactly one of these five states. A budget overrun never counts as safe, and success rates are measured against the theorem list registered before work begins.

대상 분야Where it applies

외부 입력을 받는 파서, 명령 권한 검사, 업데이트 검증, 거래 승인 모듈부터 시작합니다.We start with externally facing parsers, command authorisation, update verification and transaction approval.

신뢰 원칙Trust principles

증명 검사의 성공과, 명세가 고객 요구와 맞는지는 별개의 질문입니다. 둘 다 따로 확인합니다.A passing proof check and a specification that matches what you need are separate questions. We check both.

• LLM은 신뢰 기반 밖에 둡니다LLMs stay outside the trusted base명세 추출기, LLM 검토기, 학습한 탐색 정책의 출력은 모두 검사할 후보입니다.Spec extractors, LLM reviewers and learned search policies only produce candidates to be checked.
• 정리는 증명 전에 잠급니다Theorems are locked before proving증명 도중 정리 문장을 약화하지 않습니다. 바꿔야 하면 등록부터 고치고 이유를 남깁니다.Statements are never weakened mid-proof. Changing one means re-registering it, with the reason recorded.
• 결함을 잡지 못하는 명세는 통과가 아닙니다A spec that misses defects does not pass경계 오류, 권한 검사 제거 같은 결함 변형이 같은 정리를 만족하지 못함을 반례로 확인합니다.Injected defects — off-by-one bounds, removed permission checks — must provably fail the same theorem.
• 같은 커밋, 같은 결과Same commit, same result바이너리·명제·의미론·검사기·의존성의 판을 고정하고, 다른 장비에서도 같은 판정이 나와야 합니다.Binary, propositions, semantics, checker and dependencies are pinned; another machine must reach the same verdict.