posts/quint_connect

[giscus[bot]]

posts/quint_connect

Quint - Executable specs for reliable systems

https://quint-lang.org/posts/quint_connect

[seanchen1991]

This is really cool to see 🙂

I'm curious about the trace validation approach that was mentioned. From the Craig Howard talk, you quote:

But the next step was super cool because we said, “Hey, Q, we got this model over here. You can see the source code that was running in production on that day. Where did we screw up?”

And Q helped us find some inconsistencies.

Is this similar to the trace validation approach? Specifically the part where he mentions that AI analyzed the source code that was running in production on the day of the outage.

[bugarela]

Not really. What Craig did, according to (my interpretation of) his talk, was to compare code and spec by having AI read the code, than read the spec, and look for divergence in the definitions. What trace validation does is execute the code, log what has happened somehow, and then use that logged information to check if the execution from the application was valid according to the specification.

AI is not involved in the process of model-based testing or in the process of trace validation, it is all deterministic. AI is only involved in speeding up the effort of building code (including application-specific code) that is required to run those executions from one artifact into the other, and code that compares the results.

In simpler terms: what they did was ask AI "is my code correct according to the spec" and what we propose here is asking AI "write tests to show that my code corresponds to the spec using the Model-Based Testing technique". Trace validation would be more like the latter, just a different technique.

I also have a comparison between MBT and trace validation here: https://quint-lang.org/docs/model-based-testing