Blog

Kyriakos Georgiou

Security-Hardening Software Libraries with Ada and SPARK

Fabien Chouteau

Announcing The First Ada/SPARK Crate Of The Year Award

We're happy to announce our new programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game…

Roderick Chapman

SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at…

Jessie Glockner

Celebrating Women Engineering Heroes - International Women in Engineering Day 2021

Arnaud Charlet

Going beyond Ada 2022

Fabien Chouteau, Nicolas Setton

GNAT Community 2021 is here!

Pat Rogers

An Introduction to Jorvik, the New Tasking Profile in Ada 2022

The Ada 2022 draft defines a new tasking profile named Jorvik (pronounced “Yourvick”), based directly on the standard Ravenscar profile. Jorvik…

Fabien Chouteau

From Rust to SPARK: Formally Proven Bip-Buffers

I am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that…

Pat Rogers

On the Benefits of Families ... (Entry Families)

Simon Buist

Showing Global contracts with GNAT Studio

In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.

Roderick Chapman

Doubling the Performance of SPARKNaCl (again...)

Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack…

Roderick Chapman

Performance analysis and tuning of SPARKNaCl

This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and…