LeanTEA's killer property is that the compiler doesn't only check that your code runs; it checks that whole classes of vulnerabilities can't even be expressed. This file is the design document for that property — what's shipped, what's planned, what the threat model is, and how the type-level primitives work.

Status (2026-06-21): TEA / Persist / Rpc / Mcp surface shipped; Proof of Authorization and SafeQuery v1 shipped (see Primitives 1 and 3 below); SafeHtml and the State Machine Proof primitives are the remaining items. See ROADMAP.md for sequencing.

We aim to make four specific classes of vulnerability unrepresentable in user code that compiles:

1. SQL / command injection — concatenating user input into a query.
2. Reflected / stored XSS — putting untrusted text on the page without escaping.
3. Authorization bypass — a handler runs without confirming the caller's role.
4. Invalid state transitions — paying out below zero, double-spending, accepting an order from a deleted account.

Out of scope:

• Bugs inside the auth middleware itself (we narrow this gap by keeping the trusted core ~50 lines)
• OS / runtime / DB vulnerabilities
• Side channels (timing, cache)
• Cryptographic primitive flaws (we use stdlib + audited C)

The argument is the classic Phantom Type one: we don't prove the whole system is safe, we prove that anything user code does at the framework boundary is. That alone collapses the audit cost an order of magnitude.

Today the framework's untyped Repo.query accepts a raw String:

let xs ← repo.query s!"SELECT * FROM users WHERE id = {userInput}" #[]

This is a footgun and exactly the shape LLM-generated code reaches for. SafeQuery makes that shape unrepresentable: the new typed surface won't accept a String at all.

The typed AST lives in LeanTea.Persist.SafeQuery. Every value enters through a smart constructor that demands a typed Col E α and a ToValue α instance:

structure Col (E : Type) (α : Type) [Entity E] where
  name : String

-- Smart constructor — the only path from a typed value into a Where.
def Col.eq {E α} [Entity E] [ToValue α] (c : Col E α) (v : α) : Where E := …

The Where inductive's leaf constructors (.eq, .inList, .like, …) are private to the SafeQuery.lean file. A misguided Where.eq "email" rawUserInput from anywhere else in the codebase is a Unknown constant compile error. The only paths in are Col.eq, Col.lt, Col.inList, Col.like (typed), or the audited .trusted escape hatch.

namespace UserCols
  def email   : Col User String := ⟨"email"⟩
  def deleted : Col User Bool   := ⟨"deleted"⟩
end UserCols

-- Build a typed predicate and run it.
let q : Select User :=
  { where_  := .and (UserCols.email.eq "alice@x.com")
                    (.not (UserCols.deleted.eq true)),
    orderBy := [],
    limit   := some 10 }
let rows ← SafeQuery.run users q

• Where E AST with eq, ne, lt, gt, inList, like (prefix / suffix / contains), isNull, and, or, not.
• Select E with typed where_ / orderBy / limit / offset.
• Update E with [ UserCols.name .= "x", UserCols.flag .= true ] list literal — the .= operator builds a SetClause E.
• Delete E.
• SafeQuery.run / .count / .update / .delete runners.
• inList with variable-length placeholders rendered positionally; empty list folds to 1=0 to avoid the IN () syntax error.
• .trusted decl_name% "…raw SQL…" audited escape hatch — decl_name% resolves to the fully-qualified name of the enclosing declaration, so grep -rn '\.trusted' lists every audit point.

• JOIN across multiple entities. Rationale: a typed JOIN builder inflates the AST and the user-visible API by ~3×; for v1 we chose the FP-developer-friendly story "90% of CRUD is typed; complex multi-table SQL is .trusted with an audit tag." Audit cost collapses to grep. Revisit for v1.1.
• SUM / MAX / GROUP BY — the Repo.count shortcut covers the pagination case (Repo.count : Where E → IO Nat). Other aggregates go through .trusted.

SafeQuery.lean is 260 LOC total; the trusted core (the renderWhere / Select.render / Update.render / Delete.render fragment) is ~80 LOC. The smart constructors and Repo.run-style runners are thin shells around it. The whole module is reviewable in under an hour.

examples/Smoke/SafeQuery.lean runs eight scenarios end-to-end and shows the emitted SQL + bound parameters for each.

LeanTea.Html is almost there — Html.text already escapes strings, and the typed constructors generate well-formed markup. The hole is attribute values:

a_ [("href", userInput)] [text "click"]   -- userInput could be `javascript:…`

/-- Strings that have passed through a sanitiser. -/
structure SafeAttr where
  private mk :: value : String

namespace SafeAttr
  /-- URL attribute — only `https://`, `http://`, `mailto:`, `#`, `/` schemes. -/
  def url (raw : String) : Except String SafeAttr := …
  /-- Plain text attribute — strips `<`, `>`, quotes. -/
  def text (raw : String) : SafeAttr := …
  /-- Numeric attribute. -/
  def num (n : Int) : SafeAttr := ⟨toString n⟩
end SafeAttr

Then:

a_ [("href", urlSafe.value)] [Html.text userInput]

Html.attr is changed from (String × String) to (String × SafeAttr). The old form becomes a compile error unless the value is a string literal (which we audit specially — same Lean.Name trick).

• Html.attr requires SafeAttr instead of String.
• Html.text escapes the same as today (no API change).
• Old code mechanically migrates: ("href", x) → ("href", ← SafeAttr.url x).

~80 LOC for the type + sanitisers; ~120 LOC migrating the existing typed Html DSL call sites.

The killer demo. A handler that requires admin access cannot be called without first proving the caller is an admin. The proof is a value that only the auth middleware can mint.

inductive Capability where
  | guest
  | user
  | admin
  | owner (resourceId : String)   -- dependent on a runtime resource id
  deriving DecidableEq

structure Proof (c : Capability) where
  private mk :: subject : String

/-- Lattice: prove `c1 ≤ c2` to widen a proof. -/
class HasCapability (c1 c2 : Capability) : Prop
instance : HasCapability .admin .user  := ⟨⟩
instance : HasCapability .admin .guest := ⟨⟩
instance : HasCapability .user  .guest := ⟨⟩
instance : HasCapability c      c      := ⟨⟩

def Proof.weaken {c1 c2 : Capability} [HasCapability c1 c2]
    (p : Proof c1) : Proof c2 := ⟨p.subject⟩

/-- Only function that can fabricate a `Proof`. Verifies session +
    role from `AuthStore`. ~30 LOC of trusted code. -/
def Proof.issue (auth : AuthStore) (req : Request) (c : Capability)
    : IO (Except String (Proof c)) := …

def handleAdminDelete (proof : Proof .admin) (id : Nat) (store : Store)
    : IO Response := do
  /- Reachable only by paths where `proof : Proof .admin` exists.
     Drop the parameter and the call site won't compile. -/
  store.shapes.delete id
  return Response.text 200 s!"deleted {id} by {proof.subject}"

The naïve API Proof (.owner "doc-42") doesn't generalise. The right shape uses Lean's dependent types:

def handleEdit (id : String) (proof : Proof (.owner id))
    (newText : String) : IO Response := …

The type of proof depends on the runtime value of id. The path that extracts id from the URL and the DB row that confirms ownership must agree on the same id — the type system makes that consistency a compile-time invariant.

Neither TypeScript nor Rust can express this — they lack Π-types. Haskell's singletons library gets close but needs heavyweight encoding. Lean 4 expresses it directly.

Don't make every handler call Proof.issue manually. Lift it into the Endpoint record:

structure Endpoint (req res : Type) (c : Capability) where
  path    : String
  method  : Method
  handler : Proof c → req → IO res

The router runs Proof.issue once per request, returns 403 on failure, and only then dispatches:

def dispatch (auth : AuthStore) (e : Endpoint req res c)
    (req : Request) : IO Response := do
  match ← Proof.issue auth req c with
  | .error _ => return Response.forbidden
  | .ok p =>
    let parsed ← parseRequest e req
    let result ← e.handler p parsed
    return renderResponse result

A naïve List (Endpoint req res c) won't hold endpoints with different capabilities. Three Lean-idiomatic answers:

Option A — Sigma type (recommended)

abbrev SomeEndpoint := Σ c, Endpoint req res c

def routes : List SomeEndpoint := [
  ⟨.guest, listShapesEp⟩,
  ⟨.user,  addShapeEp⟩,
  ⟨.admin, deleteShapeEp⟩
]

The capability is erased from the static type but preserved at runtime in the Sigma's first component. Dispatch reads c off the Sigma and calls Proof.issue with it. Simplest, least clever, no macros.

Option B — HList over an indexed family

inductive Routes : List Capability → Type where
  | nil  : Routes []
  | cons : Endpoint req res c → Routes cs → Routes (c :: cs)

Preserves capabilities at the type level — useful if a metaprogram wants to enumerate them, less useful for the running router.

Option C — Existential wrapper

inductive AnyEndpoint where
  | mk : (c : Capability) → Endpoint req res c → AnyEndpoint

Equivalent to A in expressive power, slightly less ergonomic to destructure.

Decision: ship Option A. It's the minimum Lean machinery for the job and matches the way the rest of LeanTea.Rpc already works (lists of records).

Most interesting at the domain layer (transactions, orders). Lean's inductive types + dependent types make the shape obvious:

inductive OrderState where | draft | submitted | paid | shipped
inductive Transition : OrderState → OrderState → Type where
  | submit  : Transition .draft     .submitted
  | pay     : Transition .submitted .paid
  | ship    : Transition .paid      .shipped

A function apply : Transition s s' → Order s → IO (Order s') then makes invalid transitions a compile error. Out of scope for the first milestone — domain-shaped, not framework-shaped.

The proofs above hold only if the trusted core is correct. We commit to keeping it small and audit-able:

~240 LOC total. Reviewable in an afternoon. The interesting property: anything you build on top is automatically safe, because the type system rejects every call that bypasses these primitives.

1. SafeQuery for joins — the AST above is single-table. JOINs need a more elaborate From clause; do we ship a typed JOIN builder or accept .trusted for joins in the v1?
2. PathParam parsing — currently the URL id is String. For the dependent owner pattern to typecheck, we may need the framework to thread a Decidable (parsedId = proofId) proof. The simpler path: keep id : String throughout and rely on Proof.issue verifying ownership against the same string.
3. CSP / HSTS headers — automatic enforcement (similar to how Yesod injects security headers) belongs in the framework, not in user code. Likely a one-time wiring in WebApp.run.
4. Mutation in the typeclass — SafeQuery covers SELECT well; UPDATE / DELETE need a parallel design where row identifiers are typed.

These will be resolved during PoC implementation — see ROADMAP.md for sequencing.

The pitch isn't "we have type safety" — every modern language has that. The pitch is:

The compiler rejects code that violates these four properties. Compile succeeds → those four bug classes are gone, at no test cost. The auditor can verify the property by reading 240 lines.

Lean 4 specifically is the only host language where this is currently buildable. Coq is too academic for industrial uptake; F* is research-grade; Idris is unsupported; ATS is unmaintained. Lean 4 has LSP, an active community, a polished package manager (Lake), and a maintainer (Microsoft Research → independent Lean FRO).

That gap is the moat.