Trust through
Proof.

Verification is not a separate command an agent may forget to run – the Double-Lock executes inside every mutation. diagnostics list is the standalone read on workspace health. Broader layers (policy checks, test orchestration) are planned, not implemented yet.

Blueprint-style verification illustration for the verify command.

Synopsis

Two verification surfaces exist: the Double-Lock, which runs inside every mutation, and diagnostics list, the standalone read for a file or a workspace. One caveat travels with both: an LSP-clean result does not claim behavioural correctness.

SYNTAX


                                    weaver diagnostics list [--uri | --workspace] [FLAGS]

Language inferred from file extension

Surfaces

Surface	Source	Description
diagnostics list	LSP	Compiler warnings and language-server errors for a file (`--uri`) or the whole workspace (`--workspace`).
the Double-Lock	Engine	Runs inside every mutation: Tree-sitter validates the staged result, LSP observes the complete proposed delta. Not optional, not skippable.
policy Planned	Sempai	Enforce architectural constraints and forbidden patterns via Sempai queries.
tests Planned	Runner	Orchestrate test suites and report results as structured output.

ARCHITECTURE

The Verification Stack

The Double-Lock and diagnostics list form the base layer. Policy enforcement and test orchestration are planned follow-on layers.

BASE LAYER

Diagnostics

Compiler warnings and LSP errors for any file or workspace with a supported language server.

! unused variable `x`

✗ mismatched types

PLANNED

Policy Enforcement

Architectural constraints and forbidden-pattern detection via Sempai queries.

✓ no_unsafe_blocks

! cyclomatic_complexity

PLANNED

Test Orchestration

Run test suites and report results as structured JSONL for CI gating.

✓ cargo test

✓ pytest tests/

The Double-Lock, In Detail

Every proposed change is staged into one workspace view and verified twice before commit. No path silently weakens this contract.

Syntactic lock

Tree-sitter parses the final staged content of every touched file. Structural breakage – unbalanced braces, truncated blocks – is refused before any semantic work runs.

Semantic lock

The language server observes the complete proposed delta and flushes diagnostics once per language. A missing semantic backend yields an explicit unavailable or inconclusive status under declared policy – never a silent pass.

The diagnostics delta

Post-mutation diagnostics are classified rather than dumped: introduced, severity-worsened, resolved, unchanged, or relocated. Concise deltas render inline; the complete set sits behind a bounded spool reference.

{"diagnostics":{"introduced":0,"severity_worsened":0,"resolved":1,"unchanged":12,"relocated":2},"spool":"weaver jobs get txn_01j9... --json"}

An LSP-clean result does not claim behavioural correctness. The locks prove the change parses and type-checks; the test suite still owns behaviour.

Planned: Policy Rules

Planned

A future policy surface will combine standard linters with custom Sempai queries to enforce architectural constraints. The schema below is illustrative.

Block dangerous functions or imports
Enforce type hints and documentation standards
Require specific test coverage thresholds

"Verification is not just about catching bugs; it is about ensuring the AI acts within the boundaries of the system's design philosophy."

weaver.policy.yaml (illustrative)

version: "1.0"
rules:
  # Enforce security patterns
  - name: "no-raw-sql"
    severity: "error"
    query: "sempai: pattern: sql_query($X) where $X is string_literal"

  # Ensure testing standards
  - name: "test-coverage"
    severity: "warning"
    check: "coverage > 85%"

Output & Integration

CLI Output Modes

Results go to stdout; progress and warnings go to stderr. With --json, the stable machine contract streams verbatim; without it, the human renderer applies, with --limit and truncation markers keeping large workspaces bounded.

$ weaver diagnostics list --json --uri file:///src/lib.rs

// stable machine contract (--json)
{"diagnostics":[{"line":12,"column":5,"message":"unused variable `x`"}]}

Human Mode

Point at a file URI to pull every diagnostic the language server reports. Human-readable output is the default when stdout is a TTY, so recognised diagnostics render with source context instead of raw JSON.

$ weaver diagnostics list --uri file:///src/lib.rs

src/lib.rs
  --> 12:5
   |
12 | let x = 42;
       ^ unused variable `x`

Ready to secure your agents?

Learn how the sandbox keeps execution safe.

Next: Safety Model

Trust through Proof.