I don't personally have a use for this or the ability to pay for it, but I think this is a very valuable service, at least if you can demonstrate that you can d

I don't personally have a use for this or the ability to pay for it, but I think this is a very valuable service, at least if you can demonstrate that you can do it repeatably for different kinds of code bases and different kinds of specified behaviors. Obviously, given Rice's Theorem, you can't do it "repeatably" for any arbitrary problem that a customer gives you, or else you would have to be omniscient with respect to all of mathematics... but "can probably verify behaviors that are similar to those that have been able to be verified before, in code bases that are similar to those where behaviors have been formally proven in the past" is still good!