Simple, to find bugs. Whether you're doing quick iterative development, or preparing for launch, fuzzing is the ideal method to check if you don't have any bugs!
Our vulnerability scanning platform MythX also uses fuzzing. What sets Diligence Fuzzing apart from MythX is that it uses the underlying technology in a much more customized and powerful way.
Harvey, our fuzzing engine, can automatically execute millions of inputs on a smart contract. The MythX platform monitors these executions to look for known vulnerabilities. It will combine these findings with those from static analysis and symbolic execution to get you a precise analysis report!
Diligence fuzzing is different! Instead of looking for known vulnerabilities, we use Scribble properties to tell the fuzzer what smart contracts are supposed to do. While fuzzing, we’ll monitor each execution to check that the smart contract is indeed behaving correctly.
We’ve also implemented tons of features like incremental fuzzing that make property checking with Diligence Fuzzing a breeze!
Formal verification techniques are great! They allow you to prove that your smart contracts are mathematically correct. However, to get these guarantees, you’ll first need to invest a significant amount of time in manually providing the mathematical building blocks required to prove the contract.
If you’ve got months to spend and don’t plan on making changes to your codebase, then formal verification is the tool for you!
Fuzzing, on the other hand, takes a much more practical approach as it requires just a single annotation to be useful! While it can’t categorically prove the absence of bugs like formal verifiers, it gets close to it by cleverly executing millions of test cases.
Keep in mind that both formal verification and fuzzing suffer from the problem that a tool's results are only as good as the properties you write. Writing properties is often a difficult and time consuming task, and you can easily miss a critical specification, thereby allowing a bug to go unnoticed.
"formally verified" does not mean secure.
With Scribble we've made the property writing process as simple and foolproof as possible. It's accessible to developers and requires much less maintenance. Furthermore, you can use fuzzing to check your properties out-of-the-box, without the need for complex mathematical proofs.