Ora

Ora is a verification-first smart-contract language and compiler for EVM. The Asuka v0.2 release focuses on proof-carrying contracts: explicit Result values, ADTs, SMT reports, ABI lowering, metrics, CFG inspection, and fail-closed compiler behavior.

Asuka v0.2. The language surface is still evolving, but v0.2 is a release:

supported examples should compile, unsupported shapes should diagnose, and

wrong code should not become bytecode.

What Ora does

error InsufficientBalance(required: u256, available: u256);
comptime const std = @import("std");
contract Vault {     storage var totalDeposits: u256 = 0;     storage var balances: map<address, u256>;
log Deposit(account: address, amount: u256);
pub fn deposit(amount: MinValue<u256, 1>)         requires(totalDeposits <= std.constants.U256_MAX - amount)         ensures(totalDeposits == old(totalDeposits) + amount)     {         let sender: NonZeroAddress = std.msg.sender();         balances[sender] += amount;         totalDeposits += amount;         log Deposit(sender, amount);     }
pub fn withdraw(amount: MinValue<u256, 1>) -> Result<u256, InsufficientBalance> {         let sender: NonZeroAddress = std.msg.sender();         let current: u256 = balances[sender];         if (current < amount) { return Err(InsufficientBalance(amount, current)); }         balances[sender] = current - amount;         totalDeposits -= amount;         return Ok(balances[sender]);     }
pub fn balanceOf(account: address) -> u256 {         return balances[account];     } }

This contract uses refinement types (MinValue, NonZeroAddress), Result values (Result<u256, InsufficientBalance>), specification clauses (requires/ensures/old()), events (log), and explicit storage. The compiler checks the full surface; the SMT verifier proves the supported properties below and fails closed when it cannot model a proof soundly.

Asuka v0.2 highlights

• First-class Result<T, E> and error-union values with Ok, Err, match,

try, ABI support, and SMT encoding.

• Unified ADT handling for structs, tuples, enums, Result/error unions, and

source constructors.

• Z3-backed verification reports with counterexamples, trust labels, vacuity

checks, degradation reasons, and fail-closed UNKNOWN handling.

• Runtime ABI hardening: @abiEncode, dynamic public returns, custom-error

selector reverts, dispatcher decode coverage, and ABI layout unification.

• Comptime expansion for ABI helpers, ADT/Result values, partial folding, and

bounded loop unrolling.

• Tooling for source-level EVM debugging, LSP features, compiler metrics, SIR

CFG output, and MLIR/SIR inspection.

• Hardened lowering and artifact gates: unsupported shapes diagnose instead of

emitting best-effort bytecode.

For the public verifier boundary, see website/docs/compiler/what-ora-proves.md.

Installation

Prerequisites: Zig 0.15.x, CMake, Git, Z3, MLIR

git clone https://github.com/oralang/Ora.git
cd Ora
./setup.sh
zig build

Run tests:

zig build test

Docker

docker pull oralang/ora:latest
docker run --rm oralang/ora:latest --help

Run against local files:

docker run --rm -it \   -u "$(id -u):$(id -g)" \   -v "$PWD:/work" \   -w /work \   oralang/ora:latest build ora-example/apps/erc20.ora

Install the Docker launcher so ora works like a native command:

chmod +x scripts/ora-docker scripts/install-ora-docker.sh ./scripts/install-ora-docker.sh

Use a specific image tag:

ORA_IMAGE=oralang/ora:v0.2.0 ora build ora-example/apps/erc20.ora

Build image locally

docker build -t oralang/ora:local .
docker run --rm oralang/ora:local --help

Using the compiler

Scaffold a new project:

./zig-out/bin/ora init my-project

Build a contract:

./zig-out/bin/ora build contracts/main.ora

Format source:

./zig-out/bin/ora fmt file.ora          # single file ./zig-out/bin/ora fmt contracts/        # directory (recursive) ./zig-out/bin/ora fmt --check file.ora  # CI check

Emit intermediate representations:

./zig-out/bin/ora emit --emit=mlir:ora file.ora           # Ora MLIR ./zig-out/bin/ora emit --emit=mlir:sir file.ora           # SIR MLIR ./zig-out/bin/ora emit --emit=mlir:both file.ora          # Ora + SIR MLIR ./zig-out/bin/ora emit --emit=sir-text file.ora           # Sensei text IR ./zig-out/bin/ora emit --emit=bytecode file.ora           # EVM bytecode ./zig-out/bin/ora emit --emit=ast file.ora                # Parsed AST ./zig-out/bin/ora emit --emit=cfg:sir file.ora            # Control flow graph ./zig-out/bin/ora build file.ora --explain --emit=smt-report # SMT verification report

Launch the interactive debugger:

./zig-out/bin/ora debug ora-example/arithmetic_test.ora --signature 'add(u256,u256)' --arg 7 --arg 9

See DEBUGGER.md for the debugger workflow, commands, sessions, and current limits.

Build artifacts

ora build writes to artifacts/<name>/:

artifacts/<name>/abi/<name>.abi.json          # Ora ABI
artifacts/<name>/abi/<name>.abi.sol.json       # Solidity-compatible ABI
artifacts/<name>/abi/<name>.abi.extras.json    # Extended ABI metadata
artifacts/<name>/bin/<name>.hex               # EVM bytecode
artifacts/<name>/sir/<name>.sir               # Sensei IR
artifacts/<name>/verify/<name>.smt.report.md  # SMT report (markdown)
artifacts/<name>/verify/<name>.smt.report.json # SMT report (JSON)

Imports and multi-file projects

comptime const math = @import("./math.ora");
contract Calculator {     pub fn run() -> u256 {         return math.add(40, 2);     } }

Imported members are always accessed through the alias (math.add); they are never injected into local scope.

ora.toml

schema_version = "0.1"
[compiler] output_dir = "./artifacts"
[[targets]] name = "Main" kind = "contract" root = "contracts/main.ora" include_paths = ["contracts", "lib"]

See docs/ora-cli-imports-config-reference.md for the full config schema.

Verification

Z3 verification runs by default on ora build. Build mode emits artifacts, so soundness-reducing verification escape hatches are rejected there instead of producing bytecode.

./zig-out/bin/ora build file.ora                                # full verification default
./zig-out/bin/ora build file.ora --verify=full --explain --emit=smt-report
./zig-out/bin/ora emit --emit=mlir:ora file.ora --verify=basic  # reduced-trust inspection
./zig-out/bin/ora emit --emit=mlir:ora file.ora --no-verify     # inspection only; not a verified artifact

SMT reports expose structured soundnesslosses and precisionnotes. soundnesslosscapexceeded and precisionnotecapexceeded are truncation markers, not additional independent findings: they mean the bounded report list filled and later entries were omitted.

Documentation

• The Ora Little Book — 20-chapter progressive guide from first contract to production vault
• Language reference — feature docs: types, regions, error unions, traits, verification, comptime
• Compiler Field Guide — contributor onboarding (14 chapters)
• What Ora Proves — public SMT soundness model and trust boundaries
• Formal specification — type system calculus
• CLI and config reference — full CLI, import system, and ora.toml schema
• Examples — apps, vault tiers, and feature demos

Development

zig build test
zig build gate

zig build gate is the full local bar. It runs compiler tests, conformance, EVM tests, MLIR/SIR snapshot checks, negative corpus checks, verifier mutation checks, and LSP smoke checks. Use -Dskip-mlir=true for fast non-MLIR work; run a full zig build when touching src/mlir/**.

For contributor workflow details, see CONTRIBUTING.md and the Compiler Field Guide.