AdaCore: Build Software that Matters
AdaCore Hero Image

Blog

An Insight Into the AdaCore Ecosystem

I Stock 1802923559
Feb 04, 2026
Mark Hermeling

Formal Methods Practice and Theory

Formal methods offer a rigorous way to connect requirements to implementation, enabling developers to prove key properties such as the absence of…
Read More
Screenshot 2025 09 01 at 10 14 06
Sep 07, 2025

Romain Gora

Introduction to Ada: a project-based exploration with rosettas

Discover Ada through a fun, project-based tutorial! Learn the language’s clarity, safety, and modern features while building an SVG rosetta…

I Stock 2198938705 1
Aug 20, 2025

Andrea Bristol

Formal Methods in Practice: Government Lessons in Resilience and Adoption Context

As the software landscape grows ever more complex and interconnected, the demand for resilient, high-assurance systems continues to rise, especially…

I Stock 1404889383
Jul 31, 2025

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.

I Stock 1476562177
Jul 18, 2025

M. 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…

Package manager
Jul 10, 2025

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…

I Stock 937874688
Jul 08, 2025

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…

I Stock 2164131231
Jul 01, 2025

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.

I Stock 1336281573
Jun 26, 2025

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,…

I Stock 1468391854
Jun 16, 2025

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…

Regulating technology innovation
Jun 10, 2025

Charis Fisher, Cléa Mendelewski

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…

I Stock 687117042 2025 05 23 093910 mdin
May 23, 2025

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…

I Stock 2159558261
May 12, 2025

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…