Ora: comptime-first, solver-in-workflow EVM language

Language Design
1

Hi everyone,

I asked earlier if it’s OK to post about Ora here and got the green light — sharing an early preview of Ora, a smart contract language + compiler targeting the EVM:

Ora is not trying to be “Solidity with different syntax”. The goal is a Solidity-familiar surface (contracts/state/mappings/events/errors) with a different design center: decide as much as possible at compile time, keep EVM semantics explicit, and integrate verification into the normal build workflow.

Ora aims to do for formal verification what Foundry did for Solidity testing: make it fast, local, and part of the default workflow—not an afterthought.

TLDR: Ora in 30 seconds

  1. Comptime > runtime. Constant folding, refinement discharge, and proofs run before code is final. If we can prove it or fold it at compile time, we do; runtime checks are the fallback.

  2. Solver in the workflow. Specs (requires / ensures / invariant) live next to code, and Z3 runs as part of the pipeline—SMT reports and counterexamples show up in build artifacts.

  3. Explicit semantics + inspectable pipeline. Regions (storage / memory / calldata / transient) are explicit, and the compilation path is visible (Ora → Ora MLIR → SIR → EVM).

One small example (refinements + specs + typed errors)

contract MiniToken {
    storage balances: map<address, u256>;

    log Transfer(indexed from: address, indexed to: address, amount: u256);
    error InsufficientBalance(required: u256, available: u256);

    pub fn init(owner: NonZeroAddress, supply: NonZero<u256>) {
        balances[owner] = supply;
    }

    pub fn transfer(to: NonZeroAddress, amount: NonZero<u256>)
        -> !bool | InsufficientBalance
        requires balances[std.msg.sender()] >= amount
        ensures balances[std.msg.sender()] == old(balances[std.msg.sender()]) - amount
        ensures balances[to] == old(balances[to]) + amount
    {
        let from = std.msg.sender();
        let available = balances[from];
        if (available < amount) return error.InsufficientBalance(amount, available);

        balances[from] = available - amount; // checked arithmetic by default
        balances[to]   = balances[to] + amount;

        log Transfer(from, to, amount);
        return true;
    }
}

  • Refinements (NonZeroAddress, NonZero) encode invariants in types; the compiler + verifier use them to remove redundant guards or catch bugs early.

  • Errors are values: return error.X(…) is explicit and reflected in the return type !T | E…

  • Specs sit next to code: requires / ensures drive verification; if a proof succeeds, the corresponding runtime guard can be removed.

Comptime + generics (Zig-inspired, EVM-focused)

Ora tries to keep runtime bytecode simple by pushing work to compile time:

  • Comptime constant folding: pure expressions (and pure calls with constant args) fold during compilation; no storage/calldata access at comptime.

  • Generics via comptime type parameters: helpers are reusable without runtime polymorphism; each instantiation is monomorphized into concrete code you can inspect in emitted IR/bytecode.

fn max(comptime T: type, a: T, b: T) -> T {
    if (a > b) return a;
    return b;
}

pub fn demo(a: u256, b: u256) -> u256 {
    return max(u256, a, b);
}

Feedback I’d love from Solidity devs

  1. Does explicit region annotation feel like clarity or friction in real contracts?

  2. Which refinement types would you actually use day-to-day (NonZero, BasisPoints, ranges, etc.)?

  3. What’s the minimum verification workflow that would be useful (even if it’s not “prove everything”)?

  4. Tooling expectations: ABI compatibility, debugging, source maps, integration points—what matters most?

Thanks in advance (critical feedback is also welcome)

2 Likes
2

Here is what I used as “Hello world”

3

Hey, this is pretty cool. Thanks for sharing!

I need to dig deeper into this at some point and I’ll try to answer your questions. I’m seeing some odd formatting in your code snippet in the first post. Could you link to a snippet of it instead maybe? I just see [object Object], [object Object]....., so a permanent link to a snippet would be great.

This post also made us discuss a bit internally if a dedicated forum category for “languages compiling to yul” would make sense. What do you think about this initiative?

edit: checked in again now some hours later, and the code snippets look good again. Maybe just a glitch earlier.

4

Hi, thank you for your interest in Ora.

If you want to check and get a general feel of Ora, check Ora examples