### 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 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, the latest 1.40.0 PR is not merged yet.

### 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: 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:

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. I am more active on the Ada forum, I tend to post updates to the project there more often.

## Links

### GitHub Repository

https://github.com/bladeacer/adacovex

### Docs

https://adacovex.readthedocs.io/en/latest/index.html

### Changelogs

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.

[ANN]: adacovex 1.40.0: Full fledged documentation site and other niceties