Third-Party Notices

adacovex itself is Apache-2.0 (see LICENSE) and depends only on the GNAT runtime. It declares no library or tool dependencies. The following third-party components are used as tools or bundled artifacts. Their own licences cover them.

Vendored agent skill: SimpleEnglish

The SimpleEnglish skill is the third-party work that adacovex vendors into its source tree. The project uses it to write and review every page of user documentation, every Ada docstring, and every changelog under the rules of ASD-STE100 Simplified Technical English.

Component	Version	Licence	Used for
SimpleEnglish skill	1.3.0 (ASD-STE100 Issue 9, 2025-01-15)	MIT	The documentation discipline of the project: short sentences, active voice, one instruction per sentence, one word with one meaning, and no hedging

The vendored copy is at skills/simple-english/. It is SKILL.md plus references/word-swaps.md, references/use-cases.md, and references/checklist.md. The copy is unmodified upstream text, and it ships in the repository at every checkout, so the licence notice above covers every reader of the tree, not only the built binary.

Two project overrides apply on top of the skill. British English spelling replaces the American spelling that rule 1.14 names, and a paragraph holds at most four sentences, not the six that rule 6.6 names. AGENTS.md states both under Technical writing, and docs/contributing/ste100/index.md holds the controlled list of Technical Names that the standard requires.

The skill governs prose only. It is not linked into the binary, it runs no code at build time, and no generated file comes from it. adacovex dogfoods the tool it documents with, and the skill is the reason the manual reads as it does.

GNAT / GNATprove toolchain

Component	Version	Licence	Used for
GNAT compiler (GNAT Community / FSF GNAT)	toolchain-managed	GPL-3.0-or-later (with GCC Runtime Library Exception for runtime)	Compiling adacovex and target projects
GNATprove	toolchain-managed	GPL-3.0-or-later	SPARK proof analysis (covex prove)
Python 3	toolchain-managed	PSF-2.0	Build-time only: tools/gen-docs.py bundles the offline manual into the binary

Python 3 is required at build time to bundle the docs into the binary, but the shipped binary itself has no Python dependency – the manual is embedded as generated Ada string constants. Sphinx, MyST and Furo (below) run inside Python to produce that manual; Python itself is not bundled or redistributed. | Z3 / Alt-Ergo / CVC5 solvers | bundled with GNATprove | MIT / CeCILL-C / Apache-2.0 respectively | Satisfying SPARK verification conditions |

The GNAT toolchain is not embedded in the adacovex release bundle. gnatprove is not a declared dependency of the covex crate. adacovex resolves gnatprove at run time. covex prove prefers the own gnatprove dependency of the target project when the alire.toml / alire-dev.toml of the target project declares one. It deploys only the pinned gnatprove binary crate into <data>/toolchain/ via alr -n get and runs the deployed binary directly (one-time per version; later runs reuse it). adacovex itself then requires only alr on $PATH. If no dependency is declared, it falls back to a globally pinned version, then a gnatprove on $PATH. Then it falls back to a cached the toolchain cache bin/gnatprove.

Finally it falls back to a platform toolchain download. This download is a GPL-licensed GNAT/gnatprove distribution. Distributing it requires the end user to accept the GPL for that component.

Specifications

The proof-aware SBOMs that adacovex emits conform to these open specifications, and the proof report it reads follows a third:

Specification	Version	Licence	Reference
CycloneDX Software Bill of Materials	1.5	Apache-2.0	specification repository
SPDX (Software Package Data Exchange)	2.3	CC0-1.0	spdx.dev
SARIF (Static Analysis Results Interchange Format)	2.1.0	OASIS IPR policy (RF on RAND Terms)	specification repository

The CycloneDX 1.5 JSON and SPDX 2.3 JSON schemas are referenced for validation only. adacovex does not vendor or redistribute them.

SARIF is referenced for conformance only, and the same rule applies: nothing of it is vendored or redistributed. gnatprove, not adacovex, writes the gnatprove.sarif file; adacovex reads it beside gnatprove.out.

Bundled web assets

Component	Version	Licence	Used for
nomnoml	1.7.0	MIT	Dependency hierarchy diagram alternative view in the dashboard (resources/nomnoml.js, inlined into the served dashboard)
graphre	0.1.3	MIT	Graph layout engine for nomnoml (resources/graphre.js, inlined; required by the UMD wrapper of nomnoml)
FlexSearch	0.7.31	Apache-2.0	Client-side search indexing for packages, HLRs and dependencies in the dashboard (resources/flexsearch.js, inlined into the served dashboard)
yace	1.1.0	MIT	JSON / code tokenizer highlighter for the API playground (resources/yace.js, inlined into the served dashboard)
Charts.css	not bundled (inspiration)	MIT	Inspiration for the hand-rolled dashboard charts

nomnoml is bundled under resources/nomnoml.js (71 KB, MIT). It is inlined into the dashboard page shell. It renders the dependency hierarchy as a UML-style diagram. The diagram appears in the alternative view of the Dependencies tab (Tree / Diagram toggle).

The MIT licence text is preserved in the bundle header comment.

graphre is bundled under resources/graphre.js (38 KB, MIT). It is inlined before nomnoml. It provides the graphre.graphlib and Dagre layout that the UMD wrapper (global.graphre) of nomnoml requires. Without it, nomnoml.draw throws graphlib is undefined.

The MIT licence text is preserved in the bundle header comment.

FlexSearch is bundled under resources/flexsearch.js (16 KB, Apache-2.0). It is inlined into the dashboard page shell. It provides the global search box (packages, HLRs, dependencies). The search box uses an in-memory forward-tokenized index.

The index loads from /__GRAPH_JSON__ at page load. The Apache-2.0 licence text is preserved in the bundle header comment.

yace is a tiny, zero-dependency code editor component (under 2 KB) by Peter Solopov. adacovex vendors its code() tokenizer highlighter (src/highlighters/code.ts, MIT) as resources/yace.js. The tokenizer logic is unchanged: rules are tried in order at every position, and tokens are emitted as <span class="yace-tok yace-tok--<type>"> elements with no built-in colours.

The highlighter is adapted from ESM/TypeScript to a single plain-script binding that exposes window.YaceTok, so the dashboard can use it without a build step. The dashboard supplies the token colours via CSS. The API playground uses it to syntax-highlight the prettified JSON responses of the /api/* endpoints; a JSON-key rule ("name":) runs ahead of the built-in string rule so object keys colour differently from string values. The MIT licence text is preserved in the header comment of resources/yace.js.

Charts.css is not bundled or redistributed with adacovex. The dashboard charts were originally rendered with the vendored Charts.css framework (1.2.0, MIT); adacovex now ships its own patched version of those charts, hand-rolled with plain CSS and SVG and driven by the theme’s CSS variables. Charts.css is credited for inspiration, and its MIT licence terms are acknowledged here.

Documentation build tools

Component	Version	Licence	Used for
Sphinx	toolchain-managed	BSD-3-Clause	Building the manual from docs/ (Furo theme + MyST) for the deployed site and the bundled offline manual
MyST-Parser	toolchain-managed	MIT	Reading the docs/*.md pages unchanged inside Sphinx (no reStructuredText conversion)
Furo	toolchain-managed	MIT	The Sphinx HTML theme used by the manual (light/dark, no external assets)

Sphinx, MyST-Parser and Furo are build-time tools (pinned in requirements.txt, installed into the Python venv). They compile the Markdown manual; their output is embedded into the binary as Ada strings. They are not bundled or redistributed with adacovex. The user-facing documentation, and the offline manual served at /docs, credit Sphinx as the docs generator and Furo as the theme.

Site hosting

Service	Used for
Read the Docs	Hosting the deployed online manual at adacovex.readthedocs.io

The online manual is hosted on Read the Docs, a free documentation service. The same Sphinx project also builds into the offline manual bundled with the binary.

The hosting provider injects its own link-preview popup, its analytics, and its advertising slots into the online pages. The project restyles the popup in docs/_static/rtd-linkpreviews.css, adds no code of its own, and adds no analytics tag. The project owner disabled paid advertising and the flyout menu in the provider dashboard. The reader-facing statement is in docs/site-transparency.md.

Development and testing tools

Component	Version	Licence	Used for
Playwright	test dependency	Apache-2.0	End-to-end dashboard layout tests (just e2e)

Playwright is a development dependency of the e2e fixture (tests/e2e/package.json, devDependencies). It runs automated browser tests of the dashboard. adacovex classifies it as a test dependency: the package name @playwright/test carries the test label. It is not vendored or redistributed with adacovex releases.

Performance-engineering tools

These tools profile adacovex during development. adacovex does not redistribute or depend on any of them; just bench and just perf-bench degrade gracefully when they are missing.

Component	Website / source	Licence	Used for
perf (Linux tools/perf)	kernel.org (shipped with the Linux kernel)	GPL-2.0	CPU profiling and hardware-counter sampling (just perf-bench: cache-miss rates, per-symbol wall clock)
strace	github.com/strace/strace	LGPL-2.1-or-later	Syscall tracing of warm/cold runs (just perf-bench: the newfstatat/openat/getdents64 profiles that drove the walk-skip and stamp-store work)
hyperfine	github.com/sharkdp/hyperfine	Apache-2.0 OR MIT	Statistical command benchmarking (just bench: cold/warm pipeline and prove timings with mean +/- sigma)

The design of the persistent stat-stamp store (1.44.0) was informed by two projects studied for their incremental-processing techniques; neither is linked into adacovex:

Project	Website / source	Licence	What adacovex learned
Ada Language Server	github.com/AdaCore/ada_language_server	GPL-3.0-or-later (with GNAT runtime exception for its runtime)	Persistent indexed file sets and cross-session dirty tracking: re-parse only files whose on-disk state changed (see docs/contributing/perf/index.md, optimisation history 1.44.0)
tree-sitter	github.com/tree-sitter/tree-sitter	MIT	Reusable single-buffer parse input (TSInput) and incremental re-parse cost modelling

The size/mtime stamp validation additionally follows the same shape as git’s index dirty tracking, including the racy-clean guard against files modified within the same second as the record: git (GPL-2.0).

Acknowledgments

• The Ada_CRDT audit target (../Ada_CRDT) is used solely as a dogfood target.

• gnatdoc (for just doc), gnatformat (for just fmt), Alire (alr), and Playwright (for just e2e) are external tools. They are used during development only.

Full licence texts are available at:

• GPL-3.0-or-later

• GCC Runtime Library Exception