Do you have a reference where this has been done with Ada/Spark?