We should provide references to the projects that have Kontrol set up. These might include: - [Optimism](https://github.com/ethereum-optimism/optimism/tree/c38ce096def52e4acdaecb7ffd2d396f464693dd/packages/contracts-bedrock/test/kontrol) - [Solady](https://github.com/runtimeverification/kontrol-solady) - Patrick Collins' [course ](https://github.com/Cyfrin/sc-exploits-minimized/blob/main/test/invariant-break/formal-verification/KontrolTest.t.sol ) - [Secureum workshop repo](https://github.com/runtimeverification/secureum-kontrol) Ref: https://github.com/a16z/halmos/blob/main/examples/README.md