Aura · 2026 Edition

Write systems code with proof in the loop.

Aura is a proof-driven systems programming language and developer platform. It connects source semantics, Z3-backed verification, development execution, native-oriented backends and editor feedback around one language pipeline.

Get Aura Start with Aura Explore the language Source on GitHub

Active · pre-stable22 workspace cratesZ3-backed · feature-gatedAura protocol v1

bounded_transfer.aurasource → proof → execution
cell transfer(balance: u32[0..10000], amount: u32) -> u32:
    requires amount <= balance
    ensures result <= balance

    val next: u32 = balance - amount
    assert next <= balance
    nextparseindentation + cells
semarefinement + contract
verifyproof obligation
executeAVM · C · LLVM*

22Rust workspace members

3SMT profiles · fast / ci / thorough

v1Aura-specific LSP protocol

3Execution surfaces · AVM / C / LLVM*

2026Edition namespace · pre-stable

Design position

A language platform, not a compiler demo.

Aura’s repository already spans frontend, semantic analysis, IR, verification, development execution, backends, runtime, packages, FFI, language-server tooling, Sentinel, plugins, release engineering and Android integration. The website treats those as one architecture — while keeping maturity boundaries explicit.

Proof belongs in the development loop

Contracts, proof obligations and counterexamples are designed to return to source-level tooling instead of living in a separate formal-methods silo.

Fast iteration and native execution stay distinct

Aura keeps an AVM development path alongside C-oriented and evolving LLVM IR paths rather than hiding backend maturity behind one marketing label.

Trust is a first-class engineering surface

FFI, unsafe calls, solver assumptions, backends and external toolchains remain visible parts of the trusted computing base.

Compiler architecture

One semantic center. Multiple proof and execution surfaces.

The same language pipeline feeds verification, the development VM and native-oriented backends. Backend equivalence is an engineering concern of its own; a source proof is never silently promoted into a claim that every downstream compiler stage is formally correct.

Toolchain details

Proof

aura-verify

Proof obligations, Z3 profiles, counterexamples, summaries, region/linear analysis.

verification and execution stay adjacent — not conflated

Language surface

Correctness intent is syntax, not a comment.

Aura’s current implemented/reference-backed surface is intentionally smaller than a stable 1.0 specification. The language already exposes contracts, range refinements, loop reasoning, resource-sensitive rules and explicit foreign-code trust boundaries.

Contracts

requires · ensures · assert · assume

Correctness intent is visible at boundaries and inside functions.

Refinements

u32[0..100]

Range information can participate directly in proof obligations.

Loop reasoning

invariant · decreases

Loops can expose inductive invariants and termination-oriented hints.

Explicit trust

unsafe: · trusted extern cell

Foreign code is placed inside a visible trust boundary rather than hidden.

Flow

-> · ~>

The current reference distinguishes synchronous and asynchronous flow operators.

Resource semantics

Tensor · Model · Style

Current MVP rules describe move behavior for resource-like values.

Read the language overview

Verification

Proof results become developer feedback.

The verifier is only half the product. Aura’s LSP protocol carries proof phases, structured diagnostics and counterexample metadata back toward the editor so a failing obligation can become something a developer can inspect and repair.

Verification model

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

parseSource shape accepted

semaRefinement + contract visible

normalizeProof obligation produced

z3Solver-backed verification path

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

Toolchain

Build, verify, execute, inspect.

Aura exposes a real command surface today. The site distinguishes code-backed commands from experimental or evolving paths instead of presenting roadmap vocabulary as executable fact.

Build & run

code-backed

aura build · aura run

Profiles dev/release/verify; modes avm/llvm/hybrid; backend selection and native link inputs.

Verify

code-backed

aura verify

Feature-gated Z3 path with fast, ci and thorough SMT profiles plus trusted-core report output.

Developer loop

code-backed

test · lint · fmt · init

The primary CLI owns project initialization, Aura test discovery, linting and canonical formatting.

Native bridge

code-backed

aura bindgen

Bootstrap C/C++ header bridging with link inputs and best-effort refined type mapping.

Language server

code-backed

aura-lsp

Proof streaming, diagnostics, counterexample transport, cache and debugger/performance integration.

LLVM path

evolving

--mode llvm / --backend llvm

Implemented and feature-gated, but still evolving. Current source should not be marketed as a finished optimizing backend.

Aura Sentinel

The proof UI is part of the language experience.

Sentinel is a Tauri 2 + CodeMirror desktop environment built around Aura-specific language-server capabilities rather than a generic syntax skin.

Proof streamingNon-blocking start / phase / done / error / cancelled states.

Counterexample detailStructured bindings, type metadata, relevance and source mapping where available.

Debugger + telemetry infrastructureDevelopment VM and native-debug protocol layers live beside proof UX.

Explore Sentinel

sentinel · bounded_transfer.auraproof stream / illustrative UI

cell transfer(balance: u32[0..10000], amount: u32) -> u32:
    requires amount <= balance
    ensures result <= balance

    val next: u32 = balance - amount
    assert next <= balance
    next

PROOFS

requiresobligation

amount ≤ balance enters the function contract.

assertmapped

Source-level assertion remains linked to verification feedback.

protocolv1

Aura-specific extensions are versioned separately from ordinary LSP compatibility.

Ecosystem

A language needs more than syntax.

Packages, FFI, plugins, an SDK, an IDE, application UI work, Android tooling and deterministic release engineering already exist in the monorepo. They are presented as integration surfaces with their real maturity — not as blanket stability guarantees.

IDE

Aura Sentinel

Tauri 2 + CodeMirror desktop environment designed for proof-stream UX, diagnostics, counterexamples and debugger integration.

Packages

aura-pkg

Registry/resolver/cache/lockfile/security/signing modules with code-backed package command surfaces.

Plugins

Nexus

Plugin manifests and verification-aware extension paths keep domain integrations outside the core language.

Applications

Lumina

Evolving UI/application layer with Raylib support, layout, input, grid, image/media and application examples.

Platform

Android

SDK/NDK setup, runtime cross-build paths, sample APK workflow and emulator/build helper tooling.

Provenance

Release engineering

Deterministic SDK ZIPs, SHA-256, attestation JSON, optional Windows signing and Sentinel sidecar staging.

Evidence discipline

Impressive claims are useful only when they stay true.

Aura is strongest when the website states exactly what the repository establishes. The public status layer deliberately separates implementation, feature gates, evolving backends, targets and claims that are not yet justified.

Supported public claims

Proof-driven systems programming language
Z3-backed verification
Structured counterexample mapping
AVM + C-oriented execution paths
Feature-gated evolving LLVM IR backend
22-member Rust language-platform workspace
Sentinel / LSP proof tooling
Package, FFI, plugin and Android integration work

Boundaries we keep explicit

Formally verified compiler
Frozen stable v1.0 language semantics
Universal memory-safety guarantee
Production JIT / automatic AVM → LLVM promotion
Guaranteed <200ms proof latency across workloads
Universal production-ready Android support

Read the language. Inspect the proof model. Then inspect the source.

Aura is public as a serious pre-stable language platform. The website is an orientation layer; the repository remains the implementation source of truth.

Documentation GitHub