docs: bespoke architecture, roadmap, topology, and ABI definitions for alloyiser

Replace all template placeholders with alloyiser-specific content.
Architecture: API spec → Alloy model extraction and verification engine.
Machine-readable files updated with Alloy domain knowledge (SAT solving,
counterexample mapping, scope validation, JVM runtime dependency).
AI manifest resolved from template to alloyiser-specific.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,12 +1,11 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# AGENTIC.a2ml — AI agent constraints and capabilities
-# Defines what AI agents can and cannot do in this repository.
+# AGENTIC.a2ml — AI agent constraints and capabilities for alloyiser
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [agent-permissions]
 can-edit-source = true
@@ -22,6 +21,18 @@ can-create-files = true
 # - Never use banned languages (TypeScript, Python, Go, etc.)
 # - Never place state files in repository root (must be in .machine_readable/)
 # - Never use AGPL license (use PMPL-1.0-or-later)
+# - Never generate invalid Alloy syntax in .als templates
+# - Never hardcode Alloy JAR paths (must come from alloyiser.toml or environment)
+# - Never skip counterexample mapping (raw Alloy atoms are not user-facing)
+
+[domain-knowledge]
+# Alloy-specific context for AI agents:
+# - Alloy uses relational logic, not first-order logic
+# - `sig` = entity type, `field` = relation, `fact` = invariant
+# - `check` runs SAT solver to find counterexamples to assertions
+# - `run` generates satisfying instances (for visualisation)
+# - Scope bounds: Alloy checks all states up to N instances per sig
+# - Kodkod translates Alloy constraints to SAT; SAT4J solves them
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -6,12 +6,14 @@
   (version "0.1.0")
   (name "alloyiser")
   (type "tool")
-  (purpose "Extract formal models from API specs and verify with Alloy")
+  (purpose "Extract formal models from API specifications (OpenAPI, GraphQL, gRPC) and verify invariants using the Alloy Analyzer's SAT solver")
 
   (position-in-ecosystem
     (family "-iser acceleration frameworks")
     (meta-framework "iseriser")
     (relationship "sibling")
+    (domain "formal verification of API designs")
+    (unique-value "bridges API specification formats to Alloy's relational logic — finds design bugs before implementation")
     (top-3 ("typedqliser" "chapeliser" "verisimiser")))
 
   (related-projects
@@ -32,7 +34,23 @@
       (description "Database recovery via constraint propagation"))
     (project "proven"
       (relationship "dependency")
-      (description "Shared Idris2 verified library"))
+      (description "Shared Idris2 verified library — alloyiser uses proven types for model soundness proofs"))
     (project "typell"
       (relationship "dependency")
-      (description "Type theory engine"))))
+      (description "Type theory engine — could power alloyiser's constraint language"))
+    (project "boj-server"
+      (relationship "integration-target")
+      (description "BoJ MCP server — alloyiser will be a cartridge for on-demand spec verification"))
+    (project "panll"
+      (relationship "integration-target")
+      (description "PanLL workspace — alloyiser will provide a panel for visualising Alloy instance graphs")))
+
+  (external-dependencies
+    (dependency "alloy6"
+      (type "runtime")
+      (description "MIT Alloy 6 Analyzer JAR — SAT solving via Kodkod/SAT4J")
+      (url "https://alloytools.org"))
+    (dependency "openapiv3"
+      (type "build")
+      (description "Rust crate for parsing OpenAPI 3.x specifications")
+      (url "https://crates.io/crates/openapiv3"))))

.machine_readable/6a2/META.a2ml

@@ -4,38 +4,53 @@
 
 (meta
   (version "0.1.0")
-  (last-updated "2026-03-20")
+  (last-updated "2026-03-21")
 
   (architecture-decisions
-    (adr "001-iser-pattern"
+    (adr "001-alloy-as-backend"
       (status "accepted")
-      (context "Need to make powerful languages accessible without steep learning curves")
-      (decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
-      (consequences "Users write zero target language code; all complexity in the -iser"))
+      (context "Need a formal verification backend that can find design bugs in API specs without requiring user expertise in formal methods")
+      (decision "Use Alloy 6 (MIT, Daniel Jackson) — relational logic with SAT solving via Kodkod/SAT4J for bounded model checking")
+      (consequences "Alloy is well-established, has a Java API for headless use, and can exhaustively check small scopes. Requires JVM dependency for analyzer."))
 
-    (adr "002-abi-ffi-standard"
+    (adr "002-spec-to-model-pipeline"
       (status "accepted")
-      (context "Need verified interop between Rust CLI, target language, and user code")
-      (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
-      (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
+      (context "Need to transform API specifications into Alloy models without requiring users to learn Alloy syntax")
+      (decision "Pipeline: spec file -> parser -> SpecModel IR -> Alloy codegen -> .als files. Users declare invariants in TOML, alloyiser generates all Alloy code")
+      (consequences "Users never write Alloy directly. Alloyiser maps OpenAPI concepts (schemas, required, refs) to Alloy concepts (sigs, facts, relations) automatically."))
 
-    (adr "003-rsr-template"
+    (adr "003-iser-pattern"
       (status "accepted")
-      (context "Need consistent project structure across 29+ -iser repos")
-      (decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
-      (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
+      (context "Need consistent architecture across the -iser family")
+      (decision "Use manifest-driven code generation: user describes WHAT in alloyiser.toml, tool generates HOW")
+      (consequences "Users write zero Alloy code; all complexity in alloyiser. Same pattern as chapeliser, typedqliser, etc."))
+
+    (adr "004-abi-ffi-standard"
+      (status "accepted")
+      (context "Need verified interop between Rust CLI, Alloy Analyzer (JVM), and user toolchain")
+      (decision "Idris2 ABI for formal proofs of model soundness, Zig FFI for C-ABI bridge")
+      (consequences "Compile-time guarantees that model extraction preserves spec semantics. JVM bridge via JNI or subprocess."))
+
+    (adr "005-counterexample-reports"
+      (status "accepted")
+      (context "Alloy Analyzer counterexamples are XML atoms — not useful to API designers")
+      (decision "Map counterexample atoms back to original spec entities and produce human-readable violation reports with suggested fixes")
+      (consequences "Counterexample 'Pet$0' gets reported as 'The OpenAPI spec allows creating a Pet without an owner field'. Actionable output.")))
 
   (development-practices
-    (language "Rust" (purpose "CLI and orchestration"))
-    (language "Idris2" (purpose "ABI formal proofs"))
-    (language "Zig" (purpose "FFI C-ABI bridge"))
+    (language "Rust" (purpose "CLI orchestration, spec parsing, report generation"))
+    (language "Idris2" (purpose "ABI formal proofs: model extraction soundness"))
+    (language "Zig" (purpose "FFI C-ABI bridge to Alloy Analyzer (JVM)"))
+    (language "Alloy" (purpose "Generated models — .als files for SAT solving"))
     (build-tool "cargo")
     (ci "GitHub Actions (17 workflows)"))
 
   (design-rationale
     (principle "Manifest-driven"
-      (explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
-    (principle "Formally verified bridges"
-      (explanation "Idris2 dependent types prove interface correctness at compile time"))
-    (principle "Zero target language exposure"
-      (explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
+      (explanation "User intent captured in alloyiser.toml; invariants are plain-English names mapped to Alloy expressions"))
+    (principle "Find bugs before code"
+      (explanation "API design bugs (orphaned resources, impossible states, race conditions) are cheaper to fix at spec time than implementation time"))
+    (principle "Formally verified extraction"
+      (explanation "Idris2 dependent types prove that the model extraction preserves specification semantics — the generated Alloy model is faithful to the source spec"))
+    (principle "Actionable counterexamples"
+      (explanation "Reports map Alloy atoms back to spec entities, explain the violation in domain terms, and suggest fixes"))))

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,21 +1,24 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# NEUROSYM.a2ml — Neurosymbolic integration metadata
-# Configuration for Hypatia scanning and symbolic reasoning.
+# NEUROSYM.a2ml — Neurosymbolic integration metadata for alloyiser
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"  # quick | standard | deep
 report-format = "logtalk"
 
 [symbolic-rules]
-# Custom symbolic rules for this project
+# Alloyiser-specific symbolic rules:
 # - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+# - { name = "no-raw-alloy-atoms-in-output", pattern = "\\$\\d+", severity = "warning" }
+#   Counterexample atoms (Pet$0) must be mapped to spec entity names before display.
+# - { name = "scope-bound-check", pattern = "scope\\s*=\\s*0", severity = "error" }
+#   Scope bound of 0 is meaningless — Alloy needs at least 1 instance per sig.
 
 [neural-config]
 # Neural pattern detection settings

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,35 +1,38 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# PLAYBOOK.a2ml — Operational playbook
-# Runbooks, incident response, deployment procedures.
+# PLAYBOOK.a2ml — Operational playbook for alloyiser
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [deployment]
-# method = "gitops"  # gitops | manual | ci-triggered
-# target = "container"  # container | binary | library | wasm
+method = "binary"  # alloyiser ships as a Rust binary; Alloy JAR is a runtime dependency
+target = "binary"  # container | binary | library | wasm
+# Container deployment also available via Containerfile (includes JVM + Alloy JAR)
+
+[runtime-dependencies]
+# Alloy Analyzer requires a JVM (Java 11+)
+# alloyiser invokes java -jar alloy6.jar in headless mode
+# Users can set ALLOY_JAR environment variable or configure in alloyiser.toml
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/6a2/STATE.a2ml for current status
 # 2. Review recent commits and CI results
 # 3. Run `just validate` to check compliance
-# 4. Run `just security` to audit for vulnerabilities
+# 4. Run `just assail` to run panic-attacker pre-commit scan
+# 5. If Alloy codegen produces invalid .als: check src/codegen/ templates
+# 6. If SAT solver times out: reduce scope in alloyiser.toml
 
 [release-process]
-# 1. Update version in STATE.a2ml, META.a2ml, Justfile
-# 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
-# 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
+# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, Justfile
+# 2. Run `just quality` (format + lint + test)
+# 3. Run `just assail` (panic-attacker pre-commit scan)
 # 4. Tag and push
-# 5. Restore local permissions if needed: `just perms-restore`
-# 6. Run `just container-push` if applicable
+# 5. Mirrors propagate to GitLab and Bitbucket automatically
 
 [maintenance-operations]
-# Baseline audit:
-#   just maint-audit
-# Hard release gate:
-#   just maint-hard-pass
-# Permission audit:
-#   just perms-audit
+# Baseline audit: just quality
+# Pre-commit scan: just assail
+# Container build: podman build -f Containerfile -t alloyiser .

.machine_readable/6a2/STATE.a2ml

@@ -5,31 +5,34 @@
 (state
   (metadata
     (version "0.1.0")
-    (last-updated "2026-03-20")
+    (last-updated "2026-03-21")
     (author "Jonathan D.A. Jewell"))
 
   (project-context
     (name "alloyiser")
-    (description "Extract formal models from API specs and verify with Alloy")
+    (description "Extract formal models from API specs (OpenAPI/GraphQL/gRPC) and verify invariants with the Alloy Analyzer via SAT solving")
     (status "scaffold")
     (priority "—")
     (ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
 
   (current-position
     (phase "initial-scaffold")
-    (completion-percentage 5)
-    (milestone "Architecture defined, CLI scaffolded, RSR template complete"))
+    (completion-percentage 8)
+    (milestone "CLI scaffolded, manifest parser working, ABI types specialised for Alloy model constructs, full documentation written"))
 
   (route-to-mvp
-    (step 1 "Replace codegen stubs with target-language-specific generation")
-    (step 2 "Implement Idris2 ABI proofs for core invariants")
-    (step 3 "Build Zig FFI bridge")
-    (step 4 "Integration tests with real-world examples")
-    (step 5 "Documentation and examples"))
+    (step 1 "Phase 1: OpenAPI 3.x parser — extract entities/relations/constraints into SpecModel IR")
+    (step 2 "Phase 2: Alloy codegen — generate .als files with sig/field/fact/assert/check constructs")
+    (step 3 "Phase 3: Alloy Analyzer integration — run SAT solver, parse counterexamples, generate reports")
+    (step 4 "Phase 4: Multi-format support — GraphQL, gRPC .proto, JSON Schema, AsyncAPI")
+    (step 5 "Phase 5: Idris2 proofs — formally prove model extraction preserves spec semantics")
+    (step 6 "Phase 6: Ecosystem — BoJ cartridge, CI/CD action, PanLL panel, VeriSimDB storage"))
 
   (blockers-and-issues
     (none "Project is in scaffold phase — no blockers yet"))
 
   (critical-next-actions
-    (action "Implement codegen for primary use case")
-    (action "Write first working example end-to-end")))
+    (action "Implement OpenAPI 3.x parser in src/core/ using openapiv3 crate")
+    (action "Define SpecModel intermediate representation (entities, relations, constraints)")
+    (action "Write first Alloy codegen: SpecModel -> .als file with basic sigs and facts")
+    (action "Create petstore.yaml example and verify generated .als model loads in Alloy")))

0-AI-MANIFEST.a2ml

@@ -4,7 +4,7 @@
 
 ## WHAT IS THIS?
 
-This is the AI manifest for **[YOUR-REPO-NAME]**. It declares:
+This is the AI manifest for **alloyiser**. It declares:
 - Canonical file locations (where things MUST be, and nowhere else)
 - Critical invariants (rules that must NEVER be violated)
 - Repository structure and organization
@@ -86,7 +86,7 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
 This repo follows the **Dual-Track** architecture:
 
 ```
-[YOUR-REPO-NAME]/
+alloyiser/
 ├── 0-AI-MANIFEST.a2ml         # THIS FILE (start here)
 ├── README.adoc                 # High-level orientation (Rich Human)
 ├── ROADMAP.adoc                # Future direction