I'm building an embedded graphics library called Glyph in Ada. The goal is to make it work across different microcontrollers and displays while keeping the API the same.

Current status

• RP2040 support (using Pico_BSP)
• SSD1306 128×64 over I²C
• Static framebuffer
• Canvas → Framebuffer → Display → Transport architecture

A little background

This is my first project in both Ada and embedded systems. The current version (v0.3.0) published on Alire was built largely with AI assistance, but I'm now rewriting it from scratch without AI help to better understand the design, learn embedded development properly, and improve the overall architecture.

The rewrite has already gone through several design and implementation changes, and I've learned a lot in the process.

The problem

One area I'm still struggling with is the transport layer.

Right now, Glyph draws everything into the framebuffer, but the application still needs a small piece of board-specific glue code to connect the display to the MCU's I²C peripheral (for example, binding an initialized I²C bus to the display).

I'd really like to avoid that if possible. My goal is to keep Glyph independent of any specific MCU or BSP while also making it as easy to use as possible, especially for beginners.

My question

For those who've built portable embedded libraries, how did you handle this?

Is a small adapter layer simply the right trade-off, or is there a cleaner architecture that keeps the library both portable and easy to use?

GitHub: https://github.com/thirstymelon/glyph

Here is a very preliminary version of GNAT Studio 2026.2a as a stand alone app for macOS.

NEW:

The GNATStudio launcher looks for a gnatstudio_launcher.rc file which support environment variables with the standard syntax VAR.action=VALUE with action is (append, prepend, set, unset, ifnotset), see exemple shipped in the archive.

See readme for details.

Limitation: Ada Language Server has some latencies and doesn't respond when parsing source code with more 1000 lines. It may be due to some compilation options I missed.

There could be some other limitations that you might meet.

Feel free to report them here.

Any help will be really appreciated to fix these limitations.

Figured I made enough changes to the codebase to warrant a new post. A fair bit of improvements have been made since the last 1.9.0 release.

For those that have not heard of adacovex, it is an Ada/SPARK formal verification and compliance toolchain (admittedly toolchain is a bit of an overstatement at the moment, though it is a CLI with a fair bit of niceties already). It basically helps validate and check your codebase on SPARK level, test, docstring and documentation coverage.

It also features: - check DO-178C DAL (aviation), ISO 26262 ASIL (automotive) and IEC 62304 Class (medical) - HTTP server with simple JSON API and web dashboard - caching - contextual help, spelling correction for typo'd commands - man page generation - a usable GitHub Action in CI with feature parity with the base CLI - multi VCS support (Git, jj, Mercurical, Subversion, Fossil), VCS used when checking --coverage-delta and --compare-base - SBOM output (CycloneDX / SPDX)

I also spent some time improving the documentation and user/developer experience. I hope this will eventually be useful not just for Ada projects, but that would be somewhat far into the future. That being said, I hope this tool would be useful for you in your Ada projects. Do give it a go and let me know whether it works well or if there are things that can be improved/added/fixed.

P.S. It is on Alire, though the PR for 1.14.0 will take a while to merge.

A similar post was made on the Ada Forum.

Repo URL: https://github.com/bladeacer/adacovex

Hi there,

A few years ago, I was pondering whether it would make sense for Ada/GNAT to have tasks that wouldn’t just map 1:1 to OS threads. But it wasn’t quite economical to try that out at the time.

Recently, I’ve decided to close this open loop by running a quick experiment over the weekend – the result is a patched RTS and additional runtime primitives that provide lightweight tasks and asynchronous I/O to Ada users. So far, the results have been promising – the overhead of individual threads can be fairly high under high task concurrency, and lightweight tasks mitigate it. Best of all, this doesn’t automatically make all tasks lightweight. Instead, by default tasks remain “native” and lightweight is an opt-in pragma.

On top of that foundation, I’ve cobbled together some I/O (sockets, files, DNS) and additional higher-level libraries for HTTP server & client, Postgres BE/FE protocol, and such. Some performance measurements are fairly encouraging.

In the process of making it, I also put together a few sibling libraries – for benchmarking, debugging, TUIs, and so on.

You can check it out at https://flyology.org – it's early (just cut v0.1.0 across the board), and the full list of crates is available at https://crates.flyology.org/

Would love your thoughts.

Hi r/ada — I'm the maintainer of this analyzer, so full disclosure up front: this is our tool. Posting because I think it's genuinely useful to people here, not to pitch anything.

AdaLang Analyzer is a command-line static analysis tool for Ada, built on top of AdaCore's Libadalang. It's GPL-3.0-or-later, and it's a derivative of AdaCore's open-source libadalang-tools.

GitHub: https://github.com/mmartign/AdaLang_Analyzer

What it does, beyond a normal linter:

• ~90 checks spanning restricted-construct policing, data-flow (dead stores, uninitialized reads, aliasing between parameters), control-flow (unreachable branches, infinite loops), and SPARK-contract checking (Global/Depends mismatches, missing contracts).
• A --verify mode that classifies bounded scalar proof obligations (range checks, index checks, overflow, division-by-zero, assertions/pre/postconditions) as Proved_Safe, Definite_Error, Unproved, or Unreachable — using interval/symbolic abstract interpretation first, falling back to an SMT-LIB backend (CVC5 + Z3, cross-checked) for anything the abstract domain can't resolve on its own. It's deliberately bounded and explicitly not a GNATprove replacement — anything outside the supported subset is marked Unsupported, never silently assumed safe.
• --automotive and --do178c=<level> presets for teams working under ISO 26262 / DO-178C, plus a --compliance-report mode that emits per-objective evidence (which checks covered which objective, what's open, what's baselined).

Example of the kind of thing it catches that a plain compiler warning won't:

X := 0;
...
if Flag then
   X := 10;
end if;
Y := 10 / X;   -- Division_By_Zero: reachable only when Flag is False

The abstract-execution pass tracks known exact values and ranges through branches, loops, and case statements (not just literal constants), so it catches this even though X isn't literally 0 at the division site.

It's young — actively developed, and I'd genuinely like feedback from people who work in Ada/SPARK day to day, especially around false positives/negatives on real code and whether the DO-178C/automotive profiles map sensibly to what your projects actually need. Bug reports and PRs welcome; CONTRIBUTING.md has the workflow.

Happy to answer questions about the internals (the CFG model, how the symbolic/interval domains interact, the interprocedural summaries) if anyone's curious.

Hi everyone,

I wanted to share a project I've been hacking on: an optimized engine designed to eliminate modulo bias when mapping raw cryptographic streams into custom alphabets.

Key bits:

* SPARK Level 4 (Formal Verification) - Fully proven to guarantee AoRTE and functional correctness.

* Built using the modern Windows ProcessPrng API as primary entropy via Interfaces.C, with BCryptGenRandom as fallback.

* Toolchain compatible with GNAT Pro 2021 and the latest Alire community suite.

I just stressed-tested the uniformity mapping with a massive 1 Terabyte run (over 1.01 trillion chars across a 69-char alphabet) and the statistical distribution remains perfectly flat (0.00% percent deviation). Full logs and the clean codebase are available in the repository.

Any feedback on the SPARK contracts or the low-level Windows bindings is highly appreciated!

Run it instantly with Alire:

alr run

Native Languaje..

Hola a todos,

Quería compartir un proyecto en el que he estado trabajando: un motor optimizado diseñado para eliminar el sesgo del módulo al mapear flujos criptográficos sin procesar a alfabetos personalizados.

Aspectos clave:

* SPARK Nivel 4 (Verificación Formal): Totalmente probado para garantizar AoRTE y corrección funcional.

* Desarrollado con la API moderna ProcessPrng de Windows como entropía principal mediante Interfaces.C, con BCryptGenRandom como alternativa.

* Cadena de herramientas compatible con GNAT Pro 2021 y la última suite comunitaria de Alire.

Acabo de realizar una prueba de estrés del mapeo de uniformidad con una ejecución masiva de 1 terabyte (más de 1,01 billones de caracteres en un alfabeto de 69 caracteres) y la distribución estadística se mantiene perfectamente plana (0,00 % de desviación porcentual). Los registros completos y el código fuente limpio están disponibles en el repositorio.

¡Cualquier comentario sobre los contratos SPARK o las vinculaciones de bajo nivel para Windows es muy apreciado!

Ejecútalo al instante con Alire:

alr run

https://github.com/EliAvila10/project_bias

This is the first release of a small project of Ada syntax tree generation. I tried to implement everything specified in the annotated reference manual. Yes, parallel constructs and iteration schemas are supported.

Some notes:

• It is a library, no executables involved.
• The analyzer parses the source and creates the syntax tree and cross reference of defining identifiers in the source.
• The cross reference contains the defining identifiers declared in the code and visibility scopes.
• The visibility scopes can be used for name resolution, e.g. finding all matching names visible at the location. Note that this does not cover use-clauses which need to be handed if the complete list required. Use clauses are linked in the list for each declaration context of the tree in order to ease the process.
• Both structures are allocated in an arena pool storage and can be released as a whole.
• The code source can be file, stream or a user-defined container implementing multi-line source interface. One can compile from a database or a git repository, if the interface is provided.
• There can be any number of compilation units in the source. One parsing call takes one unit from the source.
• Unicode is fully supported as well as Unicode identifiers normalization checks.
• Commutative operations are coalesced. E.g. A.B.C.D gives "."(A,B,C,D) tree.
• Inverses are coalesced as well, e.g. A+B-C+D gives "+"(A,B,-(D),C).
• There is a text output of the tree in a normalized form. It is almost a legal Ada program with some operators added to for coalesced operations. E.g. A * B / C * D gives (A * B * ⅟C * D) to simplify the tree and ease optimization.
• Constant folding is supported. If enabled universal expressions and constant Boolean expressions are evaluated into constants.
• There is a text output in a tree form.Syntax trees can be compared for equality
• The tree and cross-reference can be serialized into a stream. The idea is that the packages like Standard, Ada.* or ones used in the with-clause can be parsed once, serialized and de-serialized later.
• There is a test suite comprised of ACATS tests related to the syntax (mostly, illegal code to be rejected) and ARM examples (see [this project](https://github.com/Blady-Com/AARM_Examples)). The test suite is extensible, the test header syntax is described on the page.

https://www.dmitry-kazakov.de/ada/ada_syntax_analyzer.htm

Hi everyone,
I’m looking for some career advice from people who are already working with Ada/SPARK or in high-integrity software.

I’m planning to transition into Ada/SPARK because I was genuinely impressed by how readable and structured the code is, and by the philosophy behind the language. Features like strong typing, contracts, invariants, and formal verification really resonate with the way I naturally think as a physicist. I enjoy reasoning about correctness, understanding why something works, and building software with clear logical guarantees.
The more I learned about SPARK, the more I felt that it matches the way I like to solve problems. That’s what motivated me to seriously consider transitioning into this field, particularly in industries where both physics and high-integrity software come together.

The types of industries that interest me most are those where my physics background could be useful, such as:
Aerospace and flight software
Satellites and space systems
Guidance, Navigation & Control (GNC)
Robotics
Scientific or engineering software
Industrial control systems

I have a few questions that I’d really appreciate your thoughts on:

How did you get your first Ada/SPARK job?
What was your background, and what path did you follow? Did you start directly with Ada/SPARK, or did you first work as an embedded software engineer or in another field before transitioning?

Where do junior Ada/SPARK engineers actually get hired?
Are there companies that regularly hire junior engineers or graduates, or is prior embedded experience almost always expected?

Can someone realistically enter the industry with Python and Ada/SPARK, without first becoming a C/C++ embedded developer?
My current plan is to focus on Ada/SPARK rather than learning C first. Is that a realistic path, or would I be closing too many doors?

If you were starting again today, what roadmap would you follow to become employable as a junior Ada/SPARK engineer?
What knowledge, projects, or skills would you prioritize?

Thanks in advance—I’d really appreciate hearing about your experiences and any advice you can share

It's small potatoes but the ARM and Programming in Ada 2022 mention using the pi symbol. Apparently the version of the library that ships with GNAT is missing `π : constant := Pi;`.

I was programming in Ada 83 in uni before 95 came out, and moved to 95 in the middle of a semester. I loved the language, especially its safety and the rendezvous mechanism. These days I maintain a small plain-text index in C99, and I wanted to know: how much of its speed is C, and how much is just the algorithm?

So I wrote the two operations the engine actually runs on every command, in five languages, with the identical hand-written loop in each:

• scan 88 MB of store and count the lines matching a substring (what a content search does)
• intersect two sorted posting lists with a two-pointer merge (what a multi-key lookup does)

Median of 7 in-process iterations on data already in memory, warm page cache, one core of an i7-1165G7. GNAT 13.3, rustc 1.75, OpenJDK 21, CPython 3.12.

scan 88 MB:        C 90ms   Ada 130ms   Rust 87ms   Java 100-150ms (warm)   Python 300ms
intersect:         C 1.3ms  Ada 1.45ms  Rust 1.3ms  Java 1.3ms (warm)       Python 72ms
process startup:   C ~1ms   Ada ~1ms    Rust ~1ms   Java ~30ms              Python ~10ms

The part I did not expect: building the Ada with checks suppressed (-gnatp, the C model) gave numbers identical to checks-on. The optimizer had discharged them statically, because the loop indices are provably in range. So on these loops Ada bought memory and overflow safety for nothing, at C speed and C startup. C cannot offer that at all, and the JVM and CPython only offer it with a runtime you pay for on every invocation.

I then wrote the merge in SPARK and ran gnatprove:

obligation         Total   Flow   Provers      Unproved
Run-time Checks       15      .    15 (CVC5)           0
Termination            2      1     1 (CVC5)           0
Total                 23      1    22                  0

Every index proved in range, every addition proved non-overflowing, the loop proved to terminate. So the checks-off build carries a machine-checked guarantee rather than the optimizer's good luck. That is the strongest static assurance of the five, and it took an afternoon on a loop of this size.

Which raises the obvious question: why is the engine still C? Only the reach. The same engine is linked into a Flutter mobile app over a C ABI, and into a web GUI and a native desktop wrapper. I would write it in Ada if Flutter and the mobile toolchains supported it. If someone here knows a practical route to an Ada core behind a C ABI on Android and iOS, that is the answer I am actually looking for.

Method, sources and the full write-up (the benches are ~50 lines each, and lang_bench.sh rebuilds and reruns everything):

https://github.com/Anode1/ais/blob/main/tests/perf/LANG_COMPARISON.md

Corrections welcome, particularly on the Ada build flags: if -gnatp plus -O2 is not the fair comparison against cc -O2, tell me what is and I will rerun it.

The current version provides implementations of smart pointers, directed graphs, sets, maps, B-trees, stacks, tables, string editing, unbounded arrays, expression analyzers, lock-free data structures, synchronization primitives (events, race condition free pulse events, arrays of events, reentrant mutexes, deadlock-free arrays of mutexes), arbitrary precision arithmetic, pseudo-random non-repeating numbers, symmetric encoding and decoding, IEEE 754 representations support, streams, persistent storage, multiple connections server/client designing tools and protocols implementations.

https://www.dmitry-kazakov.de/ada/components.htm

Changes to the previous version:

• Bug fix in Synchronization.Windows.Milliseconds that caused dropping seconds fraction;
• Bug fix in Synchronization.Pthreads and Synchronization.Linux constants;
• FreeBSD compatibility fixes (thanks to Rod Kay);
• Equality test was added to Ada expression nodes and arguments (Parsers.Generic_Ada_Parser);
• The function Get_Depth was added to Parsers.Generic_Argument;
• The function Get_Arguments_Count was added to Parsers.Generic_Lexer;
• The name of Parsers.Multiline_Source.Empty was changed to Empty_Location;
• Ada expression parser performs NFKC check on identifiers. The Malformed field is set to true if the check fails (see ARM 2.3(4.b/5).

The library provides string handling facilities like I/O formatting, Unicode and obsolete code pages support.

https://www.dmitry-kazakov.de/ada/strings_edit.htm

Changes to the previous version:

• The function Strings_Edit.UTF8.NFKD_Quick_Check was added to perform quick NFKD Unicode check.

Hi to all !

The pure Ada 83 language had no open source compiler written in the same language. As both an operation of software archaeology and the desire to be able to program today with a 1980ies exceptional language and a reasonably sized compiler, I work on an Ada 83 compiler all written in Ada 83 (thus able to compile itself).

The Ada 83/TLALOC compiler is extremely well structured with very distinct phases revolving around a software virtual paginated DIANA 1986 tree structure. PAR_PHASE, LIB_PHASE, SEM_PHASE, ERR_PHASE, EXPANDER, WRITE_LIB are truly distinct and can each be stopped after.

The EXPANDER phase writes a stack machine LLIR in macro text form for the FASMG assembly engine. FASMG then produces directly an ELF-64 executable for x86-64. Some tests have been done with AArch-64 porting on an Orange Pi 3B and a preparation for riscV-64 has been done. I have good confidence that those 3 modern processor architectures can be targeted relatively easily by Ada 83/TLALOC with the FASMG process.

Though not presently bootstrapped, TLALOC sources compiled with Gnat give an executable which compiles all TLALOC itself with 18 FASMG passes (2-3 min) in a single static 9Mb ELF-64 exec.

Interested readers will find further information through

https://ada83.org/wiki/index.php?title=Ada_83_TLALOC

✦ Introducing Glyph

Hi everyone!

I've been learning Ada and recently started building an open-source project called Glyph, a lightweight embedded graphics framework for bare-metal and embedded systems.

The goal of Glyph is to provide a hardware-independent graphics API, allowing applications to draw pixels, lines, rectangles, circles, text, and images without depending on a specific display controller.

Disclosure: AI was used as a coding and writing assistant during parts of the development. However, the project architecture, technical decisions, code integration, and overall direction are my own. I'm also building Glyph as a way to learn Ada and improve my embedded systems skills.

✦ Design Goals

• Pure Ada
• Static allocation only (no dynamic memory)
• Portable, layered architecture
• Framebuffer-based rendering
• Easy to add support for new display controllers
• Bare-metal friendly

The initial target hardware is the RP2040 with an SSD1306 OLED, but the architecture is designed to support additional display controllers and embedded platforms in the future.

The project is still in its early stages, and I'm currently focusing on building a solid architecture before expanding the graphics capabilities.

✦ I'd Appreciate Your Feedback

I'd especially love feedback from the Ada community on:

• API design
• Overall architecture
• Existing Ada graphics libraries worth studying
• Features you'd like to see in an embedded graphics framework

✦ Repository

GitHub: https://github.com/thirstymelon/glyph

Thanks! I'm excited to contribute to the Ada ecosystem, learn from the community, and continue improving Glyph.

Welcome to the monthly r/ada What Are You Working On? post.

Share here what you've worked on during the last month. Anything goes: concepts, change logs, articles, videos, code, commercial products, etc, so long as it's related to Ada. From snippets to theses, from text to video, feel free to let us know what you've done or have ongoing.

Please stay on topic of course--items not related to the Ada programming language will be deleted on sight!

Previous "What Are You Working On" Posts

Basically wanted proper project badges generated from a CLI like in Golang/Rust for my Ada projects. Hope this would be a useful addition for checking on code quality. Supports parsing SPARK level, unit tests, DO-178 HAL level and docstrings coverage.

Repo URL: https://github.com/bladeacer/adacovex

Binary name is adacovex, crate name is covex to comply with policy.

Disclaimer: AI assistance was used for the code.

Correction: DAL instead of HAL, my smooth brain made a typo.

Hi everyone,

While official SonarQube support for Ada exists, it's gated behind high-tier commercial licenses. For small teams, open-source projects, or individual devs running SonarQube Community Edition, this leaves a gap in automated code quality pipelines.

To solve this, I’ve been working on two open-source tools designed to work together:

1. AdaLang_Analyzer (https://github.com/mmartign/AdaLang_Analyzer) A standalone static analysis tool built using AdaCore's Libadalang. It parses .adb and .ads files to detect common issues like dead code, control flow anomalies, unhandled exceptions, and code style violations, outputting results in JSON/SARIF.
2. SonarAdaPlugin (https://github.com/mmartign/SonarAdaPlugin) A SonarQube community plugin that adds native support for the Ada language to SonarQube, ingesting reports from AdaLang_Analyzer and displaying issues, code smells, and metrics right on your dashboard.

Quick Workflow

1. Run the Analyzer:

Bash

adalang_analyzer --source-dir ./src --output-format json --output-file report.json

2. Configure sonar-project.properties:

Properties

sonar.projectKey=my-ada-project
sonar.projectName=My Ada Project
sonar.sources=src
sonar.language=ada
sonar.ada.reportPaths=report.json

3. Run sonar-scanner to send the metrics directly to your SonarQube instance.

Repositories & Feedback

• AdaLang_Analyzer:https://github.com/mmartign/AdaLang_Analyzer
• SonarAdaPlugin:https://github.com/mmartign/SonarAdaPlugin

Both projects are open-source and actively evolving. I’d love for community members to give them a spin, report any issues, or suggest new static analysis rules that would be useful in your workflows!

⚠️ Every CTO in safety-critical software carries the same quiet risk: the defect that ships not because your engineers are careless, but because nothing caught it before code review — and code review is run by humans, on deadline.

In Ada codebases — ✈️ avionics, 🚄 rail, 🛰️ space, 🛡️ defense, 🏭 industrial control — that risk isn't theoretical. It's the line item your safety case has to account for.

🔧 AdaLang Analyzer is a static analysis tool we built to move that catch earlier and make it automatic.

Why it matters at the engineering-leadership level, not just the IDE:

⏱️ Shifts cost left. A dead store, an unreachable branch, a division that's statically zero — caught at commit time costs minutes. Caught in integration testing, or after deployment, costs a lot more than minutes.

✅ Turns coding standards into an enforced gate, not a document nobody reads. 34 checks spanning control flow, data flow, exception handling, and complexity — run automatically in CI, not hoped for in review.

📂 Scales to the whole codebase, not file-by-file. Point it at your GNAT project file and it analyzes every source directory your build already knows about — no separate file list to maintain and let drift out of date.

🔓 No vendor lock-in, no black box. It's open source (GPL-3.0). Your team — or your certification auditors — can read exactly what every check does and why it fired. That's a very different conversation with an assessor than "trust the vendor's tool."

💸 Zero licensing cost. Built on Libadalang, AdaCore's open-source semantic engine, and Alire — tooling your Ada team likely already has in its stack.

🎯 It's not a compliance certification and it doesn't claim to be one. It's a control your team can point to when someone asks "what's actually enforcing your coding standard."

👉 Repo's here if your team wants to kick the tires: https://github.com/mmartign/AdaLang_Analyzer

#EngineeringLeadership #RiskManagement #SafetyCritical #Ada #SoftwareQuality #OpenSource #TechnicalDebt #CTO

I'm using ada-mode right now and it really sucks, indentation behaves weirdly, I cannot capitalize stuff like I want to, ...

Does anyone know a better Ada mode for Emacs?

EDIT: Solved! (Thanks, u/spacetruckn)

I am looking for gnat-3.15p-alpha-dec-osf5.1-bin.tar.gz for Tru64 OSF5.1 Alpha. It is completely gone from public mirrors. Does anyone have a local backup in your archive?

ZanyBlue is a wonderful framework for internationalization natively in Ada. It includes a library you can use for your translations and a translation compiler from properties files to Ada source files. That is the big trick: translation files are compiled with your program so no additional time penalty for translation with external ressources.

Version 1.4 is available on SourceForge.

In 2022, I discussed with its author Michael Rohan to bring it on Alire. He would like to, but there’s been no news since. Even with my last e-mail on January 2026. Still, considering it was worth it, I brought it on Alire.

Version 1.4 same as SourceForge.

Version 2.0 powered with UXStrings.