Ember: An Embedded Robotics Library in SPARK

This paper describes the Ember library for high-integrity embedded robotics and GNC applications developed in SPARK 2014 with formal verification. The library is based on generic packages and includes functionality as linear algebra, complex numbers, quaternions, and kinematics. Preliminary test results for linear algebra performance are very promising.