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

Cimarron adopts AdaCore’s SPARK Pro to develop verified control-critical components for a deterministic middleware framework for space applications.

NEW YORK and HOUSTON, November 2026

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.

About AdaCore

For over 30 years, AdaCore has helped people build software that matters. AdaCore provides tools for high-integrity development in Ada, SPARK, C, C++, and Rust.

We build our toolchains to meet the most rigorous standards so you can focus on your code and reach your certification goals. AdaCore supports high-integrity industries by offering compiler toolchains and analysis tools, along with certification evidence for compliance with industry standards.

We have world-leading experts in Static Analysis Testing and Dynamic Analysis Testing. AdaCore’s Static Analysis capabilities consist of CodeSonar® for powerful static analysis of Ada, C/C++, and other languages. The Dynamic Analysis Suite comprehensively supports Ada users, encompassing metrics computation, coding standard verification, cybersecurity vulnerability scanning, and high-assurance verification.

With a commitment to long-term support, AdaCore ensures the continuity and reliability of its toolchains for decades.

About Cimarron

For more than 40 years, Cimarron has delivered advanced software, engineering, and technical solutions for the aerospace, defense, and commercial space sectors. Cimarron was founded in Houston in 1981 as a specialized software firm. It has since grown into a multi-division engineering and technology company that supports some of the most demanding missions in human spaceflight and national security.

Cimarron’s Civil & Commercial Space division supports NASA and commercial space programs nationwide, including Artemis, Commercial Crew and Cargo, the International Space Station, commercial space stations, and NASA’s Mission Control Center. Its Defense & National Security division supports missile defense, nuclear triad infrastructure, advanced aircraft, and complex space and intelligence systems. Through its wholly owned subsidiary, Watring Technologies, Inc. (WTI), Cimarron delivers precision products for defense and space using AS9100D-certified processes.

Cimarron’s capabilities span advanced flight software, systems engineering, mission operations, software integration labs, and assembly, integration, and test. Products such as AURORA build on that mission software heritage. Cimarron is headquartered in Houston, Texas, with operations in Huntsville, Alabama. It has been appraised at CMMI Maturity Level 3, holds CMMC Level 2, ISO 9001:2015, and ISO 27001 certified.

Image Credit:

“AURORA Gateway Cislunar 3D Demo” credited to NASA for the Gateway 3D model and NASA Goddard for the lunar 3D model.