# Runtime Verification Docs

[![kontrol-logo](https://3381999611-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2ywokMUDgT5enW6fv34X%2Fuploads%2FoLeig4Gwr89wE6sFwjL5%2Fkontrol%20logo%20yellow.png?alt=media\&token=1023f2b7-093e-48f7-8b8a-db019af41930)](https://docs.runtimeverification.com/kontrol/)

[Kontrol](https://app.gitbook.com/o/MwuC1PgHx91Qm96rVCnq/s/T2KVb4tqbNdAsPxsEyPQ/ "mention") combines **KEVM** and Foundry, it grants developers the ability to perform formal verification without learning a new language or tool.

***

[![simbolik-logo](https://3381999611-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2ywokMUDgT5enW6fv34X%2Fuploads%2FAjtYQyu1Pla2Lb2EWKUJ%2Fsimbolik%20logo%20blue.png?alt=media\&token=b498f450-e177-4426-9467-81b32efb15f9)](https://docs.runtimeverification.com/simbolik/)

[Simbolik](https://app.gitbook.com/o/MwuC1PgHx91Qm96rVCnq/s/WhAuD1DmzZoWPS62YwmQ/) is a powerful symbolic debugger tailored for debugging Solidity smart contracts. It leverages the capabilities of the **K** framework and employs symbolic execution techniques to meticulously identify potential vulnerabilities in smart contracts.

***

[![kasmer-logo](https://3381999611-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2ywokMUDgT5enW6fv34X%2Fuploads%2FFDZzenYyzIEm8VwRb5Oa%2Fkasmer%20logo%20yellow.png?alt=media\&token=644d6f3b-d148-4189-986a-587af43389a5)](https://docs.runtimeverification.com/kasmer/)

[Kasmer](https://app.gitbook.com/o/MwuC1PgHx91Qm96rVCnq/s/LNjJhIy8IvwZQiEZCgXW/ "mention") is a tool based on rigorous formal semantics that provides property testing and verification for the MultiversX blockchain.

***

[![ERCx-logo](https://3381999611-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2ywokMUDgT5enW6fv34X%2Fuploads%2FKHih29NMp0tUGtQM0ELF%2Fimage.png?alt=media\&token=dc28565a-b57b-47da-a281-6225c5299cb5)](https://docs.runtimeverification.com/ercx)

[ERCx](https://app.gitbook.com/o/MwuC1PgHx91Qm96rVCnq/s/ywbjiQ7KftDuGzYwEwOp/ "mention") a tool built to check the *conformance* of a contract to the [ERC (Ethereum Request for Comments) standards](https://eips.ethereum.org/erc).

***

[![KaaS-logo](https://3381999611-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F2ywokMUDgT5enW6fv34X%2Fuploads%2Fgit-blob-5fe7eda8054d548356cfb259093e3713aaa7ab23%2Fkaas%20logo%20yellow.png?alt=media)](https://docs.runtimeverification.com/kaas)

[KaaS](https://app.gitbook.com/s/uVN3ospSdbIsN8UHDZSg/overview/readme "mention") CI integrated, cloud-based symbolic execution accessible via an API

\[komet]\((<https://docs.runtimeverification.com/komet/>)

### Join Us

Please come and join us in [discord](https://discord.com/invite/CurfmXNtbN) and let us know what you would like us to do next. And, if by any chance you are looking for a career change or you are a student looking for an internship, [come and talk to us](https://runtimeverification.com/careers)! We are always looking for exceptional individuals with a passion for formal methods and **K** to join the team in our office in Urbana, Singapore, or remotely from anywhere in the world.