LeanIn
LeanIn is a concurrency runtime for Lean 4: a work-stealing scheduler, with the model machine-checked. You write async code in ordinary do notation. It compiles to a state machine, so what lives across a wait is data, not a closure. The HTTP server on that runtime is what the benchmarks measure.
What it covers
The library is the concurrency toolkit: runtime, scheduler, tasks, and the async interface, with the model beside them. The pure model is machine-checked. A bridge states nine contracts for the native operations, three of them exercised by native traces. HTTP/1.1 lives in the same library.
The carrier is one thread and many connections. The scheduler follows Tokio: a local queue, a shared inject queue, and stealing. Sockets follow Node's completion loop. A finished read resumes on the loop thread as a direct call. Every connection's steps share that thread, and that is the ceiling the measurements read.
Results
- 3.05× Sixteen requests kept in flight, eight connections: 512,451 req/s against Node 22 at 168,179. The same shape is 2.59× with one connection and 2.31× with 32.
- 1.06× One request in flight per connection, eight connections. 0.98× at one connection and 0.88× at 32.
- 0.91× A new connection for every request, eight connections. 0.62× at one connection and 0.82× at 32.
- 1.4–12.5k Requests per second for Lean's shipped HTTP server on the same three shapes.
Ratios are one run of bench/screen.sh on commit 554e3b0. This instrument moves by about ±30% between runs, so the comparison is the result, not a single absolute rate.