대규모 언어 모델 (LLM) 기반의 Assertion 생성은 Register Transfer Level (RTL) 설계에 대한 형식 검증 (Formal Verification)의 접근성을 높여주고 있지만, 세 가지 실질적인 문제가 남아 있습니다. 생성된 속성(Properties)이 잘못된 이유로 통과될 수 있고, 증명 비용 (Proof cost)이 설계마다 크게 다를 수 있으며, 실패한 트레이스 (Failing traces)를 해석하기 어렵다는 점입니다. 본 논문은 이러한 문제들을 하나의 루프 안에서 해결하는 경량 오픈 소스 프레임워크를 제시합니다. 우리의 방법론은 약한 Assertion(공허한(vacuous) Assertion 및 결함이 있는 동작을 구별하지 못하는 Assertion 포함)을 거부하기 위한 변이 유도 정제 (Mutation-guided refinement), RTL 구조를 사용하여 후보 Satisfiability Modulo Theories (SMT) 백엔드 중 하나를 선택하는 솔버 선택 (Solver-selection) 단계, 그리고 증명이 실패한 이유를 설명하기 위한 인과적 서사 합성 (Causal narrative synthesis)을 결합합니다. 다양한 RTL 설계에 걸쳐, 이 프레임워크는 생성된 Assertion에 대한 신뢰도를 높이고, 고정된 솔버 선택 시 발생하는 실행 시간의 가변성을 줄이며, 반례 트레이스 (Counterexample trace)에 근거한 실패 설명을 생성합니다. 결과는 Assertion 생성 단독보다는 품질 인지형 폐쇄 (Quality-aware closure)가 실질적인 LLM 지원 형식 검증을 위한 누락된 단계임을 시사합니다.