Because you can use it to find temporal errors in your software. People in fact do. So, that proves it's worth even if one can't be sure of perfect conformance

Because you can use it to find temporal errors in your software. People in fact do. So, that proves it's worth even if one can't be sure of perfect conformance to the spec. Far as connecting specs to code, these papers did try to combine Event-B with SPARK Ada: https://scispace.com/pdf/towards-generating-spark-from-event-b-models-kyb7ctyxdk.pdf https://scispace.com/pdf/towards-generating-spark-from-event... https://rd.springer.com/chapter/10.1007/978-3-031-23119-3_13 https://rd.springer.com/chapter/10.1007/978-3-031-23119-3_13