SPARK is not used for the whole system, but for the < 5% parts, which are safety/security-related in a good architecture.