Blog
An Insight Into the AdaCore Ecosystem
MISRA for Memory Safety
Jon Andrew
CuBit: A General-Purpose Operating System in SPARK/Ada
Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only…
Nicolas Setton
GNAT Community 2020 is here!
We are happy to announce that the GNAT Community 2020 release is now available! Read the post for access to download and to find out about this…
Pat Rogers
From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks
This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification…
Abe Cohen
An Introduction to Contract-Based Programming in Ada
Johannes Kliemann
Ada on the ESP8266
Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to…
Martyn Pike
A Trivial File Transfer Protocol Server written in Ada
For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user…
Roderick Chapman
Proving properties of constant-time crypto code in SPARKNaCl
Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under…
Ghjuvan Lacambre
Time travel debugging in GNAT Studio with GDB and RR
Learn how to use GDB and RR's advanced time traveling features in GNAT Studio.
Maxim Reznik
Android application with Ada and WebAssembly
Pat Rogers
Making an RC Car with Ada and SPARK
Pierre-Marie de Rodat
A Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App
Vadim Godunko