> ## Documentation Index
> Fetch the complete documentation index at: https://docs.fased.ai/llms.txt
> Use this file to discover all available pages before exploring further.

# Formal Verification (Security Models)

# Formal Verification (Security Models)

This page tracks optional Fased **formal security models** (TLA+/TLC today; more
as needed).

**Goal (north star):** provide a machine-checked argument that Fased enforces its
intended security policy (authorization, session isolation, tool gating, and
misconfiguration safety), under explicit assumptions.

For product-facing setup guidance, start with [Security Overview](/security).
The formal models below cover bounded claims; they do not replace runtime
configuration review in Agent, Wallets, Usage, Logs, or Advanced.

**What this is (today):** an executable, attacker-driven **security regression suite**:

* Each claim has a runnable model-check over a finite state space.
* Many claims have a paired **negative model** that produces a counterexample
  trace for a realistic bug class.

**What this is not (yet):** a proof that “Fased is secure in all respects” or
that the full TypeScript implementation is correct.

## Where the models live

Models are maintained as optional external research artifacts:
[vignesh07/fased-formal-models](https://github.com/vignesh07/fased-formal-models).
The Fased TypeScript code and tests in this repository remain the implementation
source of truth.

## Important caveats

* These are **models**, not the full TypeScript implementation. Drift between
  model and code is possible.
* Results are bounded by the state space explored by TLC; “green” does not imply
  security beyond the modeled assumptions and bounds.
* Some claims rely on explicit environmental assumptions, such as correct
  deployment and correct configuration inputs.

## Reproducing results

Today, results are reproduced by cloning the models repo locally and running TLC.
A future iteration could offer:

* CI-run models with public artifacts (counterexample traces, run logs)
* a hosted “run this model” workflow for small, bounded checks

Getting started:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
git clone https://github.com/vignesh07/fased-formal-models
cd fased-formal-models

# Java 11+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>
```

### Gateway exposure and open gateway misconfiguration

**Claim:** binding beyond loopback without auth can increase exposure and make
remote compromise possible. Token/password auth blocks unauthenticated attackers
under the model assumptions.

* Green runs:
  * `make gateway-exposure-v2`
  * `make gateway-exposure-v2-protected`
* Red (expected):
  * `make gateway-exposure-v2-negative`

See also: `docs/gateway-exposure-matrix.md` in the models repo.

### Nodes.run pipeline (highest-risk capability)

**Claim:** `nodes.run` requires both node command allowlist/declaration and live
approval when configured. Approvals are tokenized to prevent replay in the
model.

* Green runs:
  * `make nodes-pipeline`
  * `make approvals-token`
* Red (expected):
  * `make nodes-pipeline-negative`
  * `make approvals-token-negative`

### Agent tool and skill gates

**Claim target:** installing or configuring a skill should not imply Agent
access, tool access, or wallet authority. Agent skill allowlists, Agent > Tools
policy, and Wallet > Skill Grants should be modeled as separate gates.

Status: model target identified; not yet represented as a published TLC target.

### Wallet and mining authority

**Claim target:** generic skills can use only explicitly granted Agent-role
wallets. Mining and Vault wallet roles remain unavailable to generic skills, and
SAT mining uses the mining runtime policy.

Status: model target identified; not yet represented as a published TLC target.

### Pairing store (DM gating)

**Claim:** pairing requests respect TTL and pending-request caps.

* Green runs:
  * `make pairing`
  * `make pairing-cap`
* Red (expected):
  * `make pairing-negative`
  * `make pairing-cap-negative`

### Ingress gating (mentions + control-command bypass)

**Claim:** in group contexts requiring mention, an unauthorized “control command” cannot bypass mention gating.

* Green:
  * `make ingress-gating`
* Red (expected):
  * `make ingress-gating-negative`

### Routing/session-key isolation

**Claim:** DMs from distinct peers do not collapse into the same session unless explicitly linked/configured.

* Green:
  * `make routing-isolation`
* Red (expected):
  * `make routing-isolation-negative`

## v1++: additional bounded models (concurrency, retries, trace correctness)

These are follow-on models that tighten fidelity around real-world failure
modes: non-atomic updates, retries, and message fan-out.

### Pairing store concurrency / idempotency

**Claim:** a pairing store should enforce `MaxPending` and idempotency even under
interleavings. In practice, “check-then-write” must be atomic/locked, and refresh
should not create duplicates.

What it means:

* Under concurrent requests, you can’t exceed `MaxPending` for a channel.

* Repeated requests/refreshes for the same `(channel, sender)` should not create duplicate live pending rows.

* Green runs:
  * `make pairing-race` (atomic/locked cap check)
  * `make pairing-idempotency`
  * `make pairing-refresh`
  * `make pairing-refresh-race`

* Red (expected):
  * `make pairing-race-negative` (non-atomic begin/commit cap race)
  * `make pairing-idempotency-negative`
  * `make pairing-refresh-negative`
  * `make pairing-refresh-race-negative`

### Ingress trace correlation / idempotency

**Claim:** ingestion should preserve trace correlation across fan-out and be idempotent under provider retries.

What it means:

* When one external event becomes multiple internal messages, every part keeps the same trace/event identity.

* Retries do not result in double-processing.

* If provider event IDs are missing, dedupe falls back to a safe key (e.g., trace ID) to avoid dropping distinct events.

* Green:
  * `make ingress-trace`
  * `make ingress-trace2`
  * `make ingress-idempotency`
  * `make ingress-dedupe-fallback`

* Red (expected):
  * `make ingress-trace-negative`
  * `make ingress-trace2-negative`
  * `make ingress-idempotency-negative`
  * `make ingress-dedupe-fallback-negative`

### Routing dmScope precedence + identityLinks

**Claim:** routing must keep DM sessions isolated by default, and only collapse
sessions when explicitly configured through channel precedence + identity links.

What it means:

* Channel-specific dmScope overrides must win over global defaults.

* identityLinks should collapse only within explicit linked groups, not across unrelated peers.

* Green:
  * `make routing-precedence`
  * `make routing-identitylinks`

* Red (expected):
  * `make routing-precedence-negative`
  * `make routing-identitylinks-negative`