Community Highlights
Bbs_lisp
bbs_lisp is an embeddable Lisp interpreter in Ada, designed for portability and suitable for both native and embedded systems, showcasing Ada’s flexibility.
BBT
BBT is a command-line tool that turns plain-English behaviour specs into automated tests, making it simple to verify command-line tool functionality.
Elogs
Elogs is a SPARK-based logging library, proven memory-safe, portable, and configurable for resource-constrained, high-integrity applications.
AdaBots
AdaBots makes coding fun for children by letting them control robots in a Minecraft-like world, fostering creativity and computational thinking through play.
HiRTOS
HiRTOS is a SPARK Ada RTOS and separation kernel with a minimal runtime, offering a complete, platform-agnostic solution for embedded developers.
SPARKNaCl
SPARKNaCl reimplements TweetNaCl in SPARK, proving high-assurance code can be performant, efficient, versatile, and deployable across diverse platforms.
Rejuvenation-Ada
Rejuvenation automates Ada project maintenance with pattern-based refactoring, offering Ada-like syntax for clear, customisable code transformations.
AVR-Ada
AVR-Ada brings Ada to AVR microcontrollers via Alire, offering configurable crates, runtime support, and peripheral access for 94 devices.
libkeccak
SPARK’s formal verification, shown in Daniel King’s libkeccak project, prevents vulnerabilities missed for years by traditional validation methods.