SpecForge for VS Code

Online Documentation

Official VS Code extension for SpecForge - an AI-powered formal specification authoring tool based on the Lilo temporal specification language.

What is Lilo?

Lilo is a formal specification language for verifying complex systems over time. It features temporal operators, records, and modular, hierarchical systems.

Features

• Syntax Highlighting: Clear and intuitive highlighting for Lilo keywords, types, operators, and comments.
• Real-time Diagnostics: Get instant feedback on parsing errors, type mismatches, and consistency checks as you type.
• Code Completion: Smart suggestions for variables, keywords, and system components.
• Code Lenses: Actionable insights and commands embedded directly in your source code.
• AI-Powered Explanations: Use the Lilo: Explain Warning command or the code lens to get clear, natural-language explanations for complex diagnostic messages.

Commands

This extension provides the following commands, which can be accessed via the Command Palette:

• SpecForge: Explain Warning: Provides an AI-generated explanation for a specific warning message in your specification.
• SpecForge: Restart Language Server: Manually restarts the SpecForge language server.
• SpecForge: Configure API Key for an LLM Provider: Configure the API key for the chosen LLM provider.

Settings

This extension contributes the following settings, which can be configured in your user or workspace settings.json file:

• specforge.apiBaseUrl: The base URL for the backend analysis server. Defaults to http://localhost:8080.
• specforge.trace.server: Traces the communication between VS Code and the language server. Can be off, messages, or verbose.
• specforge.apiKeySource: Determines how API keys for LLM providers are sourced. When set to env, API keys are inherited from the environment variables. When set to vscode, API keys are supplied through the VS Code UI (and stored in the VSCode secret storage). You can Configure API Keys for the chosen LLM Provider using the command palette.

Developer Haskell LSP

The production extension uses the JavaScript LSP server. Developers can opt into the in-progress Haskell LSP server by adding this hidden workspace setting manually:

{
  "specforge.dev.haskellLspWorkingDirectory": "/absolute/path/to/specforge/api"
}

This setting is intentionally not shown in the extension settings UI. When enabled, the extension starts cabal -v0 run -O0 specforge -- lsp-server --verbosity none from that directory. The directory must be absolute and contain cabal.project and specforge.cabal. You can also set SPECFORGE_HASKELL_LSP_WORKING_DIRECTORY to the same absolute path.