- Abstract
- 1. 1. Introduction
- 2. 2. Surface Grammar (Module 0)
- 3. 3. Typed Core Semantics
- 4. 4. Validation Modes
- 5. 5. Opaque Payloads (Non-Negotiable)
- 6. 6. Base Invariants
- 7. 7. Base Record Vocabulary
- 8. 8. Profile Mechanism
- 9. 9. Canonical Hash Form (Hashing Now, Signing Later)
- 10. 10. Citation Primitives
- 11. 11. Reserved Namespaces
- 12. 12. Security Considerations
- 13. 13. IANA Considerations
- 14. 14. Interoperability
- 15. 15. Versioning
- 16. Appendix A: Grammar Summary
- 17. Appendix B: Change Log
- 18. Appendix C: Directive Index (v1.1)
A2ML (Attested Markup Language) is a lightweight markup format that compiles to a typed, verifiable core with formal proof obligations. This specification defines the v1.1 surface grammar, typed-core semantics, validation modes (lax, checked, attested), the profile mechanism, the base record vocabulary, citation primitives, and the canonical hash form for opaque payloads and documents.
A2ML v1.1 is additive over v1.0: every conforming v1.0 document remains a conforming v1.1 document. The new surface in v1.1 — profiles, the base record vocabulary, citation primitives, and canonical hashing — is inert under the base modes and acquires meaning only when a profile selects it.
Media Type |
|
File Extension |
|
Version |
1.1.0 (Stable) |
Era |
v1 |
Date |
2026-06-03 |
Lineage |
See |
A2ML is a foundation, not a consumer. It defines neutral primitives that other formats and tools build on. A2ML names no downstream consumer normatively: the primitives in this document are deliberately generic so that independent record formats can reuse them without coupling back to A2ML’s release cadence.
This independence is load-bearing. The single most common failure in a layered estate is desync: two artefacts that should describe the same thing drift apart because each re-invents identity, provenance, and integrity. A2ML’s answer is the base record vocabulary (Section 7) — one neutral shape for "a thing that can be cited, hashed, and attributed" — reused verbatim by every downstream format.
-
Lightweight authoring: a Djot-like surface syntax.
-
Strong guarantees on demand: Idris2 dependent types for the typed core.
-
Progressive strictness: lax (warnings) → checked (errors) → attested (proofs).
-
Non-negotiable fidelity: opaque payloads preserved byte-for-byte.
-
Inert-by-default extension: new directives carry no semantics until a profile selects them. Nothing in v1.1 changes the meaning of a v1.0 document.
-
One home per concept: identity, provenance, and integrity are defined once (Section 7) and referenced, never duplicated.
The key words MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, RECOMMENDED, MAY, and OPTIONAL are to be interpreted as described in RFC 2119 and RFC 8174 when, and only when, they appear in all capitals.
A conforming A2ML v1.1 implementation MUST:
-
Parse the surface grammar (Section 2).
-
Translate the surface AST to the typed core (Section 3).
-
Support lax and checked modes (Section 4).
-
Preserve opaque payloads byte-for-byte (Section 5).
-
Implement the base invariant checks (Section 6).
-
Recognise the base record vocabulary directives and admit them without error, even when no profile is active (Section 7).
-
Compute the canonical hash form (Section 9) when asked.
The following are RECOMMENDED but not required for base conformance:
-
Attested mode (proof obligations, Section 4.3).
-
Profile resolution and enforcement (Section 8). An implementation that does not resolve profiles MUST treat an
@profiledeclaration as an inert annotation and MUST NOT reject a document for declaring one.
Line ::= CharSeq LF | CharSeq EOF
BlankLine ::= Whitespace* LF
Identifier ::= [A-Za-z][A-Za-z0-9:_-]*
QualifiedId ::= Identifier ( '/' Identifier )*
String ::= '"' ( '\\' Any | [^"] )* '"'
| "'" ( '\\' Any | [^'] )* "'"
Number ::= '-'? [0-9]+ ( '.' [0-9]+ )?
Whitespace ::= ' ' | '\t'
LF ::= '\n'QualifiedId is new in v1.1 and is used for profile identifiers and reference
classes. It is a strict superset of Identifier; an unqualified identifier is a
QualifiedId of length one.
Document ::= Preamble? Block*
Preamble ::= ProfileDecl+ // zero or more; see Section 8.1
Block ::= Heading
| DirectiveBlock
| InlineDirective
| List
| CodeBlock
| Paragraph
| BlankLine+
Heading ::= HeadingMarker SP+ TextLine LF
HeadingMarker::= '#'{1,5}
HeadingLevel ::= length(HeadingMarker)
DirectiveBlock ::= '@' Identifier Attrs? ':' LF DirectiveBody '@end' LF
InlineDirective::= '@' Identifier Attrs LF // self-closing; no body, no @end
Attrs ::= '(' Attr ( ',' Attr )* ')'
Attr ::= Identifier '=' ( QualifiedId | String | Number )
DirectiveBody ::= Block*
List ::= ListItem ( LF ListItem )*
ListItem ::= ( '-' | '*' ) SP+ Inline
Paragraph ::= Inline ( LF Inline )* LF
CodeBlock ::= '```' LangSpec? LF RawLine* '```' LF
LangSpec ::= [A-Za-z0-9_+-]+
RawLine ::= ( [^\n] )* LFA self-closing directive is a directive that carries all of its content in its
attribute list and has no body and no @end. It is written on a single line:
@profile(id=a2ml/state)
@cite(key="rfc2119", span="L10-L14")The parser distinguishes the two directive forms by lookahead: a directive line
ending in : opens a DirectiveBlock and MUST be matched by @end; a directive
line that ends after its closing ) (or its name, if no attributes) is an
InlineDirective. A directive name is either block-form or inline-form per this
specification (Section 7.3, Section 8.1, Appendix C); it MUST NOT be both.
Inline ::= InlineAtom ( SP InlineAtom )*
InlineAtom ::= Emph | Strong | Link | Ref | Text
Emph ::= '*' TextInline '*'
Strong ::= '**' TextInline '**'
Link ::= '[' TextInline ']' '(' URL ')'
Ref ::= '@ref(' QualifiedId ')'
TextInline ::= ( TextChar | '\\' Any )+
TextChar ::= [^*\[\]@\n]
URL ::= [^ )\n]+| Directive | Purpose | Attributes |
|---|---|---|
|
Document abstract |
|
|
Reference list |
|
|
Figure block |
|
|
Table block |
|
|
Byte-preserved payload |
|
|
Structural dependency |
|
Profile, base-vocabulary, and citation directives are specified in Sections 7, 8 and Appendix C.
The normative Idris2 model lives in src/A2ML/. The shape below is informative;
the source files are authoritative.
record Id where
constructor MkId
raw : String
data Block
= Section Sec
| Para String
| Bullet (List String)
| Figure Fig
| Table Tbl
| Refs (List Ref)
| Opaque Payload
| ProfileDecl ProfileId -- Section 8
| Record BaseRecord -- Section 7
| Citation CiteNode -- Appendix C
record Doc where
constructor MkDoc
profiles : List ProfileId -- declared profiles, in source order
blocks : List Block
record Payload where
constructor MkPayload
id : Maybe Id
lang : Maybe String
bytes : String -- preserved exactly; see Section 5-
Headings →
Sectionwith generated or explicitid. -
Block directives → typed blocks by directive name.
-
Self-closing directives → typed nodes (
ProfileDecl,Record,Citation). -
Lists →
Bullet. -
Paragraphs →
Para. -
@opaque→Payload, bytes preserved.
Unknown directives are retained as opaque structural nodes in lax mode and rejected in checked mode (Section 4.2), except that an implementation which does not resolve profiles MUST still accept the directives named in this specification.
Parses all valid surface syntax; emits warnings for missing IDs and unresolved references; never errors unless the syntax itself is invalid. Use for authoring.
All IDs REQUIRED on @fig, @table, and sections; all @ref(…) MUST resolve;
unknown directives are rejected. Use for production documents.
All checked-mode requirements, plus the proof obligations of Section 6 MUST discharge. When a profile is active and declares a minimum attestation level (Section 8.2), attested mode additionally discharges the profile’s obligations.
A document’s mode is chosen by the validator invocation; its profile(s) are declared in the document. A profile MAY raise the effective floor (e.g. "this profile requires at least checked mode") but a profile MUST NOT lower it. Modes and profiles compose by taking the stricter of the two at every axis.
Opaque payloads MUST be preserved byte-for-byte in the typed core. Parsers and renderers:
-
MUST NOT modify opaque payload bytes.
-
MUST preserve encoding (UTF-8 default).
-
MAY transform for an output format (e.g. PDF escaping) but MUST report every transformation.
-
MUST support round-trip: parse → serialize → parse yields an identical payload.
The integrity of an opaque payload is witnessed by its canonical hash (Section 9).
All id attributes in a document MUST be unique.
UniqueIds : Doc -> Type
uniqueIdsDec : (doc : Doc) -> Dec (UniqueIds doc)All @ref(id) and ref="id" attributes MUST reference existing IDs.
RefsResolve : Doc -> Type
refsResolveDec : (doc : Doc) -> Dec (RefsResolve doc)Specific sections MAY be required by policy or by an active profile.
|
Note
|
This section is the anti-desync primitive. It defines one neutral shape for "a thing that can be identified, located, attributed, and integrity-checked". Downstream record formats REUSE this vocabulary verbatim rather than re-inventing it. A2ML core defines the shape and names no consumer; consumers reference this section. |
When two artefacts describe the same underlying thing — a span of source, a proof obligation, an attestation receipt — they desync if each invents its own notion of identity, provenance, and integrity. The base record vocabulary fixes a single neutral shape so that "the same thing" is literally the same fields everywhere.
A base record is a directive @record whose body is a set of fields. The field
set is fixed by this specification:
| Field | Cardinality | Meaning |
|---|---|---|
|
REQUIRED |
Document-unique identifier ( |
|
REQUIRED |
The located region this record is about. See Section 7.4. |
|
OPTIONAL |
A stable structural address into a canonical syntax tree (e.g. an AffineScript node path). OPTIONAL so that non-AffineScript and source-free projects conform without it. |
|
REQUIRED |
Integrity digest of the referenced artefact, |
|
REQUIRED |
Who/what produced the record. See Section 7.5. |
|
REQUIRED |
RFC 3339 UTC instant of record creation. |
|
REQUIRED |
A reference to the artefact the record is about (URI, repo-relative path, or content address). |
|
OPTIONAL |
The profile under which this record was authored ( |
A base record with all REQUIRED fields present and well-formed is base-valid. No field of the base record carries domain semantics: a base record asserts only "this identified, located artefact had this hash, produced by this provenance, at this time". Domain meaning is added exclusively by profiles (Section 8) and by downstream formats.
@record is a block directive. Fields are key: value lines; nested records
(provenance, source_span) are written as indented key: value groups.
@record:
id: rec-001
source_span: { file: "src/Lex.affine", start: { line: 12, col: 1 }, end: { line: 14, col: 9 } }
canonical_node: "module/Lex/fn:tokenize/expr:3"
hash: "sha256:9f86d081884c7d659a2feaa0c55ad015a3bf4f1b2b0b822cd15d6c15b0f00a08"
provenance: { author: "j.d.a.jewell", tool: "a2ml-cli@1.1.0", kind: human }
timestamp: "2026-06-03T11:00:00Z"
artefact_ref: "repo:standards/a2ml/SPEC.adoc"
profile_decl: a2ml/state
@endA source_span locates a region. Its shape:
| Field | Cardinality | Meaning |
|---|---|---|
|
REQUIRED |
Repo-relative path or URI of the source artefact. |
|
REQUIRED |
|
|
REQUIRED |
|
A point span sets end = start. Byte-offset spans MAY be carried additionally in
an OPTIONAL bytes: { start, end } sub-field, but line/col is the REQUIRED form so
that text tools without a byte model still conform.
| Field | Cardinality | Meaning |
|---|---|---|
|
REQUIRED |
Human or organisational identity responsible. |
|
REQUIRED |
Producing tool, |
|
REQUIRED |
One of the closed set |
|
OPTIONAL |
When |
kind is a closed enumeration: exactly human, ai, or mechanical. A
validator MUST reject any other value in checked mode. mechanical denotes a
deterministic, non-AI process (a script, a compiler pass); ai denotes a
generative/inferential agent; human denotes direct human authorship.
In base A2ML (no profile active), @record is recognised and its REQUIRED
fields are checked for presence and well-formedness, but no field is given domain
meaning and no cross-record constraint is imposed. A profile (Section 8) MAY add:
required additional records, cross-record constraints, or a narrower kind set.
A profile MUST NOT remove a REQUIRED base field.
|
Note
|
A profile is a named validation bundle. It is non-executable: it adds required structure and tightens checks; it NEVER grants execution, network, or filesystem capability. Profiles increase validation strictness only. |
A document declares a profile with a self-closing directive in its preamble:
@profile(id=a2ml/state)-
The
idis aQualifiedIdof the form<namespace>/<name>(e.g.a2ml/state). -
A document MAY declare more than one profile; declared profiles compose by taking the union of their constraints (the stricter of any overlapping axis).
-
@profiledeclarations MUST appear before the first non-preamble block. A declaration appearing later is a checked-mode error. -
@profileis inert under base conformance: an implementation that does not resolve profiles MUST accept the declaration and ignore it (Section 1.4).
A profile definition is itself an A2ML document (Section 8.4). It MAY constrain exactly these axes, and no others:
| Axis | A profile MAY… |
|---|---|
Required sections |
name headings/sections that MUST be present (by title or id). |
Allowed directives |
restrict the directive set: a closed allow-list, a deny-list, or "base + these". A directive not permitted by an active profile is a checked-mode error. |
Required directives |
name directives (e.g. specific |
Reference classes |
constrain |
Attestation level |
declare the minimum mode ( |
A profile MUST NOT:
-
grant or imply execution, network access, or filesystem writes;
-
relax a base invariant (Section 6) or remove a REQUIRED base-record field;
-
change surface grammar or token meaning.
These prohibitions are normative and are what keeps "active"/"attested" variants (sometimes called A2MLa) safe: A2ML remains read-only; a profile only raises the bar.
Given @profile(id=ns/name), a validator resolves the definition as follows:
-
Look up
ns/namein the profile registry (Section 8.5). -
If found, load the referenced definition and pin it by its
versionandhash(Section 9). A registry entry without a hash is usable only in lax mode. -
If not found, behaviour depends on mode: lax → warn and continue inert; checked → error
unknown-profile; attested → error.
Resolution is offline and deterministic: the registry and definitions are files in the repository (or a content-addressed store), never a network fetch at validation time.
A profile definition is an A2ML document declaring @profile-def:
@profile-def(id=example/illustrative, version="1.0.0"):
required_sections:
- metadata
- position
allowed_directives: base + [ record ]
required_directives:
- { directive: record, min: 1, max: 1 }
reference_classes:
- { class: state, target: Section, required: true }
min_attestation: checked
@endThis example is illustrative of the format and exercises all five axes.
The real a2ml/* profiles shipped by this repository are in
a2ml/profiles/ (Section 11); each one constrains only the axes it needs.
The five fields map one-to-one onto the typed-core ProfileDef
(src/A2ML/Profiles.idr): required_sections, allowed_directives
(a DirectivePolicy), required_directives (each a RequiredDirective
with min/max cardinality), reference_classes, and min_attestation
(a Mode).
The @profile-def directive and its fields are themselves base A2ML; a profile
definition is therefore self-describing and can be validated by the same engine.
-
Home (one per profile): each profile definition lives at
a2ml/profiles/<namespace>-<name>/PROFILE.a2ml(e.g.a2ml/profiles/a2ml-state/PROFILE.a2ml). This is the single source of truth for that profile; its text is not duplicated elsewhere. -
Registry (verifiable index):
a2ml/profiles/REGISTRY.a2mllists every known profile as a base record (Section 7) whoseartefact_refpoints at the definition file and whosehashpins it. The registry is the verifiable index: a consumer trusts a profile only if the definition’s computed hash equals the registry’s pinned hash. -
Namespacing: the
a2ml/namespace is reserved for profiles shipped by this repository (Section 11). Downstream consumers (which A2ML core does not name) register their own profiles under their own namespaces, in their own repos, and publish their own registries. A2ML core ships only neutral primitives and thea2ml/profiles.
This realises SSOT + verifiable registry: one home per profile, a hash-pinned index, and no duplicated normative text.
v1.1 specifies hashing normatively and reserves signing for a later minor version. Implementations MUST compute hashes as below; signature fields are defined as reserved and inert.
The canonical hash of an opaque payload is:
opaque_hash = "sha256:" + lowerhex( SHA-256( payload_bytes ) )
where payload_bytes are the exact bytes preserved under Section 5, with no
normalisation whatsoever (no newline translation, no trimming, no re-encoding).
The canonical hash of a document is computed over a canonical serialization of its typed core (Section 3), not its surface bytes, so that semantically identical documents that differ only in incidental surface whitespace hash equal. The canonical serialization is:
-
Translate surface → typed core.
-
Serialize the typed core as canonical JSON per RFC 8785 (JCS): keys sorted, no insignificant whitespace, UTF-8, shortest number forms.
-
For every
Opaquenode, substitute the fieldbyteswith itsopaque_hash(Section 9.2) so that payload bytes are committed by reference, not inlined. -
doc_hash = "sha256:" + lowerhex( SHA-256( canonical_json ) ).
This makes the document hash stable under surface reformatting while remaining sensitive to any change in structure, identifiers, references, or payloads.
-
A base record’s
hashfield (Section 7.2) is theopaque_hash(Section 9.2) of the artefact named byartefact_ref, computed over that artefact’s exact bytes. -
A profile registry entry’s
hash(Section 8.5) pins the definition by theopaque_hash(Section 9.2) of the definition file’s exact bytes. (Pinning the file bytes — rather than thedoc_hashof Section 9.3 — keeps the registry verifiable with a stocksha256sumbefore the document canonicaliser is deployed. The registry MUST state which form it uses; v1.1 registries use the byte hash.)
The following are RESERVED and MUST be treated as inert in v1.1:
record Signature where
constructor MkSignature
alg : String -- reserved; "ed25519" anticipated
pubkey : String -- reserved (base64)
sig : String -- reserved (base64); over a doc_hash
signed_at : Maybe String -- reserved (RFC 3339)A v1.1 validator MUST NOT require a signature and MUST NOT reject a document that
carries reserved signature fields. Signing semantics (what is signed, trust roots,
rotation) are deferred to a later minor version. What is signed is already pinned:
a signature, when specified, will sign a doc_hash.
|
Note
|
Citation primitives are representable in base A2ML but carry no semantics by default. They are REQUIRED and validated only under a citation profile, which A2ML core does not ship (consumers define their own). This keeps citation machinery available to everyone without making any document "about citations" unless it opts in. |
| Directive | Form | Carries |
|---|---|---|
|
inline |
|
|
block |
free prose explaining why a cited claim is relied upon. |
|
inline |
provenance of a claim: |
|
inline |
a standalone |
|
inline |
a standalone |
@source_span and @canonical_node are the same located-region and structural-
address notions as the base record’s fields (Section 7), surfaced as standalone
directives so that prose can point at code without wrapping a whole @record.
With no citation profile active:
-
All five directives parse and are retained in the typed core.
-
@cite(key=…)does not requirekeyto resolve to a@refsentry. -
No cross-reference, completeness, or provenance check is applied.
They are, in base mode, structured annotations — nothing more.
A citation profile (defined by a consumer, not by A2ML core) MAY require, for
example: that every @cite(key) resolves; that every cited claim carries an
@origin; that spans are well-formed and in-bounds. Such a profile is an ordinary
profile (Section 8) and is subject to all profile prohibitions (no execution, no
relaxation of base invariants).
The a2ml/ profile namespace is reserved by this repository. v1.1 ships the
seven a2ml/ profiles for the descriptiles metadata family:
a2ml/state, a2ml/meta, a2ml/ecosystem, a2ml/agentic, a2ml/neurosym,
a2ml/playbook, a2ml/anchor.
Their definitions live under a2ml/profiles/ and are indexed in
a2ml/profiles/REGISTRY.a2ml.
Other components within this repository MAY register additional a2ml/
profiles in their own subtrees, each with its own definition file and registry
entry. A2ML core neither enumerates nor depends on them: it ships only the
mechanism (Section 8) and the seven descriptiles profiles above. No namespace other than
a2ml/ is defined by A2ML core.
Opaque payloads may contain arbitrary content. Renderers MUST escape/sanitize for
the target format (HTML: <script>, <iframe>; LaTeX: \input, \write).
Implementations SHOULD limit directive nesting depth (recommended: 100) and opaque payload size.
Checked mode MUST detect @requires cycles. Profile resolution (Section 8.3) MUST
detect cycles in profile composition and reject them.
Only SHA-256 is defined in v1.1, written sha256:. The prefix is a hash-agility
hook: future minor versions MAY define additional algorithms behind new prefixes.
A validator MUST reject an unrecognised prefix in checked mode rather than guessing.
Proposed media type application/vnd.a2ml; file extension .a2ml; no magic number;
fragment identifier #section-id. See the separate IANA registration document.
Reference implementation: the Idris2 core under src/A2ML/. Third-party
implementations MUST pass the conformance suite (docs/CONFORMANCE.adoc,
tests/vectors/). Rendering targets (HTML5, LaTeX/PDF, Markdown) are unchanged
from v1.0; Markdown remains lossy (proof obligations and hashes not preserved).
-
SemVer for specs. Additive changes (new inert directives, new profiles, new invariants that do not invalidate prior-conforming documents) are MINOR bumps.
-
Breaking changes are a MAJOR bump and an era change; "v2" is a roadmap heading, not a near-term plan.
-
Lineage convention per spec directory: one
SPEC.adoc(current normative),archive/(frozen prior versions),VERSIONS.adoc(lineage + era). SeeVERSIONS.adoc.
The complete EBNF is in docs/GRAMMAR.adoc; Section 2 is normative where the two
differ.
-
Add the profile mechanism:
@profiledeclaration,@profile-defdefinition format, resolution, and the SSOT + hash-pinned registry (Section 8, Section 11). -
Add the base record vocabulary
@record— the anti-desync primitive (Section 7). -
Add citation primitives
@cite,@rationale,@origin,@source_span,@canonical_node— inert without a citation profile (Section 10). -
Add the canonical hash form for opaque payloads and documents; reserve signing (Section 9).
-
Add self-closing (inline) directive syntax and
QualifiedId(Section 2). -
No change invalidates a v1.0-conforming document.
| Directive | Form | Since | Section |
|---|---|---|---|
|
block |
v1.0 |
2.4 |
|
block |
v1.0 |
2.4 |
|
block |
v1.0 |
2.4 |
|
block |
v1.0 |
2.4 |
|
block |
v1.0 |
2.4 / 5 |
|
block |
v1.0 |
2.4 |
|
inline |
v1.0 |
2.3 |
|
inline |
v1.1 |
8.1 |
|
block |
v1.1 |
8.4 |
|
block |
v1.1 |
7 |
|
inline |
v1.1 |
10 |
|
block |
v1.1 |
10 |
|
inline |
v1.1 |
10 |
|
inline |
v1.1 |
10 / 7.4 |
|
inline |
v1.1 |
10 / 7.2 |
Version: 1.1.0
Status: Stable
Era: v1
Date: 2026-06-03
Lineage: VERSIONS.adoc