Aura2026 Edition
Pre-stable

LSP + Aura Sentinel

Aura’s language server and desktop IDE are first-class parts of the proof-driven developer loop.

aura-lsp is more than a syntax server. Its source tree includes proof result extraction, counterexample transport, caches, performance-tuning infrastructure, debugger protocol layers and CI/differential integration work.

Aura protocol version

Aura-specific LSP extensions are versioned separately. The documented current Aura protocol version is:

text
1

Clients should gate Aura-specific behavior on that protocol version rather than assuming every server revision exposes identical experimental fields.

Sentinel

editors/sentinel-app is the dedicated desktop environment:

  • Tauri 2
  • CodeMirror 6
  • TypeScript
  • Vite
  • Vitest

Run from source:

bash
cd editors/sentinel-app
npm install
npm run tauri:dev

Why a dedicated IDE layer matters

Generic diagnostics are not always enough for formal reasoning. Aura-specific UX can represent:

  • a running proof phase,
  • counterexample trees,
  • relevant bindings,
  • source injections/ghost text,
  • proof traces,
  • debugger state,
  • verification/performance telemetry.

The goal is to turn proof failures into inspectable program feedback without requiring the developer to read raw SMT models as the primary interface.