One precise language from specification to implementation

Why Cambrian?

A smart contract project moves through several representations: business rules in plain language, a specification, Solidity code, a test suite, formal proofs. Every hand-off between them is a place where meaning can drift. Cambrian is a single declarative representation of contract behavior that every stage reads from, so the AI agents generating code and the prover establishing properties are working against one source, not five loosely related documents.

It is built for stateful semantics — the way a contract's storage changes across transactions — and for formal translation, so a property written once can be carried into a machine-checked mathematical proof without being re-stated by hand.

What Cambrian connects

One source, two renderings

A Cambrian description is the single thing every stage reads from. The Solidity you deploy and the Lean the proof runs in are generated from it — not written separately and then kept in sync by hand.

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

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

property never_overdraws:
  always (m_balance >= 0)

uint256 public balance;

function withdraw(uint256 amount) external {
  require(balance >= amount, "InsufficientBalance");
  balance -= amount;
  emit Withdrawal(msg.sender, amount);
}

theorem never_overdraws (s : State) :
    0 ≤ s.balance := by
  induction s using reachable.rec <;>
    simp_all [deposit, withdraw]

Go deeper