형식 방법론 가이드 기반의 바이브 코딩 (Vibe Coding): 모델 주도 공학 (MDE)을 통한 AI 생성 안전 필수 소프트웨어의 검증

바이브 코딩 (Vibe coding) — 최소한의 검토만으로 자연어 의도로부터 LLM (Large Language Model)이 생성한 소스 코드를 수용하는 방식 — 은 빠르며 저위험 소비자용 소프트웨어에는 적절할 수 있습니다. 하지만 DO-178C, IEC 61508 또는 ISO 26262의 규제를 받는 안전 필수 (safety-critical) 시스템의 경우, 이는 인증으로 가는 경로를 제공하지 못합니다. 대규모 언어 모델 (LLMs)은 형식적 정확성 (formal correctness) 보장을 제공하지 않으며, 기존의 해결책들은 사전 학습 데이터가 부족하고 산업용 툴체인(toolchains)에는 존재하지 않는 검증 인지 언어 (verification-aware languages; Dafny, Verus, Lean)를 대상으로 하기 때문입니다. 본 논문은 이 격차를 해소합니다. 우리는 Forge (Formal method Oriented Refinement loop for GEnerated code)를 제시합니다. 이는 확립된 모델 주도 공학 (Model-Driven Engineering, MDE) 인프라를 사용하여 형식 검증 (formal verification)을 통해 바이브 코딩을 가이드하는 폐쇄 루프 (closed-loop) 파이프라인입니다. 바이브 코딩을 통해 Java 소스 코드를 생성하면, 우리의 파이프라인은 모델 변환 (model transformations)을 통해 세 가지 서로 다른 형식주의 (formalisms)의 형식적 산출물 (formal artefacts)을 추출하며, 각 산출물은 상호 보완적인 검증기에 의해 확인됩니다: 연역적 검증 (deductive verification; Dafny), Failures-Divergences Refinement checker (FDR4)를 통한 통신 순차 프로세스 (Communicating Sequential Processes, CSP) 정제 (refinement), 그리고 Isabelle의 Z-Machines를 사용한 정리 증명 (theorem proving)이 그것입니다. 모든 검증 실패는 다음 코드 생성 반복을 유도하는 구조화된 수정 프롬프트 (structured correction prompt)가 됩니다. LLM은 초안 생성기 (draft generator) 역할을 하고, MDE 체인은 판별기 (discriminator) 역할을 수행하며, 개발자는 형식 모델을 읽을 필요가 전혀 없습니다. 실증적으로, 우리는 이 파이프라인이 LLM이 생성한 Java에 대해 표준 관련 검증 증거 (verification evidence)를 생성한다는 것을 발견했으며, 이는 인증을 향한 한 단계입니다.