Ora is a smart contract language and compiler for the EVM with two design pillars: comptime over runtime—decide as much as possible at compile time, so runtime is the fallback—and formal verification and the solver in the developer workflow, the way Foundry put serious testing into the Solidity workflow. FV and Z3 aren’t a separate research step; they’re in the loop: specs next to code, SMT reports in the build artifacts, counterexamples when a proof fails. Here’s what that looks like.

Designing types for smart contract languages has unusually high stakes. Types leak into ABI boundaries. Storage layouts become long-lived commitments. And small semantic choices can turn into permanent protocol constraints that survive long after the feature that introduced them has been forgotten. At the same time, the execution environment pushes us in the opposite direction. The EVM is a 256-bit stack machine with minimal native structure, and the most important operations in a contract—calls, state reads, state writes—carry both financial and adversarial weight. If you care about verification, those realities don't just influence the language. They define it.

Ora is a smart contract language and compiler for the EVM with explicit region/effect semantics, refinement types, and an MLIR-based pipeline backed by SMT solving. As the language matures beyond its core type system (integers, booleans, addresses, maps, structs, enums, and error unions), we keep coming back to the same problem. How do you extend a type system without freezing the language too early?

Smart contracts live in a harsher environment than normal software: execution is expensive, everything is observable, and complexity becomes attack surface. "Good compilation" isn't just about speed—it's about predictability. Smaller runtime code. Fewer branches. Fewer guards. Less that can go wrong.

Ora's comptime pipeline exists to enforce that. When an expression is provably constant, the compiler evaluates it during compilation, replaces it with a literal, and lets the rest of the pipeline operate on something simpler than what the developer wrote.

That sounds obvious. In practice, it's one of the places where many smart-contract toolchains accumulate accidental complexity.

We just published the Ora ABI v0.1 spec.
This is a tooling-first ABI model with stable type identities, a clear manifest format, and optional wire profiles for encoding.

It's the interface layer we wish every smart contract language had: self-describing, structured, and built for codegen, explorers, and UI generation.

We're removing all Solidity compiler (solc) dependencies and dropping the Yul backend from Ora.
Instead, we're building a community-driven, open intermediate representation (IR) that is not tied to any single language or toolchain.

Smart contracts need a type system that's both safe and predictable. After years of working with Solidity's implicit behaviors and Rust's complex ownership rules, we asked: what if we took the best parts of both and built something specifically for the EVM?

That's how Ora's type system came to be. It's Zig-first in philosophy (explicit, no hidden control flow), Rust-influenced in safety (affine types for resources), and EVM-native in execution (every construct maps clearly to bytecode).

Smart contracts deal with money. That means every integer operation, every division, every transfer needs to be correct. Traditional type systems catch some bugs, but they don't catch the ones that actually matter: "is this value non-zero?", "is this amount above the minimum?", "is this rate within bounds?"

Refinement types fix that. They let you express constraints directly in the type system, and the compiler enforces them—at compile time when possible, at runtime when necessary.

The Ora compiler now includes automatic state analysis that tracks every storage operation in your contracts. It's also halfway through Z3 integration for formal verification. Both are turning out to be more useful than I expected.

Hey! I'm building Ora, a smart contract language for EVM with particular features that make everything less magical