The AdaCore Blog
An Insight Into the AdaCore Ecosystem
Oct 22, 2026
Tom Bosque-Jehier
Proving Kruskal’s Algorithm in SPARK: When Generative AI Meets Formal Verification
Can Generative AI prove SPARK code? Testing Claude on formal verification of Kruskal’s MST algorithm, Gale-Shapley and sorting.
Read More
Oct 29, 2020
Arnaud Charlet
Ada 202x support in GNAT
Oct 29, 2020
Juliana Silva
Make With Ada 2020: High Integrity Sumobot
Oct 27, 2020
Fabien Chouteau
Ada for micro:bit Part 7: Accelerometer
Oct 21, 2020
Juliana Silva
Make with Ada 2020: CHIP-8 Interpreter
Laurent Zhu's and Damien Grisonnet's project was accomplished for the EPITA Ada courses and won a finalist prize in the Make with Ada 2019/20…
Oct 20, 2020
Fabien Chouteau
Ada for micro:bit Part 6: Analog Input
Oct 13, 2020
Fabien Chouteau
Ada for micro:bit Part 5: Analog Output
Oct 06, 2020
Fabien Chouteau
Ada for micro:bit Part 4: Pin Input
Oct 05, 2020
Fabien Chouteau, Emma Adby
AdaCore Code of Conduct
Sep 29, 2020
Fabien Chouteau
Ada for micro:bit Part 3: Pin Output
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Sep 28, 2020
Michael Frank
Code Obfuscator for Ada using Libadalang and SPARK
A code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This…
Sep 22, 2020
Fabien Chouteau
Ada for micro:bit Part 2: Push buttons
Sep 15, 2020
Fabien Chouteau