Focus Areas
Practical docs and research artifacts, side by side.
Language
- Region-aware types and effects
- Refinement types and error unions
- Explicit specs: requires, ensures, invariant
Compiler
- Ora MLIR lowering and verification ops
- Sensei-IR backend integration
- Z3-based SMT verification pass
Research
- Type system spec v0.11 PDF
- Comptime + SMT policy and gaps
- Refinement strategy and guard semantics
Ora in Practice
Explicit types, verification clauses, and predictable behavior.
contract Vault {
storage var balances: map[NonZeroAddress, u256];
log Transfer(sender: address, recipient: address, amount: u256);
pub fn transfer(to: address, amount: MinValue<u256, 1>) -> bool
requires balances[std.msg.sender()] >= amount
requires to != std.constants.ZERO_ADDRESS
ensures balances[to] == old(balances[to]) + amount
{
var sender: NonZeroAddress = std.msg.sender();
balances[sender] -= amount;
balances[to] += amount;
log Transfer(sender, to, amount);
return true;
}
}Research Backbone
Formal specs, implementation baselines, and open gaps are linked directly to source artifacts.
Join the Development
Focused contributions: tests, docs, and compiler work.