Neural Feasibility Certificates

Ensuring recursive feasibility is critical for safety-constrained online control under hard constraints. Since analytically constructing feasible regions and recovery policies is difficult for nonlinear systems, learning-based methods offer a flexible alternative. However, existing methods often rely on approximate boundaries and continuously constrain the nominal controller, leading to limited guarantees and unnecessary conservatism. To address these limitations, we propose a framework to synthesize and formally verify neural feasibility certificates for safety-constrained online control. Our contributions are threefold. First, we introduce a neural feasibility certificate defining an inner approximation of the instantaneous feasible set. The associated margin-triggered controller retains the original online controller when sufficient feasibility margin is available and activates a learned witness policy only near the boundary of the certified feasible region, where it drives the system back to the feasible interior in finite time. Second, we develop a synthesis and formal verification framework that jointly learns the feasibility certificate and witness policy and certifies recursive feasibility over the continuous state space. Third, we validate the proposed framework on adaptive cruise control, autonomous overtaking, and mobile robot navigation against multiple baselines, demonstrating improved feasibility with competitive safety, control performance, and computational efficiency.