adacovex

A zero-dependency Ada/SPARK command line tool for coverage analysis, proof verification, test-result parsing, multi-standard safety-compliance assessment (DO-178C / ISO 26262 / IEC 62304), and interactive dashboards. It uses only the GNAT runtime. The prove subcommand resolves gnatprove at run time, so installing adacovex installs only the binary.

Badges

The badges above reflect adacovex's self-assessment: SPARK proof level, test pass count, and DO-178C / ISO 26262 / IEC 62304 compliance tiers. Click any badge for the badge set, meanings, and regeneration guide in the docs.

Features

• Source scanning -- walks .ads files; extracts subprogram declarations, docstring annotations (Ada @param/@return/@field/@formal/@brief/@summary, Google Args:/Returns:, Sphinx :param:/:returns:), and HLR traceability tags.
• Proof analysis -- parses GNATprove gnatprove.out summaries; assesses SPARK assurance levels (Stone to Platinum).
• Test parsing -- reads test-result summaries from CI or runner logs: Markdown tables (the native test_runner format, with or without an index column), TAP (ok/not ok), GNU Automake (PASS:/FAIL:), Maven Surefire (Tests run: N), Unity (N Tests), and AUnit reports.
• Compliance -- assesses DO-178C DAL A-E criteria (HLR coverage, orphan tags, test status, minimum SPARK proof level), re-labelled for ISO 26262 (ASIL A to D / QM) and IEC 62304 (Class A to C) with dedicated --dal / --asil / --class flags.
• Multiple outputs -- ANSI report, SVG badges, Markdown reports, web dashboard + JSON API, and proof-aware SBOM (CycloneDX / SPDX).
• Differential assessment -- --compare-base / --coverage-delta snapshot a base revision on git, Mercurial, Subversion, Fossil, or jj without touching the working tree.
• Result caching -- a content-addressed on-disk cache (~/.adacovex/cache) serves unchanged scan, proof, test, HLR/LLR, and dependency-graph results.
• Tooling -- status reports toolchain and VCS state, man installs a local man page, and make check runs the full quality gate in one command.
• Scalable -- package and subprogram collections use Ada.Containers.Vectors (no compile-time count limits); fixed-size buffers scale with host word size.

Quick start

# Install (pick one)
alr install covex gnatprove       # Alire: binary on ~/.local/bin
# or the release bundle:
# curl -fsSL https://raw.githubusercontent.com/bladeacer/adacovex/main/install.sh | bash

# Assess a project (strict mode; DAL-C by default)
adacovex --target=.

# Toolchain + platform report
adacovex status --target=.

# Web dashboard at http://localhost:8080
adacovex --target=. --serve

Contributors build from source with make build (see Installation). make run-self assesses adacovex itself. make run-ada-crdt runs the Ada_CRDT regression.

Documentation

The full index lives at adacovex.readthedocs.io. Highlights:

Reference	Description
Installation	Alire / release bundle / source build
CLI Reference	Full flag table, --require-* gates, exit codes
Web Dashboard + JSON API	--serve HTML dashboard, /api/metrics, themes
SBOM	Proof-aware CycloneDX / SPDX bill of materials
VCS Support	Differential modes across git/hg/svn/fossil/jj
Standards	DO-178C / ISO 26262 / IEC 62304 abstraction, per-level criteria
HLR Index	High-level requirements traceability index
LLR Mapping	Low-level requirement-to-HLR mapping
Proving and Writing Proofs	How proving works, SPARK contracts, proof patches for vendored deps
Architecture	Design decisions, patches, toolchain resolution, overflow contract
Developer Guide	Codebase structure and repo setup for contributors
API Reference	Auto-generated package API docs (developers / auditors)
Docstring Spec	Annotation format, placement, conventions
Test Format	Supported test-result output format
Changelog	Release history
CI/CD	GitHub Action, workflows, release bundling
LLM usage	AI disclosure, trust, how LLM agents work under AGENTS.md

Installing adacovex

Declare covex in your project's alire-dev.toml, run alr install covex, or download a release bundle and build from source. Installation covers each route, including the version source per method and the man-page sync.

Platforms, toolchain, and VCS

• Platforms -- runs wherever a GNAT/Alire toolchain exists; the release binary is Linux x86-64 only for now (build from source for other platforms). See platforms.
• GNATprove resolution -- manifest pin over global pin over $PATH over cached toolchain over download (a manifest pin is authoritative). See GNATprove resolution.
• VCS -- not required for base functionality; only the differential modes need one, and they work across git, hg, svn, fossil, and jj. See VCS.

CLI reference

adacovex [options]
adacovex sbom [--format=cyclonedx-json|spdx-json] [--out=PATH]
           [--standard=NAME|--dal=LEVEL|--asil=LEVEL|--class=LEVEL]
adacovex prove [-t=PATH] [prove options]
adacovex status [-t=PATH]
adacovex man [--check|--force] [--dir=PATH]
adacovex complexity [-t=PATH]

Shorthands read well interactively: -t (--target), -m (--manifest), -s (--serve), -p (--port), -c (--cache), -b (--compare-base), -d (--coverage-delta), -l (--level, the GNATprove proof level), -r (--require-proof), and -j (--jobs). --standard= also takes a combined tier token, so --standard=asil-b means --asil=B.

The full flag table (defaults, modes, --require-* CI gates, strict vs relaxed mode, exit codes, contextual help [TOPIC], and the man subcommand) lives in CLI reference. The web dashboard and JSON API are in the web dashboard.

Examples

adacovex --target=.                                 # self-assessment
adacovex --target=. --standard=all                  # badges for every standard
adacovex --target=. --serve                         # web dashboard at :8080
adacovex --target=. --compare-base=HEAD             # differential assessment
adacovex prove --target=.                           # run gnatprove, then assess
adacovex sbom --format=cyclonedx-json --target=.    # proof-aware SBOM
adacovex status --target=.                          # toolchain + platform report
adacovex complexity --target=.                      # cyclomatic complexity check

More examples: examples.

Target project requirements

To run adacovex against a project it needs Ada sources, GNATprove output (gnatprove.out), a test-summary file, and (for DAL assessment) an docs/compliance/HLR.md document. Missing data shows N/A; DAL checks that depend on it report Unmet. Full requirements, file-discovery rules, and the non-Ada-project note: target projects.

Docstrings and patches

Subprograms are documented with -- @param / -- @return annotations (full spec); strict mode requires 100% coverage. For vendored code you cannot modify, patch files at <target>/.adacovex/patches/ overlay docstrings and SPARK proof aspects (SPARK_Mode, Pre, Post, Global): the prove subcommand merges them into a patched tree copy and proves the vendored dependencies against their contracts without touching the originals. See Architecture -- Patch System.

Compliance levels

The same evidence (proof level, passing tests, HLR traceability) is re-labelled for three functionally-equivalent safety standards. Pick a level with a standard's own naming, or pass --standard=all to run one assessment at the shared tier and emit badges for all three:

Standard	Level flag	Levels	Example
DO-178C (avionics)	--dal=	A, B, C, D, E	--dal=C = DAL-C
ISO 26262 (automotive)	--asil=	A, B, C, D, QM	--asil=B = ASIL B
IEC 62304 (medical)	--class=	A, B, C	--class=A = Class A

The evidence is identical across standards; only the integrity-level label changes. Full tier mapping and per-level criteria: Standards.

Development

make check runs the full quality gate (cheap static gates first, then build, test, prove, doc, sbom, then tree-wide count-sync checks). Other targets include build, test, prove, doc, sbom, fmt, run-self, run-ada-crdt, bump-version, release, and clean.

Run make help or see AGENTS.md for the full table. AI tools were used during development; why the code is still trustworthy: LLM usage.

CI/CD

A composite GitHub Action (./action.yml) plus ci.yml, pr-check.yml, and release.yml workflows cover the --standard=all self-assessment, the native test suite, the PR docstring-coverage gate, and releases.

Action inputs/outputs, result caching, and release bundling: CI/CD.

Verification

Check	Command	Requirement
Unit tests	make test	1637/1637 passing
Self-assessment	make run-self	100% docs, Platinum, DAL-C Achieved
SPARK proof	make prove	Platinum (878 VCs, 0 unproved under gnatprove 16.1.0)
Ada_CRDT regression	make run-ada-crdt	100% docs, DAL-C (strict mode)

See changelogs for full release notes.

Requirements

• Alire >= 2.0
• GNAT Ada compiler (managed by Alire)
• Python 3 (required at build time to bundle the dashboard and the offline manual into the binary via tools/gen-dashboard.py and tools/gen-docs.py, the latter needing sphinx + myst-parser + furo from requirements.txt; the released binary itself has no Python or runtime dependency)
• GNATprove (optional; resolved at run time by prove -- no declared dependency)
• gnatdoc_bin and gnatformat_bin (dev dependencies managed by Alire, declared in alire-dev.toml and run via alr exec for the make doc and make fmt targets -- so the published crate still installs and builds with no toolchain beyond the GNAT compiler)

Swapping the GNAT compiler (LLVM backend)

See swapping the GNAT compiler for Alire-managed and system-installed GNAT LLVM options and caveats.

Credits

Third-party attributions, licences, and bundled-asset notices: see Credits and third-party notices.

License

Apache-2.0 -- see LICENSE for details.