SPARK
A subset of Ada built for deductive formal verification, described on AdaCore’s product page. The design is subtractive: take Ada and remove the constructs that admit undefined behaviour, leaving a language whose programs can be reasoned about mechanically. Contracts — preconditions, postconditions, type invariants, assertions — are first-class language constructs rather than comments, and subprograms are treated as Hoare triples: given the precondition holds, prove the postcondition holds after execution.
What it proves: absence of runtime errors — array-bounds violations, division by zero, overflow — and, through an ownership model AdaCore says is derived from Rust with borrow checking, absence of use-after-free, uninitialized access and memory corruption. AdaCore describes the analysis as sound (no false negatives) and precise (no false positives) provided the prover does not time out. Tooling is SPARK Pro and GNATprove alongside the GNAT compilers, with certification support for DO-178 (avionics) and ISO 26262 (automotive). Domains: avionics, automotive, defence, medical devices, rail, space.
T1 — first-party for the language, and simultaneously a commercial product page, which is the weakest instance of the tier in this spoke. The soundness and precision claims are exactly what a tool paper or an independent evaluation should support, and neither is here. Flagged for the curator: if vendor product pages should sit below official language sites, this is the page to move.
The third answer to safety
synthesis records the corpus’s open disagreement about what safety is for: rust prevents the bug at compile time, elixir survives it at runtime, c declines the question. SPARK is a fourth position, and the strongest form of the first: prove the bug cannot occur, for a stated property, on this program. Not a type system ruling out a class of errors but a prover discharging obligations about specific code.
The Rust lineage is the detail worth keeping. A formal-methods language for avionics adopting ownership and borrow checking from Rust is a compile-time-safety idea moving from a general-purpose language into a certification-driven one — the reverse of the usual direction, in which safety-critical practice trickles outward.
Its cost is the one AdaCore’s page states obliquely and this corpus cannot measure: a proof needs a
specification, so someone must write the contracts, and the guarantee is only as good as what they
say. The unstated half — how much of a real system is provable in practice, and what the timeouts cost —
is the same gap ../research-wiki’s formal-verification page names for the whole field.
Related
formal-verification · rust · c · memory-management-model · programming-language · language-governance · synthesis