Toolchain

One language. Several deliberately different execution paths.

The primary CLI orchestrates parsing, semantic analysis, IR, verification, AVM execution, native-oriented backends, FFI and project tooling. The site keeps backend maturity and feature gates visible instead of collapsing them into one “native compiler” claim.

aura build main.aura
aura run main.aura
aura verify main.aura --smt-profile ci
aura test .
aura lint main.aura
aura fmt main.aura --check
aura bindgen --header demo.h --out build/bindgen

Command surfaces

Code-backed tooling, labeled by maturity.

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.

Execution model

AVM is not LLVM, and hybrid is not a JIT.

The distinction matters. AVM provides a development execution path. The C backend supplies a portable native-oriented route. LLVM IR emission exists behind a feature gate and remains evolving. Current source explicitly says automatic AVM → LLVM promotion inside hybrid execution is not yet implemented.

AVM

code-backed

Development VM / interpreter for the low-friction edit-run loop, with debug machinery in `aura-interpret`.

C backend

code-backed

C23-oriented emission is the default backend surface exposed by the CLI and a useful portability/differential anchor.

LLVM IR

evolving

Implemented, feature-gated emission with codegen/debugger/pattern modules, but source still describes parts as phase/skeleton work.

Workspace

The compiler is a monorepo architecture.

Twenty-two workspace crates separate concerns so semantics, proof, execution and tooling can evolve without turning the primary CLI into a monolith.

CrateRoleSurface

auraCLI / orchestrationworkspace

aura-lexIndentation-aware lexerworkspace

aura-parseParser + edition/feature configworkspace

aura-astSource syntax representationworkspace

aura-coreSemantic core, lowering, diagnostics, safety analysisworkspace

aura-irValidated intermediate representationworkspace

aura-verifyProof engine, Z3 integration, counterexamplesworkspace

aura-interpretAVM / development VMworkspace

aura-backend-cC23-oriented backendworkspace

aura-backend-llvmFeature-gated LLVM IR backendworkspace

aura-rtRuntimeworkspace

aura-rt-nativeNative runtime supportworkspace

aura-stdlibStandard libraryworkspace

aura-pkgPackage managerworkspace

aura-lspLanguage server + proof protocolworkspace

aura-sdkSDK crateworkspace

aura-bridgeFFI / native bridgeworkspace

aura-nexusPlugin host / integration layerworkspace

aura-plugin-luminaLumina UI/application pluginworkspace

aura-plugin-aiOptional AI pluginworkspace

aura-plugin-iotOptional IoT pluginworkspace

aura-ai-optAI-oriented optimization toolingworkspace

FFI

Bridge native code without hiding the boundary.

`aura-bridge` and `aura bindgen` create a path from C/C++ headers and link inputs into Aura. Refined type mapping is best-effort; generated bindings belong in the trusted/audited boundary.

aura bindgen \
  --header demo.h \
  --out build/bindgen \
  --refine-types

Release engineering

Artifacts can carry provenance.

The release tooling implements deterministic archive metadata/order, SHA-256 hashing, attestation JSON, optional Windows signing and Sentinel sidecar staging.

python tools/release/release.py --help