This section is a quick introduction to SpecForge’s main capabilities through a hands-on example. We’ll explore how to write specifications in the Lilo language and analyze them using SpecForge’s VSCode extension. Lilo is an expression-based temporal specification language designed for hybrid systems. Here are the key concepts: Primitive Types: Bool, Int, Float, and String Operators: Standard arithmetic (+, -, *, /), comparisons (==, <, >, etc.), and logical operators (&&, ||, =>) Temporal...


