Adacovex: code/proof/DO-178C HAL/docstring status tool

bladeacer · July 30, 2026, 1:09pm

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: GitHub - bladeacer/adacovex: Ada/SPARK code/proof coverage, SPARK level, DO-178C HAL status tool · GitHub

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

Disclaimer: AI assistance was used for the code.

Awaiting PR merge to Alire, would publish the newer upstream code changes at a later time.

dragon-spirit-wtp · July 30, 2026, 4:03pm

I am currently on a project that has to do DO-178 certification, but sadly it’s all in C. While this tool would not benefit my current project, I can appreciate what it provides.

Thanks for your contribution to the community!

bladeacer · July 30, 2026, 9:35pm

Thanks for your kind words ^_^.

I plan to perhaps add language agnostic support in the long run (Ada has a great way to exposing FFIs to C) as well as some way to check deltas on code coverage on pull requests.

The 1.0.0 PR to Alire has been merged, now I will wait till it shows up on the site and continue with dev.

ThyMYthOS · July 31, 2026, 8:39pm

Is it DO-178 HAL or DO-178 DAL? Your screenshot and link don’t match on this.

bladeacer · July 31, 2026, 10:40pm

DAL, my bad.

Must have made a typo somewhere, thanks for catching it.

bladeacer · July 31, 2026, 10:54pm

Released 1.1.0 with some fixes made, awaiting PR merge to Alire.

Changelogs:

github.com/bladeacer/adacovex

docs/changelogs/adacovex-1.1.0.md

6126238dc

# adacovex 1.1.0

Date: _2026-07-30_

## Fixes

### H1: Generic keyword bounds not matching single-line declarations

`Is_Subprogram_Decl` in `adacovex-parsers-source.adb` had off-by-one bounds:
`"genericprocedure"` (16 chars) was compared against a 15-char slice, and
`"genericfunction"` (15 chars) against a 14-char slice. Since Ada string
equality requires matching lengths, both branches never fired, meaning
`generic procedure Reset;` on a single line was invisible to the scanner.

**Impact:** Single-line generic subprograms were silently excluded from
coverage tracking, docstring requirements, and subprogram counts.

**Fix:** Bounds corrected to `>= 16` and `>= 15`.

### H2: `Determine_SPARK_Level` returning Gold for missing proof data

This file has been truncated. show original

bladeacer · August 2, 2026, 7:47am

Got adacovex to run on GitHub CI though it is about time gnatprove is listed as an explicit dependency. Needs more polish but once the update is out one can check code coverage changes between each PR or on push. I plan to publish a companion GitHub Action as well as push 1.3.0 to Alire if things go well.

bladeacer · August 3, 2026, 1:50pm

1.3.0 is out. I plan to polish github actions UX, add a SBOM flag and “bundle” gnatprove itself so it can be easily invoked alongside the binary (using alr).

bladeacer · August 5, 2026, 10:46am

1.5.0 is out. Realised I never published the draft release for 1.3.0.

Changelogs

github.com/bladeacer/adacovex

docs/changelogs/adacovex-1.5.0.md

03e35c247

# adacovex 1.5.0

Date: _2026-08-05_

Version bumped 1.4.0 -> 1.5.0.

## Changes

### C1: More standard docstring styles

The source scanner now recognizes additional standard docstring conventions,
so third-party and code-generated Ada is counted correctly:

- Comment prefixes: besides the canonical `--  ` (two dashes + two spaces),
  the single-space `-- ` and tab-separated (`--<TAB>`) styles are recognized
  as docstrings. A bare `--` or `---` divider is still not a docstring.
- Tag aliases: `@parameter` == `@param`, `@returns` == `@return`.
- Summary tags: `@brief` and `@summary` mark a subprogram as documented.

### C2: More test-result formats

This file has been truncated. show original

bladeacer · August 6, 2026, 12:41pm

Removed some of the PRs to alire-index since I realised I should not bundle gnatprove as a dep in alire.toml.

bladeacer · August 7, 2026, 1:59pm

1.6.0 is out, forgot to mention that we now have a working GitHub Action to run adacovex in CI or on PRs. There are also some other internal refinements.

As usual, PR to Alire will take a while.

Changelogs

github.com/bladeacer/adacovex

docs/changelogs/adacovex-1.6.0.md

21eb6a52b

# adacovex 1.6.0

Date: _2026-08-05_

Version bumped 1.5.0 -> 1.6.0.

## Changes

### C1: Full SPARK proof coverage (Platinum, 0 unproved)

The whole SPARK-on codebase is now fully machine-proved. Previously only the
bounded IR types (`Checked_Add32/64`, `IR_Bounds.Add32/64`) carried complete
proofs; every other SPARK unit was analyzed but not fully discharged. Now
**all 491 VCs prove** with `--prover=z3 --timeout=20`, including the run-time
range checks, assertions, functional contracts, and loop termination:

- **Renderers**: `I2S` (fixed `10**Pos` overflow by replacing exponentiation
  with a constant `Pow10` power table, loop invariants carrying the digit
  count and value bound, `Buf` initialized), `Pad2` and `Escape_JSON`
  (uninitialized-buffer fixes via `(others => ' ')`), and `ISO_From_Epoch`

This file has been truncated. show original

Build Provenance Attestation:

P.S. I have some plans for 2.0 though there needs to be fair bit more polish on the UX side of things.

bladeacer · August 8, 2026, 11:44am

Forgot to summarise the set of changes, mainly:

It does not false positive on third party/deps being SPARK proven
The badges now have better text to background contrast (e.g. no more bright background + bright text)
Codebase is fully proved now
Updated installation docs
Shown how to tie SBOM timestamp to git commit so to version control it is deterministic
Some other changes to the GitHub Actions set up

P.S. If the project goes well and language agnostic support is done properly for 2.0 I would be interested in submitting a proposal to present about the project at FOSDEM or similar events that are programming/Ada related.

The code is “decent” but not crate of the year quality yet. I will continue working on it.

bladeacer · August 10, 2026, 4:00am

So I have started dogfooding in some sense, my Ada_CRDT project now makes use of adacovex itself. This is probably a good way to find out and address any possible gaps in DX/UX going forward.

I am considering making a Matrix Room once there is demand for it (enough users). If there are any bugs or quirks, do open an issue or better yet a PR at the GitHub.