본 논문은 형식적 방법(formal methods)이 신뢰할 수 있는 소프트웨어를 생성하는 데 유용하지만 일상적인 프로그래밍에서는 거의 채택되지 않는다는 점을 배경으로, 대규모 언어 모델(LLM)을 이용한 자동 코드 생성이 증가하고 있지만 강력한 정확성 보장을 고려하는 경우는 드물다는 문제를 제기합니다. 따라서 본 연구는 Dafny, Nagini, Verus 세 가지 검증 언어에서 LLM이 검증된 코드를 생성하는 능력을 탐구합니다. 최첨단 Python 벤치마크 HumanEval에서 수동으로 큐레이션된 데이터셋을 사용하여, 양질의 결과를 얻는 데 필요한 정보 유형을 평가합니다.