비순차적 실행 (Out-of-order) 멀티프로세서는 현대 하드웨어의 핵심적인 부분이며, 이들의 검증은 다음과 같은 과제들을 해결해야 합니다. 첫째, 읽기 및 쓰기 작업이 공유 메모리에 도달하는 순서가 제한되지 않는 코어 간 인터리빙 (inter-core interleaving)입니다. 둘째, 명령어가 프로그램 순서와 다르게 실행되는 코어 내 비순차적 실행 (intra-core out-of-order execution)입니다. 이 두 가지가 결합되면 순차적 실행으로는 설명할 수 없는 약한 결과 (weak outcomes)가 발생하며, 현대의 ISA는 이러한 동작을 설명할 수 있도록 허용합니다. 그러나 마이크로아키텍처 (microarchitecture)는 심지어 과도한 비순차적 실행을 보여주며, 일시적으로 ISA에 의해 금지된 상태에 진입하기도 합니다. 이러한 상태들은 나중에 폐기되지만, 전체 시스템 검증 (full-system verification)에서 코어에 대한 추론을 복잡하게 만듭니다. 기존 연구들은 다양한 프로세서 설계를 검증해 왔으나, 이러한 약한 결과를 나타내는 비순차적 실행 멀티프로세서에 대해 무제한 검증 (unbounded verification)을 수행한 사례는 없습니다. 본 논문에서는 In-Order 약한 메모리 ISA에 대한 비순차적 실행 멀티프로세서의 첫 번째 형식 검증 (formal verification)을 제시합니다. 우리의 핵심 아이디어는 과도한 실행의 본질을 단일 명령어 목록으로 포착하는 잘 설계된 코어 사양 (core specification)입니다. 이를 바탕으로 우리는 증명을 두 단계로 분해합니다. 첫 번째는 코어 정제 (core refinement)로, 과도한 실행과 코어 인터페이스를 추론하는 데 필요한 상태를 제외한 모든 마이크로아키텍처 상태를 추상화하여 코어 구현이 이 사양을 따름을 증명합니다. 두 번째는 시스템 포함 (system inclusion)으로, 비순차적 메모리 실행과 코어 간 인터리빙을 ISA로 직렬화하며, 코어 사양 덕분에 과도한 실행을 쉽게 제거합니다. 우리의 모든 증명은 Rocq에서 기계화되었으며, 증명을 자동으로 작성하기 위해 대규모 언어 모델 (LLM) 에이전트를 적극적으로 활용하였습니다.