Would you pay to have code verified?

Question

We want to explore the possibility of verifying a few modules (at first &mdash; entire codebases later) at a reasonable fee. Context: We're working on a tool for verifying C code and want some concrete problems to throw at it. Our tooling is C-based, but we're open to code in other C-style languages.Does anyone have any functions/libraries they would actually pay to have formally verified?

zer8k · Accepted Answer

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.

schoen · Answer

Are you thinking of offering to write the formal specifications too, or try to formally verify compliance to a customer's specification?Does your tool attempt to mechanically create its own proof that the specification is satisfied by the code, or does that involve human effort? (Or both?)

ilaksh · Answer

What exactly are you verifying?Would you verify something about Rust code? And what would you verify?

eimrine · Answer

Who will verify your verification as valuable?

throwawayadvsec · Answer

so what's the difference with QA+pentesting+tdd?what do you verify?

Would you pay to have code verified?

Are you thinking of offering to write the formal specifications too, or try to formally verify compliance to a customer's specification?
Does your tool attempt to mechanically create its own proof that the specification is satisfied by the code, or does that involve human effort? (Or both?)

What exactly are you verifying?
Would you verify something about Rust code? And what would you verify?

Who will verify your verification as valuable?

so what's the difference with QA+pentesting+tdd?
what do you verify?