I don't think Rice's theorem being proven invalid (or rather, more likely (but imo unlikely), P=NP) is important to this. In fact, a somewhat loose interpretation of Rice's theorem would imply that you can not "prove your way" out of having bugs of arbitrary classes, which seems entirely compatible with "our testing framework will find bugs".

Rice's theorem is applicable; the paradox is the usual trivial case,

    if symflowerSaysItsBroken() {
        DoTheRightThing()
    } else {
        DoTheBrokeThing()
    }

I have no doubt that symbolic analysis can find a large class of problems, but if you write stuff like "we promise to find errors" you will a) dupe a lot of junior devs who will genuinely believe your tool is doing impossible magic, b) alienate experienced devs who know that's 100% marketing fluff and find nothing more specific on your site.

I'm pretty much the ideal customer for a product like this - staff+ with final say about toolchain decisions on a product with a lot of data-driven behavior. But what I want to see isn't a vague "promise" (really? is it in a contract, that you're liable for bugs your tool misses? of course not) but some actual comparison to quickcheck/fuzzing. I want to see your approach finds a superset or at least mostly-disjoint set of what we already have invested in, or finds the same set more effectively. Like, survey through the bugs fuzzing found in go stdlib and show me your tool finds them all faster.

I'm also skeptical of some "purely" coverage-driven approach from the start - coverage-driven fuzzing already has a tendency to miss interesting cases that don't come from branchiness - a classic example is subnormal value handling. Fuzzing usually still finds these eventually just by virtue of exhaustiveness; a tool driven only by symbolic methods better come armed with a _lot_ of encoded knowledge about the language semantics.

From looking at their stuff I think their value comes not from the the way they promise to write tests that exercises more code paths than human generated testing can. This is different from the Go fuzz testing approach, which requires you to write a specialized kind of test by hand. I can even imagine a future evolution of Symflower's product that writes fuzz tests for you.