Aura2026 Edition
Pre-stable
Verification

Formal reasoning as developer feedback.

Aura integrates contracts and Z3-backed verification into the ordinary toolchain. The differentiator is not merely “there is an SMT solver”; it is the path from source obligation to structured, source-oriented feedback.

Proof explorer

See how source intent travels through the verification model.

This is a precise explanatory visualization of the repository’s proof architecture — not a simulated claim that the browser is executing Z3.

Aura source

Make the boundary provable

cell bounded_inc(x: u32[0..99]) -> u32:
    requires x < 100
    ensures result <= 100

    val next: u32 = x + 1
    assert next <= 100
    next
Proof / trust flow
01
parseSource shape accepted
02
semaRefinement + contract visible
03
normalizeProof obligation produced
04
z3Solver-backed verification path

This panel explains the repository’s proof flow; it is not a browser-hosted compiler session.

Lifecycle

A proof is a pipeline with failure semantics.

Timeout and solver unknown are not proofs. Counterexamples are not just red badges. Each state needs to survive the trip back to the developer without being flattened into marketing-friendly success/failure.

01

Contract / assertion

Source intent becomes an explicit proof obligation.

02

Normalize

Semantic state is lowered into verifier-consumable constraints.

03

Solver

Feature-gated Z3 runs under fast, ci or thorough profiles.

04

Result

Proof, counterexample, timeout or unknown remain distinct outcomes.

05

Map

Counterexample data can be mapped toward Aura types and source ranges.

06

Editor

aura-lsp streams phases and structured diagnostics to Sentinel/editor clients.

Interactive profile

fast

Low-latency-oriented solver profile for the edit/verify loop.

CI profile

ci

CI-oriented defaults intended to balance depth with repeatable automation.

Deep profile

thorough

Deeper verification mode; the repository’s verification example notes quantifier acceptance under thorough.

cargo run -p aura --features z3 -- verify main.aura --smt-profile fast

# optional warm solver state inside a run
AURA_Z3_INCREMENTAL=1 cargo run -p aura --features z3 -- verify main.aura
Counterexamples

“SAT” is not a useful developer message.

The documented aura.counterexample.v2 shape can carry bindings, values, value kinds, Aura type information, relevance, source ranges and source-anchored injections when available.

Solver view

sat
(model
  (define-fun p () Int 180)
)

Developer-facing direction

assert p <= 100
       ^^^^^^^^

p: u32 = 180
relevant: true
source: this assertion
Trusted core

Verification shrinks uncertainty. It does not erase trust.

Inside the proof story
  • source contracts and assertions
  • proof obligations and modeled semantics
  • structured proof/counterexample results
  • trusted-core reports and audits
Still trusted / independently validated
  • solver implementation and invocation assumptions
  • compiler/backend correctness not formally established end-to-end
  • runtime, OS and hardware
  • explicitly trusted FFI and external toolchains

Proof-driven does not mean proof-washed.

Aura’s website deliberately refuses “formally verified compiler” and universal latency claims that the repository does not establish.

Read project status