Oh, you usually specify in multiple levels of detail in TLA+ and relate them and only informally relate them to code, but if you want a formal relation to code

Oh, you usually specify in multiple levels of detail in TLA+ and relate them and only informally relate them to code, but if you want a formal relation to code you could compile your program to TLA+ (e.g. http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). ... But you probably don't really want to do that. Code-level verification using any "deep specification" tool (TLA+, Coq, Isabelle, Lean, F* etc.) is extremely limited in scale compared to specifying in TLA+ at a higher level. Because there is no known way to directly verify programs larger than several thousand lines affordably, and because that's precisely the kinds of programs that most engineers need to verify most of the time, it's far more common to use TLA+ at a higher-than-code level.