Complete Production Webapp in Lean

Developer Paul Butcher released a production web application built entirely in Lean 4, combining a TodoMVC implementation with passwordless sign-in, SQL migrations, OpenTelemetry telemetry, an LLM assistant panel, an MCP endpoint, and infrastructure-as-code deployment to AWS Lambda. The stack spans more than a dozen Lean libraries including lean-html, lean-htmx, lean-routing, lean-middleware, lean-authentication, lean-mcp, leanpostgres, leanmigrate, lean-telemetry, lean-llmclient, lean-markdown, lean-aws, lean-aws-lambda, lean-json, leancurl, and leancrypto, with the UI rendered via HTMX and minimal JavaScript. Butcher states the codebase is total — nothing is marked partial and nothing can panic — and that security properties such as CSRF attribute handling and sign-in refusal behavior are proved as theorems, with markup, routes, and Markdown rendering formally verified.

TodoMVC https://todomvc.com in Lean 4, plus everything a production application needs around it: passwordless sign-in, SQL migrations, telemetry, an LLM assistant panel, an MCP endpoint your own agent can use, and IaC deployment to AWS Lambda. The UI is HTMX plus a very little JavaScript. Lean is a strongly typed functional language with a built-in theorem prover. This allows us to make some very strong guarantees, including: - Totality. Nothing in this application is partial and nothing in it can panic, and the same holds of almost<sup 1 user-content-fn-note-53c803df848bc019630a8fe0f22552cf </sup every library in the stack below. A loop that reads until its input runs out carries a bound and a proof that it decreases. warningAsError is on, so no unfinished proofs. - Security properties are theorems. A page carries its anti-forgery attribute exactly when it has a token to put in it csrfAttrs nonempty iff : never announcing one it lacks, never dropping one it has. A sign-in refusal is proved to speak only about the request and never about who owns the address onlySpeaksAboutTheRequest , stated over the whole outcome type. - Markup is typed and formally verified. A <div inside a <p is a type error, text content is escaped on the way in, and Node.render wellFormed proves that what comes out is well-formed HTML. - Routes are strongly typed. A handler of the wrong arity or the wrong type does not compile, and a link cannot drift from the route that serves it. - Markdown is formally verified. lean-markdown is total, never panicking or looping on any input including adversarial input. renderHtmlSafe is proved to emit well-formed HTML in which no string from the document can produce markup or break out of an attribute. - What an agent was granted bounds what it can reach. A token that was not granted todos:write reaches no tool that changes anything nothing mutates without write . - Encodings are proved to round-trip. What is written to a chat row is what is read back from it toMsg ofMsg , which matters because the conversation is replayed to the model in full on every turn. Underneath, leancrypto proves decode encode bytes = some bytes for hex, base64, base64url and Crockford base32, that its modular exponentiation agrees with base ^ exponent % modulus , and that its early-exit-free comparison is equality. Lean, Std.Http.Server , and: | lean-html https://github.com/paulbutcher/lean-html · lean-htmx https://github.com/paulbutcher/lean-htmx | typed markup and typed hx- attributes | | lean-routing https://github.com/paulbutcher/lean-routing | typed router and route table | | lean-middleware https://github.com/paulbutcher/lean-middleware | sessions, sealed cookie store, anti-forgery, fingerprinted static files, request tracing | | lean-authentication https://github.com/paulbutcher/lean-authentication | magic links, federated sign-in over OIDC, sessions, rate limiting, bounce handling, consent, and an OAuth 2.1 authorisation server | | lean-mcp https://github.com/paulbutcher/lean-mcp | an MCP server over Streamable HTTP | | leanpostgres https://github.com/paulbutcher/leanpostgres · leanmigrate https://github.com/paulbutcher/leanmigrate | libpq bindings with a connection pool; migrations as plain SQL files | | lean-telemetry https://github.com/paulbutcher/lean-telemetry | OpenTelemetry traces and logs | | lean-llmclient https://github.com/paulbutcher/lean-llmclient · lean-markdown https://github.com/paulbutcher/lean-markdown | provider-agnostic chat with tool calling; GFM for rendering replies | | lean-aws https://github.com/paulbutcher/lean-aws · lean-aws-lambda https://github.com/paulbutcher/lean-aws-lambda | SigV4 signing; the Lambda runtime interface | | lean-json https://github.com/paulbutcher/lean-json | JSON see below | | leancurl https://github.com/paulbutcher/leancurl | libcurl bindings | | leancrypto https://github.com/paulbutcher/leancrypto | SHA-2, HMAC, RSA signature verification, codecs, DER | | lean-jose https://github.com/paulbutcher/lean-jose · jose-libcrypto https://github.com/paulbutcher/jose-libcrypto | JWS, JWK and JWT; ECDSA for the ID token | | lean-libcrypto https://github.com/paulbutcher/lean-libcrypto | OpenSSL libcrypto bindings | Everything above reads and writes JSON with lean-json rather than with Lean.Data.Json . The deployed binary is ~12 MB; Lean.Data.Json is part of the compiler frontend and linking that frontend would increase the binary size by ~125MB, increasing cold start times from the current ~2 seconds to ~15 seconds. lean-json provides some stronger guarantees than Lean.Data.Json : nothing in it is partial , nothing can panic, it is proved correct against the grammar of RFC 8259, and no operation walks a value on the C stack, so a deeply nested document is a bounded error rather than a crash. Codecs, paths, deriving ToJson, FromJson and json% literals are all there; see its README https://github.com/paulbutcher/lean-json readme . Needs a Postgres, libpq and libcurl development packages, and the toolchain in lean-toolchain https://github.com/paulbutcher/lean-todomvc-max/blob/main/lean-toolchain . .devcontainer https://github.com/paulbutcher/lean-todomvc-max/blob/main/.devcontainer has all of it. lake build lake exe TodoMVC http://localhost:8080 lake test uses the same database libpq reads the connection from the usual PG variables, and the role and database they name have to exist before the first run. .devcontainer https://github.com/paulbutcher/lean-todomvc-max/blob/main/.devcontainer sets them to leantodomvc ; outside it, either export your own or create what the devcontainer expects: createuser leantodomvc createdb -O leantodomvc leantodomvc export PGHOST=localhost PGUSER=leantodomvc PGDATABASE=leantodomvc Migrations run at startup, so the database itself needs nothing in it; lake exe migrate applies and rolls them back by hand. Sign-in mail is printed to the terminal rather than sent, so following a magic link needs no mail server, and spans are printed there too in a readable form. For the assistant panel, anything that puts credentials in the environment will do: eval "$ aws configure export-credentials --profile <profile --format env " export AWS REGION=<region export BEDROCK MODEL=<model-or-inference-profile-id template.yaml https://github.com/paulbutcher/lean-todomvc-max/blob/main/template.yaml defines an AWS SAM https://aws.amazon.com/serverless/sam/ deployment: a VPC with egress through a NAT gateway, an RDS Postgres, the function behind a public function URL, interface endpoints for SES and Bedrock, secrets, a log group, a dashboard and its saved queries. You need AWS credentials, a Docker that can build linux/arm64 , and an SES identity for the address you will send from. Give its domain SPF, DKIM, DMARC and an MX record, and while the account is in the SES sandbox, verify the recipients too. Install the SAM CLI from the first-party installer https://docs.aws.amazon.com/serverless-application-model/latest/developerguide/install-sam-cli.html rather than from Homebrew, which is what .devcontainer https://github.com/paulbutcher/lean-todomvc-max/blob/main/.devcontainer does. sam build sam deploy --guided --stack-name todomvc Answer yes to "Allow SAM CLI IAM role creation" and "Function Function Url has no authentication. Is this okay?". MailFrom is the only parameter without a default. A sign-in link has to name an origin, and the function URL is not knowable until the function exists, so deploy a second time with BaseUrl set to what the first deploy printed either run sam deploy --guided a second time or edit the created samconfig.toml . Federated providers see later are configured on that second deploy too, because the redirect URIs you register need the same base URL. The first deploy prints what to register as FederatedCallback , with google , apple or github in place of <provider . For the assistant, set BedrockModel to an id enabled in your region. Most current models are reachable only through a cross-region inference profile, which aws bedrock list-inference-profiles lists. A Marketplace-served model enables itself on first invocation, and that invocation must come from a principal holding aws-marketplace:Subscribe , so prime it once from an administrative identity: aws bedrock-runtime converse --region <region --model-id "<id " \ --messages ' {"role":"user","content": {"text":"hello"} } ' Troubleshooting The Homebrew formula builds against Homebrew's Python, whose pyexpat can be linked against a newer libexpat than macOS ships; the import that fails takes the build subcommand down with it, and what you see is Error: No such command 'build' rather than anything about the loader. You may find that you need to set DOCKER HOST if sam reports no container runtime: export DOCKER HOST="unix://$HOME/.docker/run/docker.sock" An agent of your own can reach the same tools the panel has, over MCP https://modelcontextprotocol.io at /mcp . There is nothing to configure: point the agent at the endpoint and it will find its own way in. Instructions for helping the agent to do so at /connect . Spans and log records leave as one flat JSON object per line on stdout, which the runtime forwards to CloudWatch Logs. lake exe logs renders those rows back into the form the local server prints directly: sam logs --stack-name todomvc --tail | lake exe logs The local server prints that readable form already, so there is nothing to render; to produce the flat rows here too, and so to exercise the same path without deploying, ask the console exporter for them: OTEL EXPORTER CONSOLE FORMAT=flat json lake exe TodoMVC | lake exe logs The Dashboard stack output is a console URL for the dashboard the template creates: platform metrics, server latency, p99 by route, slowest requests, and errors. Beside it, under Logs Insights, the template saves the steps of an analysis loop as query definitions, from slowest routes down to a single trace read end to end. To enable federated sign-in, register an OAuth client with each provider you want and give it a redirect URI of <base-url /t/todomvc/federated/<provider /callback , matching exactly: providers compare it as a string. Apple needs a Services ID, a team id, a key id and a .p8 signing key, because its client secret is minted per request rather than held. Registering with each: Google https://developers.google.com/identity/openid-connect/openid-connect , Apple https://developer.apple.com/documentation/signinwithapple/configuring-your-environment-for-sign-in-with-apple , GitHub https://docs.github.com/en/apps/oauth-apps/building-oauth-apps/creating-an-oauth-app . A provider's secret is never configured in the clear. auth-seal , which lean-authentication https://github.com/paulbutcher/lean-authentication ships, mints the key that seals them and seals one at a time, reading it from standard input so that it reaches neither the process list nor a shell history. The tenant is todomvc and the key id is whatever AUTH SEALING KEY ID will be set to: lake exe auth-seal key once, then keep it export AUTH SEALING KEY=<that printf %s "<the secret " | lake exe auth-seal seal todomvc google client-secret 1 lake exe auth-seal seal todomvc apple signing-key 1 < AuthKey XXXX.p8 What it prints is what the corresponding variable is set to: GOOGLE CLIENT ID and GOOGLE CLIENT SECRET , GITHUB CLIENT ID and GITHUB CLIENT SECRET , and for Apple APPLE CLIENT ID , APPLE TEAM ID , APPLE KEY ID and APPLE SIGNING KEY . A client id that is set with anything else about it missing or unreadable stops the application from starting, rather than quietly dropping that provider from the sign-in page. On a deployment those are stack parameters and the key is not, because a sealed secret in a parameter file discloses nothing only so long as the key that opens it is somewhere else. It goes to the secret the stack prints as SealingKeySecret : aws secretsmanager put-secret-value \ --secret-id "$ aws cloudformation describe-stacks --stack-name todomvc \ --query "Stacks 0 .Outputs ?OutputKey=='SealingKeySecret' .OutputValue" --output text " \ --secret-string "$AUTH SEALING KEY" The function reads that secret when it is deployed rather than per request, so the deploy has to follow the write, not precede it. /account is where somebody connects a provider to the account they are already signed in as, and disconnects one. That is not the same operation as signing in with it: it is the only way to use a provider that hides the address, Apple's Hide My Email in particular, since there is then no address to recognise an existing account by. Disconnecting the last way into an account is refused. Apple cannot be exercised locally. It answers by posting the browser back rather than redirecting, which requires the state cookie to say SameSite=None , and browsers honour that only on a Secure cookie. Google and GitHub work against http://localhost unchanged. Copyright c 2026 Paul Butcher. Apache 2.0; see LICENSE https://github.com/paulbutcher/lean-todomvc-max/blob/main/LICENSE . Footnotes 1. there are a few places where we rely on bindings to libraries such as libcrypto and libcurl, plus obviously we can make no such guarantees when talking to things like Postgres. But these are very well tested and are unlikely to be the source of errors compared to application code. ↩ user-content-fnref-note-53c803df848bc019630a8fe0f22552cf