Sentinel Protocol

The custom proof-stream and counterexample contract between aura-lsp and Aura-aware editor clients.

Aura Sentinel communicates with aura-lsp through a custom proof-stream protocol layered on LSP.

Start and cancel

text

aura/proofsStreamStart
aura/proofsStreamCancel

A start request returns a stream identifier so the UI can correlate later notifications and cancellation.

States

text

start
phase
done
error
cancelled

Common phase labels include:

text

parse
sema
normalize
z3

The protocol is designed so proof work can remain non-blocking and cancellable.

Counterexample v2

When available, verification diagnostics can contain aura.counterexample.v2 structured data with bindings, type information, relevance, source ranges and source-anchored injections.

Consumers should ignore unknown fields so the schema can evolve compatibly within the protocol contract.

Stability

The repositoryâ€™s LSP stability document currently identifies Aura protocol version 1. Breaking Aura-specific extension changes should bump that protocol version rather than silently changing client assumptions.