Runtime Verification Hosts EthCluj Workshop on Formal Methods
On April 14th, Andrej Vacaru and Raoul Schaffranek from Runtime Verification were privileged to lead an online workshop hosted by the EthCluj community. We are sincerely grateful for this opportunity, which allowed us to share our passion for innovative software verification tools with an engaged audience.
The workshop provided a comprehensive introduction to Runtime Verification's advanced toolset designed to make formal methods, which involve rigorous techniques used in software development to ensure program correctness through mathematical proofs, more accessible to everyone.
Raoul initiated the session with a presentation and live demo of Simbolik, a Solidity debugger that enhances traditional debugging with symbolic execution capabilities. Symbolic execution is a method of software testing where the program is executed with symbolic inputs instead of actual data. This allows the analyzer to evaluate many execution paths simultaneously. Raoul carefully delineated the distinction between concrete execution, where the program runs with real data, and symbolic execution, which abstracts data to symbols that cover more potential scenarios in a single debugging session.
Building on this foundational knowledge, Andrej introduced Kontrol, a symbolic testing tool that embodies the same principles as Simbolik. Kontrol is specifically designed to establish program correctness and seamless integration with continuous integration (CI) systems, facilitating regular and automated checking of code changes. This tool exemplifies how symbolic testing can streamline the development process by detecting potential errors systematically and avoiding regression.
Both presentations underscored Runtime Verification's commitment to enhancing software reliability and security through cutting-edge tools, ultimately fostering a deeper understanding and broader adoption of formal methods within the Blockchain community. We look forward to continuing our collaboration with EthCluj, and further contributing to the advancement of secure and dependable software systems.
For those who missed the live event or wish to review the discussions, the full recording is now available to the public. We hope it serves as a valuable resource for developers and enthusiasts interested in advancing their knowledge of formal verification tools.
About EthCluj
ETHCluj started as a local Romanian dev community, Cluj being the main tech hub of the country. It is a community of web3 enthusiasts with a heart for Ethereum and Solidity. We're all about diving deep into blockchain programming, learning together, and sharing what we know. Our gatherings range from hands-on workshops to casual talks, designed for everyone from beginners to seasoned devs. We're here to support each other in our journey, exploring new ideas and building a strong, knowledgeable community.
About Runtime Verification
Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.