To the best of my memory commercial formal tools have been around for a decade or so. Yet the Formal Verification market is still in a state of confusion, with no single tool achieving significant market superiority. There are many startups, but none has really achieve the hoped for financial success. I believe that the principal reason for this state of affair is due to the erroneous positioning of the tools.

Functional tools are not really verification tools, or at least they should not be. Formal tools are design tools, not verification tools. Their mission should be to prevent errors, not to find them. We have the unfortunate human treat of being better at fixing error than at avoiding them. Yet error avoidance is more efficient, less costly, and almost always generates better implementations.

If a design engineer would start an implementation by writing the assertions required by the specification written in a natural language, he, or she, would be generating the equivalent of an executable specification. Such description is easier to use in discussing with the marketing department because the relationship between the collection of assertions and the written specification is more direct than when the project in an implementation language is discussed with the marketing professionals.

Then the implementation would proceed by developing the code required while obeying the rules described in the assertions. This would lead to both more straightforward design and the identification of missing requirements, in the form of absent or incorrect assertions. All this is the responsibility of the development engineer, and has nothing to do with what we traditionally call "verification".

Under this scenario, verification engineers would be responsible for inspecting the assertion, comparing them to the specification, and finding errors and omissions. Then they will generate the stimuli and expected responses, and also generate tests for corner cases and "improbable" inputs and execution states.

So, formal tools should be classified under "Formal Design" not "Formal Verification". In this manner they will be sold to the engineers responsible for using them. It is very inefficient to have verification engineers insert assertions in code written by design engineers, because they often are not familiar with the intent of the developer. By calling the tool in a manner that properly describes its use intent, we would go along way to simplify the sale process, and would, at the same time, improve its use methodology.