> because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool.

Then use a proof methodology that doesn't require exhaustive enumeration. This objection is actually fairly alarming to me; perhaps there is a larger disconnect between industrial formal techniques for hardware and software than I thought. Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings.

  Then use a proof methodology that doesn't require exhaustive enumeration.

You may as well have said "then you use a magical tool that doesn't exist".

  Strings also occupy a "large state space", but this 
  obviously doesn't prevent us from doing formal 
  verification on functions over strings.

What is your reason to think this is 'obviously' the case?

> You may as well have said "then you use a magical tool that doesn't exist".

Ok, so what this tells me is that you're not aware of what modern verification techniques look like.

There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used.

https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory

https://en.m.wikipedia.org/wiki/Homotopy_type_theory

https://leanprover.github.io/about/

http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

> What is your reason to think this is 'obviously' the case?

Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned.

Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.

  Ok, so what this tells me is that you're not aware of what 
  modern verification techniques look like.

Well, techniques are not tools. I am asserting that it is quite probable that no practically useful tool exists to non-exhaustively verify the state space laydn wants to cover.

Notwithstanding your example that it's possible to non-exhaustively verify some functions on strings. There is a quite some distance between that to verifying just any function.

  Because I've done this,

Sure, but how does that make it obvious to laydn that his state space is coverable? And what makes it so obvious to you that his state space is coverable? After all, the 'largeness' can have different sources, including those that make non-exhaustive methods infeasible.

I think this may be an example of the disconnect between research and the industry. Researchers say things are solved when they have shown something is possible and published about it. They feel it's then up to the industry to extrapolate, while research moves on to exciting new and greener pastures. Meanwhile the industry thinks the results are too meager, thinks the extrapolation involves a lot of technical difficulties and generally is not willing to spend enough money on what they cannot see as anything but a longshot.

If you do any model checking at all, with tools like SPIN or TLA+, you are already in the state-of-the-art minority in industry.

I've had great success (in software) with randomized/probability based testing. You don't walk the full state space but generate subsets randomly to walk.

If done naively, it doesn't work because you are unlikely to hit the problematic bug. So you have to be clever: do not generate inputs uniformly! Generate those inputs which are really really nasty all the time. If you find a problem, then gradually simplify the case until you have reduced the complexity to something which can be understood.

With some experience for where former bugs tend to live, I've been able to remove lots of bugs from my software in edge cases via this method. (See "QuickCheck").