검증(Verification)은 현대 칩 설계 노력의 대부분을 차지하지만, 정확성에 대한 수학적 보장을 제공하는 형식 검증(Formal Verification) 도구들은 여전히 비용이 많이 들고 라이선스 제한이 엄격합니다. 대규모 언어 모델(LLMs)이 하드웨어 설계 분야에서 가능성을 보여주었으나, 기존의 RTL 수정(RTL repair) 방식들은 입력값의 일부만 테스트하는 시뮬레이션(Simulation)을 통해 결과를 검증하거나 상용 도구에 의존하며, 형식적 증명(Formal proof)과 완전히 오픈 소스 도구 체인을 결합한 사례는 거의 없습니다. 본 논문에서는 LLM을 오픈 소스 형식 백엔드(Yosys, SymbiYosys, Z3)와 결합하여 반례 유도 반복(Counterexample-guided iteration)을 통해 RTL을 수정하는 멀티 에이전트 파이프라인을 제시합니다. 이 프레임워크는 형식적 속성(Formal properties)을 생성하고, 설계를 검증하며, 설계가 k-유도(k-induction)에 의해 올바름이 증명되거나 반복 예산이 소진될 때까지 반례(Counterexamples)를 LLM에 다시 전달합니다. ALU 사례 연구를 통해, 우리는 이 파이프라인이 정확성에 대한 형식적 증명과 함께 실제 기능적 버그를 탐지하고 수정할 수 있음을 보여줍니다. 6개의 벤치마크 제품군 전반에 걸쳐, 하나의 설계가 안정적으로 수정되었으며, 우리는 네 가지의 뚜렷한 실패 모드(Bounded-cover vacuity, Specification ambiguity, Temporal-logic bugs, Multi-property pressure)를 규명했습니다. 우리는 이 연구를 상세한 실패 분석을 포함한 타당성 조사로 정의하며, 추가적으로 오픈 소스 형식 검증 커뮤니티와 관련된 Yosys bind 지시어의 실질적인 한계를 보고합니다.