Rust의 소유권 모델(ownership model)과 타입 시스템(type system)은 강력한 메모리 안전성(memory safety) 보장을 제공하지만, unsafe 코드와 런타임 패닉(runtime panics)은 여전히 상당한 위험을 초래합니다. 메모리 안전성을 보장하기 위해서는 형식 검증(Formal verification)이 필수적이지만, 검증 하네스(verification harnesses)를 개발하는 것은 여전히 어렵고 수동적인 작업으로 남아 있습니다. 대규모 언어 모델(LLMs)이 다양한 코드 분석 작업에서 강력한 성능을 보여주었음에도 불구하고, 이를 하네스 생성에 직접 적용하면 부정확한 API 호출, 비효율적인 비결정론적 데이터 생성(nondeterministic data generation), 그리고 허구적인 수정(fabricated fixes)이 발생하는 경우가 많습니다. 본 논문에서는 기존 테스트 스위트(test suites)로부터 Rust 코드를 위한 검증 하네스를 직접 생성하기 위해 LLM을 활용하는 자동화된 워크플로우인 HarnessLLM을 제시합니다. HarnessLLM은 테스트 케이스로부터 호출 시나리오(calling scenarios)를 자동으로 추출하고, 의존성 분석(dependency analysis)을 기반으로 비결정론적 인자(nondeterministic arguments)를 생성하며, 하네스를 점진적으로 합성(synthesizes)합니다. 그 후, 중요한 코드 영역을 보존하면서 하네스를 반복적으로 개선하고, 허구적인 타입이나 함수를 LLM에 보고하여 수정을 요청합니다. 9개의 실제 Rust 코드베이스에 대한 평가 결과, HarnessLLM은 494개의 테스트 케이스에서 294개의 호출 시나리오를 94.66%의 정밀도(precision)로 추출하였으며, 각 시나리오에 대해 평균 145초 만에 하네스를 생성했습니다. 이는 해당 시나리오 중 41%만 성공한 기존 방식인 Autoharness보다 뛰어난 성능을 보였습니다. 마지막으로, 생성된 하네스를 사용하여 6개의 실제 메모리 안전성 버그를 탐지함으로써 검증에 있어 본 접근 방식의 실질적인 유용성을 입증했습니다. 저희가 알고 있는 바로는, 본 연구는 실제 Rust 프로젝트의 메모리 안전성 검증을 목표로 하네스를 생성하는 데 LLM을 사용한 첫 번째 연구입니다.