Blog
An Insight Into the AdaCore Ecosystem
Formally Verified Hashed Sets in Ada SPARK
M. Anthony Aiello
Challenging Agentic AI with SPARK using OpenUxAS
“How well does generative AI do with writing Ada?” The simple answer is: “quite well!” But the details are also interesting, so I encourage you to…
Mark Hermeling
Escaping the Haystack: CI/CD for Embedded Systems
How fast feedback loops, smart abstraction, and disciplined pipelines change the way embedded software teams work and ship.
Kyriakos Georgiou
Fuzz Everything, Everywhere, All at Once: Scaling Security with GNATfuzz
If you are developing high-integrity systems, GNATfuzz can provide the extra layer of security analysis required by modern certification standards.
Mark Hermeling
Migrating C to Ada SPARK with Agentic AI: A Practical Playbook
Agentic AI can enable teams to re-use existing code bases and carefully decide which parts to translate into Ada SPARK, avoiding problems caused by…
Olivier Henley
How Evolutek Used Ada to Build Their CanSat
AdaCore supports practical engineering projects that help students apply technical concepts to real-world problems. As part of this effort, AdaCore…
Tobias Reiher
Enabling Rust on the AMD Zynq UltraScale+ MPSoC
In this post, we’re sharing our journey of building a dedicated crate that provides support for the AMD Zynq UltraScale+ MPSoC.
Kyriakos Georgiou
Hardware-Driven Security: Can CHERI Fix the "Blind Spots" of Software Testing?
This work combines fuzz testing with CHERI hardware. Unlike heuristic-based sanitizers, CHERI uses hardware-enforced capabilities - pointers with…
M. Anthony Aiello
GNAT IQ
AdaCore is delighted to announce unlimited access to GNAT IQ, AdaCore’s AI-powered GNAT documentation chatbot, for all of our current customers.
Frederic Leger, Nicolas Roche
AdaCore Software Supply Chain Security Evolution
AdaCore has elevated its software supply chain practices and now generates its deliverables in a CMMC Level 2 and SLSA build level 3 compliant…
Mark Hermeling
Formal Methods To Improve Code Quality
Memory safety is rightly a major focus in embedded systems. This article outlines the difference between static and dynamic memory safety, and how…
Mark Hermeling
GNATpolyglot: Mastering Multiple Languages
This blog introduces GNATpolyglot, a new capability in the GNAT Pro toolchain.
Johannes Kanig
Scalable SPARK Proofs
This blog post explains how a SPARK function for counting character occurrences was formally verified to ensure both absence of runtime errors and…