This is NOT Intended to be a product/service recommendation question - I am trying really hard to word this so it isn't one.

Does anyone here perform static analysis on your code using abstract interpretation or formal methods? If so, did you have to license a tool to do it? Is this something that can be contracted out?

Here is my dillemma: My company makes embedded systems products. We are looking into some code analysis tools that use formal methods / abstract interpretation to evaluate all execution paths of code and guarantee that they will be free from run time exceptions. This does not replace function testing like unit testing or system integration testing, but it would give us extra coverage on scenarios that are hard to test in system and it would reduce the amount of time an effort that we need to put into code reviews.

We've looked at several tools and they are all great! They are also pretty expensive (~30kUSD is the price floor). I could run some numbers and prove that we will get ROI in a few years vs. doing nothing, but I am wondering if there are any other options. We also do not necessarily need to run the tool daily or nightly - our release frequency isn't that fast. Sure that would be nice, but we would also benefit greatly just being able to run the tool periodically before major milestones and releases - so a couple of times a month.

So naturally I started looking into contractors who may have the tool and could run this service for us. But I can't seem to find any. It appears the vendors who make these tools might all have clauses in their EULAs that prohibit them from using the tool on code they do not own or are not shipping in their product.

There are some open source options out there that I am aware of - but taking the time to configure that tool without support also has some implicit cost to it.

If there are contractors that are able to do this sort of thing, then perhaps I am just not searching for them the right way. Is there some other term I should be searching for?