A team of researchers from the University of Michigan, Microsoft Research, and Carnegie Mellon have created Armada, a system that uses a technique called formal verification to prove whether a piece of software will output what it is designed to produce without bugs.
Armada targets software that uses concurrent execution, a method of performance boosting, and passes systems through a series of transformations until they break down into simpler representations. The developer only has to prove that each simplified step accurately represents the more complex program from the previous step by using Armada’s high-level syntax to describe the simpler program and indicate a proof method that’s needed to support the transformation.
The automatically-generated proof runs through a prover for verification. If it fails, the user changes their description or proof method to make a new one.