SpecForge es una herramienta orientada a la especificación y el análisis de sistemas híbridos mediante el lenguaje Lilo, un lenguaje de expresiones con operadores de lógica temporal como always, eventually, past e historically, que admiten intervalos de tiempo para acotar las condiciones. Sus especificaciones se organizan en sistemas que agrupan señales (valores que varían en el tiempo), parámetros, tipos personalizados, definiciones reutilizables y los requisitos que el sistema debe cumplir.
El texto recorre un ejemplo de control de temperatura y humedad con cinco especificaciones concretas: mantener la temperatura dentro de un rango seguro, vincular la humedad al rango normal de temperatura, marcar condiciones de emergencia por debajo de 5 °C o por encima de 45 °C, y exigir la estabilización del sistema en un plazo de 10 unidades de tiempo tras una emergencia. Sobre estas especificaciones, la extensión de VSCode de SpecForge ofrece cinco capacidades de análisis: Monitor (verificar si el comportamiento registrado cumple las especificaciones), Exemplify (generar trazas válidas de ejemplo), Falsify (buscar contraejemplos respecto a un modelo del sistema), Export (convertir a JSON u otros formatos) y Animate (visualizar el comportamiento temporal). Todas estas funciones están integradas en VSCode y también disponibles desde Jupyter mediante un SDK de Python.
La guía termina señalando los capítulos de referencia para profundizar en el lenguaje Lilo, la composición de sistemas y el SDK de Python.