LLM 코딩 에이전트가 생성하는 프로그램의 규모가 커지면서 철저한 사람 검토가 어려워져 안전·보안 실패 위험이 커지고 있다. 퍼징 테스트, 정적 분석, LLM 검증기 같은 기존 방법은 많은 결함을 잡아내지만 모든 경계 사례를 다루지는 못하며, 형식 검증은 기계적으로 검증 가능한 보장을 제공하지만 전통적으로 상당한 수작업 명세와 증명 작업이 필요했다. 이 논문은 검증 인식 중간 표현으로 Dafny를 활용해 형식적 안전 보장이 딸린 실행 가능한 프로그램을 생성하는 통합 다중 에이전트 프레임워크 'MAGS'를 제안한다. MAGS는 사람이 검토한 API와 안전 요구사항을 고정한 뒤 생성된 코드를 Dafny로 변환하고, 검증기 피드백으로 위반 사항을 수정한 다음 검증된 프로그램을 다시 실행 가능한 코드로 컴파일한다. CUDA 커널 100개, 터미널 스크립트 100개, 로봇팔 작업 20개 등 총 220개 사례에서 고정된 명세에 대해 사소하지 않은 안전 보장을 갖춘 프로그램 생성에 100% 성공률을 달성했으나, 자동 형식화된 의미가 목표 동작을 완전히 포착하지 못할 때는 실패 사례도 드러났다.

• •LLM 코딩 에이전트의 대규모 코드 생성에 따른 안전·보안 검토 한계를 해결하기 위해 형식 검증 기반 다중 에이전트 프레임워크 'MAGS' 제안
• •Dafny를 검증 인식 중간 표현으로 사용, 사람 검토 API·안전요구사항 고정→코드 변환→검증기 피드백 수정→재컴파일 파이프라인
• •CUDA 커널 100개, 터미널 스크립트 100개, 로봇팔 작업 20개 총 220개 사례에서 안전 보장 프로그램 생성 100% 성공률
• •독립 평가에서 세 영역 모두 강한 성능, 단 자동 형식화가 목표 동작을 완전히 못 담을 때는 실패 사례 발견