During the development of a critical system, such as a drone autopilot, it is essential to ensure that the program is safe, for example using formal methods. To facilitate verification, we generally restrict ourselves to an abstraction of the system or a subset. This article presents the verification of a mathematical library of the Paparazzi autopilot, using the Frama-C tool, in order to guarantee the absence of runtime errors and certain functional properties.