Raoul Schaffranek

Explore how to leverage Simbolik for streamlined Solidity debugging. Learn to automate deployments, simulate user interactions, and create reusable debugging scenarios—all within Solidity.

simbolik-screenshot.png

 Using Simbolik for Solidity Debugging

This blog post continues our journey into formal verification of loops in Solidity and EVM smart contracts. It introduces loop invariants, a challenging but essential technique for reasoning about unbounded loops. We explore natural induction, apply pen-and-paper methods, and then leverage Kontrol to formally prove the equivalence of two Solidity functions, diving deep into EVM bytecode and formal verification tools.

DALL·E 2024-09-25 17.50.48 - A futuristic rollercoaster with multiple loopings, representing symbolic execution and bounded loop unrolling. The rollercoaster track is set against .webp

Formally Verifying Loops: Part 2

Explore the challenges of formal verification in Solidity and EVM smart contracts. Learn about the path explosion problem, bounded loop unrolling, and how tools like Certora Prover, Halmos, hevm, and Kontrol approach verifying loops in smart contracts.

Formally Verifying Loops: Part 1

Runtime Verification

we’re excited to introduce our latest tool: Komet, a formal verification and fuzzing tool designed specifically for Soroban smart contracts on the Stellar blockchain.

256A0EF8-BED9-408A-899E-1839CB2B243E.png

Introducing Komet: Smart Contract Testing & Verification Tool for Soroban, Created by Runtime Verification

borderless-capital.png

Borderless Capital

fenbushi-capital.png

Fenbushi Capital

hypersphere-dark.png

hypersphere.png

Hypersphere

iosg-dark.png

iosg.png

IOSG

maven-11-dark.png

maven-11.png

Maven 11

multiversx-light.png

multiversx-dark.png

MultiversX

tezos-foundation-dark.png

tezos-foundation.png

Tezos Foundation (Investor)

wave-financial-dark.png

wave-financial.png

Wave Financial

alchemix.png

Alchemix

algorand-dark.png

algorand.png

Algorand

ashswap.png

AshSwap

band protocol white.png

band logo.png

Band Protocol

casper.png

Casper protocol

eigenlayer-dark.png

eigenlayer-light.png

EigenLayer

ethereum-logo-landscape-purple.png

Ethereum

folks-finance-dark.png

folks-finance.png

Folks Finance

hatom-dark.svg

hatom.svg

Hatom

HydraDX-Pink.png

HydraDX

Logo_lido.png

Lido

maker.png

Maker

membrane-dark.png

membrane.png

Membrane Finance

MORPHO.svg

Morpho-logo-black-horizontal.png

Morpho

nasa.png

NASA

olympus-dark.png

olympus.png

Olympus DAO

polkadot-dark.png

polkadot.png

Polkadot

stake.fish-dark.png

stake.fish.png

Stakefish

StakerDao-logo.png

StakerDAO

stakewise-dark.svg

stakewise.png

StakeWise

sundaeswap-dark.png

sundaeswap.png

SundaeSwap

swell-network.png

Swell Network

tezos.png

Tezos

Umee_Logo_dark_mode.png

Umee_Logo.png

Umee

Take Your Security to the Next Level

Start Verifying For Free

Formal Verification

K as a Service

Security Audits

Learn About Our Impact on Web3 Security

Categories

Partners & Customers

Investors

Testimonials

Contact Us