Ora v0.2: Proof-Carrying Contracts
· 12 min read
Ora v0.2 is the release where the pieces start to act like one system.
The headline features are big on their own: first-class Result<T, E> values,
a unified ADT model, Z3-backed verification reports, runtime ABI encoding,
dynamic public returns, traits, debugger improvements, LSP production work,
compiler metrics, CFG output, and a real MLIR optimization pipeline.
But the real v0.2 story is simpler: Ora is moving from "a compiler with verification features" toward contracts that carry their proof obligations, their runtime checks, their ABI shape, and their debugging evidence through one pipeline.
