인공지능 (AI)의 발전은 정리 증명 (Theorem Proving)을 위한 AI가 컴퓨터 시스템을 형식적으로 검증 (formally verifying)하는 유망한 수단이 되도록 이끌었습니다. 형식 검증 (formal verification)은 필요한 전문 지식과 노력의 양 때문에 전통적으로 안전 필수 (safety-critical) 시스템을 위해 예약되어 왔으나, AI는 이러한 작업량의 상당 부분을 자동화하고 훨씬 더 접근하기 쉽게 만드는 데 도움을 줄 수 있습니다. 블록체인 기반 시스템은 점점 더 인기를 얻고 있으며 악의적인 행위자들의 빈번한 공격 대상이 되고 있으며, 이는 종종 막대한 금융 손실로 이어져 이러한 시스템을 더 잘 검증하고 취약점을 완화해야 할 필요성을 강조합니다. 이러한 시스템에서 논쟁의 여지 없이 가장 중요한 구성 요소는 잠재적으로 적대적인 환경에서 노드들이 결정에 동의할 수 있도록 하는 합의 프로토콜 (consensus protocol)입니다. 본 논문에서 우리는 Isabelle 내의 자동 정리 증명 도구인 IsabeLLM을 개선합니다. 구체적으로, 우리는 대규모 언어 모델 (Large Language Model, LLM)에 제공되는 컨텍스트를 개선하기 위해 검색 증강 생성 (Retrieval-Augmented Generation, RAG) 프레임워크, 오류 추적 (Error tracing) 및 반례 생성 (counterexample generation)을 구현합니다. 또한 효율성 향상을 위해 최신 버전의 Isabelle 및 Sledgehammer와의 호환성도 구현되었습니다. 우리는 Bitcoin의 작업 증명 (Proof of Work) 합의 검증을 완료하는 능력에 있어 두 가지 버전의 IsabeLLM의 성능을 비교합니다.