+1, what is it that you are doing.

It's early days of using it as a general purpose programming language, my initial use case was using it as a metaprogramming framework that lowered into target languages with some rigor on correspondence of the lowered artifact and the proof-amenable surface. By lines of code the biggest use case historically was describing state machines and codecs/protocols for high-assurance IO primitives: define QUIC or ZMTP once and get idealized performance C++ and Rust and Haskell (Zig coming soon) protocol suite native to io_uring.

Another big use case is GPU kernel compilation. I've encoded the polyhedral algebra used by CuTe and all of the stated theorems from nvfuser in lean4. From this you can recover scheduling and tiling properties that must be met to get equal or better performance to CASK (likely optimal) for many operations, and then lower that to PTX. Surprisingly often the candidate set for the fastest possible kernel turns out to be finite and enumerable, so fast inference.

Somewhat recently I started benchmarking stuff just directly in lean4 with a very small TCB shim to e.g. io_uring. I've done like the basic systems programming ABCs (I've got a reverse proxy that's lean4 and ~100 lines of C and shatters nginx, faster at every point on the histogram, memory use flat as a strap). Lithe runs on it so I can do web serving as fast as anything in the hyper ecosystem.

Now that I've got my feet with it I'm digging in on a serious project which is a hypervisor that addresses the deficiencies in firecracker. This is a place where some proven properties can really get you a lot of performance (something like firecracker has to be very defensive regarding e.g. virtqueue semantics in the presence of a malicious guest). Firecracker is an exceptional piece of code and it's carried me far but at agent scale it's time to go another turn of the crank on virtualization performance.