When Formal Verification with SPARK is the Strongest Link

Security is only as strong as its strongest link. That's important to keep in mind for software security, with its long chain of links, from design to development to deployment. Last year, members of NVIDIA's Offensive Security Research team (aka "red team") presented at DEF CON 29 their results on the evaluation of the security of a firmware written in SPARK and running on RISC-V. The ended up not finding vulnerabilities in the code, but in the RISC-V ISA instead. This year, the same team presented at DEF CON 30 a retrospective on the security evaluation of 17 high-impact projects since 2020. TL;DR: using SPARK makes a big difference for security, compared to using C/C++.

New features for string literals and comments in GNAT Studio

We have added several new convenience features that help work with comments and string literals in Ada code.

Fuzzing Out Bugs in Safety-Critical Embedded Software

Fuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolbox

Embedded Ada/SPARK, There's a Shortcut

For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.

Join us at the High Integrity Software (HIS) Conference 2022!

After two years of virtual events, we are very happy to report that the High Integrity Software Conference (HIS) will be making a physical comeback on Tuesday 11th October 2022 at the Bristol Marriott Hotel City Centre, Bristol, UK. Since 2014, AdaCore has been co-organising the event with Capgemini Engineering (previously known as Altran Technologies, SA). The success and growth of the conference have ensured it remains a regular fixture for returning delegates, and the exciting lineup for this year's event will ensure HIS 2022 is no exception!

Announcing Publication of the Draft Ferrocene Language Specification

We are pleased to announce the publication of the initial draft of the Ferrocene Language Specification (FLS) - a qualification-oriented document that details the Rust language as it specifically relates to Ferrocene.

Announcing The 2022 Ada/SPARK Crate Of The Year Award

We're happy to announce our the second edition of our programming competition, the Ada/SPARK Crate Of The Year Award! We believe 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.

I can’t believe that I can prove that it can sort

When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this eye-opening journey.

A New Era For Ada/SPARK Open Source Community

Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.

Announcing Updates to learn.adacore.com

Ada Crate of the Year: Interactive code search

A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.

Handling Aliasing through Pointers in SPARK

As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.

Quite Proved Image Format

A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression designed to have a very simple implementation (about 300 lines of C). Shortly, a few alternative implementations popped up here and there, and in this kind of situation we are eager to show what Ada/SPARK can bring to the table.

Ada GameDev Part 2: Making 2D maps with Tiled

In this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE library.

SPARK Crate of the Year: Unbounded containers in SPARK

Manuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/​SPARK and how he created the spark_unbound library

Ada GameDev Part 1: GEneric Sprite and Tile Engine (GESTE)

In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering and anesthetic of 8bit era game consoles to modern microcontrollers.

Proving the Correctness of GNAT Light Runtime Library

The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use at the highest levels of criticality in several industrial domains. It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. We have used SPARK to prove the correctness of 40 of them: that the code is free of runtime errors, and that it satisfies its functional specifications.

AdaCore and Ferrous Systems Joining Forces to Support Rust

For over 25 years, AdaCore has been committed to supporting the needs of safety- and mission-critical industries. This started with an emphasis on the Ada programming language and its toolchain, and over the years has been extended to many other technologies. AdaCore’s product offerings today include support for the Ada language and its formally verifiable SPARK subset, C and C++, and Simulink and Stateflow models. We have accomplished this while addressing the requirements of various safety standards such as DO-178B/C, EN 50128, ECSS-E-ST-40C / ECSS-Q-ST-80C, IEC 61508 and ISO 26262.

AdaCore at FOSDEM 2022

Like previous years, AdaCore will participate in FOSDEM. Once again the event will be online only, but this won’t prevent us from celebrating Open Source software and it is an opportunity for even more people to participate around the world.

Ada/SPARK Crate Of The Year 2021 Winners Announced!

In June of 2021 we announced the launch of a new programming competition called Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 200 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.