Merak

A language for Ethereum smart contracts that combines liquid types with explicit specifications to provide compile-time safety guarantees with minimal runtime overhead. Merak is a research project exploring the intersection of formal verification, type theory, and blockchain security. It represents a long-term vision for how smart contracts should be written: with mathematical certainty of correctness built into the development process itself.

⚠️ Development Status & Stability Notice: Merak is an experimental research language under active development. While the core architecture is taking shape, the compiler produce unverified/unsecure bytecode. The language semantics, type system, and compiler architecture are expected to evolve significantly, and future releases may introduce breaking changes without backward compatibility guarantees. While Merak currently plans to target the Ethereum Virtual Machine (EVM), alternative compilation targets and execution models are under consideration, and the intended target platform may change as the project matures.

Overview

Merak is designed to address the fundamental challenge of smart contract security: vulnerabilities that lead to catastrophic financial losses. Rather than relying primarily on runtime checks or post-deployment audits, Merak uses refinement types (liquid types) to verify safety properties at compile time.

Key Design Principles

• Verification then Erasure: Type refinements are checked at compile time and mostly erased before codegen, minimizing bytecode bloat
• Explicit Specifications: Function contracts use requires/ensures clauses (Hoare Logic style) rather than pure inference, giving developers fine-grained control over verification
• Fold/Unfold Semantics: Storage operations follow a rigorous model that captures EVM semantics and enables reentrancy safety analysis

Language Features

Refinement Types

Merak extends base types (int, address, bool) with logical predicates that constrain their values:

state var balance: {int | balance >= 0} = 0;

function withdraw(amount: {int | amount > 0 && amount <= balance}) {
    balance = balance - amount;
    // Compiler proves balance remains non-negative
}

The type system ensures that balance can never become negative, catching underflow bugs at compile time.

Function Contracts

Developers can specify preconditions and postconditions using standard Hoare Logic notation:

function transfer(to: address, amount: {int | amount > 0})
requires (balance >= amount, msg.sender == owner)
ensures (balance == old(balance) - amount)
{
    balance = balance - amount;
    // Transfer logic...
}

The compiler generates verification conditions to prove the implementation satisfies its specification.

Loop Invariants and Variants

Loops require explicit invariants (what remains true each iteration) and variants (what decreases to prove termination):

while (i < n) 
with @invariant(0 <= i && i <= n) 
     @variant(n - i)
{
    sum = sum + i;
    i = i + 1;
}

This enables verification of loops without needing unbounded unrolling.

Compiler Architecture

Merak follows a multi-phase pipeline inspired by established compiler designs (LLVM, rustc, GCC):

AST
 ↓
[✓] Phase 1: Symbol Resolution
 ↓
[✓] Phase 2: Basic Type Checking
 ↓
[✓] Phase 3: CFG Construction
 ↓
[✓] Phase 4: Dominance Analysis & Loop Detection
 ↓
[✓] Phase 5: SSA Transformation
 ↓
[✓] Phase 6: Storage Analysis (fold/unfold + reentrancy)
 ↓
[✓] Phase 7: Refinement Inference / Type Checking
 ↓
[🔄] Phase 8: EVM Bytecode Generation
 ↓
[🔄] Phase 9: Multi-level optimization passes (EVM, SSA, Bytecode)

Current Progress

Completed Phases (1-7):

• Full AST with refinement type syntax
• Basic type checking for base types
• Control Flow Graph with basic blocks
• Dominance tree and natural loop detection
• SSA transformation
• Storage analysis providing fold/unfold semantics with invalidation tracking
• Liquid types constraint generation system
• Four-phase inference algorithm: template assignment → constraint generation → iterative weakening → solution extraction
• Z3 SMT solver integration for constraint solving

In Progress (Phase 8 & Phase 9):

• EVM bytecode generation
• EVM optimizations

Planned (Phase 9 2.0):

• Multi-level optimization passes (SSA, Bytecode)

⚠️ Testing Disclaimer: For now, all tests in this project were generated by AI and reviewed until they pass. They should not be considered reliable indicators of correctness. Comprehensive test coverage and validation remain a critical TODO.

Future Roadmap

Near-term

• Finish imple mentations of EVM bytecode generation and optimizations
• Extend language with advanced features: arrays, mappings and other structures
• Extensive testing on real-world contract patterns

Medium-term (Optimizations)

• SSA-level optimizations (constant/copy propagation, dead code elimination)
• EVM-level optimizations (peephole patterns, stack optimization, gas optimization)

Long-term (UX - Developer tooling)

• Integration with existing Solidity contracts
• Language server and IDE support
• Documentation and tutorials for beginners and advanced users

Contributing

Merak is an ambitious long-term project. While it's not ready for production use, I believe formal verification is essential for blockchain's future. At this time, we are not accepting pull requests, but you can support the project via donations:

Ethereum Donation Address: 0x7ff4408bf503cdd3991771a18e8f8c364eace215

Donations will go toward:

• Development time and research
• Security audits when approaching production readiness
• Documentation and developer tooling

Contact

For questions, suggestions, or collaboration inquiries, please open an issue on this repository.

---