I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary conditions in inherited code bases and write meaningful tests for them.

You mention in the description about testing code for all possible inputs. Are you all actually doing this behind the scenes with an SMT solver? Are you using some other proof assistant (COQ, HOL, etc) to be able to use proof-by-induction techniques and thus manage the path explosion problem?

I tried out an example comparing two multiplication algorithms (see below) and the tool said it couldn't find any issues in about a minute. Curious whether it will scale to larger problem sizes.

// implementation 1 int mult(int x, int y) { return x*y; } // implementation 2 int slow_mult(int x, int y) { int result=0; if(x<0) { for(int i=x; i<0; i++) { result-=y; } } else { for(int i=0; i<x; i++) { result+=y; } } return result; }