Rocq에서 Metal까지: 형식 검증된 마이크로컨트롤러 펌웨어를 위한 파이프라인

AI가 생성한 코드가 확산됨에 따라 안전 필수 시스템 (safety-critical systems)에서 불변량 (invariants)을 강제하는 것이 점점 더 시급해지고 있습니다. 불행히도, 고수준 명세 언어 (high-level specification languages)를 지원하는 데 필요한 런타임 (runtimes)은 대부분의 임베디드 대상 (embedded targets)에 비해 너무 큽니다. 본 논문에서는 형식 검증된 (formally verified) 펌웨어가 오늘날 어떻게 실현 가능한지를 보여줍니다. 우리는 마이크로컨트롤러에서 Rocq로 추출된 Scheme를 실행하는 베어메탈 (bare-metal) 연속 전달 스타일 (Continuation Passing Style, CPS) 가상 머신 (VM)인 Encore!를 구축했습니다. 또한 펌웨어를 순수 상태 전이 함수 (pure state-transition function)로 구조화하는 방법을 제시하여, 펌웨어의 복잡도와 상관없이 검증되지 않은 호스트 계층 (unverified host layer)은 일정하게 유지하면서 핵심부를 Rocq에서 완전히 증명 가능하게 만들었습니다. 대규모 언어 모델 (Large Language Model, LLM) 지원 택틱 합성 (tactic synthesis)은 이 워크플로우에 자연스럽게 부합합니다. 즉, 형식적 정리 문구 (formal theorem statements)가 수동 코드 리뷰를 대체하여, AI가 생성한 펌웨어가 스스로를 증명할 수 있게 합니다.