All notable changes to this project are documented here. The format follows Keep a Changelog, and the project aims to follow semantic versioning.
Materialized and ran the loom-ultralight experiment (every milestone listed in the
epic's wrap.md): a Dafny + Rust harness that tests whether an LLM writes a weaker
spec when graded only on making its own implementation verify. The N=30 × 3-model
run showed a real, capability-scaling weakening localized to width-exactness,
confirmed by two independent measures — mutation kill-rate and a verifier-based
structural strength check. Decision D-0001 records a qualified proceed to
loom-light. New harness modes: --rescore (re-score cached generations with no
API) and --strength (structural per-obligation entailment).
Generalized the loom-ultralight strength gate to any registered subject (LOOM_SUBJECT)
and ran the two-arm experiment (opus-4.8, N=30/arm) on two fresh, harder invariants — the
aiwf status-transition FSM and the prosey-title check — with the discriminating mechanism
pre-registered after the M-0002 correction. The endogenous claim-weakening effect did
not reproduce on either subject (tell gaps an order of magnitude below the
pre-registered threshold): decision D-0002 records the resulting NO-GO — loom-light
is not greenlit on this evidence. Every milestone is listed in the epic's wrap.md. New
harness modes: --decide (apply the combination rule to two subjects' verdicts) and
--check-prereg-ancestry (the pre-registration-precedes-run git guard).
Re-tested the loom value-gate on a genuinely harder, decidable aiwf invariant — the
id-reallocation / reference-rewrite invariant — pre-registering both ways the incentive can
distort spec quality (under-specification and over-claiming) in a two-dimension §6 verdict
(every milestone listed in the epic's wrap.md). To make the over-claim dimension trustworthy,
the validity gate was rebuilt as a hybrid — dafny verify with a concrete-tree execution
fallback (D-0003) — and the spec instrument was certified against a bounded,
adversarially-reviewed residual with no false-valids (D-0004). On the pre-registered primary
(opus-4.8, N=30/arm) neither failure mode reproduced — both arms 30/30 valid, tell and
over-claim gaps at 0.0 — so decision D-0005 records a terminal NO-GO: the gaming
hypothesis is not supported on the primary model across four subjects now. New harness surface:
the hybrid validate_spec gate, helper-capture + guarded-quantifier-rewrite spec extraction,
and a self-contained multi-model verdict.json.
Turned loom's whole umbrella loop — a non-formal author writing prose + examples, blind subagents
authoring the formal umbrella, a Dafny verifier + gap report closing the loop — on real aiwf
code (every milestone listed in the epic's wrap.md): the decidable status-transition FSM and
string-based id-canonicalization (laddered flat → recursive). The loop turned end-to-end with the
human entirely at the prose / gap-report layer (zero Dafny/Go read) and delivered real value in
both directions the bidirectional discipline predicts — a code gap filed upstream, and
intent errors the operator accepted (the emit-wide / accept-narrow conflation). It also mapped
loom's tractability boundary on strings (modeling + concrete-checking tractable; blind
universal-property discharge degrades and a (B)-failure stops self-diagnosing). Decision D-0006
records a qualified PROCEED to build the thin loom-light tool, scoped to decidable / structured
invariants first. New design docs: docs/loom-loop-poc.md (the whole-loop direction) and
docs/loom-completeness-poc.md (its superseded predecessor + a four-reviewer critique).
Turned the D-0006 qualified proceed into a real tool (every milestone listed in the epic's
wrap.md): the overlay pattern, an opt-in loom verify runner, and five frozen contracts
(overlay boundary, gap-report schema, umbrella format, runner interface, property independence)
on a three-property Dafny seed. loom then self-hosted its own trust-critical plumbing (atomic
writes, parser/dispatch totality) using loom itself, added a second verification substrate
(TLA+/TLC) through the same seam without touching the first, and turned the authoring loop into
a real loom author command behind a blind-authoring seam (ADR-0019–ADR-0022) that resists
the endogenous claim-weakening this project's whole E-0001–E-0004 arc studied. A companion
loom suggest command closes the loop the other direction, proposing candidate umbrella stubs
from source. The epic closes with decision D-0007: productize now, explicitly alpha — a
real semver release process cut from crates/loom in place (no repository move), since every
prospective consumer at this stage is this project's own. New CLI surface: loom verify, loom author, loom suggest; new schema: gap-report.v2 (additive substrate field).
AuthoredFragment::parse (the ## lowering / ## back-translation fragment format) and
parse_request_sections (the ## intent / ## shows authoring-request format) both misread a
verbatim content line that itself began ## as a new section header, corrupting or rejecting
otherwise valid input. Both parsers now share one fencing-aware raw-section scanner: content
wrapped in a triple-backtick fence carries any ## -prefixed line through intact; unfenced
content beginning ## is still read as a header, now the documented constraint an author
command or human writer honors to carry such content safely — closing the ambiguity fully would
require making that fencing mandatory everywhere, a wire-format-breaking change out of scope
here. The shared scanner is hardened with exhaustive state-transition examples, a round-trip
property test (proptest, new dev-dependency) generating bodies that include ## -prefixed and
fence-delimiter lines, and a scoped cargo-mutants pass (11/11 logic mutants caught).
Fixed — G-0021: loom suggest no longer scans a candidate's intent prose for property:/class: key lines
parse_candidate_record read a candidate's property: and class: fields by scanning its
entire record body, including the free-text ## intent prose — so a candidate whose intent
happened to contain a line shaped like class: authorization was rejected as a false
DuplicateClass/DuplicateProperty, and a candidate that omitted class:/property: entirely
could have it silently scavenged from prose instead of rejected as MissingClass/
MissingProperty. The key-line scan is now scoped to the record's key-line region — its text
before the first ## -labeled section — via a new key_line_region helper, verified by a
proptest round-trip property and a scoped cargo-mutants pass (3/3 mutants caught).
run_dafny relied solely on a 120s wall-clock ceiling to bound a Z3 run, so the proved/error
boundary was machine-speed-dependent — the same model could prove on a fast box and time out
(error) on a slow one, violating reproducibility (G1). dafny verify is now invoked with
--resource-limit 1000000 --cores 1, a deterministic Z3 rlimit (with ~13x headroom over the
seed models' measured peak cost) that pins the boundary to verifier work instead of elapsed time;
--cores 1 keeps that work — and its rlimit accounting — single-threaded and stable across
machines. The wall-clock timeout remains only as a true-hang backstop.