단순히 도구에 접근할 수 있다는 것만으로는 LLM의 경험적 추론(empirical reasoning)을 제어 가능하게 만들지 못합니다. 받아들여지는 출력은 반드시 입증된 증거에서 파생되어야 하는 것도 아니며, 받아들여지는 추론 과정이 형식적인 검토를 견뎌야 하는 것도 아닙니다. 본 논문에서는 EG-VAR (Evidence-Grounded Verified Agentic Reasoning)을 제시합니다. 이는 Lean 4 기반의 도구 호출 아키텍처로, 여기서 Lean 커널은 도구 증명 공리(tool-attestation axioms)와 선언된 소스 리프트(declared source lifts)를 통해 검증된 주장(Verified claims)의 유일한 생성자 역할을 합니다. 모든 검증된 출력은 구조적으로 입증된 도구 호출(Thm. 3.1)과 커널이 확인한 유효 추론 체인(Thm. 3.2)에서 파생되며, 잔여 출력물은 재현 가능한 감사 추적(replayable audit trail)을 가진 정직한 Abstain으로 처리됩니다. TableBench 수치 추론(n=120)의 하위 컬렉션에서 EG-VAR는 120/120이라는 성능을 달성하여, 동일 도구 기반의 기준선(baseline)인 95%를 능가합니다. 반사실적 스트레스 테스트(5개 도메인 x 2개 모델)에서는 EG-VAR가 100% 소스 충실도를 유지하는 동안, 동일 도구 방식은 8090%로 떨어지고 (도구 미사용 시 5080%)의 성능을 보였습니다. LLM을 배포 시간 형식화기(deployment-time formalizer)로 사용할 경우, 잔여 의미론적 형식화 오류는 Sonnet에서 3.3%, Opus에서 1.7%를 기록했습니다. 우리는 EG-VAR를 고위험 경험적 주장에 대한 기술적 거버넌스 인터페이스로 위치시킵니다: 이 형식적인 사이드카(sidecar)는 목표 명제, 소스 범위, 증거 경계, 증명 의무, 그리고 Abstain 조건을 감사 가능하게 만들어, 오늘날 지원되지 않는 검증된 출력물을 제거하는 동시에 형식화 오류, 리프트 및 소스 권한 분쟁, 모호성, 그리고 Abstain을 명시적인 감사 대상으로 전환합니다. 시간이 지남에 따라 데이터셋, API, 공공 기록, 그리고 AI 생성 문서의 타입 지정 사이드카는 이러한 형식화 부담을 재사용 가능한 인프라로 상각할 수 있습니다.