Safe Stabilization of Cancer Dynamics via Formal Methods and Lyapunov Control: A Case Study on the Stepanova Model

Accurate and safe regulation of tumor growth is a central challenge in cancer therapy, where chemotherapy and immunotherapy must be coordinated to suppress malignant cells while preserving immune function. Conventional control approaches often lack formal guarantees of stability or constraint satisfaction, which limits clinical reliability. This work presents an integrated framework for nonlinear cancer dynamics that unifies formal control abstraction and control Lyapunov function principles. The method ensures asymptotic stabilization to the benign equilibrium while enforcing a safety-critical constraint on immune preservation. The use of formal methods also significantly enlarges the region from which the tumor growth dynamics can be safely stabilized. The resulting control law is computationally efficient and suitable for real-time therapy scheduling. In-silico simulations on the Stepanova tumor–immune model demonstrate that the proposed controller achieves effective tumor suppression while strictly maintaining immune safety, and are compared against an unconstrained Pontryagin-based controller.