**LLM이 훨씬 더 큰 규모의 소프트웨어 정형 검증을 가능하게 하고 있음**

- Anthropic과 Theorem은 Claude로 오픈소스 라이브러리 123개의 퍼징 진입점 239개를 정형 검증함. 발견한 버그를 수정한 뒤, 특정 실행 환경과 입력 크기 조건에서 컴파일된 코드가 충돌하지 않음을 증명  
- 무작위 입력을 대량 실행하는 퍼징과 달리, 64MB 미만의 모든 입력에서 테스트가 통과함을 증명하는 방식. 보장 범위는 단일 스레드 RISC-V 바이너리 등 명시된 실행 조건에 한정  
- 증명을 시도하는 과정에서 수백 개의 버그를 발견함. 큰 입력이나 드문 호출 순서가 필요한 메모리 오류뿐 아니라, 충돌을 일으키지 않는 논리 오류도 찾아냄  …

[https://news.hada.io/topic?id=35855](https://news.hada.io/topic?id=35855)