Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Introduction

Cambrian is a language for stateful, message-based programs. A single .cam source describes entities, routes, and state transforms once; the Cambrian transpiler then lowers that source to one of several backends:

TargetCLI flagOutput
Solidity-EVM--target evm (default)Flat Solidity (^0.8.x) plus Foundry harness
Lean-EVM--target leanLean 4 + Lake project for formal verification (same EVM domain semantics)

One program can run on-chain (EVM) or as Lean proofs of the same EVM model — and the same language ideas apply when you are not targeting a blockchain at all.

Why Cambrian?

Many systems need explicit state, clear entry points, and disciplined communication between components. General-purpose languages leave those concerns scattered across imperative updates and ad-hoc APIs. Cambrian makes entity state, routes, and inter-entity messages part of the syntax.

There is no hidden control flow and no ambiguity about what an entity does when a route runs. Specs live in the same source: test, property / fuzz, and invariant blocks lower to Foundry tests or Lean theorems depending on the target.

Smart contracts are a common use case (durable state, multi-party messaging, expensive mistakes), but they are not the only one. The model fits anywhere you want member-centric state and message-shaped interfaces.

Key Principles

Member-Centric State

Members are named, typed fields that belong to an entity. Each member declares its own transformation rules inline, specifying exactly how it changes in response to each route. This inverts the traditional pattern where a function body scatters state updates across imperative statements.

m_balance: U256 {
    in deposit(amount) => m_balance + amount
    in withdraw(amount) => m_balance - amount
}

Routes

Routes are the named entry points of an entity. They declare parameters, optional preconditions, and the actions that run when the route is invoked.

routes {
    deposit(amount: U256) => []
    withdraw(amount: U256)
        where (m_balance >= amount) : throw InsufficientBalance()
    => [
        emit Withdrawal(msg::sender, amount)
    ]
    getBalance() -> U256 => [
        return(m_balance)
    ]
}

Temporal References

The temporal reference operator ^x refers to a member’s value after its transform for the current route has been applied. Use it when another member’s transform (or a later action) must see updated state, not the pre-transform snapshot.

m_count: u64 {
    in increment() => m_count + 1
}

m_total: u64 {
    in increment() => m_total + 1
}

m_over_limit: bool {
    // Without ^, m_count / m_total would still be the old values.
    in increment() => ^m_count > 100 || ^m_total > 1000
}

Pure Functions

Cambrian distinguishes state-modifying routes from pure functions. Pure functions cannot access or modify entity state; they operate solely on their inputs and produce a deterministic output.

pure fn max(a: u64, b: u64) -> u64 {
    if a > b { a } else { b }
}

Message-Based Routing

Inter-entity communication uses the send operator ~> to dispatch typed messages. On EVM this becomes a call (with optional value); on Lean it is a world-state transition.

Transfer(to, amount) ~> Token.address()

Properties and Invariants

Verification is part of the language, not a separate toolchain glue layer.

A property is a parameterized statement about an entity, with nested concrete test instances and sampling fuzz instances:

property "increment from zero" (amount: u64) for Counter with { m_count: 0 } {
    call increment(amount)
    expect state { m_count: amount }

    fuzz { amount in 0..1000 }
}

An invariant explores random traces of routes and checks predicates after each step:

invariant "count stays non-negative" for Counter {
    init { m_count: 0 }

    action increment(amount: u64) {
        bound amount in 0..1000
    }
    action reset() { }

    check m_count >= 0
}

Plain test blocks cover fixed scenarios. The same declarations feed Foundry and Lean harnesses — see Testing and Verification.

Architecture

  .cam source  (+ optional project.yaml)
        |
        v
  Cambrian Transpiler
        |
        +---> --target evm   → Solidity + Foundry
        |
        +---> --target lean  → Lean 4 Lake project

The transpiler parses .cam files (or a multi-file project.yaml), validates them for the selected target, and emits backend-specific artifacts.

What This Book Covers

  • Getting Started — install the toolchain and compile a Counter to EVM and Lean.
  • Language Guide — entities, routes, types, events, errors, std::, shipped contract components, and multi-file projects.
  • Advanced Topics — phased routes, identity members, deterministic addresses.
  • Targets — what each backend emits and how to run it.
  • Testing and Verificationtest, property / fuzz, and invariant blocks.
  • Examples — Counter, Token, Escrow, multi-entity messaging, Governor, Uniswap V2.
  • Reference — CLI, project.yaml, keywords, grammar, validation rule codes.