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
--servefor 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 likegnatprove. 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
alireitself 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
LLM Usage Disclosure
As you can probably tell, the code is AI assisted. More about it in the docs:
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
Docs
Changelogs
- adacovex 1.40.0 - adacovex latest documentation
- 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/adacovex-code-proof-do-178c-hal-docstring-status-tool/4600
