by
Andrea Bristol
–
Ada and Rust are highlighted by the NSA and CISA in Memory Safe Language Information Sheet
Governments trust memory-safe languages like Ada and Rust — so do we. See why memory safety is essential for secure systems.
by
Anthony Aiello
–
Revisiting the Mars Rover Safety Monitor
In the blog "Let's Write a Safety Monitor for a Mars Rover", I made a big assumption in the procedure that moves that Rover forward; here, I relax that assumption and thus end with a stronger proof of safety for the Rover.
by
Fabien Chouteau
–
Announcing the 2025 Ada/SPARK Crate of the Year Award
We're happy to announce the fifth edition of our programming awards, The Ada/SPARK Crate of the Year Award! The Alire package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.
by
Fabien Chouteau
–
Solving Sudoku with AdaSAT
Originally, constraint solving in Libadalang was handled by several ad-hoc solvers built specifically for different parts of the type system. These implementations were tailored and somewhat fragile. A couple of years ago, a newer approach replaced these with a backend based on satisfiability solvers, AdaSAT. In this blog post, I will use AdaSAT to implement a Sudoku solver.
by
Andrea Bristol
–
What’s All the Fuzz About?
In this blog, we discover Fuzz Testing and how GNATFuzz can be used as part of AdaCore’s GNAT Dynamic Analysis Suite.
by
Edgar Delaporte
–
Improving SPARK Counter Examples with Fuzzing and Code Analysis
When analyzing a SPARK program with GNATprove, some verification conditions might remain unproven, whether because of a defect in the user’s code, contracts that are too weak, or sometimes because of a tool limitation. In this context, an effective way of helping developers is to provide them with counterexamples, subprogram input values that would lead to invalid executions (out-of-bounds access, division by zero, integer overflow, exceptions, etc.). The project I worked on during my internship was to take advantage of AdaCore's dynamic analysis suite (GNAT DAS) to improve the counter-example technology.
by
Stephen Hedrick
–
Navigating Mars with Rust: Developing an Autonomous Pathfinding Rover
This blog showcases how Rust was used to implement the D*-Lite pathfinding algorithm for an autonomous Mars rover simulation. It highlights Rust’s strengths—such as memory safety, strong typing, and zero-cost abstractions—in building a responsive, efficient navigation system that adapts to dynamic obstacles.
Regulating Innovation: A Day in the Life of an In-House Lawyer in Tech
AdaCore Senior Corporate Counsel, Sarah Wallace, explains why partnership and collaboration are integral to her role practicing in-house law in a technology company.
by
Tobias Reiher
–
Building a Virtual Mars Rover with SPARK and Rust
We have taken our Ada Mars Rover demo, featuring a physical robot driven by formally verified SPARK software, to the next level by introducing a simulator that allows you to experience the Rover's capabilities virtually. This simulation, implemented in Rust, accurately models the Rover's movement in an obstacle-filled environment, all while being controlled by the original SPARK code. This project exemplifies the synergy between Ada and Rust, demonstrating how these technologies can be effectively combined to build reliable, safety-critical applications.
by
Andrea Bristol
–
AdaCore and Lynx Software Technologies Reaffirm Longstanding Partnership
AdaCore and Lynx Software Technologies have reaffirmed their longstanding technology partnership to support avionics and defense customers developing safety-critical applications with Ada. Both companies will showcase their software solutions at the Army Aviation Mission Solutions Summit (“QuadA”) conference and exposition in Nashville, Tennessee, May 14-16. AdaCore and Lynx solutions are used in hundreds of military and aerospace programs worldwide.
by
Andrea Bristol
–
Formal Methods for an Insecure World
This article unpacks what it means to be Secure by Design, outlining practical measures for integrating security into the software lifecycle. It highlights the critical role of formal methods, particularly the SPARK technology, in delivering on this vision.
by
Andrea Bristol
–
Safer with Ada
What makes our software so vulnerable?The majority of today’s technical systems are largely composed of software. As such, the reliability and security of these systems depend heavily on the reliability and security of their software components. And this is precisely where a major problem lies: increasing connectivity and a large number of known vulnerabilities in commonly used software make our systems highly susceptible to attack.
by
Quentin Ochem
–
Let's play '7 differences in Ada'
Over the past few years, we've been progressively developing new GNAT extensions for the Ada programming language, which you can follow and contribute to on the github RFC page. While the implementation is ramping up, we can already share a few aspects of the language that can be tested with recent versions of the GNAT Pro compiler, which will eventually find their way to the open-source version.Let's play a game. The code below is an - arguably over-engineered - version of a tic-tac-toe game. Can you find the 7 differences (or features) introduced by the Ada extensions? Note that some of these are only visible on one line, some have an impact across the entire application.If you want to compile this code, you will need both a GNAT Pro wavefront with the latest changes in, and the switch -gnatX0 that enables all experimental features
by
Johannes Kliemann
–
CheriBSD: A Showcase for Hardware-Supported Security
Over the course of the last few years and as part of the 'Edge Avionics' project, funded by the Rapid Capabilities Office (RCO) of the UK Royal Air Force (UK RAF), AdaCore has been developing toolchain solutions for Capability Hardware Enhanced RISC Instructions (CHERI) microprocessor architectures. In addition, AdaCore evaluated security claims made by the CHERI community through the Digital Security by Design (DSbD) initiative. The goal was to inform Edge Avionics project partners about the level of security assurance offered by the Arm Morello microprocessor; a modified Arm Neoverse N1 supporting the Armv8-A architecture and conforming to the CHERI compartmentalization specification. The DSbD project is now in the final stages, the overarching goal of mass adoption of CHERI-architectures is now looked after by the CHERI Alliance.
by
Andrea Bristol
–
Ada is back in the TIOBE Index top 20
The March edition of the TIOBE Index shows Ada in the top 20, hitting position 18. This shows a renewed interest in Ada, perhaps due to the increased interest in memory-safe languages and software safety and correctness in general.
by
Anthony Aiello
–
Let’s Write a Safety Monitor for a Mars Rover!
The Ada Mars Rover shouldn’t crash into obstacles. See how we formalized this property, discovered an unstated assumption in our remote-control mode that could have led the Rover to crash, removed the assumption, and ultimately proved this property using SPARK. You’ll be surprised how little new code - including proof code - was needed!
by
Pat Rogers
–
Ada in Practice, a New Learn Course
A new Learn course is now available, focusing on how to use the Ada language to express common idioms, both language-dependent and -independent.
Building the Future: My Path from Software Research to Leadership
To celebrate Global Engineering Day, we’re looking at what it’s like to work as a truly global engineer, collaborating with international colleagues from all over the world to advance software development.
by
Justin Squirek
–
A new math library for Ada: Neo.SIMD
Developing a game engine often requires a highly optimized linear algebra library for tasks like physics, camera movement, and AI. While many languages already have mature options, Ada’s ecosystem lacks such solutions. To fill this gap, I created Neo.SIMD as part of the AdaDoom3 project. Neo.SIMD takes advantage of SIMD (Single Instruction Multiple Data) instructions, which process multiple data points in parallel and can greatly improve performance for vector and matrix operations.
by
Ben Brosgol
–
Verifying FACE® Conformance for Ada Software
The FACE® approach (Future Airborne Capability Environment®) is a joint government-industry initiative to reduce system life cycle costs for airborne software through the reuse of portable source code components. Sponsored by the US Department of Defense and currently open to the “Five Eyes” countries (Australia, Canada, New Zealand, UK and the US) the FACE approach is administered by The Open Group’s FACE Consortium and is realized through several technologies based on open standards.