Dexter is a decentralized exchange on Tezos. We used the K framework to formally verify entrypoints to the contract.

EDEN is a SNARK-friendly virtual machine and instruction set, based on the low-level functional language Nock, which is built around binary trees. These binary trees lend themselves exceptionally well to ZK operations as they are easily encoded into polynomials, and operating on them as such is very efficient. Runtime Verification were consulted on the paper to provide perspectives on the design and analyze the security of the architecture.

Alchemix is a lending and stablecoin protocol on Ethereum. The audit is an excellent example of using hand verification, where we construct important invariants and write mathematical proofs on them to convince ourselves, the developers, and anyone reading the report that the invariants hold.

EUROe is a stablecoin designed to comply with laws and regulations in Europe, making it suitable for institutional adaption.

Optimism Labs engaged Runtime Verification to formally verify parts of their core contracts, particularly the contracts of the rollup itself, and verify that deposit events are always properly emitted.