Prototype control system for a submarine, which uses Ada-SPARK to define the rules that govern the running of the submarine. The submarine can open and close airlock doors, surface and dive, and fire torpedoes, among other functionality.