우리는 요구사항 문서와 프로덕션 소스 코드 모두로부터 Alloy 형식 명세 (formal specifications)를 생성하고, 해당 명세로부터 실행 가능한 테스트 케이스를 유도하기 위해 거대 언어 모델 (LLMs)을 사용하는 것에 대한 탐색적 연구를 제시합니다. 우리는 두 개의 실제 오픈 소스 Python 라이브러리인 기능 플래그 관리 시스템인 Flipper와 데이터 검증 라이브러리인 Cerberus를 대상으로 평가를 수행했습니다. 두 사례 모두에서 LLM은 어떠한 수동 수정 없이도 작동 가능한 Alloy 명세와 실행 가능한 테스트를 생성했습니다. Flipper의 경우, 우리의 파이프라인은 기존 테스트 스위트가 놓쳤던 실제 버그를 발견했습니다. 해당 라이브러리는 중복된 플래그 이름을 조용히 허용하고 있었으며, 이는 문서에 명시된 고유성 요구사항과 정면으로 배치되는 것이었습니다. 동일한 README로부터 Alloy 단계를 건너뛰고 테스트를 생성하는 직접적인 LLM 베이스라인 (baseline)은 68%의 분기 커버리지 (branch coverage)를 달성했으나, 세 번의 독립적인 실행 모두에서 이 버그를 잡아내는 데 실패했습니다. 이는 형식적 중간 표현 (formal intermediate representation)을 도입하는 것이 커버리지 중심의 생성 방식이 놓칠 수 있는 제약 조건 수준의 결함을 드러낼 수 있음을 시사합니다. Cerberus의 경우, 코드에서 유도된 명세는 문서에서 유도된 명세가 누락했던 크기 지정 타입 (sized types)에 대한 암시적 추상화를 포착하여 두 개의 추가 테스트를 생성했습니다. 두 라이브러리 모두에서 코드 기반 명세는 문서 기반 명세(평균 SD = 5.0)보다 테스트 생성의 분산이 더 낮게(평균 SD = 2.15) 나타났으나, 이것이 일반화될 수 있는지 여부는 여전히 미해결 과제로 남아 있습니다. 색인 용어(Index Terms)—형식 명세 (formal specifications), Alloy, 거대 언어 모델 (large language models), 자동 테스트 (automated testing), 명세 드리프트 (specification drift), 소프트웨어 검증 (software validation).