When Latitude began creating their small satellite launcher, Zephyr, they recognized the importance of selecting the correct programming language and development tools to support their efforts. They chose to work with high-integrity software experts AdaCore.

Latitude, which closed a Series B funding round in January 2024, is currently preparing for Zephyr's first flight, which will occur in late 2025.

In this article, Jose Ruiz, a Product Manager at AdaCore, explores two essential factors to consider when selecting secure software for your space industry projects: memory-safe languages and formal verification.

In the competitive New Space industry, ingenuity, reliability, and cost-effectiveness are paramount. When developing new projects, the correct choice of programming language is critical. By prioritizing memory safety and embracing formal verification, organizations can enhance their software's resilience against vulnerabilities and demonstrate compliance with regulatory expectations.

Memory-safe programming languages

Memory safety is a crucial concept in software development. It addresses how an application handles memory operations such as reading, writing, allocation, and deallocation. A memory-safe application operates within the bounds of its allocated memory (it doesn't access or modify memory locations that it's not allowed to access). Improper memory management can result in severe problems in software reliability. Languages that aren't memory-safe also negatively impact stability, developer productivity, and application performance.

Organizations can substantially diminish software vulnerabilities by leveraging languages engineered to preempt memory safety issues, such as buffer overflows and use-after-free errors.

Introducing formal verification

Formal verification frameworks are instrumental in assessing the correctness of hardware and software design operations by applying formal mathematical proofs. These frameworks ensure the correctness of underlying algorithms within a system.

Despite adopting memory-safe programming languages, vulnerabilities persist in software systems. Testing alone is insufficient to comprehensively address these vulnerabilities due to the inherent complexities of code. Formal methods offer a systematic approach to demonstrating correctness and integrate verification into the development process.

The importance of compliance

Additionally, formal verification facilitates compliance with regulatory requirements and industry standards by providing concrete evidence of software correctness and security. Whether adhering to data privacy regulations, cybersecurity protocols, or quality assurance benchmarks, formal verification offers a robust framework for meeting and exceeding regulatory expectations.

Latitude and Zephyr

Latitude judged Ada and SPARK to have the best support for sound software engineering practice for their 200kg capacity launcher in LEO, thus reducing life cycle costs while meeting real-time embedded systems performance and predictability requirements.

You can read more about the partnership here in our case study.