One Spin Launchpad, the App store for Formal Verification

Formal verification is qualitatively different from most other verification. A simulation can pass or fail. But while formal verification can prove that the circuit is correct, or incorrect, it can also return “not proven” which means either that the algorithms realized that they were not powerful enough to prove a property or that the run time got excessive and it gave up.

The idea of the app as a small code object that runs in a rich environment was pioneered originally by Java apps running browsers, but it was apps on the iPhone (then copied by Android) that really raised their visibility.

This article outlines the basic idea of Launchpad that all the expertise and ideas for formal approaches are not inside any one company such as OneSpin. Formal apps can go further if the developments are opened up to expert developers.

Read more.