# Proof Spec: gitbot-fleet
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

**Repo Path**: `/var/mnt/eclipse/repos/gitbot-fleet`
**Tier**: T2 — High
**Total Theorems**: 4
**Primary Prover(s)**: Idris2 (2), TLA+ (2)
**Existing Proof Coverage**: 0 (shell + Rust, no formal proofs)

## Status Tracker

| # | Theorem | Prover | Status | Verified |
|---|---------|--------|--------|----------|
| 1 | GF1 Confidence threshold gating | I2 | [ ] Pending | — |
| 2 | GF2 Fix script idempotence | I2 | [ ] Pending | — |
| 3 | GF3 Bot action isolation | TLA | [ ] Pending | — |
| 4 | GF4 No-secrets discipline | TLA | [ ] Pending | — |

## Context

6 bots (rhodibot, echidnabot, sustainabot, glambot, seambot, finishbot) coordinated via safety triangle (eliminate ≥0.95, substitute ≥0.85, control <0.85).

### Key files
- `robot-repo-automaton/src/lib.rs` (forbids unsafe)
- `fleet-coordinator.sh` (24KB orchestration)
- `robot-repo-automaton/src/confidence.rs`
- `robot-repo-automaton/src/fixer.rs`
- `scripts/fix-believe-me.sh`

## Theorems to Prove

### GF1: Confidence threshold gating

**Target**: `verification/proofs/idris2/ThresholdGate.idr`
**Priority**: P0

**Statement**: Actions only dispatched when confidence ≥ threshold for tier.

**Obligations**:
- [ ] Model threshold check
- [ ] Prove no-bypass

---

### GF2: Fix script idempotence

**Target**: `verification/proofs/idris2/FixIdem.idr`
**Priority**: P0

**Statement**: Re-running fix script produces identical state.

**Obligations**:
- [ ] Model fix as pure function
- [ ] Prove `fix(fix(s)) = fix(s)`

---

### GF3: Bot action isolation

**Target**: `verification/proofs/tlaplus/BotIsolation.tla`
**Priority**: P1

**Statement**: No cross-contamination between bots' actions on same repo.

**Obligations**:
- [ ] Model bot fleet + locks
- [ ] Model-check mutex

---

### GF4: No-secrets discipline

**Target**: `verification/proofs/tlaplus/NoSecrets.tla`
**Priority**: P2

**Statement**: No hardcoded secrets; all env vars use `${VAR:-}` defaults.

**Obligations**:
- [ ] Grep scan
- [ ] Prove zero hardcoded matches

---

## Verification Commands

```bash
cd /var/mnt/eclipse/repos/gitbot-fleet
just proof-check-all
```

## Handoff Checklist

- [ ] All 4 proven
- [ ] Commit: `proof: complete gitbot-fleet proofs (4/4)`
