Ora Development Notebook

An experimental smart contract language with formal verification capabilities

⚠️ EXPERIMENTAL PROJECTOra is in active development and is NOT ready for production use. This is an open notebook documenting the language design and implementation progress.

✅Core CompilationLexical → Syntax → Semantic → HIR → Yul

🚧Formal VerificationIn active development

🚧Advanced SafetyMemory safety, overflow protection

Current Language SampleSubject to change

contract SimpleToken {
    storage var total_supply: u256;
    storage var balances: map[address, u256];
    
    log Transfer(from: address, to: address, amount: u256);
    
    pub fn transfer(to: address, amount: u256) -> bool {
        requires(balances[std.transaction.sender] >= amount);
        requires(to != std.constants.ZERO_ADDRESS);
        
        @lock(balances[to]);
        balances from std.transaction.sender -> to : amount;
        
        log Transfer(std.transaction.sender, to, amount);
        return true;
    }
}

Current Development Focus

📝 Grammar DefinitionRefining syntax and semantic rules

🔧 HIR ImplementationHigh-level IR for analysis passes

✅ Formal VerificationMathematical proof system design

Development Overview

Current implementation status and design decisions

Development Status

Core Pipeline: Lexical analysis → Syntax analysis → Semantic analysis → HIR → Yul → Bytecode is functional.
In Progress: Formal verification system, advanced safety checks, and comprehensive error handling.

Language Design

Error Handling: Zig-style !T error unions with explicit error declarations.
Memory Regions: Clear distinction between storage, immutable, and compile-time constants.
Safety: Explicit memory management and type safety by design.

Implementation Notes

Built with Zig: Leveraging Zig's compile-time capabilities for meta-programming.
Yul Backend: Compiles to Ethereum's intermediate language for optimal bytecode generation.
Formal Methods: Exploring mathematical proof systems for contract verification.