Ada is pretty interesting for fuzzing, since all the runtime checks (the ones your compiler couldn’t enforce statically) and all the defensive code you’ve added (through pre-/post-conditions, asserts, ...) can be leveraged as fuzzing targets. Here’s a recipe to use American Fuzzy Lop on your Ada code.

source: grugq

In the context of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution is based on static alias analysis inspired by Rust’s borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write principle.

source: HN

These two extracts, separated by more than 30 years, seem to be targeting the same set of needs. Emphasis is on safety and targeting embedded environments, with efficiency and real-time responsiveness in mind.

source: L

Time taken used to do proof is not just a number, it has significant impact on how the tools are used.