Jane Street, una de las firmas de trading cuantitativo más influyentes de Wall Street, ha anunciado la creación de un equipo dedicado a métodos formales de verificación de software, en un giro estratégico motivado por el auge de la programación agéntica. La decisión marca un cambio radical en la postura de la compañía, cuyo posicionamiento interno durante 25 años había sido de escepticismo hacia estas técnicas de verificación matemática rigurosa.
El detonante del cambio, según explica la propia empresa en su blog técnico, ha sido la irrupción de los agentes de inteligencia artificial en el flujo de trabajo de desarrollo. Aunque Jane Street reconoce que los modelos son cada vez mejores generando código útil, también advierte que ese código tiende al "slop": overly complicated, plagado de bugs extraños y casos límite, y con frecuencia violando invariantes esenciales del codebase. Esta situación ha generado un cuello de botella de verificación: los programadores humanos deben dedicar cada vez más tiempo a confirmar que el código producido por los agentes cumple los estándares de calidad.
Para la firma, los métodos formales ofrecen una salida a este cuello de botella. A diferencia de las pruebas tradicionales, que solo cubren una fracción del espacio de estados posible de un programa, las técnicas formales —como las que se aplican al microkernel seL4, verificado matemáticamente— pueden proporcionar garantías universales. SeL4, citado como ejemplo emblemático, requirió 25 años-persona de esfuerzo para verificar apenas 8.700 líneas de código en C, con una proporción de 23 líneas de demostración por cada línea de código y medio día-persona por línea verificada. Jane Street reconoce que ese coste era prohibitivo para la mayoría del software, pero argumenta que la programación agéntica ha invertido radicalmente la ecuación coste-beneficio.
El nuevo equipo aprovechará el control que Jane Street ejerce sobre OxCaml, su dialecto interno de OCaml, para integrar técnicas de demostración directamente en el lenguaje. La compañía planea explorar desde especificaciones modulares de propiedades en el sistema de tipos hasta restricciones a nivel de tipos sobre ownership y mutabilidad, con el objetivo de hacer que ciertos tipos de demostraciones sean más accesibles. Además, los agentes de IA pueden beneficiarse de la retroalimentación rica que proporcionan las pruebas formales, un canal de señal especialmente valioso cuando estos sistemas entrenan mediante aprendizaje por refuerzo o resuelven problemas de programación complejos.
Otro factor diferencial es la comunidad de programadores de Jane Street, que la empresa describe como inusualmente receptiva a herramientas avanzadas. Según el comunicado, es habitual que los usuarios internos reclamen la llegada más rápida de nuevas funcionalidades experimentales del sistema de tipos, una dinámica que contrasta con la dificultad habitual de los investigadores de lenguajes de programación para conseguir adopción real. La firma sostiene que esta base de usuarios dispuestos permite combinar mejoras a corto plazo —con impacto inmediato— con visiones más ambiciosas a varios años vista.
Jane Street aclara que su enfoque no pretende ignorar el ecosistema externo: la compañía se declara inspirada por el trabajo en torno a herramientas como Lean, Dafny, Rocq, Agda e Iris, y busca activamente formas de integrar OxCaml con esa infraestructura ya existente. Sin embargo, considera que existen ventajas únicas que solo se materializan cuando se trabaja simultáneamente sobre el lenguaje y las técnicas de demostración.
La decisión se inscribe en una conversación más amplia en la industria del software sobre cómo la inteligencia artificial generativa está transformando no solo la escritura de código, sino también los mecanismos de garantía de calidad. Startups y grupos de investigación en todo el mundo exploran cómo combinar agentes y métodos formales; Jane Street apuesta ahora a que su combinación de infraestructura lingüística propia, talento especializado y cultura técnica orientada a la corrección le otorgan una posición privilegiada para liderar ese cruce. Si la estrategia funciona, los métodos formales podrían pasar de ser una herramienta reservada a componentes críticos como microkernels o hardware, a convertirse en una pieza cotidiana del desarrollo de software, comparable en ubicuidad a los sistemas de tipos sofisticados que hoy dan soporte a la programación en lenguajes como OCaml, Haskell o Rust.