I'm confused about what this is. Is basically doing formal verification on the things spec'd out?