Pyra: a smart contract language for the EVM

A compiled, statically typed language with Python-like syntax. It compiles directly to EVM bytecode. The focus is clarity, safety, and predictable gas use.

Philosophy

• Python-like, indentation-based syntax
• Static typing
• Ahead-of-time compilation
• Predictable gas usage
• Security-focused: reentrancy checks and arithmetic checks
• Minimal runtime
• EVM-first: compiles directly to EVM bytecode (no Yul dependency)

Language design

Syntax

Inspired by Python, but statically typed and compiled:

let total_supply: uint256 = 10000

def transfer(to: address, amount: uint256):
    if amount > 0:
        call_contract(to, amount)

Features

• Indentation-based blocks
• Immutable by default; use mut for mutable state
• Static typing with built-in types
• Abstractions compile with no runtime overhead
• Generics/templates are resolved at compile time
• Reentrancy protection is enabled by default
• Compile-time gas estimation
• Built-in hooks for formal verification
• No inheritance; prefer modular composition
• No runtime garbage collection
• Compile-time constants using const

Built-in types

• uint256, int256, bool, address, bytes
• Fixed-size arrays
• struct (custom types)
• Generic containers such as Vec<T> and Map<K, V> (compile-time optimized)
• No dynamic arrays or mappings in v1

Compiler architecture

Source Code (.pyra)
  ↓
Rust Lexer/Parser (logos + chumsky)
  ↓
AST + Type Checking + Verification (single pass)
  ↓
Direct EVM Bytecode Generation
  ↓
Optimized EVM Bytecode (.bin)

Compiler notes

• Implemented in Rust
• Single-pass compilation: parse, type-check, and verify in one pass
• Direct bytecode generation: no Yul or solc dependency
• Parallel and incremental compilation
• Zero-copy parsing to reduce allocations

Compiler stack

How it differs from Vyper

1. Abstractions without runtime cost

Write high-level code that compiles to the same bytecode as hand-written versions:

# This generic function...
def safe_add<T: Numeric>(a: T, b: T) -> T:
    return a + b

# ...generates identical bytecode to:
def add_uint256(a: uint256, b: uint256) -> uint256:
    return a + b

2. Compile-time gas estimation

# Compiler provides gas costs:
def transfer(to: address, amount: uint256):  # Gas: 21,000 + 5,000 SSTORE
    balances[msg.sender] -= amount           # Gas: 5,000 SSTORE
    balances[to] += amount                   # Gas: 20,000 SSTORE

3. Built-in formal verification

def withdraw(amount: uint256):
    require amount <= balances[msg.sender]
    # @verify: balance_sum_invariant
    # @verify: no_overflow_underflow
    # @verify: reentrancy_safe
    balances[msg.sender] -= amount
    msg.sender.transfer(amount)

4. Generics and templates

Type-safe code reuse without runtime cost:

# Generic data structures
struct Vault<T: Token> {
    token: T,
    balance: uint256
}

# Generic functions with constraints
def swap<A: ERC20, B: ERC20>(token_a: A, token_b: B, amount: uint256)

5. Automatic reentrancy protection

Built into the language:

def withdraw(amount: uint256):
    # Automatically generates a reentrancy guard
    balances[msg.sender] -= amount
    msg.sender.transfer(amount)  # Guarded by default

Security features

• Automatic reentrancy protection on external calls
• Overflow and underflow checks unless explicitly marked unchecked
• Formal verification integration
• Compile-time bounds checking for array access
• Immutable by default to prevent accidental state changes
• Gas limit analysis
• Compile-time integer overflow detection

v1 goals

• Rust-based lexer and parser with logos and chumsky
• Single-pass AST and type checker
• Direct EVM bytecode generator
• Compile-time gas estimation
• Basic formal verification (Z3 integration)
• Automatic reentrancy protection
• Generics with no runtime overhead
• CLI tool (pyra build ...)
• Example contracts (ERC20, vault, DEX)

Project structure

pyra/
├── compiler/              # Rust compiler codebase
│   ├── src/
│   │   ├── lexer.rs       # logos-based lexer
│   │   ├── parser.rs      # chumsky grammar
│   │   ├── ast.rs         # AST definitions
│   │   ├── typer.rs       # Type checker and inference
│   │   ├── verifier.rs    # Formal verification (Z3)
│   │   ├── gas.rs         # Gas estimation engine
│   │   ├── codegen.rs     # Direct EVM bytecode generation
│   │   ├── security.rs    # Reentrancy and security analysis
│   │   └── main.rs        # CLI entry point
│   ├── Cargo.toml
│   └── build.rs
├── contracts/             # Example .pyra contracts
├── tests/                 # Foundry/Hardhat integration tests
├── stdlib/                # Standard library (Pyra code)
├── README.md
└── docs/

Roadmap

Future features

• ZKVM-compatible backend (Cairo, Risc0)
• Gas profiler CLI with optimization suggestions
• WASM output for off-chain simulation
• Contract interface generator (ABIs)
• Multi-chain support (EVM, Solana, Move)
• Built-in DeFi primitives (AMM, lending, governance)
• IDE integration (VS Code, Neovim)

Quick start

# Install (crates.io)
cargo install --locked pyra-compiler

# If crates.io publish isn't done yet
# cargo install --locked --git https://github.com/DavidIfebueme/pyra pyra-compiler

# Compile example contracts
pyra build contracts/ERC20.pyra
pyra build contracts/Vault.pyra

Outputs:

• <Contract>.abi
• <Contract>.bin

Performance

The compiler includes Criterion benchmarks under compiler/benches/ to track lexer/parse/codegen performance.

Author

Built by DavidIfebueme

Disclaimer

This is an experimental project. Use at your own risk. Not production-ready until v1 is officially tagged and audited.