A curated list of awesome resources related to the Ada and SPARK programming language
-
Updated
Sep 22, 2026
A curated list of awesome resources related to the Ada and SPARK programming language
SHA-3 and other Keccak related algorithms in SPARK/Ada.
SPARK Proof Analysis Tool
A cryptographic framework, proven for correctness in SPARK
Minimalist cooperative operating system supporting multiple tasks with MMU protection
Formally verified implementation of the CoAP protocol in SPARK/Ada
FLAC audio encoder/decoder in SPARK/Ada
Modular shell configuration manager - declarative, idempotent, written in Ada for safety-critical reliability
An attempt to verify functions from Curve25519 implementation in SPARK2014
A high-assurance identifier and redirect service with formally verified core logic.
Small language models trained only on code that seven independent proof systems agree is correct: Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq and F*, each also refuting a deliberately broken copy of every kept program.
Rust-Ada-Zig TUI library: Zig FFI bridge between Rust core and Ada/SPARK TUI
Ada TUI for managing rclone cloud mount configurations with rate limiting and SDP security
A powerful, type-safe directory tree export and navigation tool written in Ada 2022
DNS record randomization tool for deprecated HINFO and LOC records. Built with Ada for maximum security and type safety.
Ada/SPARK repository auditor (health, compliance, security posture)
To associate your repository with the spark-ada topic, visit your repo's landing page and select "manage topics."