버그 찾기 넘어 증명까지… Theorem의 무료 검증
3줄 요약
- Theorem이 자격을 충족한 오픈소스 프로젝트에 AI 기반 정형 검증을 무료로 제공한다.
- 10월 22일 첫 공개 증명 묶음에는 25개 프로젝트의 퍼즈 테스트 대상 60개가 포함됐다.
- 증명은 특정 실행 파일과 조건에 한정되며, 핵심 유지관리자가 신청해야 한다.
Theorem은 오픈소스 검증 프로그램 OSS Verify를 무료로 안내하고 있다. 코드에 여러 입력을 넣어 오류를 찾는 퍼즈 테스트에서 더 나아가, 정해진 조건 아래 오류가 없다는 수학적 증명을 만드는 방식이다. 공개 증명 저장소의 첫 배포 변경 기록은 날짜를 10월 22일로 적고, 25개 프로젝트의 퍼즈 테스트 대상 60개에 대한 증명을 담았다고 설명한다.
대상은 소스 코드 전체가 아니라 컴파일된 특정 테스트 실행 파일이다. AI가 만든 증명은 Rocq 증명 검사기로 확인한다. 상세 범위 문서에 따르면 입력 파일은 64 MiB 미만이어야 하고 메모리 예산 조건도 따른다. 퍼즈 테스트 대상은 임의의 입력을 받아 검사할 코드를 실행하는 함수다.
보장 범위를 넓혀 읽으면 안 된다. 공식 문서는 다른 컴파일러·설정·아키텍처의 빌드, 메모리 예산을 넘는 입력, 프로세스 모형이 다루지 않는 동작을 제외한다. 단일 스레드 모형이며 메모리 누수 등 일부 검사도 빠진다. 따라서 프로젝트 전체에 버그가 없다는 인증은 아니다.
신청은 핵심 유지관리자가 공식 저장소에 풀 리퀘스트를 보내는 방식이다. 공개 저장소·오픈소스 라이선스·퍼즈 테스트 대상·빌드 가능 여부·보안 연락처 등의 조건이 있다. Theorem은 발견 사항을 비공개로 전달하며, AI가 만든 보고서와 패치가 틀리거나 불완전할 수 있어 검토가 필요하다고 밝힌다. 이 기사는 증명 검사나 서비스 신청을 직접 수행한 결과가 아니다.
왜 중요한가
AI Ping은 AI가 제안한 결과를 별도 검사기로 확인하는 구조에 주목한다. 도입 판단에는 증명 개수와 함께 어떤 빌드·입력·오류 유형을 다루는지도 봐야 한다.
누구에게 중요한가
- 개발자
- 유지관리 중인 프로젝트의 테스트 대상과 빌드 조건을 먼저 확인하고, 전달받은 패치는 직접 검토하자.
출처
- OSS Verify — Free formal verification for open source — Theorem
- OSS Verify — enrollment and build instructions — Theorem Labs
- What gets proven — exact binaries, input limits and exclusions — Theorem Labs
- OSS Verify proofs — 2026.10.0 release changelog — Theorem Labs
