HACKER Q&A
📣 tomas789

How to start with formal verification to find bugs


We have a large codebase of a mostly functional code. Most of the code looks roughly like this

  def CalculateX(entity1: Type1, entity2: Type2):
    when:
    | entity1 is big -> 5
    | entity1 is not big -> 6
    | entity2 is round and entity1 purple -> 5
The conditions in the pattern matching block can get quite complex. The function might be defined for all instances if Type1 and Type2 but that is not required. Reasoning about a single function is reasonably easy. But we often find a bug where a function should be defined for all combinations of its input parameters but it is calling a function which is not defined for a requested case.

We do all kinds of things to ensure it is reasonably correct but it seems like it is never enough. We are toying around with an idea of formal verification of our code. I don't know from which angle to attack this issue first. I was playing with Z3 and Coq but they are like a distinct system. What is a typical workflow of how to verify a program? Do we have to rewrite it first in a formal verification system or is it possible to use some sort of source-to-source translation? Is there a way to make sure this translation is correct? How do I find a system that will be up for the task? How do I know it is computationally tractable?

  👤 red0point Accepted Answer ✓
I think you’re looking at a program verification problem.

With this tool: http://viper.ethz.ch/ You essentially sprinkle your functions with pre- and post conditions (& loops), press „verify“ and it will verify the correctness of your program code.

There are multiple frontends you can use for different languages. Behind the scenes your code + annotations are converted from e.g. Python/Rust/Go to an intermediate language (Viper), which is then verified.

👤 throwaway81523
> What is a typical workflow of how to verify a program?

If you mean an existing program, it is usually not done that way. Instead, you develop the program and the proofs at the same time, so they go hand and hand with each other.

If you just mean checking exhaustiveness of a case statement, compilers can often do that for you.

👤 manx
Which programming language are you using? It looks to me like you need exhaustiveness checking for pattern matching. Languages like Scala, OCaml, Purescript or Haskell support this out of the box.

Am I overlooking something?