Aura2026 Edition
Pre-stable

Getting Started

Build, run and verify Aura from the public repository without assuming unpublished binary artifacts.

Aura is an active, pre-stable programming-language platform. The most reliable way to start today is from the repository source.

Prerequisites

For the core compiler and AVM path:

  • a current stable Rust toolchain,
  • Git,
  • a C compiler / Clang for C-backed native and compatibility paths.

Optional integrations require additional toolchains:

  • Z3 for solver-backed verification,
  • LLVM for the feature-gated LLVM IR path,
  • Node.js / npm + Tauri prerequisites for Aura Sentinel,
  • Java + Android SDK/NDK for Android tooling.

Clone the repository

bash
git clone https://github.com/danielforface/aura-lang.git
cd aura-lang

Inspect the primary command surface rather than relying on historical docs:

bash
cargo run -p aura -- --help

Write a small Aura program

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

    val next: u32 = x + 1
    assert next <= 100
    next

Aura uses significant indentation. Current language syntax is summarized in the Language Reference.

Build

bash
cargo run -p aura -- build main.aura

The primary CLI exposes build profiles (dev, release, verify) and execution modes (avm, llvm, hybrid). Backend maturity is not uniform; see Toolchain & Project Layout.

Run in the development path

bash
cargo run -p aura -- run main.aura

The AVM / development VM is the clearest low-friction execution path. Current source explicitly notes that automatic AVM → LLVM promotion in hybrid execution is not yet implemented, so hybrid should not be interpreted as a production JIT.

Verify with Z3

With the Z3 feature/toolchain available:

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

Profiles exposed by the CLI:

  • fast — interactive/low-latency-oriented,
  • ci — CI-oriented,
  • thorough — deeper verification.

Optional incremental solver state inside a run:

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

A latency target such as <200ms P95 is not a universal website benchmark unless a reproducible measurement artifact accompanies it.

Test, lint and format

bash
cargo run -p aura -- test .
cargo run -p aura -- lint main.aura
cargo run -p aura -- fmt main.aura --check
cargo run -p aura -- fmt main.aura --write

Continue