This group from Vermont Technical College is famous for being the only ones whose CubeSat micro satellite (out of 12 university CubeSats) remained functional during two years, when the second best team only achieved four months of functioning time. They already used SPARK for this first project, and credited the use of SPARK for being essential in getting perfect software on board. You may also have seen their CubeSat on the cover of the SPARK 2014 book, which is not a surprise as Peter Chapin from this group is one of the authors!

Thanks to this past success, NASA has selected this group to develop the flight software for a much bigger system, a micro satellite that is 6 times bigger and which involves 6 partners, whose mission is to map water vapor and ice on the moon. In this project too they will use SPARK to help them get perfect software. You can see the details in their paper or their presentation at HILT 2016, just a few weeks ago. Interestingly, one of the hurdles that they mention in this paper, having to do with the restrictions of the Ravenscar profile of Ada (XDR encoding/decoding of messages), has recently been lifted in SPARK: SPARK now supports the Extended Ravenscar profile whose goal is precisely to allow the kind of code that will be useful for the Lunar IceCube mission.

If you are interested in following this project, look at their website. The Lunar IceCube will be launched in 2018.