The Ariane 5 Launcher and Mars Polar Lander were destroyed due to software defects. The European Space Agency ESA wants to ban such risks. Using software tools that trace bugs automatically. Advances in theoretical computer science are at the heart of these tools. We'll present recent experiences in applying such techniques to make satellites and launchers such as the Ariane 6 more reliable.