Aura2026 Edition
Pre-stable

Proof System

Contracts, proof obligations, Z3 profiles, counterexamples and trust boundaries in Aura.

Aura’s identity is proof-driven development. The proof system integrates source-level intent, solver-backed verification and editor-facing feedback.

Source vocabulary

  • requires — precondition
  • ensures — postcondition
  • assert — proof obligation
  • assume — explicit trusted assumption
  • invariant — loop invariant
  • decreases — termination-oriented hint
  • range refinements such as u32[0..100]
  • quantifiers where supported

Z3 path

Z3 support is feature-gated:

bash
cargo run -p aura --features z3 -- verify main.aura

SMT profiles:

text
fast
ci
thorough

Optional incremental mode:

bash
AURA_Z3_INCREMENTAL=1 cargo run -p aura --features z3 -- verify main.aura

The existence of performance tuning/caching code does not by itself prove a universal <200ms latency result.

Result semantics

A verification run can produce more than a binary “green/red” answer. A timeout or solver unknown must never be presented as proof.

Conceptually:

text
obligation
  → solver
     ├─ proved
     ├─ counterexample/model
     ├─ unknown
     └─ timeout/error
  → structured diagnostics
  → LSP / editor

Counterexample mapping

The documented aura.counterexample.v2 schema can carry:

  • binding name/value,
  • value kind,
  • Aura type where known,
  • relevance,
  • source range,
  • source-anchored injections.

This is how a solver model can become a developer message such as “this assertion fails when x = 12 here” rather than raw SMT output.

Trust

Aura does not claim that the compiler itself is formally verified end-to-end. Proofs about modeled source semantics still depend on a trusted/dependently validated stack including solver assumptions, compiler/backend correctness, runtime/platform behavior and explicitly trusted FFI.

See Sentinel Protocol for how proof results travel to tooling.