Language explorer

Read Aura syntax with its proof semantics beside it.

This is an interactive documentation explorer, not a browser-hosted Aura compiler or Z3 session. It intentionally demonstrates syntax and reasoning vocabulary without fabricating verification results.

Aura source explorernot a live compiler

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

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

What to notice

requires establishes a precondition

ensures describes the result contract

assert becomes a proof obligation

u32 range refinement carries bound information