Blog

Emma Adby

Make with Ada 2020: LoRaDa := Ada + LoRa;

Hedley Rainnie's project combines 6 different SoCs all programmed in Ada performing as a LoRa network. He also showcases a BLE bridge to a LoRa…

Claire Dross

Relaxing the Data Initialization Policy of SPARK

SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like…

Emma Adby

Make with Ada 2020: Disaster Management with Smart Circuit Breaker

Shahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the…

Emma Adby

Make with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded Device

Team CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an…

Emma Adby

Make with Ada 2020: The SmartBase - IoT Adjustable Bed

John Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed…

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…