# VS Code TLA+
## Metadata
**Status**:: #x
**Zettel**:: #zettel/fleeting
**Created**:: [[2026-01-15]]
**Parent**:: [[TLA+]], [[♯ Visual Studio Code]]
**URL**:: [github.com](https://github.com/tlaplus/vscode-tlaplus).
## Usage
### TLC
Use the command `TLA+: Check model with TLC`. The default workers number is too small. Try a larger one such as 10 when the checking process is too slow.
The VS Code extension requires a [[TLC Model Checker Config]].
- `SPECIFICATION`: name of the main temporal predicate.
- `PROPERTIES`: arbitrary temporal properties
- `INVARIANT`: shortcut to write `Spec => []Inv`
A general pattern to check models via the `.cfg` files is writing a wrapper module such as:
```tla
---- MODULE MCWriteThroughCache ----
EXTENDS WriteThroughCache
------
MCSend(p, d, miOld, miNew) == miNew = <<p, d>>
MCReply(p, d, miOld, miNew) == miNew = <<p, d>>
MCInitMemInt == {<<CHOOSE p \in Proc: TRUE, NoVal>>}
MCQLen == 1
======
```
And then verify this wrapper module using a `.cfg` file to do the constant assignments:
```
SPECIFICATION Spec
CONSTANTS
Send <- MCSend
Reply <- MCReply
InitMemInt <- MCInitMemInt
QLen <- MCQLen
Proc = {p1, p2}
Addr = {a1, a2, a3}
Val = {v1, v2}
NoVal = NoVal
```
TLA file does not support model value literals. The work around is declaring them as constants then assigning in the config file.
```
// tla
CONSTANTS d1, d2
// cfg
CONSTANTS
d1 = d1
d2 = d2
```
### PlusCal
Use snippet `pluscal` to insert the block. Run `TLA+: parse module` to run the transpiler.