With agent asssistance, we don't need writing annoying formal spec and proof anymore. Then formal verification can be a practical and useful tool in daily programming, especially for "deep module" whose spec is much simpler than implementation.