Skip to main content

One post tagged with "lsp"

View All Tags

Ora v0.2: Proof-Carrying Contracts

· 12 min read
axe
Creator of Ora

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.