Crypto review
Contracts, circuits, clients, cryptography. If an agent or a compiler sits next to the vault, it goes in the threat model.
Surfaces
- EVM contracts in Solidity and Vyper. Proxies, upgrades, and the deployment scripts that set them up.
- Non-EVM programs too: Rust on Solana, Move, CosmWasm. Account and permission models that EVM habits get wrong.
- Circuits and proof systems. Circom, Halo2, Noir, Plonky-style stacks, recursion. Trusted-setup and transcript handling around them.
- Clients and node software. Consensus and networking, where a parsing bug is a chain split.
- Cryptographic protocols and key handling. Signature schemes, threshold and MPC signing, key derivation. The wallet policy engine that decides when to sign.
- Bridges and cross-chain messaging: relayers, light clients, and the finality assumptions each side makes.
Failure modes we review
- Accounting invariants that break. Reentrancy, rounding that leaks value across many small calls, share-price manipulation on first deposit, fee paths that skip the sum.
- Uninitialized implementations, storage collisions across proxy versions, admin roles granted to a keeper that a model drives.
- Oracle dependence: stale prices, single-source feeds, manipulable TWAP windows, and parameters a model or off-chain job can write without bounds.
- Underconstrained circuits. Missing range checks and unconstrained witnesses. Soundness holes from an optimizer or a compiler pass, and completeness bugs that only fail on production inputs.
- Signatures and replay: missing domain separators, malleable encodings, nonces tracked in the wrong place, intents valid on a chain they were never meant for.
- Key custody in automation. Private keys in the environment of the same process that executes untrusted input. Signing policies that trust a simulation result. No second signer on high-value paths.
- Governance and timelock bypasses, emergency paths that skip the delay, pause mechanisms a compromised keeper can trigger.
- MEV-shaped assumptions: ordering, front-running, sandwich paths that a spec treats as atomic. The chain does not.
Formal methods, when they earn a place
We write invariants for accounting, access control, and state machines that can be stated over a bounded state. Where a property is worth proving, we write the spec and run it against the bytecode or the circuit. The report says which properties were proved, which were tested, and which were only read.
A proof is as good as its spec. We will not use a prover to narrate what a model does. The code around the proof still gets read. A learned heuristic in a compiler pass can drop a range check the handwritten circuit still had. The proof still passes.
What we will not take
- Simple token rubber stamps. A standard ERC-20 with a launch thread is not a review.
- Quick looks that skip the join. If an agent holds the key and the request puts that out of scope, we will ask why before we say yes.
- A review that treats the model as a black box that cannot fail. The report will name the model as in-scope or as explicitly out. Not as a footnote.
- Contest or bounty runs staffed from a marketplace. Different product, different firm.
Request a scoping call
Tell us the chains, the languages, and the proof system if there is one. And whether anything that is not a human can sign. Crypto-only scope is a real engagement. A join hidden inside one is a rewrite.