Focus Areas
Practical docs and research artifacts, side by side.
Language
- Region-aware types and effects
- Refinement types and Result/error unions
- Unified ADTs and exhaustive matching
Compiler
- Ora MLIR lowering and verification ops
- Sensei-IR backend integration
- MLIR optimization, CFG, metrics, and Z3
Research
- Type system spec v0.11 PDF
- Comptime, SMT, and proof trust boundaries
- Refinement strategy and guard semantics
Ora in Practice
Explicit errors, verification clauses, and predictable behavior.
error InsufficientBalance(required: u256, available: u256);
contract Vault {
storage var balances: map<NonZeroAddress, u256>;
pub fn withdraw(amount: MinValue<u256, 1>)
-> Result<u256, InsufficientBalance>
requires balances[std.msg.sender()] >= amount
ensures_ok(balances[std.msg.sender()] == old(balances[std.msg.sender()]) - amount)
{
let sender: NonZeroAddress = std.msg.sender();
let current: u256 = balances[sender];
if (current < amount) {
return Err(InsufficientBalance(amount, current));
}
balances[sender] -= amount;
return Ok(balances[sender]);
}
}Research Backbone
Formal specs, implementation baselines, and proof-boundary docs are linked directly to source artifacts.
Join the Development
Focused contributions: tests, docs, and compiler work.