SpecForge is a platform for authoring formal specifications using the Lilo language, an expression‑based temporal specification language designed for hybrid systems. The platform provides a VSCode extension for writing, type‑checking, and analyzing specifications, as well as a Python SDK for programmatic access and Jupyter notebook integration.

Lilo includes primitive types (Bool, Int, Float, String), standard operators, and rich temporal operators such as always, eventually, past, and historically, which can be qualified with time intervals. Specifications are organized into systems containing signals, parameters, custom types, definitions, and requirements.

The VSCode extension offers multiple analysis modes: Monitor checks recorded traces against specs, Exemplify generates satisfying example traces, Falsify searches for counterexamples using registered falsifiers, Export converts specs to formats like JSON, and Animate visualizes behavior over time. Analyses can be saved and reopened within the editor.

A temperature control example demonstrates safety specs for temperature and humidity, emergency conditions, and recovery requirements. Further chapters cover the full Lilo language, system composition, and the Python SDK for deeper integration.