Blog
An Insight Into the AdaCore Ecosystem
Challenging Agentic AI with SPARK using OpenUxAS
Arnaud Charlet
The Power of Technology Integration and Open Source
Michael Frank
Learning SPARK via Conway's Game of Life
How I learned to write SPARK-provable code using Conway's Game Of Life
Claire Dross
Pointer Based Data-Structures in SPARK
As seen in a previous post, it is possible to use pointers (or access types) in SPARK provided the program abides by a strict memory ownership policy…
Arnaud Charlet
Combining GNAT with LLVM
Emma Adby
The Make with Ada competition is back!
Maxim Reznik, Yannick Moy
First Ada Virtual Conference organized by and for the Ada community
The Ada Community has gathered recently around a new exciting initiative - an Ada Virtual Conference, to present Ada-related topics in a 100% remote…
Isabelle Vialard
Secure Use of Cryptographic Libraries: SPARK Binding for Libsodium
The challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you…
Joffrey Huguet, Johannes Kanig
Proving a simple program doing I/O ... with SPARK
The functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip,…
Juan Zamorano
Using Ada for a Spanish Satellite Project
Yannick Moy, Raphaël Amiard, Tucker Taft
RFCs for Ada and SPARK evolution now on GitHub
Interested in participating in the evolution of the Ada or SPARK languages? We have something for you.
Claire Dross
Using Pointers in SPARK
In this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core…
Nicolas Setton