Edit on GitHub

What is Ada and SPARK?

Ada is a state-of-the art programming language that development teams worldwide are using for critical software: from microkernels and small-footprint, real-time embedded systems to large-scale enterprise applications, and everything in between.

SPARK is formally analyzable subset of Ada — and toolset that brings mathematics-based confidence to software verification.

Try Ada Now:

with Ada.Text_IO; use Ada.Text_IO; procedure Learn is subtype Alphabet is Character range 'A' .. 'Z'; begin Put_Line ("Learning Ada from " & Alphabet'First & " to " & Alphabet'Last); end Learn;

Check out the interactive courses and labs to learn more about Ada and SPARK.

Download Ada and SPARK tools

Gnatcommunity Download

Try Ada and SPARK now with GNAT Community edition.

GNAT Community includes the Ada compiler and toolchain, the SPARK verifier and provers, and the GNAT Studio IDE.


We’re calling on developers across the globe to build cool embedded applications using the Ada and SPARK programming languages and are offering over $9,000 in total prizes! Click on the banner above to learn more.