0-AI-MANIFEST.a2ml

# STOP - CRITICAL READING REQUIRED

**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**

## WHAT IS THIS?

This is the AI manifest for **tlaiser**. It declares:
- Canonical file locations (where things MUST be, and nowhere else)
- Critical invariants (rules that must NEVER be violated)
- Repository structure and organization

**tlaiser** extracts state machine specifications from existing code and
model-checks them with TLA+/PlusCal. TLA+ (by Leslie Lamport) is the gold
standard for specifying and verifying concurrent/distributed systems. PlusCal
is its imperative-style front-end. The TLC model checker exhaustively explores
all possible states to find invariant violations and liveness failures.

Pipeline: source code -> state machine extraction -> TLA+/PlusCal spec
generation -> TLC model checking -> invariant violation report.

## CANONICAL LOCATIONS (UNIVERSAL RULE)

### Machine-Readable Metadata: `.machine_readable/` ONLY

These 6 a2ml files MUST exist in `.machine_readable/6a2/` directory ONLY:
1. **STATE.a2ml** - Project state, progress, blockers
2. **META.a2ml** - Architecture decisions, governance
3. **ECOSYSTEM.a2ml** - Position in -iser ecosystem, relationships
4. **AGENTIC.a2ml** - AI agent interaction patterns
5. **NEUROSYM.a2ml** - Neurosymbolic/Hypatia integration config
6. **PLAYBOOK.a2ml** - Operational runbook

**CRITICAL:** If ANY of these files exist in the root directory, this is an ERROR.

### Anchor File: `.machine_readable/anchors/ANCHOR.a2ml` ONLY

Canonical authority and semantic-boundary declaration MUST exist at:

` .machine_readable/anchors/ANCHOR.a2ml `

Do not place `ANCHOR.a2ml` at repository root.

### Maintenance Policies: `.machine_readable/policies/` ONLY

Canonical maintenance/governance files MUST exist under:

` .machine_readable/policies/ `

Minimum required files:
- `MAINTENANCE-AXES.a2ml`
- `MAINTENANCE-CHECKLIST.a2ml`
- `SOFTWARE-DEVELOPMENT-APPROACH.a2ml`

Do not place maintenance policy files in repository root.

### Bot Directives: `.machine_readable/bot_directives/` ONLY

Bot-specific instructions for automated agents.

### Contractiles: `.machine_readable/contractiles/` ONLY

Policy enforcement contracts (k9, dust, lust, must, trust).

### AI Configuration & Guides: `.machine_readable/ai/` ONLY

- `AI.a2ml` - Language-specific or LLM-specific patterns
- `PLACEHOLDERS.md` - Bootstrap guide

### Community & Forge Metadata: `.github/` ONLY

- `CODEOWNERS` - Review assignments
- `MAINTAINERS` - Machine-readable contact list
- `SUPPORT` - Support channels
- `SECURITY.md` - Technical security policy
- `CONTRIBUTING.md` - Technical contribution manual
- `CODE_OF_CONDUCT.md` - Conduct rules

### Agent Instructions

- `0-AI-MANIFEST.a2ml` - THIS FILE (universal entry point)

## DOMAIN CONTEXT

### TLA+ / PlusCal / TLC

- **TLA+**: Temporal Logic of Actions — formal specification language for
  concurrent and distributed systems, created by Leslie Lamport
- **PlusCal**: Imperative-style front-end that compiles to TLA+
- **TLC**: Model checker that exhaustively explores all reachable states
- **Temporal operators**: Box (always), Diamond (eventually), LeadsTo
- **Properties**: Safety (bad things never happen), Liveness (good things
  eventually happen), Fairness (enabled actions eventually execute)

### Key Types (defined in src/interface/abi/Types.idr)

- `StateMachine` — states, transitions, guards, actions, initial state
- `TemporalFormula` — Box/Diamond/LeadsTo/WeakFairness/StrongFairness
- `SafetyProperty` — invariants checked as Box(P)
- `LivenessProperty` — progress checked as Diamond(P) or P LeadsTo Q
- `Invariant` — state predicate that must hold in every reachable state
- `ModelCheckResult` — pass/safety-violation/liveness-violation/deadlock

## CORE INVARIANTS

1. **No state file duplication** - Root must NOT contain STATE.a2ml, META.a2ml, etc.
2. **Single source of truth** - `.machine_readable/` is authoritative
3. **No stale metadata** - If root state files exist, they are OUT OF DATE
4. **License consistency** - All code MPL-2.0 unless platform requires MPL-2.0
5. **Author attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
6. **Container images** - MUST use Chainguard base (`cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`)
7. **Container runtime** - Podman, never Docker. Files are `Containerfile`, never `Dockerfile`
8. **Container orchestration** - `selur-compose`, never `docker-compose`
9. **ABI-FFI standard** - Idris2 for ABI proofs, Zig for FFI C-ABI bridge
10. **No banned patterns** - No believe_me, assert_total, unsafeCoerce, sorry, Admitted, Obj.magic

## REPOSITORY STRUCTURE

```
tlaiser/
├── 0-AI-MANIFEST.a2ml         # THIS FILE (start here)
├── README.adoc                 # TLA+ model checking orientation
├── ROADMAP.adoc                # Phase 0-6 development plan
├── CONTRIBUTING.adoc           # Human contribution guide
├── Justfile                    # Task runner
├── Cargo.toml                  # Rust project manifest
├── Containerfile               # OCI build (Chainguard base)
├── LICENSE                     # MPL-2.0
├── src/                        # Source code
│   ├── main.rs                 # CLI (init/validate/generate/build/run/info)
│   ├── lib.rs                  # Library API
│   ├── manifest/               # tlaiser.toml parser
│   ├── codegen/                # TLA+/PlusCal spec generation
│   ├── core/                   # State machine IR, extraction engine
│   ├── definitions/            # TLA+ property definitions
│   ├── errors/                 # Error types and diagnostics
│   └── interface/              # Verified Interface Seams
│       ├── abi/                # Idris2 ABI (Types, Layout, Foreign)
│       ├── ffi/                # Zig FFI (libtlaiser C-ABI bridge)
│       └── generated/          # Auto-generated C headers
├── docs/                       # Documentation
│   └── architecture/           # TOPOLOGY.md, diagrams
├── .machine_readable/          # ALL machine-readable metadata
│   └── 6a2/                    # STATE/META/ECOSYSTEM/AGENTIC/NEUROSYM/PLAYBOOK
├── examples/                   # Example tlaiser.toml manifests
├── tests/                      # Rust integration tests
├── verification/               # Formal verification artifacts
└── container/                  # Stapeln container ecosystem
```

## SESSION STARTUP CHECKLIST

- Read THIS file (0-AI-MANIFEST.a2ml) first
- Understand canonical location: `.machine_readable/`
- State understanding of canonical locations
- Read .machine_readable/6a2/STATE.a2ml for current project state

## ATTESTATION PROOF

**"I have read the AI manifest for tlaiser. All machine-readable content (state files, anchors, policies, bot directives, contractiles, AI guides) is located in `.machine_readable/` ONLY, and community metadata is in `.github/`. I will not create duplicate files in the root directory."**