Ok, thanks! Sounds more like the assurance level of running model checkers on protocol code with user-supplied specs. It can catch lots of problems but no guara

Ok, thanks! Sounds more like the assurance level of running model checkers on protocol code with user-supplied specs. It can catch lots of problems but no guarantees on all inputs/paths.