LSP + Aura Sentinel (VS Code)

Plugin-aware diagnostics, overlays, and live proof feedback in the editor.

Components

• aura-lsp computes diagnostics by parsing, type-checking, then verifying with Z3.
• Aura Sentinel (VS Code extension) runs aura-lsp and renders additional UX.

Protocol reference: /docs/sentinel-protocol.

See also: Lumina Sentinel for proof-driven UI rendering and span-accurate geometry failures: /docs/lumina-sentinel.

Plugin-aware diagnostics

When verification succeeds, plugins may emit informational diagnostics that attribute the proof to a plugin id and (optionally) include:

• exact SMT formula used in the proof
• related information pointing to the enabling aura.toml entry
• structured fields like mask and range

Sentinel overlays

Aura Sentinel renders Nexus proof diagnostics as:

• gutter icons for verified lines (IoT chip / AI neural)
• hover text showing mask/range + SMT
• a sidebar “Nexus Plugins” view listing active plugins and trust state
• inlay hints for IoT verified ranges

How to run (dev)

In this repo:

• VS Code extension: editors/vscode
• LSP binary: built from the workspace (cargo build -p aura-lsp)

Typical workflow:

1. Open editors/vscode in VS Code
2. Run “Run and Debug” (Extension Development Host)
3. Open an .aura file in the new window