Relational database management systems rely on mathematically sound schema designs to prevent data anomalies. Boyce-Codd Normal Form (BCNF) decomposition is a foundational algorithm for eliminating structural redundancies. However, its implementations in modern software rarely possess machine-checked proofs of correctness. This thesis bridges the gap between axiomatic relational theory and verified executable software by formalizing the complete BCNF decomposition pipeline within the Lean 4 theorem prover.

We start by formalizing functional dependencies, Armstrong's Axioms, and a computable attribute closure algorithm. By constructing a semantic counterexample relation, we mathematically prove the soundness and completeness of the syntactic derivations. We then implement the recursive BCNF decomposition algorithm. Overcoming the strict totality requirements of Lean 4, we prove the algorithm's well-founded termination based on strictly decreasing schema cardinality. Through structural induction on the generated decomposition tree, we verify that the algorithm guarantees global losslessness and complete BCNF compliance across all terminal sub-schemas.

Additionally, to resolve the non-computability of classical choice over abstract finite sets, we introduce a refinement architecture that transitions the declarative specification into deterministic, list-based computations. By proving a strict bisimulation between the mathematical and executable implementations, we transfer all correctness guarantees to the natively executable bytecode. Overall, this research provides a fully verified, computable normalization tool, advancing the application of interactive theorem proving in formal data engineering.