AdaCore Blog

Explore how AI changes what's worth grading in computer science, and how SPARK gives you something that still differentiates students.

See how layered abstraction bridges specs and arrays in SPARKlib's hashed set implementation.

See how AI's coding speed multiplies your liability in C/C++, and how SPARK changes that equation

Look at how far AI-assisted SPARK has come: this blog covers rewriting memcp from Python into SPARK, proved to Silver in about a week — what the AI handled alone, where it stumbled at the FFI boundary, and what that gap tells us.

See how a rule-by-rule comparison of SPARK against MISRA C shows most hazards become moot by design, the rest proven or rejected by the compiler, leaving only a short list of genuine human responsibilities.

Learn how pairing LLM translation with GNATpolyglot's automated bindings collapses the cost of evaluating memory safety in your automotive firmware.

See how GNATpolyglot lets you call high-integrity Ada/SPARK code from C++, Java, and Rust, with the binding layer regenerated automatically as your system evolves.

Discover why your compiler counts as a supply-chain component under the Cyber Resilience Act, and how GNAT Pro delivers the SBOM, vulnerability monitoring, and certification evidence to prove it.

This blog explores how SPARK prevents mistakes and reduces the defects in your source code by up to 70%.

See how SPARK both helps with autonomy- and control-relevant problems on the Mars Rover and integrates productively into agentic AI.

In this blog we have created a table listing each CWE and/or CWE class, along with how each programming language addresses that category.

We're happy to announce the sixth edition of our programming awards, The Ada/SPARK Crate of the Year Award!

Hear about what it’s like to work in technical roles at AdaCore from our Director of Field Engineering and a Senior Software Engineer.

This blog explores how static analysis compares to using an LLM to find defects in source code, and when would you use one over the other.

This blog walks through a concrete example of how to get a unified code coverage picture from two separate execution environments.

This post walks through how we added libtest support to GNAT Pro for Rust using the AMD Zynq UltraScale+ MPSoC as the concrete example.

This blog explores whether SPARK be used to prove something about the time complexities of Linear_Search and Binary_Search

A previous blog explored the verification of the formal hashed sets package in SPARKlib. This post will explain the techniques used to simplify the proof by hiding unnecessary information from the solvers.

This blog explores the use of Google Test to drive our unit test cases, combined with GNATcoverage to measure our code coverage.

Integrating Ada code into Zephyr can be simple as a single LLM prompt and a single make command. This post is about what happens between make and a flashed binary.