I think there are certain core-functionalities that could benefit from being written in SPARK -- things like the core of the OS, common networking facilities/network stack (the IRONSIDES DNS is a good step in that direction).