# \[ANN\]: adacovex 1.40.0: Full fledged documentation site and other niceties
**URL:** https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701
**Category:** Releases
**Tags:** spark, ada, alire
**Created:** [August 31, 2026, 1:38pm UTC](https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701 "2026-08-31T13:38:46Z")
**Posts on this page:** 4
**Page:** 1
### Author:  [@bladeacer](https://forum.ada-lang.io/u/bladeacer)
#### Post date: [August 31, 2026, 1:38pm UTC](https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701/1 "2026-08-31T13:38:46Z")
### Project status
So the last time I posted about the tool, it was still rough around the edges in some aspects. Admittedly there are still things I want to fix, though the recent changes up to the current version. Took my time to implement changes before making this topic.
### About
tldr; fancy descriptor is “Ada/SPARK formal verification and compliance toolchain”. Though in short, adacovex wraps plenty of things together so that you have:
- Interface with gnatprove for formal verification (gnatprove call resolved at runtime, not bundled), get proof metrics, reliability and hopefully better developer experience
- [shields.io](http://shields.io) style badges you can display on SPARK level, test count, DO-178C/ISO-26262/IEC-62304 status, docstring and proof coverage
- Output CycloneDX or SPDX JSON (detects system, dev, test deps etc. Language specific support has a decent way to go but there are some better supported ones for a start)
- Web Dashboard + REST (outputs JSON) API (Overview, Proof, Tests, Compliance, Dependencies, Charts, API playground)
- Bundled documentation in the binary so you can read the friendly manual offline (exposed alongside `--serve` for dashboard under `/docs/` endpoint
- VCS support and differential analysis (PR checks, release gating on e.g. test count)
- Oh and you can write patches so you can formally verify your vendored Ada deps.
- Result caching (so it does not take 40s and 10 CPU cores even when you run gnatprove again on the same unchanged code)
- Code complexity checking
- A functional GitHub Action so you can run adacovex in CI with (almost where it makes sense) feature parity with the base CLI
- You can `alr install adacovex`, though the latest 1.40.0 PR is not merged yet.
### Dashboard Screenshots
### Architectural decisions
Some architectural decisions I stick to
- Pure-stdlib Ada source code wise (in base `alire.toml`, though there are dev dependencies which are resolved like `gnatprove`. A Python script is also used to bundle the HTML pages in a compressed manner into the Ada code itself. I will be working towards better ways to compress the dashboard and docs because I believe their additions do add a fair bit to the binary size at the end.
- This has the added benefit of letting us support any platform `alire` itself does.
- We vendor deps where necessary, like for the dashboard (FlexSearch, yace etc)
- Unix philosophy of
- being relatively single purpose
- plain text I/O
- composable tooling
- sane exit codes
- minimal docstring writing so you do not have to refactor your code just to use adacovex on you existing project
More about architectural decisions in the docs: [adacovex Architecture Decisions - adacovex latest documentation](https://adacovex.readthedocs.io/en/latest/contributing/architecture.html)
### LLM Usage Disclosure
As you can probably tell, the code is AI assisted. More about it in the docs:
> **[AI / LLM Usage in this Project - adacovex latest documentation](https://adacovex.readthedocs.io/en/latest/contributing/llm-usage.html)**
### Conclusion
Hope that this would be useful for your Ada projects, especially for those who would like some better developer experience in trying to achieve DO-178C compliance or just need to have some tooling over base gnatprove. Do give it a try and let me know if any issues or bugs occur by opening a GitHub Issue. Cheers, bladeacer.
> P.S. will be taking a break from dev for a week or two
## Links
### GitHub Repository
- [GitHub - bladeacer/adacovex: Ada/SPARK formal verification and compliance toolchain. · GitHub](https://github.com/bladeacer/adacovex)
### Docs
- [adacovex latest documentation](https://adacovex.readthedocs.io/en/latest/index.html)
### Changelogs
- [adacovex 1.40.0 - adacovex latest documentation](https://adacovex.readthedocs.io/en/latest/changelogs/adacovex-1.40.0.html)
- Well there are other changelogs all the way since I started working on the code but I will omit here for brevity, you can check out the changelogs in the docs directly if interested.
### Previous Posts on the tool
[https://forum.ada-lang.io/t/ann-adacovex-1-14-0-multiple-compliance-standards-plenty-of-qol-updates/464](https://forum.ada-lang.io/t/ann-adacovex-1-14-0-multiple-compliance-standards-plenty-of-qol-updates/464)4
[https://forum.ada-lang.io/t/adacovex-code-proof-do-178c-hal-docstring-status-tool/4600](https://forum.ada-lang.io/t/adacovex-code-proof-do-178c-hal-docstring-status-tool/4600)
---
### Author:  [@bladeacer](https://forum.ada-lang.io/u/bladeacer)
#### Post date: [September 2, 2026, 12:34pm UTC](https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701/2 "2026-09-02T12:34:20Z")
adacovex 1.40.0 is up on Alire 😃
---
### Author:  [@bladeacer](https://forum.ada-lang.io/u/bladeacer)
#### Post date: [September 3, 2026, 2:14pm UTC](https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701/3 "2026-09-03T14:14:51Z")
There are some performance improvements I am working on which should make proving much quicker in future updates. So far I am seeing promising results.
---
### Author:  [@bladeacer](https://forum.ada-lang.io/u/bladeacer)
#### Post date: [September 13, 2026, 2:05pm UTC](https://forum.ada-lang.io/t/ann-adacovex-1-40-0-full-fledged-documentation-site-and-other-niceties/4701/4 "2026-09-13T14:05:35Z")
Fingers crossed here, I aim to send the next PR submission to Alire over the next few days.
If you would like to look into the performance improvements thus far in details:
> **[Performance - adacovex latest documentation](https://adacovex.readthedocs.io/en/latest/contributing/perf.html)**
Docs and GitHub Releases latest version is v1.45.0, though I will only create the `alr publish` PR after I implement 1.48.0 (whole bunch of added flags and sensible CLI shorthands).