Ansatz es una librería de Clojure que permite escribir programas verificados formalmente sin salir del ecosistema de la JVM. Está construida sobre el Calculus of Inductive Constructions (CIC), la misma teoría de tipos que sustenta Lean 4, e implementa el núcleo de Lean 4 en Java. De este modo, las pruebas mecanizadas que produce Ansatz son válidas también en Lean 4 y viceversa, y pueden exportarse a la sintaxis de Lean 4. La herramienta contrasta contra Mathlib, con más de 210.000 teoremas y 648.000 declaraciones, y contra CSLib, que reúne algoritmos verificados.
Para los desarrolladores que ya utilizan malli, el salto es gradual: los esquemas m/=> se convierten en firmas de tipo del núcleo, las funciones pasan a estar comprobadas por la máquina y el código resultante sigue ejecutándose como Clojure corriente. La librería incluye refinamientos (por ejemplo, [:int {:min 1}] lleva su cota como Prop en el tipo), estructuras con campos nombrados que se compilan a defrecord, tipos inductivos definidos por el usuario, pattern matching recursivo con comprobación de terminación mediante medidas como sizeOf, y un verificador diferencial que detecta fallos de elaboración bien tipados pero infieles al código fuente.
El repositorio expone también ejemplos avanzados: árboles rojo-negro con pruebas de preservación de validez tras rotaciones, listas ordenadas con demostración de que insertSorted conserva la ordenación, y teoremas resueltos con tácticas automáticas como omega, grind, simp o induction. En la práctica, Ansatz está pensado para quienes necesiten garantías formales de corrección en programas que se ejecutan en producción sobre la JVM, sin renunciar a la ergonomía de Clojure.