Abstract
Background: Current artificial pancreas systems for Type 1 diabetes rely on control algorithms with soft safety constraints, which provide no formal guarantees against life-threatening hypoglycemia.Methods: This paper introduces a novel Control Barrier Function Model Predictive Control (CBF-MPC) framework that provides mathematically provable safety certificates for glucose regulation by encoding clinical safety boundaries (70–180 mg/dL) as a control barrier function.Results: We establish theoretical conditions for recursive feasibility and safety under bounded disturbances, prove that the optimization problem is convex and solvable in polynomial time, and demonstrate the safety mechanism through numerical verification.Conclusions: The framework bridges formal methods from control theory with clinical needs in diabetes management, offering a pathway toward certifiably safe artificial pancreas systems.