\subparagraph*{Data availability.}
The Isabelle/HOL development and regression corpus are public on GitHub.
The earlier Zenodo archive~\cite{voblint} lacks the vendored solver, the
claims behind \cref{tab:contexts}, the profiling snapshot, and the table
scripts. A reproducible release must archive these dependencies together.
The upstream solver artifact is public~\cite{tilscher26artifact}, but
Voblint depends on a modified fork that is not publicly accessible.
Reproducing this development requires that exact dependency.

\subparagraph*{Declaration about GenAI/LLM use.}
The author extensively used Anthropic's Claude, OpenAI's ChatGPT and Codex,
and Cursor. Under the author's supervision, these tools produced a large
share of the implementation. This included Isabelle proofs after definitions
and interfaces stabilized, cross-theory refactorings, and conversions of
tactic-style proofs to structured Isar. They helped adapt the local traces of Schwarz et al.\ to
procedure activations and refine the trace requirements. Agents wrote much
of the command-line interface, regression corpus, and consistency tooling.
The author chose the research direction, selected and revised designs, and
approved definitions and theorem statements; Isabelle checked every proof.
The tools also assisted with literature search and drafting and revising the
text and figures, which the author reviewed. Grammarly checked spelling and
grammar.