A good moment to remind everyone:
Verification: Code does what it says.
Validation: Code does what Specifications say.
Specifications: Were hopefully correctly modeled to the Problem.
In IEEE terms:
> Verification: "Are we building the product right?" > Validation: "Are we building the right product?")
You can write mathematically flawless code that highly efficiently solves the wrong problem.
---
While I think formal verification is the future (essential for cybersecurity), it's not a silver bullet for the other 2 items, which are way more ambiguous. I think however they can all iterate on each other and improve the project overall, but it still depends on competent steering
If you have had experiences with good approaches for verification Validation & Specification framework, do let us know about them.
> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.
Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."
It's still great if the assertions in your code are provably correct.
Isn't it more like:
where with formal verification, the specifications are lower-level, so validation is extra-important.