We report a Lean 4 formal audit accompanying the paper "Completing the Arakawa–Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras" (arXiv:2607.25249). In a single Lean source, the development kernel-checks the paper-local deductive architecture used for the new maximal-ideal cases: affine-kernel detection and lifting, extremal PBW-line deductions, finite Ramond–Casimir arithmetic and case enumerations, reduced-simplicity contradiction schemes, and the case-level affine conclusions for the level -1 D_l family and the positive-parameter cases of D4, E6, E7, and E8. It also audits the paper's alternative D_l level -2 argument and the separate rank-reduction application of Section 8. Previously published exceptional n=0 cases are not claimed as newly formalized results of this bundle. The released project builds successfully with the pinned Lean/Mathlib environment and contains live #print axioms queries for the principal final wrappers. The development does not reconstruct affine vertex algebras, minimal W-algebras, BRST/DS reduction, Ramond Zhu theory, or Li spectral flow from foundational definitions in Mathlib. Those ingredients, together with the concrete realization of case-specific representation-theoretic objects, are exposed as theorem parameters and semantic interfaces. Accordingly, the precise verification claim is a kernel-checked deduction of the paper-local proof from explicitly stated VOA/BRST/DS boundary inputs, rather than a from-scratch formalization of the ambient representation theory.