Sorry for the slow reply. I used to work for Praxis (now part of Altran) who used to be the owners of the SPARK tech, in fact I spent a while working in the SP

Sorry for the slow reply. I used to work for Praxis (now part of Altran) who used to be the owners of the SPARK tech, in fact I spent a while working in the SPARK team on the automated theorem prover technology. Howerver this was a consultancy working in the aerospace and defense industry, and it frequently working away from home at the client's sites, on frequently very poorly run projects. I loved the technology, but I found the way things got done frustrating. Building software in SPARK for stage equipment sounds like a good fit. I'd be very interested to hear how you get on.