Formally Verified Security

Tests check examples. Proofs check everything.

A test suite verifies that specific inputs produce expected outputs. A formal proof examines every possible path through the system and guarantees the property holds universally. There are no edge cases left uncovered.

MultiMail's security properties are verified using Lean 4, the same formal verification language used in pure mathematics research. The Lean type checker mechanically validates each proof step. If the proof compiles, the property is guaranteed — not by our word, but by mathematical law.

Proof 1 — Authorization Model

No API call can access another tenant's data

We modeled all 84 API endpoints and formally proved four properties of the authorization system:

Tenant isolation

Every resource-accessing endpoint verifies tenant ownership.

28 endpoints accept a resource ID (mailbox, email, webhook, domain). Each one checks that the resource belongs to the caller's tenant before returning data or performing any action. The proof is bidirectional — the list is both complete and accurate.

Scope enforcement

Every authenticated endpoint has a scope guard.

All 49 authenticated endpoints have an assigned scope (read, send, admin, or oversight). None are accidentally unguarded. If a new endpoint is added without a scope assignment, the proof fails to compile.

Read cannot mutate

A read-scoped key cannot trigger any outbound action.

Read-scoped API keys cannot send emails, delete data, call external APIs, or modify resources visible to other parties. Every mutating endpoint requires send, admin, or oversight scope.

Admin is the only escalation

No scope implies any other scope — except admin, which satisfies all.

Read does not imply send. Send does not imply admin. Oversight is independent. The admin scope is the only cross-scope escalation path, and it's named explicitly — not a hidden behavior.

Assumption: The endpoint-to-scope mapping is the specification — we assume it correctly reflects intended access policy.

Mitigation: The scope map is mechanically extracted from the TypeScript source (not hand-maintained). CI runs this extraction on every push and fails the build if the Lean model and the source code diverge. The proof is always current.

Proof 2 — Approval Flow

No email reaches delivery without operator approval

In gated oversight modes, outbound emails must be approved by a human operator before delivery. We proved this guarantee holds for every possible path through the email lifecycle — not just the paths we tested.

Email submitted ───> scanning ───> Operator Approval ───> Delivered In gated oversight modes (gated_send and gated_all), every path to delivery passes through Operator Approval. The proof covers all internal states and transitions exhaustively.

Approval flow completeness

In gated modes, every path to delivery passes through operator approval.

When a mailbox is set to gated_send or gated_all, we exhaustively checked every possible sequence of state transitions. Whether an email is sent immediately, scheduled for later, or routed through any combination of internal states — delivery is impossible without first entering the approval queue.

Approval is the sole gate

In gated modes, remove the approval step and delivery becomes impossible.

Approval isn't one path to delivery — it's the only path. In gated oversight modes, if you take away the operator's ability to approve, no email can ever reach a recipient. The approval step isn't a checkpoint on a highway — it's the only bridge across the river.

Axiom boundary: None. This proof is purely structural — no cryptographic or external assumptions. 7 states, 11 transitions, exhaustively verified.

Proof 3 — Identity Headers

Every identity claim is cryptographically bound

Every outbound email carries a signed identity header (ECDSA P-256) containing the operator name, oversight mode, capabilities, and verification status. We proved that the signature construction correctly binds all fields — tampering with any field breaks the signature.

Signature binding

A valid signature uniquely determines the identity claim.

If a signature verifies successfully, the identity claim it contains is exactly what was originally signed. You cannot reuse a signature for a different identity. All 8 fields — operator, oversight mode, capabilities, verified status, creation date, service, timestamp, and reputation hash — are bound.

Tamper evidence

Changing any field produces a different payload that breaks the signature.

Proved individually for each critical field: an agent cannot impersonate a different operator, claim a different oversight mode, add capabilities it wasn't granted, or forge a verified status. Each field change is detectable.

Key binding

Signatures only verify against the operator's registered public key.

Substituting a different public key fails verification. Even if an attacker served a different key, legitimate signatures would not verify against it. The signature is cryptographically bound to a specific key pair.

Axiom boundary: We assume ECDSA P-256 is a sound signature scheme (standard cryptographic assumption, validated by NIST, used in TLS worldwide). What we prove is that our usage of ECDSA correctly binds all identity fields to the signature. Serialization determinism is guaranteed by construction — we use sorted-key canonical serialization, producing identical byte output regardless of runtime or JS engine.

What these proofs cover

These proofs cover the 82 authenticated API endpoints — every endpoint that accepts an API key. Two public onboarding endpoints (account creation and key retrieval) are excluded from the formal proofs. They are secured by Stripe session entropy, a one-time-read key retrieval with 1-hour expiry, Turnstile challenge, IP and fingerprint rate limiting, and disposable email detection.

The Lean 4 type checker runs in CI on every push. If a new endpoint is added without updating the proof model, the build fails. The proofs are always current with the deployed code.

Proof source is available on request.

Proof checksums

SHA-256 hashes of the compiled proof certificates. These are pinned to Lean 4 v4.28.0 — if the proofs change, the hashes change. Proof source available on request; these hashes verify the files you receive match what we committed to publicly.