LeanIn es una biblioteca de concurrencia para Lean 4 que implementa un runtime con un planificador de robo de trabajo (work-stealing) inspirado en Tokio y Node.js. Su objetivo principal es permitir el uso de técnicas de concurrencia de alto rendimiento dentro de un asistente de pruebas formales, superando las limitaciones de concurrencia nativa de Lean. La clave técnica de la librería es la defuncionalización, que utiliza datos en lugar de closures para gestionar el estado, lo que permite una compilación eficiente y la verificación formal de las propiedades de seguridad.
El proyecto demuestra su viabilidad mediante un servidor HTTP/1.1, donde las pruebas muestran que LeanIn alcanza velocidades comparables a Node.js en ciertos escenarios de alta concurrencia, aunque con una menor escalabilidad en cargas extremas debido a su arquitectura de un solo hilo para el carrier. La librería incluye interfaces para tareas, asincronía y estructuras de datos, y su modelo teórico ha sido verificado por máquina, garantizando la corrección de los contratos primitivos.
El ecosistema se construye sobre Lake y Nix, utilizando la versión 4.35 de Lean 4 para aprovechar el marco de precondiciones más débiles (WP). El código asíncrono se compila a una máquina de estados plana, eliminando la necesidad de closures enlazadas. Esta herramienta es relevante para desarrolladores de Lean que buscan integrar concurrencia realista en sus proyectos, ofreciendo un puente entre la formalización matemática y el rendimiento de sistemas concurrentes modernos.