diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md
new file mode 100644
index 0000000000..0de1643756
--- /dev/null
+++ b/docs/src/adr/005adr-json.md
@@ -0,0 +1,202 @@
+# ADR-005: JSON Serialization Format
+
+| author       | revision |
+| ------------ | --------:|
+| Jure Kukovec |        1 |
+
+This ADR documents our decision on serializing the Apalache internal representation (IR) as JSON.
+The purpose of introducing such a serialization is to expose the internal representation in a standardized format, which can be used for persistent storage, or for analysis by third-party tools in the future.
+
+## 1. Serializable classes
+
+The following classes are serializable:
+1. TLA+ expressions `TlaEx` and subclasses thereof:
+  1. Named expressions `NameEx`
+  1. Literal values `ValEx` for the following literals:
+    1. Integers `TlaInt`
+    1. Strings `TlaStr`
+    1. Booleans `TlaBool`
+    1. Decimals `TlaDecimal`
+  1. Operator expressions `OperEx`
+  1. LET-IN expressions `LetInEx`
+1. TLA+ declarations `TlaDecl` and subclasses thereof:
+  1. Variable declarations `TlaVarDecl`
+  1. Constant declarations `TlaConstDecl`
+  1. Operator declarations `TlaOperDecl`
+  1. Assumption declarations `TlaAssumeDecl`
+  1. Theorem declarations `TlaTheoremDecl`
+1. TLA+ modules `TlaModule`
+
+## 2. Disambiguation field
+
+Every serialization will contain a disambiguation field, named `kind`. This field holds the name of the class being serialized. For example, the serialization of a `NameEx` will have the shape
+```
+{
+  "kind": "NameEx"
+  ...
+}
+```
+
+## 3. Serializing tagged entities
+
+Serializations of entities annotated with a `TypeTag` will have an additional field named `type`, containing the type of the expression (see [ADR-002][], [ADR-004][] for a description of our type system and the syntax for types-as-string-annotations respectively), if the tag is `Typed`, or `Untyped` otherwise. For example, the integer literal `1` is represented by a `ValEx`, which has type `Int` and is serialized as follows:
+```
+{
+  "kind": "ValEx",
+  "type": "Int"
+  ...
+}
+```
+in the typed encoding, or 
+```
+{
+  "kind": "ValEx",
+  "type": "Untyped"
+  ...
+}
+```
+in the untyped encoding.
+
+## 4. Source information
+Entities in the internal representation are usually annotated with source information, of the form `{filename}:{startLine}:{startColumn}-{endLine}:{endColumn}`, relating them to a file range in the provided specification (from which they may have been transformed as part of preprocessing).
+JSON encodings may, but are not required to, contain a `source` providing this information, of the following shape:
+```
+{
+  "source": {
+    "filename" : <FILENAME>,
+    "from" : {
+      "line" : <STARTLINE>,
+      "column" : <STARTCOLUMN>
+    },
+    "to" : {
+      "line" : <ENDLINE>,
+      "column" : <ENDCOLUMN>
+    }
+  }
+}
+```
+or
+```
+{
+  "source": "UNKNOWN"
+}
+```
+if no source information is available (e.g. for expressions generated purely by Apalache).
+Serializations generated by Apalache are always guaranteed to contain a `source` field entry.
+
+Example:
+```
+{
+  "kind" : "NameEx",
+  "type" : "Int",
+  "name" : "myName",
+  "source": {
+    "filename" : "MyModule.tla",
+    "from" : {
+      "line" : 3,
+      "column" : 5
+    },
+    "to" : {
+      "line" : 3,
+      "column" : 10
+    }
+  }
+}
+```
+
+## 5. Root wrapper
+JSON serializations of one or more `TlaModule`s are wrapped in a root object with two required fields:
+ -`version`, the value of which is a string representation of the current JSON encoding version, shaped `{major}.{minor}`, and
+ -`modules`, the value of which is an array containing the JSON encodings of zero or more `TlaModule`s
+It may optionally contain a field `"name" : "ApalacheIR"`.
+This document defines JSON Version 1.0. If and when a different JSON version is defined, this document will be updated accordingly.
+Apalache may refuse to import, or trigger warnings for, JSON objects with obsolete versions of the encoding in the future.
+Example:
+```
+{
+  "name": "ApalacheIR",
+  "version": "1.0"
+  "modules" = [
+    {
+      "kind": "TlaModule",
+      "name": "MyModule",
+      ...
+    },
+    ...]
+}
+```
+
+## 6. General serialization rules
+
+The goal of the serialization is for the JSON structure to mimic the internal representation as closely as possible, for ease of deserialization. 
+Concretely, whenever a class declares a field `fld: T`, its serialization also contains a field named `fld`, containing the serialization of the field value.
+For example, if `TlaConstDecl` declares a `name: String` field, its JSON serialization will have a `name` field as well, containing the name string.
+
+If a class field has the type `Traversable[T]`, for some `T`, the corresponding JSON entry is a list containing serializations of the individual arguments. For example, `OperEx` is variadic and declares `args: TlaEx*`, so its serialization has an `args` field containing a (possibly empty) list.
+
+As a running example, take the expression `1 + 1`, represented with the correct type annotations as 
+```
+OperEx( 
+  oper = TlaArithOper.plus, 
+  args = Seq( 
+    ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) ), 
+    ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) )
+    ) 
+  )( typeTag = Typed( IntT1() ) )
+```
+
+Since both sub-expressions, the literals `1`, are identical, their serializations are equal as well:
+```
+{
+  "kind": "ValEx",
+  "type": "Int",
+  "value": {
+    "kind": "TlaInt",
+    "value": 1
+  }
+}
+```
+
+Observe that we choose to serialize `TlaValue` as a JSON object, which is more verbose, but trivial to deserialize. It has the following shape
+```
+{
+  "kind": <KIND> ,
+  "value": <VALUE>
+}
+```
+
+The `value` field depends on the kind of `TlaValue`:
+1. For `TlaStr`: a JSON string
+1. For `TlaBool`: a JSON Boolean
+1. For `TlaInt(bigIntValue)`: 
+  1. If `bigIntValue.isValidInt`: a JSON number
+  2. Otherwise: `{ "bigInt": bigIntValue.toString() }`
+1. For `TlaDecimal(decValue)`: a JSON string `decValue.toString`
+
+The reason for the non-uniform treatment of integers, is that Apalache encodes its TLA+ integers as `BigInt`, which means that it permits values, for which `.isValidInt` does not hold. 
+
+While it might seem more natural to encode the entire `TlaValue` as a JSON primitive, without the added object layer, we would have a much tougher time deserializing.
+We would need a) a sensible encoding of `BigInt` values, which are not valid integers, and b) a way to distinguish both variants of `BigInt`, as well as decimals, when deserializing (since JSON is not typed).
+We could encode all values as strings, but they would be similarly indistinguishable when deserializing. Importantly, the `type` field of the `ValEx` expression is not guaranteed to contain a hint, as it could be `Untyped`
+
+Take `jsonOf1` to be the serialization of `ValEx( TlaInt( 1 ) )( typeTag = Typed( IntT1() ) )` shown above. The serialization of `1 + 1` is then equal to
+```
+{
+  "kind": "OperEx",
+  "type": "Int",
+  "oper": "PLUS",
+  "args": [jsonOf1, jsonOf1]
+}
+```
+In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` field in the serialization equals `oper.name`.
+
+## 7. Implementation
+
+The implementation of the serialization can be found in the class
+`at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][].
+
+[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+
+[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
+
+[TlaToJson]: https://github.com/informalsystems/apalache/blob/unstable/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala
new file mode 100644
index 0000000000..ea89e7e92a
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDecoder.scala
@@ -0,0 +1,15 @@
+package at.forsyte.apalache.io.json
+
+import at.forsyte.apalache.tla.lir.{TlaDecl, TlaEx, TlaModule}
+
+/**
+ * A JsonDecoder defines a conversion from a json (as represented by T) to a TLA+ expression/declaration/module
+ *
+ * @tparam T Any class extending JsonRepresentation
+ */
+trait JsonDecoder[T <: JsonRepresentation] {
+  def asTlaModule(moduleJson: T): TlaModule
+  def asTlaDecl(declJson: T): TlaDecl
+  def asTlaEx(exJson: T): TlaEx
+  def fromRoot(rootJson: T): Traversable[TlaModule]
+}
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala
new file mode 100644
index 0000000000..16bdbd5b9a
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonDeserializationError.scala
@@ -0,0 +1,4 @@
+package at.forsyte.apalache.io.json
+
+/** Thrown, when importing from JSON fails, due to malformed input */
+class JsonDeserializationError(msg: String) extends Exception(msg)
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala
index f6a8ffdab6..3a38a9a1e8 100644
--- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonEncoder.scala
@@ -10,4 +10,5 @@ trait JsonEncoder[T <: JsonRepresentation] {
   def apply(ex: TlaEx): T
   def apply(decl: TlaDecl): T
   def apply(module: TlaModule): T
+  def makeRoot(modules: Traversable[TlaModule]): T
 }
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala
index 0e3811f6ea..b7f5bd48d3 100644
--- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonRepresentation.scala
@@ -6,4 +6,5 @@ package at.forsyte.apalache.io.json
  */
 trait JsonRepresentation {
   def toString: String
+  def getFieldOpt(fieldName: String): Option[this.type]
 }
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala
new file mode 100644
index 0000000000..08ceccab04
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonToTla.scala
@@ -0,0 +1,208 @@
+package at.forsyte.apalache.io.json
+
+import at.forsyte.apalache.tla.imp.src.{SourceLocation, SourceStore}
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.src.{SourceLocation, SourcePosition, SourceRegion}
+import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaDecimal, TlaInt, TlaStr}
+import convenience.tla
+import UntypedPredefs._
+import at.forsyte.apalache.tla.lir.io.TypeTagReader
+
+/**
+ * A semi-abstraction of a json decoder.
+ * It is independent of the concrete JsonRepresentation, resp. ScalaFactory implementation.
+ * Inverse to TlaToJson, i.e. as{X}( TlaToJson( a : X) ) == a, where X = TlaEx/TlaDecl/TlaModule
+ */
+
+class JsonToTla[T <: JsonRepresentation](
+    scalaFactory: ScalaFactory[T], sourceStoreOpt: Option[SourceStore] = None
+)(implicit typeTagReader: TypeTagReader)
+    extends JsonDecoder[T] {
+
+  private def missingField(fieldName: String): JsonDeserializationError =
+    new JsonDeserializationError(s"JSON has no field named [$fieldName].")
+
+  private def getOrThrow(json: T, fieldName: String): T =
+    json.getFieldOpt(fieldName).getOrElse { throw missingField(fieldName) }
+
+  private def asFParam(json: T): OperParam = {
+    val kindField = getOrThrow(json, TlaToJson.kindFieldName)
+    val kind = scalaFactory.asStr(kindField)
+
+    kind match {
+      case "OperParam" =>
+        val nameField = getOrThrow(json, "name")
+        val name = scalaFactory.asStr(nameField)
+        val arityField = getOrThrow(json, "arity")
+        val arity = scalaFactory.asInt(arityField)
+        OperParam(name, arity)
+      case _ => throw new JsonDeserializationError(s"$kind is not a valid OperParam kind")
+    }
+  }
+
+  private def asTlaVal(json: T): TlaValue = {
+    val kindField = getOrThrow(json, TlaToJson.kindFieldName)
+    val kind = scalaFactory.asStr(kindField)
+
+    kind match {
+      case "TlaStr" =>
+        val valField = getOrThrow(json, "value")
+        val valStr = scalaFactory.asStr(valField)
+        TlaStr(valStr)
+      case "TlaDecimal" =>
+        val valField = getOrThrow(json, "value")
+        val valStr = scalaFactory.asStr(valField)
+        val dec = BigDecimal(valStr)
+        TlaDecimal(dec)
+      case "TlaInt" =>
+        val valField = getOrThrow(json, "value")
+        val bi = valField.getFieldOpt("bigInt") map { biField =>
+          BigInt(scalaFactory.asStr(biField))
+        } getOrElse {
+          BigInt(scalaFactory.asInt(valField))
+        }
+        TlaInt(bi)
+      case "TlaBool" =>
+        val valField = getOrThrow(json, "value")
+        val valBool = scalaFactory.asBool(valField)
+        TlaBool(valBool)
+      case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaValue kind")
+    }
+  }
+
+  def getSourceLocationOpt(json: T): Option[SourceLocation] = for {
+    sourceObj <- json.getFieldOpt(TlaToJson.sourceFieldName)
+    fileName <- sourceObj.getFieldOpt("filename") map scalaFactory.asStr
+    fromObj <- sourceObj.getFieldOpt("from")
+    toObj <- sourceObj.getFieldOpt("to")
+    fromLine <- fromObj.getFieldOpt("line") map scalaFactory.asInt
+    fromCol <- fromObj.getFieldOpt("column") map scalaFactory.asInt
+    toLine <- toObj.getFieldOpt("line") map scalaFactory.asInt
+    toCol <- toObj.getFieldOpt("column") map scalaFactory.asInt
+  } yield SourceLocation(
+      fileName,
+      SourceRegion(
+          SourcePosition(fromLine, fromCol),
+          SourcePosition(toLine, toCol)
+      )
+  )
+
+  def setLoc(identifiable: Identifiable, locationOpt: Option[SourceLocation]): Unit =
+    sourceStoreOpt foreach { store =>
+      locationOpt foreach { loc =>
+        store.add(identifiable.ID, loc)
+      }
+    }
+
+  override def asTlaModule(moduleJson: T): TlaModule = {
+    val kindField = getOrThrow(moduleJson, TlaToJson.kindFieldName)
+    val kind = scalaFactory.asStr(kindField)
+    if (kind != "TlaModule")
+      throw new JsonDeserializationError(s"JSON kind is $kind, expected TlaModule")
+
+    val nameField = getOrThrow(moduleJson, "name")
+    val name = scalaFactory.asStr(nameField)
+    val declField = getOrThrow(moduleJson, "declarations")
+    val declObjSeq = scalaFactory.asSeq(declField)
+    val decls = declObjSeq map asTlaDecl
+
+    new TlaModule(name, decls)
+  }
+
+  override def asTlaDecl(declJson: T): TlaDecl = {
+    val typeField = getOrThrow(declJson, TlaToJson.typeFieldName)
+    val tag = scalaFactory.asStr(typeField)
+    val typeTag = typeTagReader(tag)
+    val kindField = getOrThrow(declJson, TlaToJson.kindFieldName)
+    val kind = scalaFactory.asStr(kindField)
+    val decl = kind match {
+      case "TlaTheoremDecl" =>
+        val nameField = getOrThrow(declJson, "name")
+        val name = scalaFactory.asStr(nameField)
+        val bodyField = getOrThrow(declJson, "body")
+        val body = asTlaEx(bodyField)
+        TlaTheoremDecl(name, body)(typeTag)
+      case "TlaVarDecl" =>
+        val nameField = getOrThrow(declJson, "name")
+        val name = scalaFactory.asStr(nameField)
+        TlaVarDecl(name)(typeTag)
+      case "TlaConstDecl" =>
+        val nameField = getOrThrow(declJson, "name")
+        val name = scalaFactory.asStr(nameField)
+        TlaConstDecl(name)(typeTag)
+      case "TlaOperDecl" =>
+        val nameField = getOrThrow(declJson, "name")
+        val name = scalaFactory.asStr(nameField)
+        val recField = getOrThrow(declJson, "isRecursive")
+        val isRecursive = scalaFactory.asBool(recField)
+        val bodyField = getOrThrow(declJson, "body")
+        val body = asTlaEx(bodyField)
+        val paramsField = getOrThrow(declJson, "formalParams")
+        val paramsObjList = scalaFactory.asSeq(paramsField).toList
+        val fParams = paramsObjList map asFParam
+        val opDecl = TlaOperDecl(name, fParams, body)(typeTag)
+        opDecl.isRecursive = isRecursive
+        opDecl
+
+      case "TlaAssumeDecl" =>
+        val bodyField = getOrThrow(declJson, "body")
+        val body = asTlaEx(bodyField)
+        TlaAssumeDecl(body)(typeTag)
+      case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaDecl kind")
+    }
+    setLoc(decl, getSourceLocationOpt(declJson))
+    decl
+  }
+
+  override def asTlaEx(exJson: T): TlaEx = {
+    val kindField = getOrThrow(exJson, TlaToJson.kindFieldName)
+    val kind = scalaFactory.asStr(kindField)
+    if (kind == "NullEx") NullEx // TODO: We really shouldn't support NullEx long-term
+    val typeField = getOrThrow(exJson, TlaToJson.typeFieldName)
+    val tag = scalaFactory.asStr(typeField)
+    val typeTag = typeTagReader(tag)
+    val ex = kind match {
+      case "NameEx" =>
+        val nameField = getOrThrow(exJson, "name")
+        val name = scalaFactory.asStr(nameField)
+        NameEx(name)(typeTag)
+      case "ValEx" =>
+        val valueField = getOrThrow(exJson, "value")
+        val value = asTlaVal(valueField)
+        ValEx(value)(typeTag)
+      case "OperEx" =>
+        val operField = getOrThrow(exJson, "oper")
+        val operString = scalaFactory.asStr(operField)
+        val argsField = getOrThrow(exJson, "args")
+        val argsObjSeq = scalaFactory.asSeq(argsField)
+        // TODO: Implement a oper.name -> oper mapping and avoid Builder hackery
+        val args = argsObjSeq map asTlaEx map { BuilderTlaExWrapper }
+        tla.byName(operString, args: _*).withTag(typeTag)
+      case "LetInEx" =>
+        val bodyField = getOrThrow(exJson, "body")
+        val body = asTlaEx(bodyField)
+        val declsField = getOrThrow(exJson, "decls")
+        val declsObjSeq = scalaFactory.asSeq(declsField)
+        val decls = declsObjSeq map asTlaDecl
+        assert(decls forall { _.isInstanceOf[TlaOperDecl] })
+        val operDecls = decls map { _.asInstanceOf[TlaOperDecl] }
+        LetInEx(body, operDecls: _*)(typeTag)
+      case _ => throw new JsonDeserializationError(s"$kind is not a valid TlaEx kind")
+    }
+    setLoc(ex, getSourceLocationOpt(exJson))
+    ex
+  }
+
+  override def fromRoot(rootJson: T): Traversable[TlaModule] = {
+    val versionField = getOrThrow(rootJson, TlaToJson.versionFieldName)
+    val version = scalaFactory.asStr(versionField)
+    val current = JsonVersion.current
+    if (version != current)
+      throw new JsonDeserializationError(s"JSON version is $version, expected $current.")
+
+    val modulesField = getOrThrow(rootJson, "modules")
+    val modulesObjSeq = scalaFactory.asSeq(modulesField)
+
+    modulesObjSeq map asTlaModule
+  }
+}
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala
new file mode 100644
index 0000000000..e9c4cfbf65
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/JsonVersion.scala
@@ -0,0 +1,12 @@
+package at.forsyte.apalache.io.json
+
+/**
+ * JSON serialization versions need not be tied to Apalache versions
+ * (Apalache versions, obtained from at.forsyte.apalache.tla.tooling.Version
+ * cannot be read here anyway, due to tooling -> import dependencies)
+ */
+object JsonVersion {
+  val major = 1
+  val minor = 0
+  def current: String = s"$major.$minor"
+}
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala
new file mode 100644
index 0000000000..3157cda824
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/ScalaFactory.scala
@@ -0,0 +1,13 @@
+package at.forsyte.apalache.io.json
+
+/**
+ * Generates Scala primitives/collections from JSON primitives/arrays.
+ * Inverse to JsonFactory, i.e. as{X}( JsonFactory.from{x}(v: X) ) == v, for X = Int/Str/Bool/Traversable
+ * @tparam T Any class extending JsonRepresentation
+ */
+trait ScalaFactory[T <: JsonRepresentation] {
+  def asInt(json: T): Int
+  def asStr(json: T): String
+  def asBool(json: T): Boolean
+  def asSeq(json: T): Seq[T]
+}
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
index f851120228..b79f28aa14 100644
--- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
@@ -3,6 +3,7 @@ package at.forsyte.apalache.io.json
 import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaDecimal, TlaInt, TlaStr}
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.io.TypeTagPrinter
+import at.forsyte.apalache.tla.lir.storage.SourceLocator
 
 /**
  * A semi-abstraction of a json encoder.
@@ -49,14 +50,12 @@ import at.forsyte.apalache.tla.lir.io.TypeTagPrinter
  *    }
  *  ]
  * }
- *
- * @param factory A json factory for the `T` variant of JsonRepresentation
- * @tparam T Any class extending JsonRepresentation
  */
-class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTagPrinter: TypeTagPrinter)
+class TlaToJson[T <: JsonRepresentation](
+    factory: JsonFactory[T], locatorOpt: Option[SourceLocator] = None
+)(implicit typeTagPrinter: TypeTagPrinter)
     extends JsonEncoder[T] {
-  val kindFieldName: String = "kind"
-  val typeFieldName: String = "type"
+  import TlaToJson._
 
   implicit def liftString: String => T = factory.fromStr
 
@@ -64,129 +63,175 @@ class TlaToJson[T <: JsonRepresentation](factory: JsonFactory[T])(implicit typTa
 
   implicit def liftBool: Boolean => T = factory.fromBool
 
-  override def apply(ex: TlaEx): T = ex match {
-    case NameEx(name) =>
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(ex.typeTag),
-          kindFieldName -> "NameEx",
-          "name" -> name
-      )
-
-    case ValEx(value) =>
-      val inner = value match {
-        case TlaStr(strValue) =>
-          factory.mkObj(
-              kindFieldName -> "TlaStr",
-              "value" -> strValue
-          )
-        case TlaDecimal(decValue) =>
-          factory.mkObj(
-              kindFieldName -> "TlaDecimal",
-              "value" -> decValue.toString() // let the parser care when reading
-          )
-        case TlaInt(bigIntValue) =>
-          val intVal: T =
-            if (bigIntValue.isValidInt) liftInt(bigIntValue.toInt)
-            else factory.mkObj("bigInt" -> bigIntValue.toString())
-          factory.mkObj(
-              kindFieldName -> "TlaInt",
-              "value" -> intVal
-          )
-        case TlaBool(boolValue) =>
-          factory.mkObj(
-              kindFieldName -> "TlaBool",
-              "value" -> boolValue
-          )
-        case _ =>
-          //unsupported (TlaReal, TlaPredefSet)
-          factory.mkObj()
+  /**
+   * If a SourceLocator is given, prepare a `sourceFieldName` field, holding a JSON
+   * with file & position info, in addition to the given fields.
+   */
+  private def withOptionalLoc(identifiable: Identifiable)(fields: (String, T)*): T = {
+    val locFieldOpt: Option[T] = locatorOpt map { locator =>
+      locator.sourceOf(identifiable.ID) map { sourceLoc =>
+        factory.mkObj(
+            "filename" -> sourceLoc.filename,
+            "from" -> factory.mkObj(
+                "line" -> sourceLoc.region.start.line,
+                "column" -> sourceLoc.region.start.column
+            ),
+            "to" -> factory.mkObj(
+                "line" -> sourceLoc.region.end.line,
+                "column" -> sourceLoc.region.end.column
+            )
+        )
+      } getOrElse {
+        "UNKNOWN" // Locator is given, but doesn't know the source
       }
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(ex.typeTag),
-          kindFieldName -> "ValEx",
-          "value" -> inner
-      )
-
-    case OperEx(oper, args @ _*) =>
-      val argJsons = args map apply
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(ex.typeTag),
-          kindFieldName -> "OperEx",
-          "oper" -> oper.name,
-          "args" -> factory.fromTraversable(argJsons)
-      )
-    case LetInEx(body, decls @ _*) =>
-      val bodyJson = apply(body)
-      val declJsons = decls map apply
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(ex.typeTag),
-          kindFieldName -> "LetInEx",
-          "body" -> bodyJson,
-          "decls" -> factory.fromTraversable(declJsons)
-      )
-
-    case NullEx =>
-      factory.mkObj(kindFieldName -> "NullEx")
+    }
+    factory.mkObj((locFieldOpt map { sourceFieldName -> _ }) ++: fields: _*)
   }
 
-  override def apply(decl: TlaDecl): T = decl match {
-    case TlaTheoremDecl(name, body) =>
-      val bodyJson = apply(body)
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(decl.typeTag),
-          kindFieldName -> "TlaTheoremDecl",
-          "name" -> name,
-          "body" -> bodyJson
-      )
-
-    case TlaVarDecl(name) =>
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(decl.typeTag),
-          kindFieldName -> "TlaVarDecl",
-          "name" -> name
-      )
-
-    case TlaConstDecl(name) =>
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(decl.typeTag),
-          kindFieldName -> "TlaConstDecl",
-          "name" -> name
-      )
-
-    case decl @ TlaOperDecl(name, formalParams, body) =>
-      val bodyJson = apply(body)
-      val paramsJsons = formalParams map { case OperParam(paramName, arity) =>
-        factory.mkObj(
-            kindFieldName -> "OperParam",
-            "name" -> paramName,
-            "arity" -> arity
+  override def apply(ex: TlaEx): T = {
+    def withLoc(fields: (String, T)*): T = withOptionalLoc(ex)(fields: _*)
+    ex match {
+      case NameEx(name) =>
+        withLoc(
+            typeFieldName -> typeTagPrinter(ex.typeTag),
+            kindFieldName -> "NameEx",
+            "name" -> name
         )
-      }
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(decl.typeTag),
-          kindFieldName -> "TlaOperDecl",
-          "name" -> name,
-          "formalParams" -> factory.fromTraversable(paramsJsons),
-          "isRecursive" -> decl.isRecursive,
-          "body" -> bodyJson
-      )
-
-    case TlaAssumeDecl(body) =>
-      val bodyJson = apply(body)
-      factory.mkObj(
-          typeFieldName -> typTagPrinter(decl.typeTag),
-          kindFieldName -> "TlaAssumeDecl",
-          "body" -> bodyJson
-      )
+
+      case ValEx(value) =>
+        val inner = value match {
+          case TlaStr(strValue) =>
+            factory.mkObj(
+                kindFieldName -> "TlaStr",
+                "value" -> strValue
+            )
+          case TlaDecimal(decValue) =>
+            factory.mkObj(
+                kindFieldName -> "TlaDecimal",
+                "value" -> decValue.toString() // let the parser care when reading
+            )
+          case TlaInt(bigIntValue) =>
+            val intVal: T =
+              if (bigIntValue.isValidInt) liftInt(bigIntValue.toInt)
+              else factory.mkObj("bigInt" -> bigIntValue.toString())
+            factory.mkObj(
+                kindFieldName -> "TlaInt",
+                "value" -> intVal
+            )
+          case TlaBool(boolValue) =>
+            factory.mkObj(
+                kindFieldName -> "TlaBool",
+                "value" -> boolValue
+            )
+          case _ =>
+            //unsupported (TlaReal, TlaPredefSet)
+            factory.mkObj()
+        }
+        withLoc(
+            typeFieldName -> typeTagPrinter(ex.typeTag),
+            kindFieldName -> "ValEx",
+            "value" -> inner
+        )
+
+      case OperEx(oper, args @ _*) =>
+        val argJsons = args map apply
+        withLoc(
+            typeFieldName -> typeTagPrinter(ex.typeTag),
+            kindFieldName -> "OperEx",
+            "oper" -> oper.name,
+            "args" -> factory.fromTraversable(argJsons)
+        )
+      case LetInEx(body, decls @ _*) =>
+        val bodyJson = apply(body)
+        val declJsons = decls map apply
+        withLoc(
+            typeFieldName -> typeTagPrinter(ex.typeTag),
+            kindFieldName -> "LetInEx",
+            "body" -> bodyJson,
+            "decls" -> factory.fromTraversable(declJsons)
+        )
+
+      case NullEx =>
+        factory.mkObj(kindFieldName -> "NullEx")
+    }
   }
 
-  override def apply(module: TlaModule): T = {
-    val declJsons = module.declarations map { d =>
-      apply(d)
+  override def apply(decl: TlaDecl): T = {
+    def withLoc(fields: (String, T)*): T = withOptionalLoc(decl)(fields: _*)
+    decl match {
+      case TlaTheoremDecl(name, body) =>
+        val bodyJson = apply(body)
+        withLoc(
+            typeFieldName -> typeTagPrinter(decl.typeTag),
+            kindFieldName -> "TlaTheoremDecl",
+            "name" -> name,
+            "body" -> bodyJson
+        )
+
+      case TlaVarDecl(name) =>
+        withLoc(
+            typeFieldName -> typeTagPrinter(decl.typeTag),
+            kindFieldName -> "TlaVarDecl",
+            "name" -> name
+        )
+
+      case TlaConstDecl(name) =>
+        withLoc(
+            typeFieldName -> typeTagPrinter(decl.typeTag),
+            kindFieldName -> "TlaConstDecl",
+            "name" -> name
+        )
+
+      case decl @ TlaOperDecl(name, formalParams, body) =>
+        val bodyJson = apply(body)
+        val paramsJsons = formalParams map { case OperParam(paramName, arity) =>
+          factory.mkObj(
+              kindFieldName -> "OperParam",
+              "name" -> paramName,
+              "arity" -> arity
+          )
+        }
+        withLoc(
+            typeFieldName -> typeTagPrinter(decl.typeTag),
+            kindFieldName -> "TlaOperDecl",
+            "name" -> name,
+            "formalParams" -> factory.fromTraversable(paramsJsons),
+            "isRecursive" -> decl.isRecursive,
+            "body" -> bodyJson
+        )
+
+      case TlaAssumeDecl(body) =>
+        val bodyJson = apply(body)
+        withLoc(
+            typeFieldName -> typeTagPrinter(decl.typeTag),
+            kindFieldName -> "TlaAssumeDecl",
+            "body" -> bodyJson
+        )
     }
+  }
+
+  override def apply(module: TlaModule): T = {
+    val declJsons = module.declarations map apply
     factory.mkObj(
         kindFieldName -> "TlaModule",
+        "name" -> module.name,
         "declarations" -> factory.fromTraversable(declJsons)
     )
   }
+
+  override def makeRoot(modules: Traversable[TlaModule]): T = {
+    val moduleJsons = modules map apply
+    factory.mkObj(
+        "name" -> "ApalacheIR",
+        versionFieldName -> JsonVersion.current,
+        "modules" -> factory.fromTraversable(moduleJsons)
+    )
+  }
+}
+
+object TlaToJson {
+  val kindFieldName: String = "kind"
+  val typeFieldName: String = "type"
+  val sourceFieldName: String = "source"
+  val versionFieldName: String = "version"
 }
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala
index 7a297c6755..d4db947c08 100644
--- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/TlaToUJson.scala
@@ -2,8 +2,11 @@ package at.forsyte.apalache.io.json.impl
 
 import at.forsyte.apalache.io.json.TlaToJson
 import at.forsyte.apalache.tla.lir.io.TypeTagPrinter
+import at.forsyte.apalache.tla.lir.storage.SourceLocator
 
 /**
  * A json encoder, using the UJson representation
  */
-class TlaToUJson(implicit typTagPrinter: TypeTagPrinter) extends TlaToJson[UJsonRep](UJsonFactory)(typTagPrinter)
+class TlaToUJson(locatorOpt: Option[SourceLocator] = None)(
+    implicit typeTagPrinter: TypeTagPrinter
+) extends TlaToJson[UJsonRep](UJsonFactory, locatorOpt)(typeTagPrinter)
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala
index 649b89853e..909504a143 100644
--- a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonRep.scala
@@ -7,4 +7,14 @@ import at.forsyte.apalache.io.json.JsonRepresentation
  */
 sealed case class UJsonRep(protected[json] val value: ujson.Value) extends JsonRepresentation {
   override def toString: String = ujson.write(value, indent = 2, escapeUnicode = false)
+
+  /**
+   * If `this` represents a JSON object defining a field
+   * `fieldName : val`, the method returns a Some(_), containing the representation of `val`,
+   *  otherwise (if `this` is not an object or if it does not define a `fieldName` field) returns None.
+   */
+  override def getFieldOpt(fieldName: String): Option[this.type] = for {
+    objAsMap <- value.objOpt
+    fieldVal <- objAsMap.get(fieldName)
+  } yield UJsonRep(fieldVal).asInstanceOf[UJsonRep.this.type]
 }
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala
new file mode 100644
index 0000000000..f97a0fbb9b
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonScalaFactory.scala
@@ -0,0 +1,26 @@
+package at.forsyte.apalache.io.json.impl
+
+import at.forsyte.apalache.io.json.{JsonDeserializationError, ScalaFactory}
+
+/**
+ * ScalaFactory for the UJsonRep variant of JsonRepresentation
+ */
+object UJsonScalaFactory extends ScalaFactory[UJsonRep] {
+  override def asInt(json: UJsonRep): Int =
+    json.value.numOpt map { _.toInt } getOrElse {
+      throw new JsonDeserializationError("Not an integer.")
+    }
+
+  override def asStr(json: UJsonRep): String = json.value.strOpt getOrElse {
+    throw new JsonDeserializationError("Not a string.")
+  }
+
+  override def asBool(json: UJsonRep): Boolean = json.value.boolOpt getOrElse {
+    throw new JsonDeserializationError("Not a Boolean.")
+  }
+
+  override def asSeq(json: UJsonRep): Seq[UJsonRep] =
+    json.value.arrOpt map { _ map UJsonRep } getOrElse {
+      throw new JsonDeserializationError("Not an array.")
+    }
+}
diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala
new file mode 100644
index 0000000000..835e2ac358
--- /dev/null
+++ b/tla-import/src/main/scala/at/forsyte/apalache/io/json/impl/UJsonToTla.scala
@@ -0,0 +1,11 @@
+package at.forsyte.apalache.io.json.impl
+
+import at.forsyte.apalache.io.json.JsonToTla
+import at.forsyte.apalache.tla.imp.src.SourceStore
+import at.forsyte.apalache.tla.lir.io.TypeTagReader
+
+/**
+ * A json decoder, using the UJson representation
+ */
+class UJsonToTla(sourceStoreOpt: Option[SourceStore] = None)(implicit typeTagReader: TypeTagReader)
+    extends JsonToTla[UJsonRep](UJsonScalaFactory, sourceStoreOpt)(typeTagReader)
diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala
index 7fa8354332..7347c02b0d 100644
--- a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala
+++ b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestTlaToUJson.scala
@@ -18,7 +18,7 @@ class TestTlaToUJson extends FunSuite with BeforeAndAfterEach with TestingPredef
   }
   val enc = new TlaToUJson
 
-  val kindField = enc.kindFieldName
+  val kindField = TlaToJson.kindFieldName
 
   def getEncVal(ex: TlaEx): ujson.Value = enc(ex).value
   def getEncVal(decl: TlaDecl): ujson.Value = enc(decl).value
diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala
new file mode 100644
index 0000000000..df0efc4f91
--- /dev/null
+++ b/tla-import/src/test/scala/at/forsyte/apalache/io/json/TestUJsonToTla.scala
@@ -0,0 +1,66 @@
+package at.forsyte.apalache.io.json
+
+import at.forsyte.apalache.io.json.impl.{TlaToUJson, UJsonToTla}
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.convenience.tla
+import org.junit.runner.RunWith
+import org.scalatest.{BeforeAndAfterEach, FunSuite}
+import org.scalatest.junit.JUnitRunner
+import at.forsyte.apalache.tla.lir.UntypedPredefs._
+import at.forsyte.apalache.tla.lir.io.{TypeTagPrinter, UntypedReader}
+
+@RunWith(classOf[JUnitRunner])
+class TestUJsonToTla extends FunSuite with BeforeAndAfterEach with TestingPredefs {
+  implicit val reader = UntypedReader
+  implicit val printer = new TypeTagPrinter {
+    override def apply(tag: TypeTag): String = ""
+  }
+
+  val dec = new UJsonToTla(sourceStoreOpt = None)
+  val enc = new TlaToUJson(locatorOpt = None)
+
+  test("dec(enc(x)) =?= x") {
+    val exs: Seq[TlaEx] = Seq(
+        tla.and(tla.name("x"), tla.bool(true)),
+        tla.ite(tla.name("p"), tla.name("A"), tla.name("B")),
+        tla.letIn(
+            tla.appOp(tla.name("A"), tla.int(1)),
+            tla
+              .declOp(
+                  "A",
+                  tla.plus(tla.name("p"), tla.int(1)),
+                  OperParam("p")
+              )
+              .withTag(Untyped())
+              .asInstanceOf[TlaOperDecl]
+        )
+    )
+
+    exs foreach { ex =>
+      assert(dec.asTlaEx(enc(ex)) == ex)
+    }
+
+    val decls: Seq[TlaDecl] = Seq(
+        tla.declOp("X", tla.eql(tla.name("a"), tla.int(1)), OperParam("a")),
+        TlaAssumeDecl(tla.eql(tla.int(1), tla.int(0))),
+        TlaConstDecl("c"),
+        TlaVarDecl("v")
+    )
+
+    decls foreach { decl =>
+      assert(dec.asTlaDecl(enc(decl)) == decl)
+    }
+
+    val modules: Seq[TlaModule] = Seq(
+        new TlaModule("Empty", Seq.empty),
+        new TlaModule("Module", decls)
+    )
+
+    modules foreach { m =>
+      assert(dec.asTlaModule(enc(m)) == m)
+    }
+
+    assert(dec.fromRoot(enc.makeRoot(modules)) == modules)
+  }
+
+}
diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
index 036f69f1f4..f36fe16377 100644
--- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
+++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
@@ -81,7 +81,8 @@ class EtcTypeCheckerPassImpl @Inject() (val options: PassOptions, val sourceStor
     val outFile = new File(outdir.toFile, s"out-$prefix-$name.json")
     val writer = new PrintWriter(new FileWriter(outFile, false))
     try {
-      val jsonText = new TlaToUJson().apply(module).toString
+      val sourceLocator: SourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener)
+      val jsonText = new TlaToUJson(Some(sourceLocator)).makeRoot(Seq(module)).toString
       writer.write(jsonText)
       logger.debug(" > JSON output: " + outFile)
     } finally {
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala
new file mode 100644
index 0000000000..8e6d8eff3e
--- /dev/null
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/io/TypeTagReader.scala
@@ -0,0 +1,15 @@
+package at.forsyte.apalache.tla.lir.io
+
+import at.forsyte.apalache.tla.lir.{TypeTag, Untyped}
+
+/**
+ * Recovers TypeTags from their string representations.
+ * Inverse of TypeTagPrinter.
+ */
+trait TypeTagReader {
+  def apply(tagStr: String): TypeTag
+}
+
+object UntypedReader extends TypeTagReader {
+  override def apply(tagStr: String): TypeTag = Untyped()
+}