diff --git a/spec/ARG-PROFILE.adoc b/spec/ARG-PROFILE.adoc
new file mode 100644
index 0000000..c82ee19
--- /dev/null
+++ b/spec/ARG-PROFILE.adoc
@@ -0,0 +1,247 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= ARG-PROFILE — My
+:toc: left
+:toclevels: 2
+
+[cols="1,3"]
+|===
+| Field | Value
+
+| Language | My (`.my`, four dialects)
+| Repository | https://github.com/hyperpolymath/my-lang
+| Current ARG Grade | *D-leaning-E*  (toy-project usable in places, but multi-dialect ambition not yet matched by external adoption)
+| Assessed | 2026-05-28
+| Assessor | Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+| ARG Spec Version | 1.0
+| FRG Profile | spec/FRG-PROFILE.adoc
+| TRG Profile | spec/TRG-PROFILE.adoc (TBD)
+|===
+
+== About this profile
+
+My is a progressive-disclosure language with four dialects (visual
+blocks → solo → duet → ensemble) and four-dialect structure
+mirrored in `dialects/` + `crates/` + `proofs/`. It has the most
+*architectural* maturity of the three audit-cohort languages
+(11 production crates including `my-ai`, `my-cli`, `my-dap`,
+`my-debug`, `my-fmt`, `my-hir`, `my-lang`, `my-lint`, `my-llvm`,
+`my-lsp`), an EBNF grammar (`grammar.ebnf`, 381 lines), and a
+playground directory. The honest current ARG grade is D-leaning-E
+— the language *has* the surfaces but they are sparsely populated
+for external adoption.
+
+ARG = D-leaning-E. The full chain of axes:
+
+* ARG: D-leaning-E
+* TRG: TBD (likely D given 11 crates)
+* FRG: E (see `spec/FRG-PROFILE.adoc` — proofs/ exists with subdirs
+  but PROOF-NEEDS.md indicates no domain-specific Idris2 proofs
+  have landed yet)
+* CRG: TBD
+* RSR: Compliant at TRG-D level
+
+Cross-axis rule: ARG ≤ TRG holds.
+
+== Grade rationale (evidence for D-leaning-E)
+
+[cols="2,1,4", options="header"]
+|===
+| Criterion | Met? | Evidence
+
+| *D1 — Landing page / README*
+| YES
+| `README.adoc` (top-level, comprehensive; "Let learning unfold"
+  lead; OpenSSF Best Practices badge)
+
+| *D2 — Elevator pitch*
+| YES
+| README "Progressive-disclosure programming language with
+  first-class AI integration — four dialects scaling from visual
+  blocks to agentic orchestration"
+
+| *D3 — Provenance*
+| YES
+| MAINTAINERS.adoc + LICENSE + CITATION (via CONTRIBUTING.adoc) +
+  CODE_OF_CONDUCT
+
+| *TRG ≥ D estate-wide*
+| LIKELY YES
+| 11 crates implementing the toolchain spine (cli, lsp, dap,
+  formatter, linter, codegen via my-llvm, debug)
+
+| *RSR-compliant at TRG-D*
+| YES
+| SPDX headers, MPL-2.0 + PMPL choice declared, comprehensive
+  estate-discipline files present
+
+| *O1 — 5-minute hello-world*
+| PARTIAL
+| `examples/` directory exists; not explicitly time-measured
+
+| *O2 — Tutorial covering distinctive features*
+| PARTIAL
+| `docs/` covers dialects but tutorial form is sparse
+
+| *O4 — Cookbook ≥ 3 worked examples ≥ 100 LoC each*
+| UNCLEAR
+| examples/ present; LoC threshold not verified
+
+| *R1 — Reference manual*
+| PARTIAL
+| `IMPLEMENTATION.md` + docs/; not "complete reference"
+
+| *R3 — Formal grammar*
+| YES
+| `grammar.ebnf` (381 lines)
+
+| *Δ1 — Stable release artefacts*
+| PARTIAL
+| Git tags; not signed release process documented
+
+| *External programs ≥ 100 LoC each parse/typecheck/run*
+| UNCLEAR
+| Not externally verified
+
+| *Diversity-metrics: ≥ 2 distinct external authors*
+| NO
+| Founder is sole author
+
+| *O3 — Playground*
+| PARTIAL (D-permissive; required from C)
+| `playground/` directory exists; browser-runnable status TBD
+
+| *R2 — Stdlib reference*
+| NO
+|
+
+| *R4 — Operational/denotational semantics*
+| NO
+|
+
+| *R5 — Stable error-code index*
+| NO
+|
+
+| *C1-C5 community*
+| PARTIAL
+| Issue tracker, CONTRIBUTING (.adoc + .md), CoC, MAINTAINERS;
+  no public discussion venue
+
+| *Δ2-Δ5 distribution*
+| PARTIAL
+| Cargo workspace; versioning policy implicit
+
+| *E1-E4 education*
+| NO
+| (Despite the "Me-curious / educators" target audience)
+
+| *X1-X4 ecosystem*
+| NO
+|
+
+| *VeriSimDB attestation*
+| NO (D-permissive; required from C)
+|
+|===
+
+== Honest reading
+
+My is *architecturally* the most ambitious of the three audit cohort
+languages: four dialects, AI integration via `my-ai`, debug-adapter
+protocol, full LSP, codegen via LLVM. The architecture *sets up*
+ARG-C territory but the *content* of each surface is sparsely
+populated.
+
+The honest current grade is *D-leaning-E*:
+
+* D criteria mostly satisfied at the level of "the surface exists",
+* but the cookbook + external-author diversity floor for honest D is
+  not met,
+* and the strong vision (educators, AI-native, progressive disclosure)
+  has not yet translated into adoption surfaces matching that
+  ambition.
+
+This is the inverse of ephapax's pattern: ephapax has strong FRG
+ambition with sparse ARG surfaces. My has strong ARG architecture
+with sparse FRG/proof-content.
+
+== Language-specific tightening
+
+For My, the following ARG tightening applies:
+
+* *Grade C tightening:* The dialects (`solo`, `duet`, `ensemble`,
+  `me`) MUST each have ≥ 3 cookbook examples honouring the
+  progressive-disclosure principle (an example in `me` MUST be
+  reachable from an `ensemble` example via the disclosure path).
+* *Grade B tightening:* The AI-integration claim (`my-ai`) MUST be
+  exercised by ≥ 5 external users (the AI-native positioning of the
+  language is load-bearing — adoption MUST exercise it).
+* *Grade A tightening:* The "Me-curious / educators" target MUST be
+  validated by at least one external educator using `me` dialect
+  in a multi-week curriculum.
+
+== What is NOT yet met (honest gaps)
+
+* No external authors at the diversity floor.
+* No browser-runnable playground confirmed.
+* No stdlib reference (despite `lib/`).
+* No operational-semantics document.
+* No stable error-code index (despite `my-lint` infrastructure).
+* No public discussion venue.
+* No education materials despite educator-target audience.
+* No release-process documentation (Δ3).
+
+== Path to next grade (honest D — toy-project usable)
+
+* Author 3 cookbook examples ≥ 100 LoC each, one per dialect (solo,
+  duet, ensemble) at minimum.
+* Time-measure the hello-world clean-install path.
+* Recruit 2 distinct external program authors.
+* Tag a signed release artefact via documented process.
+
+*Realistic timeline estimate:* 2-3 months — the surfaces exist; they
+need population.
+
+== Path to grade beyond that (C — alpha gate)
+
+* Confirm playground browser-runnable.
+* Stdlib reference per `lib/` symbol.
+* Operational semantics document at R4.
+* Stable error-code index (use `my-lint` codes as seed).
+* Public discussion venue.
+* RFC/ADR process activated (the `INTENT.contractile` +
+  `MUST.contractile` structure is the seed — needs RFC bridge).
+* Slide deck (E1) for the progressive-disclosure pedagogy.
+* 10 dogfood users meeting diversity-metrics.
+* ≥ 2 substantive domains, ≥ 3 cookbook examples each.
+* VeriSimDB ingestion.
+
+== Demotion risk
+
+* *Lowest:* `playground/` not browser-runnable on inspection — drops
+  toward E.
+* *Medium:* Multi-dialect ambition becomes "vapourware" perception
+  if dialects ship empty — risks F over time.
+* *Catastrophic:* `my-ai` claim not exercised by real AI integration
+  (`my-ai` becoming a placeholder) — risks F for misrepresentation.
+
+== Iteration history
+
+[cols="1,1,4", options="header"]
+|===
+| Date | Grade | Notes
+
+| 2026-05-28 | D-leaning-E | Initial ARG assessment. Strong architecture (11 crates, 4 dialects, EBNF, playground/ dir) but surfaces sparsely populated. Diversity-floor and content-density gates are the binding constraints for honest D.
+|===
+
+== Review cycle
+
+* *Routine:* Reassess on every release cycle.
+* *Immediate:* Reassess within 7 days of any demotion trigger.
+
+== Footer
+
+This profile is itself a VCL-total proposition. `DECLARE`'d to
+VeriSimDB on each commit (once ingestion wired).
diff --git a/spec/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc
new file mode 100644
index 0000000..ecaaace
--- /dev/null
+++ b/spec/FRG-PROFILE.adoc
@@ -0,0 +1,229 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= FRG-PROFILE — My
+:toc: left
+:toclevels: 2
+
+[cols="1,3"]
+|===
+| Field | Value
+
+| Language | My (`.my`, four dialects)
+| Repository | https://github.com/hyperpolymath/my-lang
+| Current FRG Grade | *X*  (no formalisation in any qualifying prover; PROOF-NEEDS.md explicitly records that template ABI scaffolding was removed without replacement)
+| Assessed | 2026-05-28
+| Assessor | Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+| FRG Spec Version | 1.0
+| ARG Profile | spec/ARG-PROFILE.adoc
+| TRG Profile | spec/TRG-PROFILE.adoc (TBD)
+| Formalisation Directory | `proofs/` exists with subdirs (`duet/`, `ensemble/`, `me/`, `shared/`, `solo/`, `verification/`, `white-papers/`) but PROOF-NEEDS.md records that the template-ABI scaffolding was REMOVED without domain-specific replacement
+| Qualifying Prover(s) | (none mechanised at the calculus level)
+|===
+
+== About this profile
+
+My is FRG-X. The `proofs/` directory exists with dialect-aligned
+subdirectories suggesting *intended* per-dialect formalisation, but
+`PROOF-NEEDS.md` explicitly records (2026-03-29):
+
+[quote]
+____
+Template ABI removed -- was creating false impression of formal
+verification. The removed files (Types.idr, Layout.idr, Foreign.idr)
+contained only RSR template scaffolding with unresolved
+{{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.
+
+When this project needs formal ABI verification, create
+domain-specific Idris2 proofs following the pattern in repos like
+typed-wasm, proven, echidna, or boj-server.
+____
+
+This is *good FRG-discipline* — the language honestly retracted a
+formalisation claim that was scaffolding-only — but it leaves My
+at FRG-X (no formal artefact in a qualifying prover).
+
+FRG = X. The full chain of axes:
+
+* FRG: X
+* ARG: D-leaning-E (see `spec/ARG-PROFILE.adoc`)
+* TRG: TBD (likely D)
+* CRG: TBD
+* RSR: Compliant at TRG-D level
+
+Cross-axis rule: ARG-A requires FRG ≥ B; My's FRG-X is currently
+the binding constraint for any ARG progression past C (where
+foundations evidence starts to interact).
+
+== Declared TypeLL level
+
+* *TypeLL level claimed:* L4 (Type compatibility) *operationally*
+* *Honest level for FRG:* L4 — implementation enforces affine /
+  borrow / progressive-disclosure types, but no mechanised soundness
+  claim. The dialect structure (solo / duet / ensemble / me)
+  *aspires* to layered type-safety progression but no formal
+  encoding establishes this.
+* *Levels not yet claimed:* L5-L10. Progressive-disclosure pedagogy
+  is orthogonal to FRG levels; FRG asks about *foundations*, not
+  pedagogy.
+
+== Grade rationale (evidence for X)
+
+[cols="2,1,4", options="header"]
+|===
+| Criterion | Met? | Evidence
+
+| *M1 — Abstract syntax formalised*
+| NO
+| `grammar.ebnf` exists (381 lines) but EBNF is not a qualifying-
+  prover encoding. AST exists in Rust crates only.
+
+| *M2 — Typing judgment formalised*
+| NO
+| Typing exists in `my-hir` / `my-lint` Rust crates only
+
+| *M3 — Operational semantics formalised*
+| NO
+|
+
+| *M4 — Preservation theorem stated*
+| NO
+|
+
+| *M5 — Progress theorem stated*
+| NO
+|
+
+| *P1-P4*
+| NO
+|
+
+| *V1 — Single qualifying prover used for M1-M5*
+| NO
+| `proofs/` directory has dialect-aligned subdirs but no mechanised
+  content. The Idris2 template scaffolding was explicitly REMOVED
+  on 2026-03-29 per `PROOF-NEEDS.md`.
+
+| *TypeLL L1-L4*
+| YES (operationally)
+| Implementation enforces
+
+| *TypeLL L5-L10*
+| NO
+|
+
+| *B0 — Zero banned constructs in proof tree*
+| YES (vacuously)
+| No proof tree exists
+
+| *B1 — CI banned-construct lint*
+| N/A
+|
+
+| *VeriSimDB attestation*
+| NO
+|
+
+| *PROOF-NEEDS.md*
+| YES (good discipline)
+| Exists and HONESTLY records the absence of formalisation —
+  this is exactly the discipline FRG rewards even at X
+|===
+
+== Honest reading
+
+My is FRG-X. There is no formalisation. The honest discipline of
+*removing* the template-ABI scaffolding that was creating a false
+impression of formal verification is the *right* move — it
+*evacuates a path to FRG-F* (which would apply if the scaffolding
+had been left in place while being held out as evidence).
+
+By removing the scaffolding without replacement, the language
+recorded itself as FRG-X with PROOF-NEEDS.md honesty. This is the
+correct grade.
+
+Note: the README OpenSSF Best Practices badge link suggests pursuit
+of the OpenSSF criteria, which include some formalisation-related
+items. These are CRG/TRG/RSR concerns, not FRG.
+
+== Language-specific tightening
+
+For My, the following FRG tightening applies:
+
+* *Grade E tightening:* The formalisation MUST cover the *base*
+  dialect (`solo`) syntax + typing first. The progressive-disclosure
+  ambition means the dialects are an ordering on type-richness; the
+  formalisation must start at the simplest and add layered
+  obligations.
+* *Grade D tightening:* Preservation MUST be stated *per dialect*:
+  preservation-solo, preservation-duet, preservation-ensemble,
+  preservation-me, with explicit composition rules for the
+  inclusion `solo ⊆ duet ⊆ ensemble ⊆ me`.
+* *Grade C tightening:* The borrow checker MUST be modelled in the
+  formal calculus, not stubbed out. (My's borrow-check is genuine
+  per `crates/my-lint/`; the formal encoding must match.)
+
+== What is NOT yet met (honest gaps)
+
+* No `formal/` directory at all (the `proofs/` directory is the
+  intended placement but is currently empty of mechanised content).
+* No qualifying-prover encoding of AST, typing, or semantics.
+* No preservation / progress statements.
+* No PROOF-STATUS.a2ml.
+* No banned-construct CI lint (vacuous now, but needs to exist by
+  the time mechanisation lands at E).
+
+== Path to next grade (E — well-formedness only)
+
+* Pick a qualifying prover for My's formalisation. Recommendation:
+  Idris2 (estate-natural for AI-integration narrative; matches
+  template-ABI removal note's suggestion of "typed-wasm, proven,
+  echidna, boj-server" pattern).
+* Create `formal/` directory or repurpose `proofs/`.
+* Encode `solo` dialect AST (start with the smallest dialect).
+* Encode `solo` dialect typing judgment.
+* Wire CI to build the formalisation.
+* Author per-dialect `PROOF-NEEDS.md` (the top-level one is good but
+  the dialect structure invites per-dialect break-down).
+
+*Realistic timeline estimate:* 3-6 months given the dialect
+multiplicity. Starting with `solo` dialect only could land FRG-E
+within 1-2 months.
+
+== Path to grade beyond that (D — preservation stated)
+
+* Encode operational semantics for `solo` dialect.
+* State preservation + progress for `solo`.
+* Track open obligations in PROOF-NEEDS.md.
+* Wire banned-construct lint to CI.
+
+== Demotion risk
+
+* *Lowest:* From X, there is no lower-non-F grade — but
+  reintroducing template-scaffolding-as-evidence without removing
+  it again would drop to F (the failure mode the 2026-03-29
+  retraction prevented).
+* *Catastrophic:* Claiming formal verification in the README or
+  marketing without backing — risks F.
+
+== Iteration history
+
+[cols="1,1,4", options="header"]
+|===
+| Date | Grade | Notes
+
+| 2026-03-29 | X | Template-ABI scaffolding removed (Types.idr, Layout.idr, Foreign.idr) per honest-retraction discipline. PROOF-NEEDS.md records the retraction.
+| 2026-05-28 | X | Initial FRG assessment. Honest X. proofs/ subdir structure present but empty of mechanised content. Discipline of retraction is correct; path forward is creation of domain-specific Idris2 proofs starting with `solo` dialect.
+|===
+
+== Review cycle
+
+* *Routine:* Reassess on every release cycle.
+* *Immediate:* Reassess within 7 days of any demotion trigger.
+* *Formalisation creation:* Reassess when first qualifying-prover
+  file lands in `proofs/` or `formal/`.
+
+== Footer
+
+This profile is itself a VCL-total proposition. `DECLARE`'d to
+VeriSimDB on each commit (once ingestion wired).