Secure contracts by construction.
Lithe is a smart-contract language for the EVM. Entrypoints are state transitions with explicit effects, typed failures, and deterministic storage. The compiler enforces the security rules that Solidity leaves to convention.
import "std/evm";
error InsufficientBalance of record {
available : wei;
required : wei;
}
event Withdrawn of record {
indexed account : address;
amount : wei;
}
storage is record {
balances : map(address, wei);
}
external payable function deposit() is {
storage.balances[Evm.sender()] := storage.balances[Evm.sender()] + Evm.value();
}
external function withdraw(const amount : wei)
raises InsufficientBalance
is {
const balance : wei := storage.balances[Evm.sender()];
assert(
balance >= amount,
InsufficientBalance { available = balance; required = amount; }
);
storage.balances[Evm.sender()] := balance - amount;
emit Withdrawn { account = Evm.sender(); amount = amount; };
defer Evm.transfer(Evm.sender(), amount);
}Why now
Smart contracts are now written with AI and attacked with AI. In Anthropic's SCONE-bench, AI agents produced working exploits for 51% of 405 real exploited contracts, and scanning a new contract for bugs cost about $1.22.
The bugs that lose the most money are not exotic. In 2024, access-control flaws caused about two thirds of smart-contract losses: a missing caller check, an open initializer, an unguarded upgrade. Reentrancy caused under 3%. Lithe turns these conventions into compiler rules, so neither the developer nor the model has to remember them.
What you get
A state-changing call to another contract runs after your entrypoint has finished its own work, so a callee never sees half-updated state.
Errors are types. Every external function lists the errors it can raise in raises, and the compiler checks that the list is complete.
pure, view, and stateful functions are verified against their bodies. A view cannot write storage, emit, or defer.
State invariants, what each function does, and exactly when it reverts in a spec file beside the contract. lithe prove proves them, one transition phase at a time, for every input and order of calls.
The default storage lays out exactly as Solidity's does. Named domains sit at ERC-7201 roots and survive upgrades and refactors.
Modules own their storage and functions. A contract says which functions it exposes, so nothing becomes public by accident.
upgradeable compiles to UUPS. The upgrade guard and one-time migrations are part of the language.
Across real contracts, including OpenZeppelin tokens and Synthetix staking, Lithe emits about 32% less runtime code than optimized solc, with identical storage, logs, and return data.
The compiler reports what every entrypoint reads, writes, emits, defers, and raises, as text for reviewers or JSON for tools.