LeanIn 以 Lean 4 定理證明器構建 Tokio 風格排程器，效能勝過 Node.js

Have you been hearing whispers about Lean 4? The ultimate hallucination killer, a tool that uses mathematical proofs to force large language models to actually verify their logic instead of just guessing.

But labelling Lean 4 as just an academic tool or an AI proof assistant misses a key use. Lean 4 was completely rebuilt as a heavily optimised, natively compiled systems language.

We wanted to see what would happen if we took it out of the lab and put it to work on backend infrastructure. The result is LeanIn: a multi-threaded, work-stealing concurrency runtime written natively in Lean 4.

What is great about it is that Our LeanIn server actually outpaces Node.js across almost all standard performance benchmarks.

Here is a look at why we built it, how a math language manages to beat a heavily optimised V8 event loop, and why formal verification might be the next big shift in systems engineering.

Let us begin with a problem. Concurrency is a Nightmare to Test

If you write backend systems, you will have felt the pain of concurrency bugs. Race conditions, deadlocks, and corrupted states. All non-deterministic. They will pass your CI pipeline 100 times in a row, only to crash your server at 3:00 AM under a highly specific, microsecond-level load spike.

Traditional testing relies on heuristics and stress-testing. Throwing simulated traffic at the wall and hoping the bugs reveal themselves.

By building our scheduler in Lean 4, we took a different route: mathematical proof. Lean’s type system allows us to encode the actual state transitions of our scheduler. This means we can formally verify that tasks are never dropped, queues never deadlock, and memory is handled correctly. The compiler will not let us build the project if the logic is flawed.

Historically, this level of safety meant your code ran in a slow, interpreted environment. You had to choose between mathematical certainty and execution speed. LeanIn proves that trade-off is no longer a trade-off.

How Does Lean 4 Outperform Node.js?

How does a language famous for math proofs beat out Node.js, the (probably very disputed) undisputed queen of asynchronous web servers?

It comes down to architecture and memory management:

1. True Multi-Threading via Work Stealing
Node.js relies on a single-threaded event loop. While great for pure I/O, as soon as you mix in CPU-bound micro-tasks, the loop bottlenecks. LeanIn is heavily inspired by Rust’s Tokio runtime. It uses a multi-threaded work-stealing algorithm. If one worker thread gets bogged down, idle threads will steal tasks from its queue, dynamically balancing the load and keeping throughput massive.

2. Destructive Updates (FBIP)
Functional programming is usually memory-hungry because it relies on immutable data, meaning lots of copying. Lean 4 solves this with a paradigm called Functional But In-Place (FBIP). The compiler tracks reference counts statically. If it knows a piece of data only has one reference, it mutates the memory buffer directly under the hood. You get the safety of pure functional programming with the cache-locality and speed of C.

3. No Stop-the-World Garbage Collection
Node.js uses the V8 engine, which relies on a tracing garbage collector. Under heavy concurrent load, GC pause times can spike your tail latency. Lean 4’s memory model reclaims memory deterministically the moment a reference count drops to zero. In our benchmarks, this allowed LeanIn to keep P99 latencies remarkably flat compared to Node's latency spikes.

4. Native C Compilation
Lean 4 doesn’t run on a virtual machine. It compiles down to highly optimised C code, which is then compiled to a native binary.

Should we stop using languages without dependent types?

For a long time, the software industry accepted a compromise: if you wanted blazing-fast performance, you used a language that let you shoot yourself in the foot. If you wanted safety, you accepted runtime bloat.

What we’ve found building LeanIn is that theorem provers have quietly evolved. You can now build infrastructure that is formally verified to be correct and fast enough to challenge industry-standard runtimes like Node.js.

We think this is the future of high-stakes backend development. If you’re dealing with financial systems, secure pipelines, or heavy concurrent loads, you shouldn't have to guess if your thread scheduling is safe.

If you want to dive into the code, check out the implementation, or run the benchmarks yourself, we’ve open-sourced the project.

Drop by the repo, give it a star, and let us know what you think:
👉 scidonia/leanin on GitHub