AGENTS.md@src/gnn/formal_specs git:20260213.b9e0b79A

Immutable. This exact content is served forever at /api/v1/blob/e0133bcc40501ede.

# GNN Formal Specifications Module

## Purpose

This module contains **formal mathematical specifications** of GNN models in 8 different proof and specification languages. These provide machine-verifiable foundations for the GNN type system and model structure.

## Formal Specification Files

| File | Language | Focus |
|------|----------|-------|
| `isabelle_spec.thy` | Isabelle/HOL | Higher-order logic formalization of GNN types |
| `lean_spec.lean` | Lean 4 | Dependent type verification of GNN models |
| `coq_spec.v` | Coq | Constructive proof of GNN properties |
| `agda_spec.agda` | Agda | Dependently-typed GNN specification |
| `alloy_spec.als` | Alloy | Relational model checking for GNN constraints |
| `z_spec.zed` | Z-notation | Set-theoretic specification of GNN semantics |
| `tlaplus_spec.tla` | TLA+ | Temporal logic specification of GNN state machines |
| `maxima_spec.mac` | Maxima | Symbolic computation verification |

## Integration Points

- **Parsers** (`gnn/parsers/`): Each formal language has a corresponding parser (e.g., `lean_parser.py`, `coq_parser.py`, `isabelle_parser.py`)
- **Serializers** (`gnn/parsers/`): Each formal language has a corresponding serializer for round-trip conversion
- **Type Systems** (`gnn/type_systems/`): Scala and Haskell type system implementations complement these formal specs

## For AI Agents

1. Use these specs as the **ground truth** for GNN model structure and constraints
2. Each spec can be used to verify that parser output conforms to the formal model
3. All 8 formats achieve 100% round-trip fidelity via the embedded data architecture