Seedup
Articles

아티클

개발 뉴스, AI 제품 흐름, 오픈소스 신호, 논문 리뷰를 한국어로 정리해 바로 읽고 만들 수 있게 모았습니다.

인기 글논문 리뷰

arXiv · 2026. 7. 7.

Harnessing Code Agents for Automatic Software Verification

이 논문은 AI가 수학 증명처럼 엄격한 소프트웨어 검증(Coq, Lean)을 '완전 자동'으로 할 수 있음을 보여줍니다. 기존엔 전문가가 일일이 증명 전략을 짜야 했지만, Claude Code 같은 범용 코드 에이전트에게 '이 렘마 증명해줘'라고만 맡기고, 검증 하네스(자동 채점기)가 통과할 때까지 피드백 루프를 돌리면 됩니다. 그 결과, 동시성/메모리 검증의 표준인 Iris 라이브러리 4,257개 렘마, Rust 표준 라이브러리 검증 217개, 기존 LLM 증명기가 8분의 1만 풀던 reglang 318개, Lean 4로 포팅 중인 iris-lean 72개를 **모두 100% 자동으로 증명**했습니다. 전문가 개입 제로, 실패 제로.

자세히 읽기
NewPopular뉴스/글논문
총 44개 아티클