Sort of a meta question: this is a well trodden path. Code verification is very popular with government types. Have you considered trying to figure out what the

Sort of a meta question: this is a well trodden path. Code verification is very popular with government types. Have you considered trying to figure out what they're using and what they're paying? I see this as the same problem starting a CA is. To get trust you need to build trust. It's a catch 22. Formal verification is not necessary for 99% of code. Of that small 1% of code bases you're talking about aerospace, government contract work, and medical technology. I wouldn't even know how to guess at a price because if you can beat them at their own game you can probably attach as many zeroes as you want to it. What do you do if your verification fails though? Any company worth their salt will sue you into the ground. Especially if it results in a shuttle turning into a lawn dart. One last thing: are you verifying code or compiler? Especially with compiled languages verifications would have to be pegged to a compiler version, distributor, and standard. There's a reason aerospace is about 20 years behind modern compilers and it's not bureaucracy.