lean4agent/README.md

Lean4Agent — a11oy workflow-invariant formalization (ROADMAP / EXPERIMENTAL)

Status: ROADMAP. This directory is a scaffold that formalizes the safety invariants of the a11oy governed-agent workflow in Lean 4. It is not a completed machine-checked verification yet. The UI and docs render these invariants as "ROADMAP — statements formalized, proofs in progress" and must never describe them as "verified" until lake build passes with zero sorry.

Inspired by Lean4Agent (arXiv:2606.06523), which formalizes agent workflow invariants in Lean 4.

Files

• WorkflowInvariants.lean — the irreducible governed-decision pipeline (gate → lambda → recommend → sign → replay) and 5 safety invariants:
  • INV 1 destructive_unapproved_denied — proved (no sorry)
  • INV 2 injection_always_denied — proved
  • INV 3 oversize_denied — proved
  • INV 4 canonical_pipeline_policy_first — ROADMAP (sorry)
  • INV 5 replay_is_deterministic — ROADMAP (placeholder statement)

These mirror the runtime enforcement points: the _a11oy_arena_inspect threat gate and the Colang ROE flows in policy/colang/roe_core.co.

Roadmap to "verified"

1. Add lakefile.lean + pin a Lean toolchain (lean-toolchain).
2. Discharge INV 4 and INV 5 (remove every sorry).
3. Add a CI job that runs lake build and fails on any sorry / axiom.
4. Emit a build manifest; the Eval/Policy tab then cites "N/M a11oy workflow invariants machine-checked, as-of ".

Until step 3 is green, the honest claim is: 3 of 5 invariant statements are proved in isolation; the full-pipeline and determinism theorems are roadmap.