Lean 4 and the Suspiciously Fast Website

Congratulations, the leak is extremely fast

Imagine you run a publishing platform. Two customers, Acme and Beta, both have an article at /en/articles/launch. Editors preview drafts. Visitors read published posts. Everything works, but rendering the same page repeatedly feels wasteful.

So you add a cache:

cache[path] = renderedPage

CPU usage drops. Latency looks fantastic.

Then somebody visits Beta's launch page and gets Acme's announcement. An editor opens a preview, the cache remembers it, and the next anonymous visitor gets tomorrow's news today.

Congratulations. You've optimized the incident.

This is a hypothetical example, but the mechanism is ordinary: a cache decides which requests are allowed to reuse the same response. That decision can cross a security boundary just as easily as an authorization check can.

I've written before about squeezing a lot of traffic through a $4 VPS. Doing less work remains an excellent way to make a website cheaper. The interesting question is what happens when we want a stronger argument that the work we're skipping was safe to skip.

That's where Lean 4 gets interesting.

The theorem prover joins the performance review

Lean is a programming language and an interactive theorem prover. You can describe a function, state a property about it, and construct a proof that Lean's kernel checks. The property can cover every input permitted by the model, including combinations you didn't think to put in a test fixture. The Lean documentation explains that checking process.

Wanting to build the most efficient website is a reasonable starting point. But a theorem prover does not know whether your homepage downloads twelve megabytes of hero images. It needs a more specific question.

For this experiment, that question is:

Can we reuse a previously rendered public response while preserving the response the ordinary handler would have produced?

That's small enough to reason about and useful enough to matter. It also lands squarely in platform security: we're changing a shared delivery mechanism that serves multiple customers.

The proof itself doesn't need to run on every request. Lean erases proof terms during compilation, and proof-bearing subtypes can have the runtime representation of their underlying value. Your actual visibility checks, database lookups, and cache operations still cost something.

Math has not negotiated a discount with your database.

Give the cache a smaller job

Let's build a concrete design around that publishing platform. We'll cache the rendered response for one allowlisted article route, eligible only for anonymous, explicitly public, nonpersonalized GET requests.

Everything authenticated, personalized, private, or administrative takes the ordinary authorization path. So do previews and denied requests. Those requests neither read nor populate this shared public cache.

A trusted adapter resolves the host to a tenant, resolves the URL to a canonical article, and checks the article's current public visibility before every application-cache lookup. It doesn't accept a tenant ID supplied by a convenient query parameter. Ambiguous or unsupported requests fall back to the normal handler or get rejected.

Then it builds a key:

Key = (tenant, canonicalResource, locale, renderingRevision)

The tenant separates Acme from Beta. The canonical resource keeps equivalent URLs from becoming competing identities. The locale separates translations.

The revision is where the homework starts. It must cover everything that changes the rendered result: article content, templates, relevant configuration, and other dependencies. A field named revision does not automatically know you deployed a new template.

Likewise, a cookie, query parameter, or request header cannot secretly change the output while the key stays identical. Either represent that variation, handle it outside the cached response under an explicit contract, or make the request ineligible. This first experiment deliberately chooses the narrow route.

The request flow is boring in a useful way:

Resolve trusted tenant and canonical article
    -> Confirm current public visibility and cache eligibility
    -> Construct complete key
    -> Hit: return cached public response
    -> Miss: render public response, store it, return it

Anything ineligible -> ordinary authorization and rendering

For a single-owner blog, tenant can be constant. The separation between public articles and editor previews still matters. OWASP's cache security guidance describes why missing request context and stale access decisions cause trouble here.

Give the cache something to prove

The Lean example for this design is an uncompiled proof candidate. It has not yet been checked by Lean or deployed. Treat the following as the proposed contract, not a completed verification result.

Its central invariant says that every stored entry equals what the public renderer produces for that full key:

def Valid (render : Key → Response) (cache : Cache Response) : Prop :=
  ∀ key value, cache key = some value → value = render key

Read that as: for any key and value, if the cache contains that value at that key, the value must equal render key.

That's the entire definition of a valid cache in this model. Empty entries are fine. Wrong entries aren't.

The proposed serve_correct theorem then has this shape, in abbreviated notation:

Given: Valid(publicRender, cache)

Serving a request produces:
  optimizedResponse = uncachedResponse
  AND
  Valid(publicRender, resultingCache)

There are three cases to account for. On a public hit, the invariant supplies the equality we need. On a public miss, we call the same renderer and store its result. On a sensitive request, we call the ordinary sensitive handler and leave the public cache alone.

An empty cache gives us the starting point. Preserving validity after each request lets the argument continue across a sequence, while the renderers remain fixed.

Now try sneaking the editor's preview into a public cache entry. To preserve the invariant, we'd have to establish:

previewResponse = publicRender key

For a draft that differs from the published article, that equality is false. We have a concrete counterexample to the rule. A proof of this preservation statement cannot go through for arbitrary preview output without changing the assumptions or the design.

That's the useful friction. “But the unit tests passed” is no longer the whole conversation.

Before calling any of this checked, the candidate needs successful compilation and kernel checking, review for unresolved proof placeholders, and inspection of the theorem's assumptions. Lean's proof validation guidance also makes the bigger point: a valid proof can still prove the wrong requirement.

The theorem prover is very literal. That is both its appeal and your problem.

What exactly did we put inside “response”?

Suppose the cached HTML is correct, but the response includes another user's Set-Cookie header.

A proof about HTML strings can happily miss that.

The model's Response type is generic. For this use case, it should cover the status, body, and relevant observable headers, so redirects and cookies don't disappear from the thing we're comparing. Even that response equality does not establish anything about timing, logs, or other side effects.

There's a similar trap with tenants. Writing Acme's key should leave Beta's cache entry unchanged. That's another property specified in the model. But the renderer could still query the wrong customer's database rows and put them under a beautifully isolated key.

Map isolation cannot establish data ownership. The original renderer and its authorization logic still need to be correct. Matching an insecure origin perfectly would preserve its mistake perfectly.

The adapter matters just as much. Lean doesn't inspect a live HTTP request and decide whether our published classification was honest. We have to connect the real request, current publication state, and modeled key correctly.

For a first implementation, I'd keep the existing web stack and use Lean as an executable reference model. Compare a real cache implementation against it using generated request sequences. The prototype's mathematical map is intentionally simple. It isn't a Redis replacement.

Those comparisons provide evidence for the cases tested, not a universal proof of the adapter. Compiling Lean directly into the service is another option, but native execution brings its own compiler and runtime trust boundary. Either route needs an honest account of how the model meets production code.

“Unpublish” is a surprisingly large button

Our cache is valid. An article is public. An anonymous request passes the visibility check.

Then an editor unpublishes the article.

What happens to the request already in flight?

The model above doesn't answer that. It fixes pure renderers and doesn't model concurrent withdrawal. A real design needs to define when withdrawal takes effect and how serving coordinates with it. Otherwise, there's a time-of-check/time-of-use race between “this is public” and “send these bytes.”

Immutable revision keys help distinguish versions. They don't revoke an old version's permission to be served. Changing content or policy requires appropriate invalidation or a new snapshot with the invariant re-established.

Now put a CDN in front. If it returns cached HTML before the application runs, our carefully placed visibility gate never executes. The CDN needs its own delivery and revocation policy, including purge behavior and an explicit allowance, if any, for propagation delay.

HTTP cache directives need similar precision. no-cache does not mean “never store this.” private and no-store have different jobs. Adding no-store later doesn't delete copies already held by caches. These distinctions are specified in RFC 9111.

This is why the example starts with an application rendering cache. Expanding the proof's scope to distributed publication and revocation would be a separate, larger piece of work. It deserves an actual design, not a confident arrow labeled “CDN.”

There is a real precedent for this

Cedar, the authorization language and engine, uses an approach worth borrowing.

AWS describes verification-guided development with Lean: executable specifications, proofs of selected properties, a production Rust implementation, and differential random testing comparing the implementations.

That gives the proof and the tests different jobs. The proof examines a stated property of the model. The comparisons look for disagreements between the model and implementation. It doesn't amount to a universal equivalence proof of every line of production Rust.

One particularly relevant property in Cedar's Lean specification is sound policy slicing. Under the required conditions, evaluating an appropriate subset of policies preserves the authorization result of evaluating the full policy store.

That's a performance optimization with a security obligation attached. Evaluate less, preserve the decision.

The conditions matter. Casually dropping a relevant forbid policy could turn a denial into an allowance. A sound slice has to justify what it leaves out.

Our cache exercise follows the same engineering instinct on a smaller scale: identify repeated work, define the behavior that must survive, and make the optimization answer to that definition.

Fine. Is it faster?

No benchmark has been run for this prototype. Response equivalence alone establishes no speedup, memory bound, or constant-time lookup.

We can still make the experiment concrete. Suppose a workload has 90,000 eligible public requests, 10,000 sensitive requests, and a 90% hit rate among the public requests.

Without cache: 90,000 + 10,000 = 100,000 renders
With cache:     9,000 + 10,000 =  19,000 renders

That's 81% fewer renders in a hypothetical workload. It is not an 81% latency improvement. We still pay for visibility checks, cache lookups, misses, memory, invalidation, and synchronization.

To find out whether it earns its complexity, compare cache-disabled and cache-enabled builds on identical hardware, data, and request traces. Run cold and warm caches, then vary concurrency, article popularity, tenant count, and publication churn. Repeat the runs and report variation.

Look at three things: rendering and database work, CPU and memory use, and tail latency at the same offered load and error rate. If you're claiming the website feels faster, measure browser performance too. Saving origin CPU won't rescue an oversized hero image.

Before celebrating, run the uncomfortable cases through the actual proxy and application: identical paths across tenants, users with different permissions, previews, and unpublishing during traffic. Compare full responses and state changes. Deliberately remove tenant or revision from the key and confirm the checks catch the broken design.

For an already static blog, a custom verified rendering cache may be an excellent learning exercise and a poor infrastructure purchase. Pre-rendering and ordinary CDN delivery may already eliminate the repeated work you're trying to save. The proof and maintenance effort belong in the cost calculation too.

That's where I'd draw the line on “the most efficient website.” Define the workload, measure the expensive part, and choose a small optimization whose security contract you can explain.

Lean becomes useful when it helps make that contract precise enough to check. And if the result is fast, we should be able to explain exactly why it is allowed to be.