Certified Steady-State Parameter-Interval Design for Uncertain Biomolecular Models using a Global Shaving Contractor

The design of parameter intervals that provably enforce steady-state specifications in biomolecular circuits is challenging due to nonlinear reaction kinetics, parametric uncertainty, and the under-determined nature of steady-state constraints. Most validated approaches either rely on recursive subdivision (set inversion) or may stall due to dependency effects when applied directly in parameter space, limiting scalability in moderate to high dimensions. This paper introduces a global shaving contractor that contracts an initial parameter box by repeatedly applying certified interval-exclusion tests against a prescribed steady-state set. The proposed procedure returns a guaranteed outer enclosure of the feasible parameter set and provides finite-termination guarantees, along with worst-case bounds on the number of inclusion-function evaluations. Case studies spanning low-dimensional motifs and a sixteen-parameter integral-feedback model, including bistability specifications for a CRISPRi toggle switch, demonstrate substantial contraction of design domains without subdivision. The resulting certificates support uncertainty-aware circuit tuning, rigorous parameter screening, and robust design workflows in systems & synthetic biology and related nonlinear dynamical-system design problems.