Formal Verification simplified with K


The Symbolic Debugger is a powerful tool tailored for Solidity smart contract debugging. Leveraging the capabilities of the K framework, it employs symbolic execution techniques to meticulously identify potential vulnerabilities in your smart contracts. Conveniently available as a VSCode extension, you can seamlessly integrate it into your development environment directly from the VSCode marketplace.

Raoul trust x

Raoul presented the Symbolic Debugger at Trust X 2023.