A new method to design, implement and verify optimization algorithms to enable their use onboard space systems

Increasing autonomy and resilience in space missions demands advanced onboard decision-making capabilities. While numerical optimisation is central to such autonomy—illustrated by its role in real-time trajectory planning for vertical rocket landings—it is still rarely used online in critical systems due to the challenges of ensuring correctness and robustness. It is however a key enabler to advanced autonomy for future space missions. We propose a novel framework for the automated design and formal verification of optimisation algorithms, tailored for use in safety-critical onboard systems. Our key innovation lies in recasting optimisation algorithms as discrete-time dynamical systems, enabling the reuse of formal verification techniques originally developed for Guidance, Navigation and Control (GNC) systems. This approach allows us to verify algorithm-level properties (e.g. convergence, stability, constraint satisfaction) not just at the model level, but at the code level, using formal tools, namely deductive methods and abstract interpretation. We will demonstrate this framework on embedded implementations of real-time convex optimisation solvers and highlight its integration potential in existing flight and space software pipelines.