GitHub - JoshuaPurtell/lithe: simple web service in lean4

A lightweight web framework for Lean 4 with an Axum-inspired router, type-safe extractors, and middleware.

What is Lean 4? Lean is a functional programming language and theorem prover developed by Microsoft Research. It combines a powerful type system with the ability to write mathematical proofs, making it ideal for building verified, high-assurance software.

Features

• Router — Path parameters, query parsing, method routing
• Extractors — JSON, Form, Path, Query, Headers, Auth, State
• Middleware — CORS, CSRF, rate limiting, timeouts, logging, metrics
• Streaming — SSE, WebSocket, chunked responses
• Storage — SQLite integration via lean-sqlite

Installation

Add to your lakefile.lean:

-- Latest stable release (recommended)
require lithe from git "https://github.com/JoshuaPurtell/lithe" @ "v0.1.0"

-- Or track main branch (latest features, may be unstable)
require lithe from git "https://github.com/JoshuaPurtell/lithe" @ "main"

Then build:

Note: Requires Lean 4.27.0+ (see lean-toolchain).

Versioning

Lithe follows Semantic Versioning. Pin to a specific version tag (e.g., v0.1.0) for stability in production.

Quick Start

import Lithe

open Lithe

def hello : Handler :=
  fun _ => pure (Response.text "Hello, World!")

def app : Router :=
  Router.empty
    |> Router.get "/hello" hello

-- Test in-memory
#eval Lithe.run app { method := .GET, path := "/hello", query := "", headers := #[], body := .empty }

Running with HTTP (Rust Shim)

For production HTTP serving, use the Rust shim:

cd examples/hello
lake build

cd ../../rust/lithe-shim
cargo run

curl http://127.0.0.1:3000/hello
# Hello, World!

Environment Variables

Middleware Example

import Lithe

open Lithe

def app : Router :=
  Router.empty
    |> Router.withMiddleware (cors { origins := #["https://example.com"] })
    |> Router.withMiddleware (rateLimit { maxRequests := 100, windowMs := 60000 })
    |> Router.get "/api/data" dataHandler

Project Structure

Lithe/
├── Core/           # Handler, Context, Error types
├── Http/           # Request, Response, Status, WebSocket, SSE
├── Router/         # Path matching, routing
├── Extractor/      # JSON, Form, Path, Query extractors
├── Middleware/     # CORS, CSRF, Auth, Logging, etc.
├── Storage/        # SQLite integration
└── FFI/            # Rust shim exports

Examples

Security Notes

• TLS: Not handled by Lithe. Use a reverse proxy (Caddy/Nginx) or add TLS at the Rust layer.
• CSRF: Use the csrf middleware for cookie-based auth.
• Sessions: Set Secure, HttpOnly, SameSite=Strict on cookies.

Demo: Lean Crafter

As a demonstration, I've built Crafter—a 2D survival game—entirely in Lean 4 and hosted it on the web using Lithe.

🎮 Play it live | 📦 Source code

License

MIT — see LICENSE