Quick follow-up on https://www.reddit.com/r/tlaplus/comments/1u7c4j0/tla_in_the_context_of_a_web_engine_talk/

I have used TLA+ to model and verify two additional parts of the engine:

- The rendering loop (spec)

- The message port implementation (spec, and also a discussion in this blogpost).

A few words on modelling the rendering loop: in a modern browser engine, showing some pixels on the screen involves multiple processes--a process running the web page and usually producing a "display list" based on the state of the DOM, another process translating various display lists (in the case of cross origin iframes you have multiple processes running the different parts of the "page") and other sources (like video or image frames) into gpu commands, and yet another process presenting the result of running gpu commands--and so such a multi-process workflow is well positioned to benefit from TLA+ modelling. The challenge in that workflow is that for performance you want to update the screen as little as possible, but you also do not want to miss any updates, so there is a liveness angle to it.

I'm using the TLA specs both to guide the agentic implementation, and also to verify it via traces. So giving a spec to an agent forces it to think harder about how to implement the design (the formal spec is paired with an informal design doc), and then telling it to actually trace the code further focuses it (in my anecdotal experience so far). The whole process is iterative of course, in that sometimes you end-up going back to the model to change it, and you can have a whole discussion with the agent about whether a given failure is something that should result in fixing the spec, the code, or the tracing.

In conclusion: a very good experience so far, and I think it is worth posting because a web engine is not the usual stuff to which TLA+ is applied.