Specifications

Formal specifications and technical references for the Ora language and compiler. Aimed to be precise, but the implementation evolves quickly, so treat them as living specs.

Language specifications

Grammar

Formal BNF and EBNF grammar for Ora syntax.

MLIR Integration

Ora MLIR semantics, lowering strategy, and IR structure.

Sensei-IR (SIR)

Backend IR used for Ora lowering toward EVM bytecode.

Formal Verification

Research-oriented description of the verification model and constraints.

API Documentation

Compiler CLI and library interfaces.

Status and alignment

For the implemented baseline, see:

• TYPE_SYSTEM_STATE.md
• FIRST_PHASE_COMPLETENESS.md
• docs/ORA_FEATURE_TEST_REPORT.md

For research context and rationale, see:

• Type System
• Comptime
• SMT Verification
• Refinement Types

These documents are closer to compiler reality than any single narrative page.

Contributing

If you update a specification, also update the corresponding implementation notes or tests. Specs should either describe the current behavior or clearly label the gaps.