What does long-term success look like for a verification tool like SAW? For us, it involves improving the quality, correctness, and security of as much code as possible. We know that the best way to get there is not Galois hoarding all of the proofs and proof skills and keeping you all out. We love the proofs, but now we need to set them free. 

With that in mind, we set some of our best teachers to create a new introduction to SAW. It was written by Dylan Mcnamee, David Christiansen, and Chris Phifer and should take you from a machine with no SAW at all to writing your first few proofs. It’s built around a number of guided examples, guided by exercises. We’ve already used it to bring some new users up to speed, improving it each time. We’d love any feedback you have on the training, either by email or posted as issues or pull requests in its repository.

Should I use SAW?

Like any method for increasing the probability of your code being correct, using SAW is a matter of weighing the cost of applying the method with the benefits it will provide. 

The benefits of SAW include:

• Dramatic reduction or elimination of bug classes in C code.
• Ongoing correctness guarantees when included in a CI system.
• Unambiguous specifications for functions that can be used for code review and developer communication.
• New reasoning abilities for developers.

The first two points can be objectively measured to some extent. They imply that SAW will become more valuable as the cost of any given bug increases. The second two points suggest that a team’s performance will be altered if it uses a tool like SAW in such a way that it can be hard to measure.

The cost of applying SAW is a function of:

• Code complexity
• How often code is changed
• Engineer Capability
• The tool itself

Again, the first two are somewhat measurable. A program that has already been written might be easy or hard to verify, as will each update to that program. Engineer capability is a more complicated point. While it can take a while for an engineer to become an expert with SAW, SAW can also make engineers expert in C. This is because SAW is not just a program proof tool. It is a program understanding tool. We have seen our proof engineers comprehend extremely challenging code-bases in a matter of months when they approach it through the lens of SAW.

The final point is on us. We are working on many fronts to build SAW into a tool that is easy to use. One effort we have going on included the documentation that inspired that post. We’ve also been investing in user experience with a new API-based Python interface, making SAW more programmable and usable than ever before.

Watch our blog for updates on these efforts!