adacovex Documentation¶
This page is the index for all adacovex documentation. Pick a section relevant to you, or read the pages in the order below.
Read Site transparency first. It is the first entry in the sidebar, so you can reach it from every page. It states what the online manual records when you read it: search, traffic analytics, advertising, and the flyout menu.
All documentation uses British English and ASD-STE100 Simplified Technical English. The controlled Technical Names dictionary lives in STE100 Technical Names; use it before you use a technical word in any doc, docstring, or changelog.
Getting started¶
Installation – install the binary or the action.
Target projects – what a target needs.
Using adacovex¶
Usage guide – the self-contained user guide, grouped by task: install and run, assess a project, read the results, publish in CI, and manage the toolchain. Start at installation.
CLI reference – every command, flag, and exit code. The detailed flag pages are assessment flags and subcommands, serving, CI, and tool options, and emitted reports and differential modes.
Web dashboard – the HTML report, the JSON API, the dependency views, the metric charts, the themes, and the bundled offline manual.
SBOM – the bill-of-materials generator, with dependency resolution for licences and versions.
Global configuration and state – the optional the global configuration file file, the environment variables, and the cache and toolchain directories.
Standards – DO-178C, ISO 26262, and IEC 62304 levels. The per-standard detail is on DO-178C and the DAL levels, ISO 26262 and the ASIL levels, IEC 62304 and the safety classes, and Selecting a standard.
Platforms – supported platforms and toolchain state.
VCS support – differential assessment across git, hg, svn, fossil, and jj.
CI/CD – the GitHub Action and the workflow summary. The workflow internals are on CI/CD workflows, summaries, and release bundling, the action’s inputs and outputs are on the composite action, and the release bundling, floating tags, and consumer manifests are on Release bundling, tags, and consumer manifests.
Changelog – release history.
Contributing to adacovex¶
Developer guide – the contributor handbook: setup, gates, and release workflow. The source layout, the pipeline, and the generated artifacts are on the repository layout.
Proving and writing proofs – how to run and write SPARK proofs. Writing proof patches over vendored code is on Proof patches.
Architecture – the full technical design. The deeper pages are dependency management and the toolchain, verification and proof patches, outputs and formats, and pipeline, platforms, and delivery.
Requirements – the dependency categorisation.
Performance – the benchmark categories and the current numbers, with how to run them, the per-phase prove timings and its 1.55.0 re-baseline, plus the optimisation history.
gnatprove-friendly IR – the design exploration for synthesising bounded, contract-carrying code.
STE100 Technical Names – the controlled dictionary of rules and entries, split into seven lexicons: the Ada language, proof and compliance, tooling, hardware, the tools and files, the reports and concepts, and the web site terms.
LLM usage – guidance for AI agents.
Maintainer references¶
Proof ledger – the verified-VC history and the skipped units audit.
Compliance outputs – VERIFICATION.md, TRACE.md, and the HLR/LLR indexes.
HLR index and LLR mapping.
Badges – the badge set the self-assessment emits.
API reference – the generated package documentation.
tldr page – the cheat sheet for the CLI, which
adacovex tldrinstalls into the local tldr client.
The docs live under docs/ as a Sphinx project (docs/conf.py with
MyST, plus a root docs/index.md holding the toctree). The pages are grouped
by audience: docs/usage/ for end users, docs/contributing/ for
contributors, and the top-level references plus docs/proof/,
docs/compliance/, and docs/badges/ for maintainers. Build and sync
instructions live in the developer guide.