Cimarron Selects AdaCore's SPARK Pro for AURORA Resilient Space Middleware

SPARK, the formally verifiable subset of the Ada language, has been adopted by Cimarron for the control-critical core of its Advanced Unified Runtime for On-orbit Resilient Applications product, AURORA, a reusable middleware framework for space-system applications. Cimarron selected AdaCore's SPARK Pro early in the AURORA development effort.

Cimarron implemented the control-critical path in SPARK: execution arbitration, actuation limiting, redundancy management, and fault-response decision logic. The remaining operational and advisory functions are implemented in a memory-safe language, and the SPARK components are linked into the runtime across defined interface boundaries.

The architecture is organized around a deterministic, frame-based execution model. Before any proposed actuation can reach an actuator path, it must pass through limiting and agreement logic in the verified core. Autonomy and AI functions may propose actions, but do not command directly. Cimarron designed AURORA for single-string through redundant multi-string deployments with configurable agreement policy and fault-tolerance behavior for fail-stop and omission faults.

SPARK provers run as a dedicated proof stage in Cimarron's continuous integration workflow, so proof results are produced and reviewed on the same cadence as the project's other engineering evidence.

"SPARK was the right fit for the areas of AURORA where we needed the strongest assurance: the logic that arbitrates execution, constrains actuation, and handles fault-response decisions," said Kevin Gordon, Vice President, Advanced Product Development at Cimarron.

"The question we hear most often from engineering leaders is not whether formal methods work; it is how a team new to them gets started without disrupting delivery," said Tony Aiello, Product Manager, AdaCore. "The answer is usually layered: structured training, a carefully chosen pilot, ongoing mentorship, and step-by-step integration into the CI/CD pipeline the team already uses. Cimarron's experience with AURORA is a good illustration of that path."

By applying SPARK to AURORA's control-critical core, Cimarron is building a foundation for space middleware in which key control and fault-response logic can be reviewed not only through tests and runtime evidence, but also through formal proof.