Targets Overview

The Cambrian transpiler is a domain × language matrix. A domain fixes the execution semantics (what a send, address, or balance means). A language is the carrier syntax the emitter writes. Each public CLI flag selects one supported cell of that matrix.

cambrian-transpiler <input.cam|project.yaml> -o <dir> --target evm|lean

The default target is evm. In project.yaml, set target: evm or target: lean. Unknown names are rejected — there is no silent fallback to a default.

Domain × language

Domain	Meaning	Languages	CLI targets
EVM	Synchronous call / CREATE2 / ETH-balance model	Solidity, Lean	`evm`, `lean`

Same-domain cores share semantics. A .cam program that is valid for Domain EVM should behave the same under --target evm and --target lean (modulo Lean-only validation such as L5–L14).

On the EVM domain, evm::* intrinsics and E-family rules apply. Lean keeps property blocks as theorems; --target evm expands them into concrete tests and fuzz cases. Multi-entity invariants are accepted on both public targets.

Informal names vs CLI vs output

Informal name	CLI / `project.yaml`	Domain	Language	Typical output
Solidity@ETH / Solidity-EVM	`--target evm` (default)	EVM	Solidity	Flat `src/*.sol` (`pragma solidity ^0.8.24`), Foundry tests, `foundry.toml`
Lean-EVM	`--target lean`	EVM	Lean 4	Lake project: `Cambrian/Generated/.lean`, `Spec.lean`, `World.lean`, `lakefile.toml`

# EVM Solidity + Foundry
cambrian-transpiler contracts/counter.cam -o /tmp/out-evm --target evm

# Lean 4 model of the same EVM domain
cambrian-transpiler contracts/counter.cam -o /tmp/out-lean --target lean
cambrian-transpiler contracts/counter.cam -o /tmp/out-lean --target lean --check-lean

--check-lean runs lake build in the output directory after a Lean emit; on other targets it only warns.

Capability matrix

Capability	`evm`	`lean`
Models EVM (`evm::*`, CREATE2, payable, …)	yes	yes
Desugars `property` → `test` / `fuzz`	yes	no (keeps theorems)
Multi-entity invariants	yes	yes
Primary test oracle	`forge test`	`lake build`

Choosing a target

Ship on Ethereum → evm (Foundry / solc via forge).
Prove EVM-domain properties → lean (same semantics, theorem statements; main proofs may be sorry).

Active conformance policy for new language features prioritises Solidity@ETH, then Lean. Details live in the language repo’s docs/TESTING_TARGETS.md.

Chapter map

Chapter	Contents
Solidity-EVM	Flat Solidity, Foundry, CambrianFactory, payable, events/errors
Lean-EVM	Lake layout, World/`*Spec`, sorry policy, L-rules