Project Configuration

Lilo projects can use an optional specforge.toml configuration file at the project root.

For getting started, you can skip this configuration entirely and simply place your .lilo specification files and data files directly in the root of your project. SpecForge will work with sensible defaults.

When you do use specforge.toml, you must specify [project].source. Other missing fields use sensible defaults. The Python SDK and the VS Code extension read this file and apply the semantics accordingly.

The configuration file is useful for:

• Setting a project name and explicit source path
• Customizing language behavior (interval mode, freeze)
• Adjusting diagnostics settings (consistency, redundancy, optimize, unused defs) and their timeouts
• Customizing analysis code lenses shown by the editor
• Registering system_falsifier entries for falsification analysis
• Defining validation_rules for spec search validation

Below are the schema and defaults, followed by a complete example.

Schema and defaults

Top-level keys and their defaults when omitted:

• project

  • name (string).
    • Default: "".
    • On init: set to the provided name; otherwise to the name of the project root directory.
  • source (path string). Required when specforge.toml is present. Use "." for source files in the project root.

• language

  • interval.mode (string). Supported: "static". Default: "static"
  • freeze.enabled (bool). Default: true

• diagnostics

  • consistency.enabled (bool). Default: true
  • consistency.timeouts — SMT solver timeouts for consistency checks:
    • named (seconds, float). Timeout per individual named specification. Default: 0.5
    • system (seconds, float). Timeout for the whole-system consistency check (all specs checked together). Default: 1.0
  • redundancy.enabled (bool). Default: true
  • redundancy.timeout (seconds, float). Timeout per individual named specification. Default: 0.5
  • guard_analysis.enabled (bool). Default: true
  • guard_analysis.timeout (seconds, float). Timeout per individual guarded specification. Default: 0.5
  • optimize.enabled (bool). Default: true
  • unused_defs.enabled (bool). Default: true

• code_lenses

  • satisfiability.enabled (bool). Show satisfiability analysis code lenses. Default: true
  • satisfiability.timeouts — SMT solver timeouts for satisfiability code lenses:
    • named (seconds, float). Timeout per individual named specification. Default: inherits diagnostics.consistency.timeouts.named
    • system (seconds, float). Timeout for the whole-system consistency check. Default: inherits diagnostics.consistency.timeouts.system
  • redundancy.enabled (bool). Show redundancy analysis code lenses. Default: false
  • redundancy.timeout (seconds, float). Timeout per individual named specification. Default: inherits diagnostics.redundancy.timeout

  Omitted code lens fields inherit from their corresponding diagnostics settings, except code_lenses.redundancy.enabled, which defaults to false.

• [[system_falsifier]] (array of tables, optional)

  • Each entry: name (string), system (string), script (string)
  • If absent or empty, the key is omitted from the file and treated as an empty list

• [[validation_rules]] (array of tables, optional)

  • Each entry: antecedent (query string), consequent (query string)
  • Used by specforge validate when invoked without --antecedent/--consequent. See Validation.
  • If absent or empty, the key is omitted from the file and treated as an empty list

Default file:

[project]
name = ""
source = "src/"

Example specforge.toml

An example project with overrides.

[project]
name = "my-specs"
source = "src/"

[language]
freeze.enabled = true
interval.mode = "static"

[diagnostics.consistency]
enabled = true

[diagnostics.consistency.timeouts]
named = 5.0
system = 10.0

[diagnostics.optimize]
enabled = true

[diagnostics.redundancy]
enabled = false
timeout = 0.5

[diagnostics.guard_analysis]
enabled = true
timeout = 0.5

[diagnostics.unused_defs]
enabled = false

[code_lenses.satisfiability]
enabled = true

[code_lenses.redundancy]
enabled = true
timeout = 0.5

[[system_falsifier]]
name = "Psitaliro ClimateControl Falsifier"
system = "climate_control"
script = "falsifiers/falsify_climate_control.py"

[[system_falsifier]]
name = "Psitaliro ALKS falisifier"
system = "lane_keeping"
script = "falsifiers/alks.py"

[[validation_rules]]
antecedent = "label:todo"
consequent = "priority:>50"

[[validation_rules]]
antecedent = "label:blue OR label:green"
consequent = "label:grue"