Three Challenges






How to design the verification tool?
How to express correctness constraints?
How to express operator intent?