The weakness of formal verification systems is that they turn the problem of writing correct programs into the problem of writing correct specifications, which is just as difficult, while adding extra layers of complexity. How do your tools address this difficulty?