3 posts tagged with "verification"

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.