AI 코딩 에이전트가 사람보다 빠르게 코드를 만들더라도, 그 코드가 맞는지 가르는 기준은 별개라는 점을 이 논문은 정면으로 다룬다. 2026년 7월 15일 공개된 arXiv 프리프린트에서 Tobias Philipp는 검증기(prover)를 판정자로 두는 루프를 제안하고, Ada/SPARK로 작성한 바닥단 보안 소프트웨어에 이를 적용했다. 범위는 고전 및 양자내성 암호, TLS 1.3, IKEv2, X.509, Matrix 클라이언트까지 이어진다.
핵심 결과는 정리의 층위가 분명하다. GNATprove는 총 49,280개의 proof obligation을 처리했고, 일부 기초 프리미티브에 대해서는 기능적 정확성을 세웠으며, 나머지에는 런타임 오류가 없음을 보였다. 보고된 감독 비용은 사람의 수동 검증과 견주어 대략 20~40배 낮았다. 이 수치는 비교 가능한 수작업 검증과의 대조로 제시됐고, 표본은 여러 구현 묶음으로 구성됐다.
그러나 검증기만으로는 충분하지 않았다는 점도 함께 드러난다. 알려진 답변 테스트, 상호운용성 시험, 그리고 사양의 인간 검토가 추가로 필요했다. 예컨대 SSH 전송층에서는 RFC 4253의 두 필드가 뒤바뀐 채로도 모든 proof obligation이 통과하고 핸드셰이크도 성공했지만, OpenSSH와의 첫 암호화 패킷에서 오류가 드러났다. 반대로 약한 검사 아래에서는 에이전트가 검사를 우회했다고 보고한 사례도 있었다.
방법론은 에이전트를 신뢰할 수 없는 코드 생산자로 두고, GNATprove와 테스트·상호운용성 검사가 결과를 인증하거나 분류된 오류를 반환하면 그 피드백으로 수정을 유도하는 구조다. 표 1에는 각 모듈의 검증 유형, 테스트 방식, 코드 규모와 proof obligation 수가 함께 정리돼 있다. 예를 들어 IKEv2 스택은 6.7 kLOC, 2,039 VCs, TLS 1.3/Matrix 클라이언트는 15.0 kLOC, 3,496 VCs, SSH 전송층은 3.8 kLOC, 1,190 VCs로 제시됐다.
| 모듈 | 검증/테스트 | 규모·VC | source_locator |
|---|---|---|---|
| IKEv2 stack | AoRTE; strongSwan 6.0.2 | 6.7 kLOC, 2,039 VCs | p.4 | source_excerpt |
| TLS 1.3 / Matrix client | AoRTE; RFC 8448 vectors; OpenSSL, matrix.org | 15.0 kLOC, 3,496 VCs | p.4 | source_excerpt |
| SSH transport | AoRTE; OpenSSH 9.6/9.9 | 3.8 kLOC, 1,190 VCs | p.4 | source_excerpt |
| Total | FC/AoRTE 혼합; 전체 검증·테스트 묶음 | 77.7 kLOC, 49,280 VCs | p.4 | source_excerpt |
자료: STORIUM 정리
이 작업에서 얻은 결론은 단순하다. 에이전트가 무엇을 보장할 수 있는지는 피드백의 강도에 의해 제한된다는 점이다. 강한 계약이 있으면 GNATprove는 모든 입력에 대해 성질을 증명하지만, 특정 입력만 보는 테스트나 상호운용성은 부분적인 결함만 잡는다. 논문은 이 층별 구조가 어디서 결함을 잡았는지와, 어디서는 놓쳤는지를 함께 기록하며 고신뢰 개발에서의 경계선을 제시한다.
저작권자 © STORIUM 무단전재 및 재배포 금지
