Blog
An Insight Into the AdaCore Ecosystem
Announcing Advent of Ada/SPARK 2025: Coding for a Cause!
Léo Germond
Building a GNAT SAS analysis pipeline on GitLab
This is the first part of a series in which we’ll implement a GNAT SAS analysis pipeline for Ada code on GitLab by making use of GNAT SAS 24 new…
Forough Goudarzi
Memory Safety in Ada and SPARK through Language Features and Tool Support
This blog post describes how Ada and SPARK provide memory safety through a combination of language features, run-time checks, and static and dynamic…
Forough Goudarzi
An Introduction to Memory Safety Concepts and Challenges
This blog post explains the concept of memory safety and the most common memory errors. Then, it introduces three memory-safe languages that have…
Joakim Strandberg
Announcing Ada binding to the wolfSSL library
Today, we at wolfSSL (https://www.wolfssl.com/) are happy to announce the availability of an Ada/SPARK binding that enables Ada applications to use…
Olivier Henley
A little bit of Photoshop® using GNAT for CUDA®
Today I want to go over some internal mechanisms of a Photoshop-like application to better illustrate an up-and-coming tech, GNAT for CUDA®,…
Jose Ruiz
Bare-metal C++ development environment for certifiable safety-critical applications
We are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting…
Nicolas Roche, Olivier Ramonat
Identifying and authorizing users at AdaCore
Back in the 90s when AdaCore was founded, the state of IT security was very different. A unique Unix login and password were enough to connect to a…
Elsa Ferrara
SPARK Tetris on the Raspberry Pi Pico
Tetris was the first computer game played in space but let's review our ambitions for the time and try to implement it on a Raspberry Pico first. …
Fabien Chouteau
Announcing the 2023 Ada/SPARK Crate of the Year Award
We're happy to announce the third edition of our programming awards, The Ada/SPARK Crate of the Year Award! This time with a different approach as…
Pat Rogers
Extending Priority Inheritance Beyond Protected Operations
This blog entry shows how to define protected types that extend the language-defined priority inheritance for protected actions to the statements…
Elsa Ferrara
Formal Proof on Device Drivers with SPARK
Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. On…
Thijs Dreef
Designing a WebAssembly toolchain for Ada/SPARK
WebAssembly (Wasm) is a binary instruction format for a stack-based virtual machine, which was designed as a portable compilation target for…