TodoMVC 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
partialand nothing in it can panic, and the same holds of (almost<sup>1</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.warningAsErroris 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, andNode.render_wellFormedproves 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.
renderHtmlSafeis 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:writereaches 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 provesdecode (encode bytes) = some bytesfor hex, base64, base64url and Crockford base32, that its modular exponentiation agrees withbase ^ exponent % modulus, and that its early-exit-free comparison is equality.
Lean, Std.Http.Server, and:
| lean-html ·lean-htmx | typed markup and typed hx-* attributes |
| lean-routing | typed router and route table |
| lean-middleware | sessions, sealed cookie store, anti-forgery, fingerprinted static files, request tracing |
| lean-authentication | magic links, federated sign-in over OIDC, sessions, rate limiting, bounce handling, consent, and an OAuth 2.1 authorisation server |
| lean-mcp | an MCP server over Streamable HTTP |
| leanpostgres ·leanmigrate | libpq bindings with a connection pool; migrations as plain SQL files |
| lean-telemetry | OpenTelemetry traces and logs |
| lean-llmclient ·lean-markdown | provider-agnostic chat with tool calling; GFM for rendering replies |
| lean-aws ·lean-aws-lambda | SigV4 signing; the Lambda runtime interface |
| lean-json | JSON (see below) |
| leancurl | libcurl bindings |
| leancrypto | SHA-2, HMAC, RSA signature verification, codecs, DER |
| lean-jose ·jose-libcrypto | JWS, JWK and JWT; ECDSA for the ID token |
| 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.
Needs a Postgres, libpq and libcurl development packages, and the toolchain in lean-toolchain. .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 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 defines an AWS 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 rather than from Homebrew, which is what .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 .
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 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, Apple, GitHub.
A provider's secret is never configured in the clear. auth-seal, which 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.
Footnotes #
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. ↩