Ada/SPARK

The "."Ada horizon" logo maker website.

Collection of verified functions and data types in SPARK.

A collections of small nifty demos/sample code that may help better layout data or structure project.

Standard Ada library specification as defined in Reference Manual.

Reference Card / Cheatsheet of Ada Attributes, Aspects, Pragmas and Standard Library.

The HAC Ada Compiler - a small, quick Ada compiler fully in Ada.

A community project to build an Ada compiler, toolchain, and IDE-system.

Ada compiler written in Scala that targets LLVM.

Free Software Foundation compiler for the Ada programming language which forms part of the GNU Compiler Collection. It supports all versions of the language, i.e. Ada 2022, Ada 2012, Ada 2005, Ada 95 and Ada 83.

GNAT Community edition. A release of AdaCore GNAT for free software developers, hobbyists, and students. The run-time libraries provided with GNAT Community are licensed under GPLv3 without linking exception. It supports Ada 2012 only.

A Lightweight Editor for Ada, aims to provide an easy, script-world-like, "look & feel" for developing Ada projects of any size and level, while enabling access to full-scale development tools like GNAT. LEA includes HAC, the HAC Ada Compiler.

Maintained Ada Bundle : Complete Ada-Mode for Vim/Neovim.

Ada/SPARK support for org-babel : Evaluate source code blocks with Gnu Emacs and org files.

Doom Emacs Ada language module with syntax highlighting, LSP and Alire support.

Basic syntax highlighting for Ada and GPR.

VSCode extension Ada programmers which provides a few utility functions.

A catalog of ready-to-use Ada libraries plus a command-line tool (alr) to obtain, compile, and incorporate them into your own projects. It aims to fulfill a similar role to Rust's cargo or OCaml's opam.

A tool for automatically creating an AppImage executable from an Alire crate.

An integrated build and source/package management tool with a more hands-on versioning approach. Alternative to alire and gprbuild. Optimized for CI/CD pipelines.

Adacore multi-language software build tool.

Administration tool for Ravenports http://www.ravenports.com.

Next D/Ports build tool for live systems (Alternative for Portmaster and Portupgrade tools).

CMake macros for simple gnat project inclusion.

Ada language support for CMake.

CMake language support for Ada, fork of [plplot]'s cross-platform support code.

An opinionated package management tool for Ada.

SPARK formal verification automated with Travis CI.

Ada Toolchains for GitHub Actions.

A logging framework close to Java log4j framework, support for properties, serialization/deserialization framework for XML/JSON/CSV, Ada beans framework, encoding/decoding framework (Base16, Base64, SHA, HMAC-SHA), a composing stream framework (raw, files, buffers, pipes, sockets), several concurrency tools (reference counters, counters, pools, fifos, arrays), process creation and pipes, support for loading shared libraries (on Windows or Unix), HTTP client library on top of CURL or AWS.

This is the core module of the GNAT Components Collection.

This is the bindings module of the GNAT Components Collection.

This is the DB module of the GNAT Components Collection.

This is a set of helpers for writing JSON-intefaces it contains JSON parses for most of the Ada runtime components.

An interface collection to be used with applications for component based systems. It aims to be easily portable/platform independent and is compatible with the [ada-runtime].

A set of Ada components to allow 3D simulations, games and GUI's in Ada.

A set of general libraries and thick bindings for use with the AURA package management/build tool. Includes TCP, TLS, HTTP, a high-performance JSON parser/generator, and a formally verified (SPARK) UTF-8 stream decoder.

PolyORB provides a uniform solution to build distributed applications relying either on middleware standards.

Ada graphical toolkit based on Gtk3 components.

GNU Ada Visual Interface.

GUI implemented on its own task, so it doesn't require that its client give up a thread of control. Derived from [gnoga].

GUI based on [adawebpack].

Ada binding of the ImGui library.

Ada binding to the Nuklear GUI library and the Nuklear-SDL renderer.

Advanced UNIX Terminal UI Ada Binding Package.

Ada binding to the readline library.

GL Object Based Engine for 3D.

A 3D engine for DOS-talgics.

Ada OpenGL Framework.

Id Software's Id-tech-4-BFG in the Ada programming language.

Code generator used to generate an Ada Web Application or database mappings from hibernate-like XML description, YAML doctrine model or UML models.

Ada Wiki is a small library that provides a Wiki engine.

OAuth 2.0 client and server framework to secure web applications.

This library provides the support for a simple Expression Language close to the Java Unified Expression Language (EL).

Ada Server Faces allows to create web applications using the same pattern as the Java Server Faces (See JSR 252, JSR 314 and JSR 344).

Ada Servlet allows to create web applications using the same pattern as the Java Servlet (See JSR 154, JSR 315).

Ada unit testing framework.

Simple tool to black box check the behavior of an executable through the command line.

Behavior Driven Development in Ada.

Supports functional testing using Tcl scripts.

Ada testing framework, part of Tada.

Logging framework for embedded systems absent of runtime errors.

A4A is a framework for designing industrial automation applications using the Ada language.

An interactive context-based text search tool for searching large codebases.

This tool allows monitoring power consumption of multiple platforms and processes.

Simple memory analysis tool intended to help understand where the memory is used in a program.

GNATcoverage is a tool to analyze and report program coverage.

SPARK formal verification toolset.

The Ada Conformity Assessment Test Suite, customised for GCC.

Tools for grading ACATS results, modified for Unix-like systems.

An open source ASN.1 generator to Ada type declarations and encoders/decoders.

AADL model processor: mappings to Ada code; Petri Nets; scheduling tools (MAST, Cheddar); WCET; REAL.

Finite-state machine generator.

Generator of JUnit-compatible XML reports in Ada.

RecordFlux: Toolset for the formal specification of messages and the generation of verifiable binary parsers and message generators in SPARK.

Advanced Resource Embedder to embed files in binaries by producing C, Ada or Go source files.

Ada-tailored UML Modeling Language.

This tool generates Ada framework code and documentation from UML models.

Ada Keystore - protect your sensitive data with secure storage.

Collection of basic math routines in Ada.

Collection of mathematical, 100% portable, packages in the Ada programming language.

Mandelbrot renderer in "ASCII" (unicode actually, but text nonetheless).

Interface to dense linear algebra packages.

Software libraries for solving models described in Mathematical GeoEnergy (Wiley, 2018).

Compute the N-th root of a matrix.

Ada binding to the fast Stachniss' Hungarian solver.

Utility library to pretty print physical values in proper metric units.

Adacore server implemention of the the Microsoft Language Protocol for Ada and SPARK.

Language Server Protocol for Ada.

Prototype implementation of LSP client - Visual Studio 2017.

Generic Ada Library for Algorithms and Containers.

PragmAda Reusable Components (PragmARCs) from PragmAda S/W Engineering.

Simple Ada library for generating UUIDs.

Genetic Algorithm Implementation for Ada.

Small Library for Sodoku grid solving / finding.

Simple Layer 3 Protocol.

A package providing a reference-counted access type Smart_Pointer.

Hungarian Algorithm implementation in Ada.

NBAda : An Ada library of lock-free data structures and algorithms.

Simple blockchain in Ada.

Gnutella2 (G2) network server leaf.

Ada General Purpose Library (Miscellaneous utilities, with a robotic flavor).

Ada binding for Z3.

Bounded containers for embedded systems.

Ada Implementation of the Threefish-256 Encryption Algorithm.

Trivial implementation of fletcher_16 checksum computation algorithm.

Base58 encoding and decoding in Ada.

This is a crypto library for Ada with a nice API and is written for the i386 and x86_64 hardware architecture.

A cryptographic library implemented in SPARK.

A pure Ada implementation of the SipHash PRF.

A SPARK implementation of the Keccak family of sponge functions and related constructions.

Ada/SPARK implementation of the Ascon Authenticated Encryption with Additional Data Algorithm.

Ada/SPARK implementation of the SipHash keyed hash function.

Ada/SPARK implementation of the NORX Authenticated Encryption with Additional Data Algorithm.

SPARK 2014 re-implementation of the TweetNaCl crypto library.

Timed One-Time-Pad (RFC 6238) implementation in SPARK.

Extremely fast non-cryptographic Hash algorithm, xxhash is working at speeds close to RAM limits.

A secure cryptographic library (libsodium for Ada).

Ada Binding for the libsecret library.

SPARK83 implementation of the BLAKE2s hash function.

Programming library for dealing with the Zip compressed archive file format.

Ada binding for liblzma compression library.

An Ada 2012 library for document container files (Based on [zip-ada]).

Implementing promises in Ada. Type-safe, efficient, thread-safe.

Task pool system for jobs.

An Ada 2012 implementation of the Rx methodology.

A fuzzy inference system library for Ada.

Ada library and tools for the analysis of Complex Networks and more.

Library for parsing and semantic analysis of Ada code. It is meant as a building block for integration into other tools (IDE, static analyzers, etc).

Ada code analyzer.

Grammar handling and parser generation Ada library.

Pretty printing library for Ada.

Incremental analysis in Ada.

Simple command-line argument parsing.

Embeddable Forth interpreter written in Ada.

Tools for writing lexers / parsers in Ada.

An Ada implementation of XPath 1.0.

Embeddable Lisp interpreter.

The Ini file manager consists of a package, Config, which can read and modify informations from various configuration files known as "ini" files.

Experimental Ada code generation support for Google Protocol Buffers.

A Google Protocol Buffers implementation in Ada, using [matreshka].

Experimental YAML 1.3 implementation in Ada.

An Ada 2012 library for parsing JSON.

A formally verified JSON library in SPARK.

The XML/Ada toolkit.

Library for emitting XML from Ada programs.

A formally verified XML library in SPARK.

Create Excel files with basic formats.

Multi-format image decoder library for Ada.

Ada package for producing easily and automatically PDF files, from an Ada program, with text, vector graphics, images (JPEG).

Implementation of Midi / MidiFile reading and writing.

Ada Bar Codes provides a package for generating various types of bar codes (1D, or 2D like QR codes) on different output formats, such as PDF or SVG.

Various binary-to-ASCII codecs such as Base64.

A library of access routines to Axon's ABF file format (electrophysiology, most common) in Ada.

TOML parser for Ada.

URI and MIME parser & manipulation library.

Magic Number Recognition Library Ada binding (libmagic (3)).

URI and MIME parser & manipulation library.

IPv4 socket library (TCP, UDP, and multicast).

Binding to the ZeroMQ comunications-library.

Binding for the MQTT broker Mosquitto.

Binding for the C librdkafka library, allows sending and receiving from a Kafka bus.

A formally verified implementation of CoAP, the Constrained Application Protocol.

Binding to the ZeroMQ comunications-library.

With the AXMPP library you can connect to a Jabber server to send and receive messages.

Ada 2012 library for WeeChat plug-ins.

A WeeChat plug-in written in Ada 2012 that plays sounds using Canberra.

A WeeChat plug-in written in Ada 2012 that displays emoji.

AWS templates engine.

Thick Ada binding for OpenGL and GLFW.

Multiplatform Ada/OpenGL bindings (ported to native/OpenGL, A2JS/WebGL and WebAssembly/WebGL).

Ada 2012 bindings to SDL 2.

Ada bindings to NanoVG.

FreeType binding for Ada 2005.

Ada binding to the Simple and Fast Multimedia Library.

Support for CUDA (Compute Unified Device Architecture) from AdaCore.

An Ada binding for the OpenCL host API.

Ada binding to the Boehm-Demers-Weiser conservative garbage collector.

An Ada binding for the GNU Binutils BFD library. It allows to read binary ELF, COFF files by using the GNU BFD.

Ada 2012 bindings for the Opus audio codec.

Ada 2012 bindings for libcanberra, an implementation of the XDG Sound Theme and Name Specifications.

Ada bindings for libsoundio.

Ada binding to OpenAL which tries to mimic original API while using Ada types.

Ada binding to OpenAL.

Sound Synthesizer Library implemented in Ada.

A linux-sound-playing package for Ada apps that can asynchronously start and stop music loops, as well as initiate transient sounds.

A MOD, XM, S3M, and IT music tracker player written in Ada, using SDL2 for audio output and UI rendering.

Reference counting approaches to resource management.

Stream utilities for Ada2005 and 2012.

An extensible template engine akin to jinja but using [template-parser] and intended for command line usage.

Open Source Licenses library for Ada.

Easy to use logging facilities for output to console in Ada programs.

Command-line utility that picks a file from a folder hierarchy with probability proportional to its size.

Convenience subprograms to interact with C strings.

Tool to imports CVS repository shared on Ada Conformity Assessment Authority into the Git repository.

Library and tool for transparently handling data and configuration file access in an Ada application. Supports macOS, Linux and Windows.

Provides GCC 'specs' files to cope with SDK policy changes.

Unicode extended strings.

Portable implementation of getopt(3) in Ada.

Portable implementation of getopt(3) in Ada.

Ada client library for ROS2/RCL.

Ada bindings for the player robotic platform.

A fork of Florist which is available as an Alire crate.

Ada Windows POSIX binding.

Ada Posix Binding to Video 4 Linux, used for RPI.

An Ada 2012 library for monitoring filesystem events using Linux' inotify API.

Minimal binding to libdl.

Small Ada library that helps in writing safer suid programs.

POSIX Ada binding, IEEE Standards 1003.5(b,c).

Ada API to the Windows library.

Ada bindings to the Microsoft NetFramework Api.

Ada bindings for the Microsft WinRT Api.

Ada bindings for the Microsoft Win32 Api.

Tcl Ada SHell (Tash) is an Ada binding to Tcl/Tk.

Tcl Ada SHell Younger (Tashy) is derivate of Tash, focused mostly on Tk binding.

Derivate of Tashy that aims to be more idiomatic and uses a more permisive license.

Ada binding for Lua.

Ada bindings to the Lua language.

NLS thin Ada binding (gettext (3), textdomain (3), bindtextdomain (3)).

A lightweight development framework whose purpose is the implementation of Ada-based software systems. It supports a plethora or CPU architectures and development boards.

Robotics with Ada, ARM, and Lego.

A component-based, model-driven framework for constructing reliable and reusable real-time software.

A graphics initialization (aka modesetting) library for embedded environments, implemented in SPARK.

Source code for the full Ada + SPARK Crazyflie 2.0 firmware.

Ada drivers for various MCU and sensors.

emBRICK driver and support for emBRICK in Ada.

Ada/SPARK driver for the DecaWave DW1000 ultra-wideband (UWB) radio chip.

Ada/SPARK drivers to control the on-board peripherals of the DecaWave EVB1000 evaluation board.

This contains explorations, for AdaPilot, of implementing drivers for the AdaRacer MCU, using the Ravenscar profile of Ada 2012 from AdaCore and device bindings generated using SVD2Ada.

Software controller for solenoid engines (Ada/STM32F4).

Embedded network stack (Ethernet driver, IPv4, UDP, DNS, DHCP, NTP) for STM32F746 or STM32F769.

This project shows how to initialize a SensorTile and how to send sensor data over BLE from a SensorTile to a suitable host.

This library is trying to be a simple widget tool kit for embedded platforms.

Simple audio synthesis library that can run on bareboard devices.

Sprite and tile 2D render engine designed to run on micro-controllers.

Multi-robot task allocation library.

STM32 UI library and tools (graphs, images, 12 hour clock).

Ada binding for the Pebble Time smartwatch.

Ada bindings for wiringPi.

Waking up with a fresh cup of coffee.

Square Inch Synthesizer.

Simulated railway network in SPARK/Ada.

Raspberry Pi using a BBC Micro:Bit as temperature sensor.

Wee Noise Maker is an open source pocket synthesizer.

Program that interacts with the AdaFruit BNO055 breakout board in order to send orientation data to a host computer.

Program simulating a railway network with trains, switches and signaling. The signaling system is proven with SPARK/Ada to ensure that trains cannot collide.

Ethernet traffic monitor on a STM32F746 board.

An Ada binding generator from SVD descriptions for bare board ARM devices.

A free, portable Zip Archive Manager.

A program for drawing or retouching {picture}s in LaTeX.

The Corporate Bullshit Generator.

Graphical ([gtkada]) file manager for Linux.

A Web browser with safety focus.

Yet Another Static Site Generator (like Jekyll or Hugo).

A simple 3DS Max model renderer.

A stand-alone lightweight auxiliary video player support for `BlackVideo`.

A G-code parser and CNC controller (in Ada).

Apollo 11 lunar lander simulator ([gtkada]/Cairo).

VHDL 2008/93/87 simulator.

Distributed Simulation of Transport Networks.

Multi engine/algorithms COVID-19 simulator. Ada, Qt code under the hood.

Mars Polar Lander (Crash) Simulator ([gtkada], [aicwl]).

Moving airplane causes Stereo Sound Doppler effect ([gtkada]).

A Pascal to Ada translator.

Implementation of Turbo Pascal 7.0 units with [gtkada].

Implementation of Turbo Pascal 7.0 units with [gnoga].

Code generator for Tiled the map editor.

Translator for a Java valid source code in Ada source code.

Ada binding generator for C++.

Converts Ada sources' ASIS representation to XML, so as to make it easier to develop reporting and transformational tools using (for example) XSLT.

Helper conversor of Visual Basic Microsoft Windows Forms applications to Gtk and Ada.

Non interactive POSIX shell for Windows, aimed at GNU software builds. 2-3 times faster than Cygwin.

An Ada 2012 emulation of Charles Babbage's Analytical Engine.

A component to aid in writing shell-like applications in Ada.

Data General DASHER terminal emulator using [gtkada].

Assembler/Emulator for a fictional CPU architecture. IDE implemented in [gtkada].

Ada implementation of D'Hondt electoral result calculator.

William Whitaker's WORDS, a Latin dictionary.

Chess engine written in Ada.

An Ada/SPARK alternative to sudo and doas.