An AdaCore intern has rewritten the CrazyFlie drone software, originally in C, into SPARK. In addition to fixing some bugs, this allowed to prove absence of runtime errors. I will present the various technics used to achieve that result, and plan to do a live demo of free fall detection.