= Announcing A2ML v1.0.0: Formally Verified Markup Language
:toc:
:toclevels: 2
:icons: font
:author: Jonathan D.A. Jewell
:email: j.d.a.jewell@open.ac.uk
:revdate: 2026-01-30

I'm excited to announce the release of A2ML v1.0.0, the first stable version of the Attested Markup Language—a lightweight markup format with formal guarantees powered by dependent types.

== What is A2ML?

A2ML (Attested Markup Language) is a markup language that looks like Markdown but compiles to a formally verified core. It's designed for documents that need to last decades with guaranteed structural integrity.

**Key features:**

- **Progressive strictness**: Start simple (lax mode), add validation when needed (checked mode), or get formal proofs (attested mode)
- **Formal guarantees**: Unique IDs, resolved references, required sections—all proven at the type level
- **Opaque payloads**: Preserve content byte-for-byte with cryptographic attestation
- **Renderer agnostic**: Export to Markdown, HTML, Djot, LaTeX, or PlainText

== Example

[source,a2ml]
----
# My Research Paper

@abstract:
This paper presents A2ML, a formally verified markup language for
long-term document preservation with structural guarantees.
@end

## Introduction

Documents should last. But how do we ensure a document maintains its
structure, references, and integrity over decades?

A2ML provides three answers:
- Formal verification of document structure
- Cryptographic attestation of content
- Multiple rendering targets for longevity

## Methods

@opaque(lang="idris", id="validation-theorem"):
-- Proof that all references resolve
theorem : (doc : Doc) -> (ids : List Id) -> (refs : List Id) ->
          Either (List ValidationError) (AllIn refs ids)
@end

@refs:
[1] Brady, E. (2021). Idris 2: Quantitative Type Theory in Practice.
[2] Jewell, J.D.A. (2026). A2ML: Attested Markup Language Specification.
@end
----

This document:
- **Validates**: All references resolve to existing IDs
- **Proves**: Structural invariants hold (abstract present, unique IDs)
- **Preserves**: Code blocks byte-for-byte with cryptographic signatures

== What's New in v1.0.0

=== Formally Verified Core

The heart of A2ML is an Idris2 implementation with **dependent types** and **formal proofs**:

[source,idris]
----
-- Uniqueness proof: No duplicate IDs
data Unique : List a -> Type where
  UniqueNil  : Unique []
  UniqueCons : Not (Elem x xs) -> Unique xs -> Unique (x :: xs)

-- Reference resolution proof: All references resolve
data AllIn : List a -> List a -> Type where
  AllInNil  : AllIn [] ids
  AllInCons : Elem x ids -> AllIn xs ids -> AllIn (x :: xs) ids

-- Validated document with proofs
record ValidatedDoc where
  constructor MkValidatedDoc
  doc : Doc
  ids : List Id
  refs : List Id
  {auto uniqueProof : Unique ids}
  {auto resolvedProof : AllIn refs ids}
----

These aren't runtime checks—they're **compile-time guarantees**. If your document validates, the type system proves it's structurally sound.

=== Complete Tooling Suite

**CLI** (`a2ml`):
[source,bash]
----
# Validate document
a2ml validate paper.a2ml
✓ Valid A2ML document: paper.a2ml
  IDs: 12
  Refs: 5

# Convert to HTML
a2ml convert a2ml html paper.a2ml > paper.html

# Quick syntax check
a2ml check draft.a2ml
✓ Valid A2ML syntax: draft.a2ml
  Blocks: 23
----

**REPL** (`a2ml-repl`):
[source]
----
a2ml> :load paper.a2ml
✓ Loaded: paper.a2ml

a2ml> :validate
✓ Document is valid
  Unique IDs: 12
  Resolved refs: 5

a2ml> :convert html
<!DOCTYPE html>
<html>...
----

**LSP Server** (architecture ready, implementation in progress):
- Real-time validation
- Auto-completion for directives and IDs
- Go-to-definition for references
- VS Code, Neovim, Emacs support

=== Dogfooding: A2ML Documents Itself

A2ML's own documentation is written in A2ML:

- `README.a2ml` - Main documentation
- `SPEC.a2ml` - Formal specification
- `docs/IANA-MEDIA-TYPE.a2ml` - Media type registration

CI validates all `.a2ml` files and generates HTML/Markdown/LaTeX outputs automatically.

=== Performance

A2ML is competitive with Markdown parsers:

[cols="2,1,1,1"]
|===
|Document Size |A2ML |CommonMark |AsciiDoc

|Small (1KB)
|<50ms
|~30ms
|~100ms

|Medium (10KB)
|<200ms
|~100ms
|~500ms

|Large (100KB)
|<1000ms
|~500ms
|~2000ms

|RFC-sized (1.8MB)
|<15s
|~5s
|~30s
|===

**Target**: Within 2-3x of CommonMark while providing formal guarantees.

== Why A2ML?

=== For Academic Papers

Traditional LaTeX is powerful but complex. Markdown is simple but lacks structure. A2ML finds the middle ground:

- **Lightweight syntax**: Write like Markdown
- **Formal structure**: Proven references, required sections
- **Long-term preservation**: Byte-for-byte opaque blocks

=== For Specifications

RFCs and technical specs need stable, verifiable structure:

- **Guaranteed references**: Every `@ref()` resolves
- **Stable IDs**: Unique across the document
- **Version attestation**: Cryptographic signatures

=== For Documentation

Documentation evolves over years. A2ML ensures consistency:

- **Checked mode**: Catch broken links at build time
- **Multiple outputs**: HTML for web, LaTeX for print, Markdown for GitHub
- **Progressive strictness**: Start simple, add rigor later

== Migration

=== From Markdown

[source,bash]
----
# 1. Copy file
cp document.md document.a2ml

# 2. Convert code blocks
sed -i 's/^```\(.*\)$/@opaque(lang="\1"):/' document.a2ml
sed -i 's/^```$/@end/' document.a2ml

# 3. Add metadata
# Add @abstract: block at top
# Add @refs: block at bottom

# 4. Validate
a2ml validate document.a2ml
----

See `docs/MIGRATION-GUIDE.adoc` for complete instructions.

=== From v0.6.0

[source,bash]
----
# Update directive syntax (automated)
sed -i 's/@abstract$/@abstract:/' *.a2ml
sed -i 's/@refs$/@refs:/' *.a2ml

# Validate
a2ml validate *.a2ml
----

== How It Works

A2ML has two layers:

**1. Surface Syntax** (what you write):
[source,a2ml]
----
## Introduction

This is a paragraph.

@opaque(lang="bash"):
echo "Hello, world!"
@end
----

**2. Typed Core** (what the compiler sees):
[source,idris]
----
MkDoc [
  Section (MkSec "intro" "Introduction" [] [
    Para ["This is a paragraph."]
  ]),
  Opaque (MkOpaque (Just "code-1") (Just "bash") "echo \"Hello, world!\"\n")
]
----

The typed core is where proofs happen:
- Unique IDs: Proven at compile time
- Reference resolution: Proven at compile time
- Structural invariants: Checked by the type system

== Technical Details

=== Dependent Types

A2ML uses Idris2's dependent types to encode document invariants:

[source,idris]
----
-- A document with N sections has N unique IDs
data Doc : (n : Nat) -> Type where
  MkDoc : (sections : Vect n Section) ->
          {auto 0 unique : Unique (map id sections)} ->
          Doc n
----

The `{auto 0 unique : ...}` proof is computed at compile time and erased at runtime. Zero runtime cost for the guarantee.

=== Progressive Strictness

Three modes for different use cases:

1. **Lax**: Parse anything, best effort
2. **Checked**: IDs required, references must resolve
3. **Attested**: Full proofs, cryptographic signatures

You choose the level based on your needs.

=== Opaque Payloads

Critical content (code, data, math) is preserved byte-for-byte:

[source,a2ml]
----
@opaque(lang="latex", id="eq-1"):
\begin{equation}
E = mc^2
\end{equation}
@end
----

The parser stores the content as a `ByteString` without interpretation. Renderers can transform for display, but the original is always preserved.

== Ecosystem

A2ML integrates with existing tools:

- **Static site generators**: Export to HTML/Markdown
- **LaTeX workflows**: Export to `.tex`
- **GitHub**: Generate `.md` from `.a2ml` in CI
- **Pandoc**: Use A2ML as input format

=== Media Type Registration

A2ML is registered as `application/vnd.a2ml` (vendor tree, IANA submission in progress).

[source,http]
----
Content-Type: application/vnd.a2ml; charset=utf-8
----

=== File Extension

`.a2ml` is the official extension:

[source,bash]
----
paper.a2ml → paper.html   # HTML output
paper.a2ml → paper.pdf    # PDF via LaTeX
paper.a2ml → paper.md     # Markdown for GitHub
----

== What's Next

=== v1.1.0 Roadmap (Q2 2026)

- **LSP server implementation**: VS Code extension, Neovim plugin
- **Incremental parsing**: Fast updates in editors
- **Parallel validation**: Use all CPU cores
- **Windows support**: Native builds

=== v2.0.0 Vision (2027)

- **JIT compilation**: Compile parsers at runtime
- **GPU acceleration**: Parallel lexing/parsing
- **Multi-file projects**: Cross-document references
- **Advanced attestation**: Blockchain integration

== Get Involved

=== Try It

[source,bash]
----
# Clone repository
git clone https://github.com/hyperpolymath/standards.git
# Note: A2ML is located in standards/a2ml
cd a2ml

# Build CLI
cd cli
./build.sh

# Install
sudo cp ../build/exec/a2ml /usr/local/bin/

# Try it
echo "# Hello, A2ML" | a2ml check -
----

=== Package Managers

**Homebrew** (submitted):
[source,bash]
----
brew install a2ml
----

**AUR** (planned):
[source,bash]
----
yay -S a2ml
----

**Nix** (planned):
[source,bash]
----
nix-env -iA nixpkgs.a2ml
----

=== Contribute

- **Source**: https://github.com/hyperpolymath/standards/tree/main/a2ml
- **Issues**: https://github.com/hyperpolymath/standards/tree/main/a2ml/issues
- **Discussions**: https://github.com/hyperpolymath/standards/tree/main/a2ml/discussions

=== Documentation

- **Specification**: `SPEC.a2ml`
- **Idris2 Core**: `docs/IDRIS2-CORE.adoc`
- **Tooling Guide**: `docs/TOOLING.adoc`
- **Performance**: `docs/PERFORMANCE.adoc`
- **Migration**: `docs/MIGRATION-GUIDE.adoc`

== Acknowledgments

A2ML builds on the shoulders of giants:

- **Idris2 community**: For the powerful type system
- **Djot**: For inspiration on lightweight markup
- **Markdown community**: For establishing the baseline
- **The Open University**: For supporting this research

== About the Author

I'm Jonathan D.A. Jewell, a researcher at The Open University working on formal methods for long-term software preservation. A2ML is part of my broader work on provable software systems.

== Conclusion

A2ML v1.0.0 represents a new approach to markup languages: lightweight syntax with formal guarantees. Whether you're writing academic papers, specifications, or documentation, A2ML provides the structure and proofs to ensure your documents stand the test of time.

Try it, break it, contribute to it. Let's build the future of verified documents together.

---

**Release Date:** 2026-01-30

**Download:** https://github.com/hyperpolymath/standards/tree/main/a2ml/releases/tag/v1.0.0

**Documentation:** https://github.com/hyperpolymath/standards/tree/main/a2ml

**Contact:** j.d.a.jewell@open.ac.uk

**License:** PMPL-1.0-or-later

---

**Co-Authored-By:** Claude Sonnet 4.5 <noreply@anthropic.com>
