rosie-qwen3.8-27b-ada

Rosie — a SPARK Ada adapter for Qwen3.8-27B

Rosie is a QLoRA adapter that makes Qwen3.8-27B write SPARK Ada: package specifications with contracts, and the bodies that discharge them. She is the planner and coder inside a factory where GNATprove is the judge, not the model. Nothing she writes is trusted because she wrote it; it is trusted because gnatprove --level=2 --checks-as-errors=on discharged it, or it is thrown away.

This is v0.3, which remains the champion for body-fill after v0.4 and v0.5 were measured against her and lost. The numbers are below, including the ones that do not flatter her.

What she is for

Given prose describing a unit — its types, its operations, and what must be true of each result — she emits a complete .ads or .adb. In the loop she was trained for, a failing round is fixed by changing the prose and re-planning, never by hand-editing her output. That constraint is what makes her useful: every accepted artefact is reproducible from the prose that produced it.

She is not a chat assistant and she is not a general Ada tutor. She is a component in a pipeline whose last word belongs to a prover.

How to use

from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base = AutoModelForCausalLM.from_pretrained("Qwen/Qwen3.8-27B", torch_dtype="bfloat16")
model = PeftModel.from_pretrained(base, "FelicitusBigbeaver/rosie-qwen3.8-27b-ada")
tok = AutoTokenizer.from_pretrained("Qwen/Qwen3.8-27B")

She responds best to a prompt that states the output format first and the contract requirements as a numbered list of operations. Ask for the compilation unit and nothing else — no preamble, no fences — and give the postcondition in words rather than in Ada.

Then prove what comes back. If it does not discharge, the prompt is the thing to change.

Training data, stated honestly

What this adapter (v0.3) was trained on, from its training log (run started 2026-08-29, finished 2026-09-01): 11,977 documents, 105.0 MB of text, 34.9 M tokens. The training script took every *.ads, *.adb and *.ada file under the corpus root, the Wikibooks Ada plain-text dump, and the learn.adacore.com *.rst courses. Nothing was up-weighted. Every document was seen once per epoch.

Licences in the corpus are mixed, and several are copyleft. CORPUS_MANIFEST.md, shipped in this repo, lists the licences tree by tree, generated with two-pass detection: a LICENSE/COPYING file first, then the per-file headers. That second pass matters, because Ada projects commonly state the licence in every file header and ship no LICENSE file at all.

⚠ The manifest describes the corpus tree as it stood on 2026-09-16, not exactly as v0.3 saw it (corrected 2026-09-16). The tree changed after this run: the darkfactory/ tree was added on 2026-09-04 for v0.4 (see below), and applying v0.3's own selection rules to today's tree yields 11,194 documents against the 11,977 the log recorded — so the tree is not the one v0.3 read, and the difference has not been traced file by file. The per-tree licences below are therefore the best available record, not an exact inventory of these weights.

• GPL-3.0-or-later (aunit, cubit, kushtibot, polyorb), mostly with the GCC Runtime Library Exception.
• GPL-3.0-or-later WITH GCC Runtime Library Exception, stated in file headers rather than a LICENSE file: gnoga (1152 of 3625 files), cubedos (29 of 259), spark-examples (10 of 873).
• Apache-2.0: ewok-kernel, hirtos, recordflux.
• BSD: libkeccak (LICENSE file); adacore-drivers (762 of 1023 headers); sparknacl (1 of 119).
• CC BY 4.0: learn-adacore — the learn.adacore.com courses, © AdaCore, licensed under Creative Commons Attribution 4.0 (https://creativecommons.org/licenses/by/4.0/), source https://learn.adacore.com (sources: https://github.com/AdaCore/learn). Used unmodified as RST source text for training; no endorsement by AdaCore is implied. CC-BY-SA: the Wikibooks text dump.
• Undetermined - no LICENSE file and no header detected: libsparkcrypto, spark-by-example, wikibooks-ada. That is not a claim of public domain. It is a statement that automatic detection found nothing, and anyone intending to rely on one of those trees should check it directly.

Where a count is given it is a count, not a generalisation to the whole tree.

Publishing model weights trained on GPL-licensed source is an unsettled question in law. We are not asserting that it is settled. We are stating what went in so that anyone who disagrees can see exactly what they are disagreeing about.

Correction, 2026-09-16. An earlier version of this card said that a darkfactory/ tree, "our own proven catalogue … and the GNAT explain-code manuals", was up-weighted ×8 in this adapter. That was wrong on both counts. The tree was assembled on 2026-09-04 for the v0.4 run, three days after v0.3 finished; v0.3 had no up-weighting and never saw it. The paragraph described v0.4's corpus. The manuals in that tree are also not ours, and the earlier wording presented them as if they were:

• manuals/explain_codes/ — the explain-code texts shipped with SPARK (share/spark/explain_codes in https://github.com/AdaCore/spark2014; the files are byte-identical to those installed with gnatprove FSF 15.0) — AdaCore's SPARK toolset. The files carry no per-file notice; the spark2014 repository is distributed under GPL-3.0.
• manuals/how_to_write_loop_invariants.txt and manuals/how_to_investigate_unproved_checks.txt — sections 7.7 and 7.8 of the SPARK User's Guide (27.0w), © 2011–2026 AdaCore and Capgemini Engineering, under the GNU Free Documentation License.

None of this is in these v0.3 weights. It is stated here so that the v0.4 and v0.5 cards, when published, credit it correctly, and so that no reader is left believing AdaCore's documentation is our catalogue.

⚠ Two further provenance caveats, both real:

1. The manifest in this repo is GENERATED from the corpus tree. An earlier hand-written manifest documented only 8 of the trees; it is superseded and is not published here, because a provenance statement that reads as complete while omitting most of the corpus misleads rather than merely omits. As noted above, even the generated manifest describes today's tree, not the tree on 2026-08-29.
2. A directory named darkfactory-pending/ now sits in the corpus root. It was created 2026-09-12, eleven days after this adapter finished training, and it contains no Ada files. Nothing from it is in these weights. It is noted because a later training script's exclusion filter compares the path component darkfactory exactly and would not skip it.

Training procedure

Sequence length is 2048 rather than 4096 because a 27B QLoRA at 4096 overshot the 32 GiB card by roughly 3 GiB at step 0. That is a hardware limit, not a considered choice, and it is the first thing worth changing on a larger card.

Evaluation

The bench is 58 SPARK body-fill tasks (NumPy routines specified as SPARK contracts). A task passes only when gnatprove discharges every check — the judge is the prover, so the score is not a human or model opinion.

Promotion rule, fixed before the runs: a challenger replaces the champion only if its three-run mean beats the champion's by more than their combined range. v0.5 came in 2.7 below and was more variable, so it did not replace v0.3.

Where v0.5 is better, stated because it matters: on spec emission — expression functions and case-expressions inside contracts — v0.5 improved on v0.3, which is what its training supplement targeted. The coherent reading is that a spec-focused fine-tune bought spec-emission gains at a body-fill cost. If you are emitting specs rather than filling bodies, v0.3 may not be your best choice.

Limitations and known failure modes

These are recorded from real forge rounds, not speculation:

• Declarations with no expression. Her most expensive failure: emitting a function declaration carrying a postcondition but no expression body. The prover then generates zero obligations, the summary reads "0 unproved" because nothing was checked, and it looks like success. Any harness using her must refuse a package with contracts and no expressions.
• Non-inductive loop invariants. She writes invariants that are plausible and true but not inductive, so the proof stalls. Flat conditional expressions discharge where loops do not.
• 'Result without its function prefix, and re-emitting spec contract aspects onto the body (a compile break).
• Duplicate completions of expression functions already completed in a private part.
• No implication operator. Ada has none; she will sometimes reach for =>, which is association syntax and produces a composite-type error.

Prompts that state these rules explicitly avoid most of them, which is itself a finding: the seat's prose, not the model, was the cause of most regressions.

Licence

Released under Apache-2.0, following the base model Qwen/Qwen3.8-27B. The adapter weights carry the base model's licence deliberately — a software licence such as AGPL fits a set of weights badly, and the decision was made explicitly rather than by default.

The corpus provenance section above is part of this release for a reason: if you believe the copyleft material in the corpus changes what this licence can mean, you have the list needed to make that argument.

Not affiliated with AdaCore. GNAT, SPARK and GNATprove are AdaCore's. AdaCore has not reviewed or endorsed this adapter. Rosie depends on their prover to be useful at all, and learned in part from their published courses; that is a debt, not an association.

Provenance of the claims on this card

Every number here comes from a recorded run: the battery scores from a same-box comparison under identical sampling, the hyperparameters from the training script and checkpoint state, and the corpus figures from the v0.3 training log. The card previously took its corpus figures from the corpus tree as it stood at publication; that tree had changed since training, which is how the v0.4 darkfactory/ paragraph came to be attached to v0.3. Corrected 2026-09-16.

If something here is wrong, we would rather be told.