Real world applications of TLA+: <a href="https://foundation.tlapl.us/industry/index.html" rel="nofollow">https://foundation.tlapl.us/industry/index.html.
The Intel paper shows how TLA+ was applied as a step prior to writing the hardware description. I'm not sure if it caught on, it seems like other tools are used nowdays, does anyone here in the VLSI industry know?
The last I learned of this was at the talk Temporal specification languages in industrial hardware verification by Simon Jantsch of Siemens at the ETAPS 2025 industry day track. Unfortunately I can't find the video posted anywhere, but predominantly the talk spoke of using proprietary symbolic model checkers for Linear Temporal Logic (LTL). It is reasonable to call TLA+ a successor to LTL, although LTL is definitely still used.
peterus · · focus · HN ↗
The Intel paper shows how TLA+ was applied as a step prior to writing the hardware description. I'm not sure if it caught on, it seems like other tools are used nowdays, does anyone here in the VLSI industry know?
ahelwer · · focus · HN ↗