diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index 63adb94fc..fc2f05713 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -40,7 +40,7 @@ the end of file.
     quint parse ./testFixture/modulesAndJunk.qnt 2>&1 | sed 's#.*quint/\(testFixture\)#Q/\1#g'
 
 <!-- !test out junk -->
-    Q/testFixture/modulesAndJunk.qnt:9:1 - error: extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
+    Q/testFixture/modulesAndJunk.qnt:9:1 - error: [QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
     9: the parser
        ^^^
 
@@ -289,7 +289,7 @@ exit $exit_code
   1 failed
 
   1) failingTest:
-      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      HOME/failingTestCounters.qnt:45:10 - error: [QNT508] Assertion failed
       45:          assert(n == 0),
     Use --seed=0x1 --match=failingTest to repeat.
 
@@ -349,7 +349,7 @@ exit $exit_code
   1 failed
 
   1) failingTest:
-      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      HOME/failingTestCounters.qnt:45:10 - error: [QNT508] Assertion failed
       45:          assert(n == 0),
 
 [Frame 0]
@@ -790,7 +790,7 @@ exit $exit_code
   1 failed
 
   1) mintTwiceThenSendError:
-      HOME/coin.qnt:176:5 - error: mintTwiceThenSendError returns false
+      HOME/coin.qnt:176:5 - error: [QNT511] Test mintTwiceThenSendError returned false
       176:     run mintTwiceThenSendError = {
 
 [Frame 0]
@@ -913,11 +913,11 @@ exit $exit_code
 ```
 
   _1040compileError
-      HOME/_1040compileError.qnt:2:3 - error: QNT500: Uninitialized const n. Use: import <moduleName>(n=<value>).*
+      HOME/_1040compileError.qnt:2:3 - error: [QNT500] Uninitialized const n. Use: import <moduleName>(n=<value>).*
 2:   const n: int
      ^^^^^^^^^^^^
 
-      HOME/_1040compileError.qnt:5:12 - error: Name n not found
+      HOME/_1040compileError.qnt:5:12 - error: [QNT502] Name n not found
 5:     assert(n > 0)
               ^
 
@@ -931,18 +931,18 @@ error: Tests failed
 output=$(quint run testFixture/_1041compileConst.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' \
-  -e 's#^.*_1041compileConst.qnt#      HOME/_1041compileConst.qnt#g'
+  -e 's#^.*_1041compileConst.qnt#HOME/_1041compileConst.qnt#g'
 exit $exit_code
 ```
 
 <!-- !test exit 1 -->
 <!-- !test out run uninitialized -->
 ```
-<module_input>:2:3 - error: QNT500: Uninitialized const N. Use: import <moduleName>(N=<value>).*
+HOME/_1041compileConst.qnt:2:3 - error: [QNT500] Uninitialized const N. Use: import <moduleName>(N=<value>).*
 2:   const N: int
      ^^^^^^^^^^^^
 
-<module_input>:5:24 - error: Name N not found
+HOME/_1041compileConst.qnt:5:24 - error: [QNT502] Name N not found
 5:   action init = { x' = N }
                           ^
 
diff --git a/quint/src/ErrorMessage.ts b/quint/src/ErrorMessage.ts
new file mode 100644
index 000000000..ce488f62c
--- /dev/null
+++ b/quint/src/ErrorMessage.ts
@@ -0,0 +1,62 @@
+/* ----------------------------------------------------------------------------------
+ * Copyright (c) Informal Systems 2023. All rights reserved.
+ * Licensed under the Apache 2.0.
+ * See License.txt in the project root for license information.
+ * --------------------------------------------------------------------------------- */
+
+/**
+ * Error messages with source locations.
+ *
+ * @author Gabriela Moreira
+ *
+ * @module
+ */
+
+import { compact } from 'lodash'
+import { QuintError, quintErrorToString } from './quintError'
+
+/**
+ * An error message whose locations have been resolved.
+ */
+export interface ErrorMessage {
+  explanation: string
+  locs: Loc[]
+}
+
+export interface Loc {
+  source: string
+  start: { line: number; col: number; index: number }
+  end?: { line: number; col: number; index: number }
+}
+
+/**
+ * Map an identifier to the corresponding location in the source map, if possible.
+ * @param sourceMap the source map
+ * @param id the identifier to map
+ * @returns the location, if found in the map, or the unknown location
+ */
+export function sourceIdToLoc(sourceMap: Map<bigint, Loc>, id: bigint): Loc {
+  let sourceLoc = sourceMap.get(id)
+  if (!sourceLoc) {
+    console.error(`No source location found for ${id}. Please report a bug.`)
+    return unknownLoc
+  } else {
+    return sourceLoc
+  }
+}
+
+export function fromQuintError(sourceMap: Map<bigint, Loc>): (_: QuintError) => ErrorMessage {
+  return error => {
+    const loc = error.reference ? sourceMap.get(error.reference) : undefined
+    return {
+      explanation: quintErrorToString(error),
+      locs: compact([loc]),
+    }
+  }
+}
+
+// the default error location that usually indicates a bug in our code
+const unknownLoc: Loc = {
+  source: '<unknown>',
+  start: { line: 0, col: 0, index: 0 },
+}
diff --git a/quint/src/builtin.ts b/quint/src/builtin.ts
index 957167e80..75621c5fe 100644
--- a/quint/src/builtin.ts
+++ b/quint/src/builtin.ts
@@ -15,8 +15,7 @@
 import { DocumentationEntry, produceDocs } from './docs'
 import { resolve } from 'path'
 import { readFileSync } from 'fs'
-import { ErrorMessage, parsePhase1fromText } from './parsing/quintParserFrontend'
-import { Either } from '@sweet-monads/either'
+import { ParseResult, parsePhase1fromText } from './parsing/quintParserFrontend'
 import { lf } from 'eol'
 
 import { IdGenerator } from './idGenerator'
@@ -26,7 +25,7 @@ import { IdGenerator } from './idGenerator'
  *
  * @returns a map of builtin definition names to their documentation
  */
-export function builtinDocs(gen: IdGenerator): Either<ErrorMessage[], Map<string, DocumentationEntry>> {
+export function builtinDocs(gen: IdGenerator): ParseResult<Map<string, DocumentationEntry>> {
   const path = resolve(__dirname, 'builtin.qnt')
   // Read file and remove windows line endings (\r) using `lf`
   const sourceCode = lf(readFileSync(path, 'utf8'))
diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index 90e6fd082..4db35941e 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -14,8 +14,7 @@ import { cwd } from 'process'
 import chalk from 'chalk'
 
 import {
-  ErrorMessage,
-  Loc,
+  SourceMap,
   compactSourceMap,
   parseDefOrThrow,
   parsePhase1fromText,
@@ -23,6 +22,7 @@ import {
   parsePhase3importAndNameResolution,
   parsePhase4toposort,
 } from './parsing/quintParserFrontend'
+import { ErrorMessage } from './ErrorMessage'
 
 import { Either, left, right } from '@sweet-monads/either'
 import { EffectScheme } from './effects/base'
@@ -122,7 +122,7 @@ interface LoadedStage extends ProcedureStage {
 
 interface ParsedStage extends LoadedStage {
   modules: QuintModule[]
-  sourceMap: Map<bigint, Loc>
+  sourceMap: SourceMap
   table: LookupTable
   unusedDefinitions: UnusedDefinitions
   idGen: IdGenerator
@@ -163,9 +163,9 @@ interface ErrorData extends ProcedureStage {
   sourceCode: string
 }
 
-type ErrResult = { msg: String; stage: ErrorData }
+type ErrResult = { msg: string; stage: ErrorData }
 
-function cliErr<Stage>(msg: String, stage: ErrorData): Either<ErrResult, Stage> {
+function cliErr<Stage>(msg: string, stage: ErrorData): Either<ErrResult, Stage> {
   return left({ msg, stage })
 }
 
@@ -210,35 +210,30 @@ export async function parse(loaded: LoadedStage): Promise<CLIProcedure<ParsedSta
       const mainPath = resolver.lookupPath(dirname(path), basename(path))
       return parsePhase2sourceResolution(idGen, resolver, mainPath, phase1Data)
     })
-    .mapLeft(newErrs => {
-      const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-      return { msg: 'parsing failed', stage: { ...parsing, errors } }
-    })
     .chain(phase2Data => {
       if (args.sourceMap) {
         // Write source map to the specified file
         writeToJson(args.sourceMap, compactSourceMap(phase2Data.sourceMap))
       }
-      return parsePhase3importAndNameResolution(phase2Data).mapLeft(newErrs => {
-        const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-        return { msg: 'parsing failed', stage: { ...parsing, errors } }
-      })
+      return parsePhase3importAndNameResolution(phase2Data)
     })
     .chain(phase3Data => {
-      return parsePhase4toposort(phase3Data).mapLeft(newErrs => {
-        const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-        return { msg: 'parsing failed', stage: { ...parsing, errors } }
-      })
+      return parsePhase4toposort(phase3Data)
     })
     .map(phase4Data => ({ ...parsing, ...phase4Data, idGen }))
+    .mapLeft(({ errors, sourceMap }) => {
+      const newErrorMessages = errors.map(mkErrorMessage(sourceMap))
+      const errorMessages = parsing.errors ? parsing.errors.concat(newErrorMessages) : newErrorMessages
+      return { msg: 'parsing failed', stage: { ...parsing, errors: errorMessages } }
+    })
 }
 
-export function mkErrorMessage(sourceMap: Map<bigint, Loc>): (_: [bigint, QuintError]) => ErrorMessage {
-  return ([key, value]) => {
-    const loc = sourceMap.get(key)!
+export function mkErrorMessage(sourceMap: SourceMap): (_: QuintError) => ErrorMessage {
+  return error => {
+    const loc = error.reference ? sourceMap.get(error.reference) : undefined
     return {
-      explanation: quintErrorToString(value),
-      locs: [loc],
+      explanation: quintErrorToString(error),
+      locs: loc ? [loc] : [],
     }
   }
 }
@@ -256,8 +251,7 @@ export async function typecheck(parsed: ParsedStage): Promise<CLIProcedure<Typec
   if (errorMap.length === 0) {
     return right({ ...typechecking, ...result })
   } else {
-    const errorLocator = mkErrorMessage(sourceMap)
-    const errors = Array.from(errorMap, errorLocator)
+    const errors = errorMap.map(mkErrorMessage(sourceMap))
     return cliErr('typechecking failed', { ...typechecking, errors })
   }
 }
@@ -384,7 +378,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
   const testOut = compileAndTest(compilationState, mainName, flattenedTable, options)
 
   if (testOut.isLeft()) {
-    return cliErr('Tests failed', { ...testing, errors: testOut.value })
+    return cliErr('Tests failed', { ...testing, errors: testOut.value.map(mkErrorMessage(testing.sourceMap)) })
   } else if (testOut.isRight()) {
     const elapsedMs = Date.now() - startMs
     const results = testOut.unwrap()
@@ -398,7 +392,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
           const errNo = chalk.red(namedErrors.length + 1)
           out(`    ${errNo}) ${res.name} failed after ${res.nsamples} test(s)`)
 
-          res.errors.forEach(e => namedErrors.push([res.name, e, res]))
+          res.errors.forEach(e => namedErrors.push([res.name, mkErrorMessage(testing.sourceMap)(e), res]))
         }
       })
     }
@@ -516,7 +510,8 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   const result = compileAndRun(newIdGenerator(), prev.sourceCode, mainStart, mainEnd, mainName, mainPath, options)
 
   if (result.status === 'error') {
-    const errors = prev.errors ? prev.errors.concat(result.errors) : result.errors
+    const newErrors = result.errors.map(mkErrorMessage(prev.sourceMap))
+    const errors = prev.errors ? prev.errors.concat(newErrors) : newErrors
     return cliErr('run failed', { ...simulator, errors })
   } else {
     if (verbosity.hasResults(verbosityLevel)) {
@@ -544,7 +539,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
         const jsonObj = addItfHeader(prev.args.input, result.status, trace.value)
         writeToJson(prev.args.outItf, jsonObj)
       } else {
-        const newStage = { ...simulator, errors: result.errors }
+        const newStage = { ...simulator, errors: result.errors.map(mkErrorMessage(prev.sourceMap)) }
         return cliErr(`ITF conversion failed: ${trace.value}`, newStage)
       }
     }
@@ -561,7 +556,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
         ...simulator,
         status: result.status,
         trace: result.states,
-        errors: result.errors,
+        errors: result.errors.map(mkErrorMessage(prev.sourceMap)),
       })
     }
   }
@@ -604,7 +599,8 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
   // while solving #1052.
   const resolutionResult = parsePhase3importAndNameResolution(prev)
   if (resolutionResult.isLeft()) {
-    return cliErr('name resolution failed', { ...verifying, errors: resolutionResult.value })
+    const errors = resolutionResult.value.errors.map(mkErrorMessage(prev.sourceMap))
+    return cliErr('name resolution failed', { ...verifying, errors })
   }
 
   verifying.table = resolutionResult.unwrap().table
@@ -698,9 +694,10 @@ export async function docs(loaded: LoadedStage): Promise<CLIProcedure<Documentat
   const { sourceCode, path } = loaded
   const parsing = { ...loaded, stage: 'documentation' as stage }
   return parsePhase1fromText(newIdGenerator(), sourceCode, path)
-    .mapLeft(newErrs => {
-      const errors = parsing.errors ? parsing.errors.concat(newErrs) : newErrs
-      return { msg: 'parsing failed', stage: { ...parsing, errors } }
+    .mapLeft(({ errors, sourceMap }) => {
+      const newErrorMessages = errors.map(mkErrorMessage(sourceMap))
+      const errorMessages = parsing.errors ? parsing.errors.concat(newErrorMessages) : newErrorMessages
+      return { msg: 'parsing failed', stage: { ...parsing, errors: errorMessages } }
     })
     .map(phase1Data => {
       const allEntries: [string, Map<string, DocumentationEntry>][] = phase1Data.modules.map(module => {
diff --git a/quint/src/errorReporter.ts b/quint/src/errorReporter.ts
index cf3915dc5..30b754181 100644
--- a/quint/src/errorReporter.ts
+++ b/quint/src/errorReporter.ts
@@ -16,7 +16,7 @@
 
 import { Maybe, just } from '@sweet-monads/maybe'
 
-import { ErrorMessage } from './parsing/quintParserFrontend'
+import { ErrorMessage } from './ErrorMessage'
 
 /** Generate a string with formatted error reporting for a given error message
  *
diff --git a/quint/src/flattening/fullFlattener.ts b/quint/src/flattening/fullFlattener.ts
index 7f88c2d83..1b5ff53d1 100644
--- a/quint/src/flattening/fullFlattener.ts
+++ b/quint/src/flattening/fullFlattener.ts
@@ -17,12 +17,13 @@ import { IdGenerator } from '../idGenerator'
 import { moduleToString } from '../ir/IRprinting'
 import { FlatModule, QuintModule, isDef } from '../ir/quintIr'
 import { LookupTable } from '../names/base'
-import { Loc, ParserPhase3, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
+import { ParserPhase3, SourceMap, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { inlineTypeAliases } from '../types/aliasInliner'
 import { flattenModule } from './flattener'
 import { flattenInstances } from './instanceFlattener'
 import { unshadowNames } from '../names/unshadower'
+import { quintErrorToString } from '../quintError'
 
 /**
  * Flatten an array of modules, replacing instances, imports and exports with
@@ -40,7 +41,7 @@ export function flattenModules(
   modules: QuintModule[],
   table: LookupTable,
   idGenerator: IdGenerator,
-  sourceMap: Map<bigint, Loc>,
+  sourceMap: SourceMap,
   analysisOutput: AnalysisOutput
 ): { flattenedModules: FlatModule[]; flattenedTable: LookupTable; flattenedAnalysis: AnalysisOutput } {
   // FIXME: use copies of parameters so the original objects are not mutated.
@@ -111,11 +112,11 @@ export function flattenModules(
   }
 }
 
-function resolveNamesOrThrow(modules: QuintModule[], sourceMap: Map<bigint, Loc>): ParserPhase3 {
+function resolveNamesOrThrow(modules: QuintModule[], sourceMap: SourceMap): ParserPhase3 {
   const result = parsePhase3importAndNameResolution({ modules, sourceMap })
   if (result.isLeft()) {
     modules.forEach(m => console.log(moduleToString(m)))
-    throw new Error('Internal error while flattening ' + result.value.map(e => e.explanation))
+    throw new Error('Internal error while flattening ' + result.value.errors.map(quintErrorToString))
   }
 
   return result.unwrap()
diff --git a/quint/src/flattening/instanceFlattener.ts b/quint/src/flattening/instanceFlattener.ts
index 7df1c59c5..49fd8671a 100644
--- a/quint/src/flattening/instanceFlattener.ts
+++ b/quint/src/flattening/instanceFlattener.ts
@@ -18,7 +18,7 @@ import { IRTransformer, transformModule } from '../ir/IRTransformer'
 import { addNamespaceToDefinition } from '../ir/namespacer'
 import { QuintApp, QuintDeclaration, QuintModule, QuintName, isDef } from '../ir/quintIr'
 import { LookupTable, builtinNames } from '../names/base'
-import { Loc } from '../parsing/quintParserFrontend'
+import { SourceMap } from '../parsing/quintParserFrontend'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { dependentDefinitions, getNamespaceForDef } from './flattener'
 import { generateFreshIds } from '../ir/idRefresher'
@@ -42,7 +42,7 @@ export function flattenInstances(
   modulesByName: Map<string, QuintModule>,
   lookupTable: LookupTable,
   idGenerator: IdGenerator,
-  sourceMap: Map<bigint, Loc>,
+  sourceMap: SourceMap,
   analysisOutput: AnalysisOutput
 ): QuintModule[] {
   const flattener = new InstanceFlattener(modulesByName, lookupTable, idGenerator, sourceMap, analysisOutput)
@@ -61,14 +61,14 @@ class InstanceFlattener implements IRTransformer {
 
   /* Parameters for `generateFreshIds` */
   private idGenerator: IdGenerator
-  private sourceMap: Map<bigint, Loc>
+  private sourceMap: SourceMap
   private analysisOutput: AnalysisOutput
 
   constructor(
     modulesByName: Map<string, QuintModule>,
     lookupTable: LookupTable,
     idGenerator: IdGenerator,
-    sourceMap: Map<bigint, Loc>,
+    sourceMap: SourceMap,
     analysisOutput: AnalysisOutput
   ) {
     this.modulesByName = modulesByName
diff --git a/quint/src/generated/Quint.g4 b/quint/src/generated/Quint.g4
index 40dd4accf..6c7c445e4 100644
--- a/quint/src/generated/Quint.g4
+++ b/quint/src/generated/Quint.g4
@@ -145,7 +145,7 @@ expr:           // apply a built-in operator via the dot notation
         |       expr op=(GT | LT | GE | LE | NE | EQ) expr          # relations
         |       qualId '\'' ASGN expr                               # asgn
         |       expr '=' expr {
-                  const m = "QNT006: unexpected '=', did you mean '=='?"
+                  const m = "[QNT006] unexpected '=', did you mean '=='?"
                   this.notifyErrorListeners(m)
                 }                                                   # errorEq
                 // Boolean operators. Note that not(e) is just a normal call
diff --git a/quint/src/generated/QuintParser.ts b/quint/src/generated/QuintParser.ts
index dee78856d..aacec8b3e 100644
--- a/quint/src/generated/QuintParser.ts
+++ b/quint/src/generated/QuintParser.ts
@@ -2405,7 +2405,7 @@ export class QuintParser extends Parser {
 						this.state = 601;
 						this.expr(21);
 
-						                            const m = "QNT006: unexpected '=', did you mean '=='?"
+						                            const m = "[QNT006] unexpected '=', did you mean '=='?"
 						                            this.notifyErrorListeners(m)
 						                          
 						}
diff --git a/quint/src/index.ts b/quint/src/index.ts
index d80b9c9df..918b2ed6e 100644
--- a/quint/src/index.ts
+++ b/quint/src/index.ts
@@ -24,3 +24,4 @@ export { newIdGenerator, IdGenerator } from './idGenerator'
 export { fileSourceResolver, stringSourceResolver } from './parsing/sourceResolver'
 export { format } from './prettierimp'
 export { prettyQuintEx, prettyTypeScheme, prettyQuintDeclaration } from './graphics'
+export { Loc } from './ErrorMessage'
diff --git a/quint/src/ir/idRefresher.ts b/quint/src/ir/idRefresher.ts
index 246258b08..d0e1a637f 100644
--- a/quint/src/ir/idRefresher.ts
+++ b/quint/src/ir/idRefresher.ts
@@ -15,7 +15,7 @@
 
 import { IRTransformer, transformDefinition } from './IRTransformer'
 import { IdGenerator } from '../idGenerator'
-import { Loc } from '../parsing/quintParserFrontend'
+import { SourceMap } from '../parsing/quintParserFrontend'
 import { AnalysisOutput } from '../quintAnalyzer'
 import { QuintDef, QuintEx, QuintLambda } from './quintIr'
 import { QuintType } from './quintTypes'
@@ -37,7 +37,7 @@ import { QuintType } from './quintTypes'
 export function generateFreshIds(
   def: QuintDef,
   idGenerator: IdGenerator,
-  sourceMap: Map<bigint, Loc>,
+  sourceMap: SourceMap,
   analysisOutput: AnalysisOutput
 ): QuintDef {
   const transformer = new IdRefresher(idGenerator, sourceMap, analysisOutput)
@@ -46,10 +46,10 @@ export function generateFreshIds(
 
 class IdRefresher implements IRTransformer {
   private idGenerator: IdGenerator
-  private sourceMap: Map<bigint, Loc>
+  private sourceMap: SourceMap
   private analysisOutput: AnalysisOutput
 
-  constructor(idGenerator: IdGenerator, sourceMap: Map<bigint, Loc>, analysisOutput: AnalysisOutput) {
+  constructor(idGenerator: IdGenerator, sourceMap: SourceMap, analysisOutput: AnalysisOutput) {
     this.idGenerator = idGenerator
     this.sourceMap = sourceMap
     this.analysisOutput = analysisOutput
diff --git a/quint/src/ir/quintIr.ts b/quint/src/ir/quintIr.ts
index 7700f9aee..663816d3a 100644
--- a/quint/src/ir/quintIr.ts
+++ b/quint/src/ir/quintIr.ts
@@ -20,14 +20,6 @@ export interface WithId {
   id: bigint
 }
 
-/**
- * An error message that needs a source map to resolve the actual sources.
- */
-export interface IrErrorMessage {
-  explanation: string
-  refs: bigint[]
-}
-
 /**
  * Quint expressions and declarations carry an optional type tag.
  * If a type tag is missing, it means that the type has not been computed yet.
diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts
index 6085250e7..9c312c562 100644
--- a/quint/src/parsing/ToIrListener.ts
+++ b/quint/src/parsing/ToIrListener.ts
@@ -19,12 +19,15 @@ import {
 } from '../ir/quintIr'
 import { ConcreteFixedRow, QuintSumType, QuintType, Row, RowField, isUnitType, unitType } from '../ir/quintTypes'
 import { strict as assert } from 'assert'
-import { ErrorMessage, Loc } from './quintParserFrontend'
+import { SourceMap } from './quintParserFrontend'
 import { compact, zipWith } from 'lodash'
 import { Maybe, just, none } from '@sweet-monads/maybe'
 import { TerminalNode } from 'antlr4ts/tree/TerminalNode'
 import { QuintTypeDef } from '../ir/quintIr'
 import { zip } from '../util'
+import { QuintError } from '../quintError'
+import { differentTagsError, lowercaseTypeError, tooManySpreadsError } from './parseErrors'
+import { Loc } from '../ErrorMessage'
 
 /**
  * An ANTLR4 listener that constructs QuintIr objects out of the abstract
@@ -49,12 +52,12 @@ export class ToIrListener implements QuintListener {
    */
   typeStack: QuintType[] = []
 
-  sourceMap: Map<bigint, Loc> = new Map<bigint, Loc>()
+  sourceMap: SourceMap = new Map()
 
   /**
    * If errors occur in the listener, this array contains explanations.
    */
-  errors: ErrorMessage[] = []
+  errors: QuintError[] = []
 
   private sourceLocation: string = ''
 
@@ -335,14 +338,12 @@ export class ToIrListener implements QuintListener {
   // type T
   exitTypeAbstractDef(ctx: p.TypeAbstractDefContext) {
     const name = ctx.qualId()!.text
+    const id = this.getId(ctx)
 
     if (name[0].match('[a-z]')) {
-      const msg = 'QNT007: type names must start with an uppercase letter'
-      this.pushError(ctx, msg)
+      this.errors.push(lowercaseTypeError(id, name))
     }
 
-    const id = this.getId(ctx)
-
     const def: QuintTypeDef = {
       id,
       kind: 'typedef',
@@ -356,14 +357,12 @@ export class ToIrListener implements QuintListener {
   exitTypeAliasDef(ctx: p.TypeAliasDefContext) {
     const name = ctx.qualId()!.text
     const type = this.popType().value
+    const id = this.getId(ctx)
 
     if (name[0].match('[a-z]')) {
-      const msg = 'QNT007: type names must start with an uppercase letter'
-      this.pushError(ctx, msg)
+      this.errors.push(lowercaseTypeError(id, name))
     }
 
-    const id = this.getId(ctx)
-
     const def: QuintTypeDef = {
       id,
       kind: 'typedef',
@@ -594,11 +593,10 @@ export class ToIrListener implements QuintListener {
       this.pushApplication(ctx, name, args)
     } else {
       // accessing a tuple element, a record field, or name in a module
+      const id = this.getId(ctx)
       const m = name.match(/^_([1-9][0-9]?)$/)
       if (m) {
         // accessing a tuple element via _1, _2, _3, etc.
-
-        const id = this.getId(ctx)
         const idx: QuintEx = {
           id,
           kind: 'int',
@@ -607,20 +605,6 @@ export class ToIrListener implements QuintListener {
 
         this.pushApplication(ctx, 'item', [callee!, idx])
       } else {
-        // accessing a record field or a name in a module
-        if (
-          name === 'in' ||
-          name === 'and' ||
-          name === 'or' ||
-          name === 'iff' ||
-          name === 'implies' ||
-          name === 'subseteq'
-        ) {
-          const msg = 'QNT006: no keywords allowed as record fields in record.field'
-          this.pushError(ctx, msg)
-        }
-
-        const id = this.getId(ctx)
         const field: QuintEx = {
           id,
           kind: 'str',
@@ -782,8 +766,8 @@ export class ToIrListener implements QuintListener {
       this.pushApplication(ctx, 'Rec', pairs.flat())
     } else if (spreads.length > 1) {
       // error
-      const msg = 'QNT012: ... may be used once in { ...record, <fields> }'
-      this.pushError(ctx, msg)
+      const id = this.getId(ctx)
+      this.errors.push(tooManySpreadsError(id))
     } else {
       // { ...record, field1: value1, field2: value2 }
       // translate to record.with("field1", value1).with("field2", value2)
@@ -1118,22 +1102,20 @@ export class ToIrListener implements QuintListener {
     if (singletonUnions && singletonUnions[0].kind === 'union') {
       const tag = singletonUnions[0].tag
       let records = singletonUnions[0].records
+      const id = this.getId(ctx)
       for (let i = 1; i < size; i++) {
         const one = singletonUnions[i]
         if (one.kind === 'union') {
           if (one.tag === tag) {
             records = records.concat(one.records)
           } else {
-            const tags = `${tag} and ${one.tag}`
-            const msg = 'QNT011: Records in disjoint union have different tag fields: '
-            this.pushError(ctx, msg + tags)
+            this.errors.push(differentTagsError(id, tag, one.tag))
           }
         } else {
           // istanbul ignore next
           assert(false, 'exitTypeUnionRec: no union in exitTypeUnionRec')
         }
       }
-      const id = this.getId(ctx)
       this.typeStack.push({ id, kind: 'union', tag, records })
     } else {
       const ls = this.locStr(ctx)
@@ -1238,16 +1220,6 @@ export class ToIrListener implements QuintListener {
     })
   }
 
-  // push an error from the context
-  private pushError(ctx: ParserRuleContext, message: string) {
-    const start = { line: ctx.start.line - 1, col: ctx.start.charPositionInLine, index: ctx.start.startIndex }
-    // istanbul ignore next
-    const end = ctx.stop
-      ? { line: ctx.stop.line - 1, col: ctx.stop.charPositionInLine, index: ctx.stop.stopIndex }
-      : start
-    this.errors.push({ explanation: message, locs: [{ source: this.sourceLocation, start, end }] })
-  }
-
   // pop a type
   private popType(): Maybe<QuintType> {
     // the user has specified a type
diff --git a/quint/src/parsing/parseErrors.ts b/quint/src/parsing/parseErrors.ts
new file mode 100644
index 000000000..196758e95
--- /dev/null
+++ b/quint/src/parsing/parseErrors.ts
@@ -0,0 +1,36 @@
+import { QuintError } from '../quintError'
+
+export function lowercaseTypeError(id: bigint, name: string): QuintError {
+  return {
+    code: 'QNT007',
+    message: 'type names must start with an uppercase letter',
+    reference: id,
+    data: name[0].match('[a-z]')
+      ? {
+          fix: {
+            kind: 'replace',
+            original: `type ${name[0]}`,
+            replacement: `type ${name[0].toUpperCase()}`,
+          },
+        }
+      : {},
+  }
+}
+
+export function tooManySpreadsError(id: bigint): QuintError {
+  return {
+    code: 'QNT012',
+    message: '... may be used once in { ...record, <fields> ',
+    reference: id,
+    data: {},
+  }
+}
+
+export function differentTagsError(id: bigint, tag: string, otherTag: string): QuintError {
+  return {
+    code: 'QNT011',
+    message: `Records in disjoint union have different tag fields: ${tag} and ${otherTag}`,
+    reference: id,
+    data: {},
+  }
+}
diff --git a/quint/src/parsing/quintParserFrontend.ts b/quint/src/parsing/quintParserFrontend.ts
index c291ee39f..237f8e7b7 100644
--- a/quint/src/parsing/quintParserFrontend.ts
+++ b/quint/src/parsing/quintParserFrontend.ts
@@ -17,84 +17,28 @@ import { QuintLexer } from '../generated/QuintLexer'
 import * as p from '../generated/QuintParser'
 import { QuintListener } from '../generated/QuintListener'
 
-import { IrErrorMessage, QuintDeclaration, QuintDef, QuintEx, QuintModule, isDef } from '../ir/quintIr'
+import { QuintDeclaration, QuintDef, QuintEx, QuintModule, isDef } from '../ir/quintIr'
 import { IdGenerator, newIdGenerator } from '../idGenerator'
 import { ToIrListener } from './ToIrListener'
 import { LookupTable, NameResolutionResult, UnusedDefinitions } from '../names/base'
 import { resolveNames } from '../names/resolver'
-import { QuintError, quintErrorToString } from '../quintError'
+import { QuintError } from '../quintError'
 import { SourceLookupPath, SourceResolver, fileSourceResolver } from './sourceResolver'
 import { CallGraphVisitor, mkCallGraphContext } from '../static/callgraph'
 import { walkModule } from '../ir/IRVisitor'
 import { toposort } from '../static/toposort'
 import { ErrorCode } from '../quintError'
-import { compact } from 'lodash'
-
-export interface Loc {
-  source: string
-  start: { line: number; col: number; index: number }
-  end?: { line: number; col: number; index: number }
-}
-
-// the default error location that usually indicates a bug in our code
-const unknownLoc: Loc = {
-  source: '<unknown>',
-  start: { line: 0, col: 0, index: 0 },
-}
-
-/**
- * An error message whose locations have been resolved.
- */
-export interface ErrorMessage {
-  explanation: string
-  locs: Loc[]
-}
+import { Loc } from '../ErrorMessage'
 
 /**
  * A source map that is constructed by the parser phases.
  */
 export type SourceMap = Map<bigint, Loc>
 
-/**
- * Map an identifier to the corresponding location in the source map, if possible.
- * @param sourceMap the source map
- * @param id the identifier to map
- * @returns the location, if found in the map, or the unknown location
- */
-export function sourceIdToLoc(sourceMap: SourceMap, id: bigint): Loc {
-  let sourceLoc = sourceMap.get(id)
-  if (!sourceLoc) {
-    console.error(`No source location found for ${id}. Please report a bug.`)
-    return unknownLoc
-  } else {
-    return sourceLoc
-  }
-}
-
-// an adapter from IrErrorMessage to ErrorMessage
-export function fromIrErrorMessage(sourceMap: SourceMap): (err: IrErrorMessage) => ErrorMessage {
-  return msg => {
-    return {
-      explanation: msg.explanation,
-      locs: msg.refs.map(id => sourceMap.get(id) ?? unknownLoc),
-    }
-  }
-}
-
-export function fromQuintError(sourceMap: Map<bigint, Loc>): (_: QuintError) => ErrorMessage {
-  return error => {
-    const loc = error.reference ? sourceMap.get(error.reference) : undefined
-    return {
-      explanation: quintErrorToString(error),
-      locs: compact([loc]),
-    }
-  }
-}
-
 /**
  * The result of parsing, T is specialized to a phase, see below.
  */
-export type ParseResult<T> = Either<ErrorMessage[], T>
+export type ParseResult<T> = Either<{ errors: QuintError[]; sourceMap: SourceMap }, T>
 
 /**
  * Phase 1: Parsing a string of characters into intermediate representation.
@@ -129,7 +73,7 @@ export type ExpressionOrDeclarationParseResult =
   | { kind: 'declaration'; decl: QuintDeclaration }
   | { kind: 'expr'; expr: QuintEx }
   | { kind: 'none' }
-  | { kind: 'error'; messages: ErrorMessage[] }
+  | { kind: 'error'; errors: QuintError[] }
 
 /**
  * Try parsing text as an expression or a top-level declaration.
@@ -144,11 +88,11 @@ export function parseExpressionOrDeclaration(
   idGenerator: IdGenerator,
   sourceMap: SourceMap
 ): ExpressionOrDeclarationParseResult {
-  const errorMessages: ErrorMessage[] = []
-  const parser = setupParser(text, sourceLocation, errorMessages)
+  const errors: QuintError[] = []
+  const parser = setupParser(text, sourceLocation, errors, sourceMap, idGenerator)
   const tree = parser.declarationOrExpr()
-  if (errorMessages.length > 0) {
-    return { kind: 'error', messages: errorMessages }
+  if (errors.length > 0) {
+    return { kind: 'error', errors: errors }
   } else {
     const listener = new ExpressionOrDeclarationListener(sourceLocation, idGenerator)
 
@@ -156,7 +100,7 @@ export function parseExpressionOrDeclaration(
     listener.sourceMap = sourceMap
 
     ParseTreeWalker.DEFAULT.walk(listener as QuintListener, tree)
-    return listener.result
+    return listener.result ?? { kind: 'error', errors: listener.errors }
   }
 }
 
@@ -170,20 +114,21 @@ export function parsePhase1fromText(
   text: string,
   sourceLocation: string
 ): ParseResult<ParserPhase1> {
-  const errorMessages: ErrorMessage[] = []
-  const parser = setupParser(text, sourceLocation, errorMessages)
+  const errors: QuintError[] = []
+  const sourceMap: SourceMap = new Map()
+  const parser = setupParser(text, sourceLocation, errors, sourceMap, idGen)
   // run the parser
   const tree = parser.modules()
-  if (errorMessages.length > 0) {
+  if (errors.length > 0) {
     // report the errors
-    return left(errorMessages)
+    return left({ errors: errors, sourceMap: sourceMap })
   } else {
     // walk through the AST and construct the IR
     const listener = new ToIrListener(sourceLocation, idGen)
     ParseTreeWalker.DEFAULT.walk(listener as QuintListener, tree)
 
     if (listener.errors.length > 0) {
-      return left(listener.errors)
+      return left({ errors: listener.errors, sourceMap: listener.sourceMap })
     } else if (listener.modules.length > 0) {
       return right({ modules: listener.modules, sourceMap: listener.sourceMap })
     } else {
@@ -240,11 +185,12 @@ export function parsePhase2sourceResolution(
             .concat([importeePath])
             .map(p => `'${p.toSourceName()}'`)
             .join(' imports ')
-          const err = fromIrErrorMessage(sourceMap)({
-            explanation: `Cyclic imports: ${cycle}`,
-            refs: [decl.id],
-          })
-          return left([err])
+          const err: QuintError = {
+            code: 'QNT098',
+            message: `Cyclic imports: ${cycle}`,
+            reference: decl.id,
+          }
+          return left({ errors: [err], sourceMap: sourceMap })
         }
         if (sourceToModules.has(importeePath.normalizedPath)) {
           // The source has been parsed already. Just push the module rank,
@@ -256,12 +202,12 @@ export function parsePhase2sourceResolution(
         const errorOrText = sourceResolver.load(importeePath)
         if (errorOrText.isLeft()) {
           // failed to load the imported source
-          const err = fromIrErrorMessage(sourceMap)({
-            // do not use the original message as it propagates absolute file names
-            explanation: `import ... from '${decl.fromSource}': could not load`,
-            refs: [decl.id],
-          })
-          return left([err])
+          const err: QuintError = {
+            code: 'QNT013',
+            message: `import ... from '${decl.fromSource}': could not load`,
+            reference: decl.id,
+          }
+          return left({ errors: [err], sourceMap: sourceMap })
         }
         // try to parse the source code
         const parseResult = parsePhase1fromText(idGen, errorOrText.value, importeePath.toSourceName())
@@ -297,7 +243,7 @@ export function parsePhase2sourceResolution(
  */
 export function parsePhase3importAndNameResolution(phase2Data: ParserPhase2): ParseResult<ParserPhase3> {
   return resolveNames(phase2Data.modules)
-    .mapLeft(errors => errors.map(fromQuintError(phase2Data.sourceMap)))
+    .mapLeft(errors => ({ errors, sourceMap: phase2Data.sourceMap }))
     .map((result: NameResolutionResult) => ({ ...phase2Data, ...result }))
 }
 
@@ -321,13 +267,16 @@ export function parsePhase4toposort(phase3Data: ParserPhase3): ParseResult<Parse
   return cycleOrModules
     .mapLeft(cycleIds => {
       // found a cycle, report it
-      const errorCode: ErrorCode = 'QNT099'
-      return [
-        {
-          locs: cycleIds.toArray().map(id => sourceIdToLoc(phase3Data.sourceMap, id)),
-          explanation: `${errorCode}: Found cyclic declarations. Use fold and foldl instead of recursion`,
-        },
-      ] as ErrorMessage[]
+      return {
+        errors: cycleIds.toArray().map((id): QuintError => {
+          return {
+            code: 'QNT099',
+            message: 'Found cyclic declarations. Use fold and foldl instead of recursion',
+            reference: id,
+          }
+        }),
+        sourceMap: phase3Data.sourceMap,
+      }
     })
     .mapRight(modules => {
       // reordered the declarations
@@ -380,7 +329,7 @@ export function parse(
     .chain(phase3Data => parsePhase4toposort(phase3Data))
 }
 
-export function parseDefOrThrow(text: string, idGen?: IdGenerator, sourceMap?: Map<bigint, Loc>): QuintDef {
+export function parseDefOrThrow(text: string, idGen?: IdGenerator, sourceMap?: SourceMap): QuintDef {
   const result = parseExpressionOrDeclaration(text, '<builtins>', idGen ?? newIdGenerator(), sourceMap ?? new Map())
   if (result.kind === 'declaration' && isDef(result.decl)) {
     return result.decl
@@ -390,15 +339,27 @@ export function parseDefOrThrow(text: string, idGen?: IdGenerator, sourceMap?: M
 }
 
 // setup a Quint parser, so it can be used to parse from various non-terminals
-function setupParser(text: string, sourceLocation: string, errorMessages: ErrorMessage[]): p.QuintParser {
+function setupParser(
+  text: string,
+  sourceLocation: string,
+  errors: QuintError[],
+  sourceMap: SourceMap,
+  idGen: IdGenerator
+): p.QuintParser {
   // error listener to report lexical and syntax errors
   const errorListener: any = {
-    syntaxError: (recognizer: any, offendingSymbol: any, line: number, charPositionInLine: number, msg: string) => {
+    syntaxError: (_recognizer: any, offendingSymbol: any, line: number, charPositionInLine: number, msg: string) => {
+      const id = idGen.nextId()
       const len = offendingSymbol ? offendingSymbol.stopIndex - offendingSymbol.startIndex : 0
       const index = offendingSymbol ? offendingSymbol.startIndex : 0
       const start = { line: line - 1, col: charPositionInLine, index }
       const end = { line: line - 1, col: charPositionInLine + len, index: index + len }
-      errorMessages.push({ explanation: msg, locs: [{ source: sourceLocation, start, end }] })
+      const loc: Loc = { source: sourceLocation, start, end }
+      sourceMap.set(id, loc)
+
+      const code = (msg.match(/QNT\d\d\d/)?.[0] as ErrorCode) ?? 'QNT000'
+
+      errors.push({ code, message: msg.replace(`[${code}] `, ''), reference: id })
     },
   }
 
@@ -421,15 +382,7 @@ function setupParser(text: string, sourceLocation: string, errorMessages: ErrorM
 
 // A simple listener to parse a declaration or expression
 class ExpressionOrDeclarationListener extends ToIrListener {
-  result: ExpressionOrDeclarationParseResult = {
-    kind: 'error',
-    messages: [
-      {
-        explanation: 'unknown parse result',
-        locs: [],
-      },
-    ],
-  }
+  result?: ExpressionOrDeclarationParseResult
 
   exitDeclarationOrExpr(ctx: p.DeclarationOrExprContext) {
     if (ctx.declaration()) {
diff --git a/quint/src/quintAnalyzer.ts b/quint/src/quintAnalyzer.ts
index e9f9cda7a..92738f491 100644
--- a/quint/src/quintAnalyzer.ts
+++ b/quint/src/quintAnalyzer.ts
@@ -31,7 +31,7 @@ export type AnalysisOutput = {
 }
 
 /* A tuple with a list of errors and the analysis output */
-export type AnalysisResult = [[bigint, QuintError][], AnalysisOutput]
+export type AnalysisResult = [QuintError[], AnalysisOutput]
 
 /**
  * Analyzes multiple Quint modules and returns the analysis result.
@@ -80,7 +80,7 @@ class QuintAnalyzer {
   private modeChecker: ModeChecker
   private multipleUpdatesChecker: MultipleUpdatesChecker
 
-  private errors: [bigint, QuintError][] = []
+  private errors: QuintError[] = []
   private output: AnalysisOutput = { types: new Map(), effects: new Map(), modes: new Map() }
 
   constructor(lookupTable: LookupTable, previousOutput?: AnalysisOutput) {
@@ -108,12 +108,12 @@ class QuintAnalyzer {
 
     // TODO: Type and effect checking should return QuintErrors instead of error trees
     this.errors.push(
-      ...errorTrees.map(([id, err]): [bigint, QuintError] => {
-        return [id, { code: 'QNT000', message: errorTreeToString(err), reference: id, data: { trace: err } }]
+      ...errorTrees.map(([id, err]): QuintError => {
+        return { code: 'QNT000', message: errorTreeToString(err), reference: id, data: { trace: err } }
       })
     )
 
-    this.errors.push(...modeErrMap.entries(), ...updatesErrMap.entries())
+    this.errors.push(...modeErrMap.values(), ...updatesErrMap.values())
 
     // We assume that ids are unique across modules, and map merging can be done
     // without collision checks
diff --git a/quint/src/quintError.ts b/quint/src/quintError.ts
index 6cbe4c5b0..065fdd694 100644
--- a/quint/src/quintError.ts
+++ b/quint/src/quintError.ts
@@ -45,6 +45,16 @@ export type ErrorCode =
   | 'QNT007'
   /* QNT008: Simple identifiers cannot be qualified (i.e. contain `::`) */
   | 'QNT008'
+  /* QNT009: Missing arguments or parameters. You should omit the parentheses */
+  | 'QNT009'
+  /* QNT011: Records in disjoint union have different tag fields: <tag> and <otherTag> */
+  | 'QNT011'
+  /* QNT012: '...' may be used once in '{ ...record, <fields> }' */
+  | 'QNT012'
+  /* QNT013: import ... from <source>: could not load */
+  | 'QNT013'
+  /* QNT098: Cyclic imports */
+  | 'QNT098'
   /* QNT099: Found cyclic definitions */
   | 'QNT099'
   /* QNT101: Conflicting definitions for '<name>' */
@@ -67,6 +77,30 @@ export type ErrorCode =
   | 'QNT407'
   /* QNT500: Unitialized constant */
   | 'QNT500'
+  /* QNT501: Internal compiler error */
+  | 'QNT501'
+  /* QNT502: Variable not set */
+  | 'QNT502'
+  /* QNT503: Invalid arithmetics */
+  | 'QNT503'
+  /* QNT504: Range out of bounds */
+  | 'QNT504'
+  /* QNT505: Tail on empty list */
+  | 'QNT505'
+  /* QNT506: Invalid slice */
+  | 'QNT506'
+  /* QNT507: Missing map key */
+  | 'QNT507'
+  /* QNT508: Assertion failed */
+  | 'QNT508'
+  /* QNT509: Called oneOf() in an empty set */
+  | 'QNT509'
+  /* QNT510: Array acces out of bounds */
+  | 'QNT510'
+  /* QNT511: Test returned false */
+  | 'QNT511'
+  /* QNT512: Simulation failure */
+  | 'QNT512'
 
 /* Additional data for a Quint error */
 export interface QuintErrorData {
diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts
index 85355b355..2386a43fe 100644
--- a/quint/src/quintVerifier.ts
+++ b/quint/src/quintVerifier.ts
@@ -15,7 +15,7 @@
  */
 
 import { Either, chain, left, right } from '@sweet-monads/either'
-import { ErrorMessage } from './parsing/quintParserFrontend'
+import { ErrorMessage } from './ErrorMessage'
 import path from 'path'
 import fs from 'fs'
 import os from 'os'
diff --git a/quint/src/repl.ts b/quint/src/repl.ts
index 4f343c4bb..0f061103d 100644
--- a/quint/src/repl.ts
+++ b/quint/src/repl.ts
@@ -32,7 +32,7 @@ import {
 import { formatError } from './errorReporter'
 import { Register } from './runtime/runtime'
 import { TraceRecorder, newTraceRecorder } from './runtime/trace'
-import { ErrorMessage, parseDefOrThrow, parseExpressionOrDeclaration } from './parsing/quintParserFrontend'
+import { parseDefOrThrow, parseExpressionOrDeclaration } from './parsing/quintParserFrontend'
 import { prettyQuintEx, printExecutionFrameRec, terminalWidth } from './graphics'
 import { verbosity } from './verbosity'
 import { Rng, newRng } from './rng'
@@ -42,6 +42,8 @@ import { cwd } from 'process'
 import { newIdGenerator } from './idGenerator'
 import { moduleToString } from './ir/IRprinting'
 import { EvaluationState, newEvaluationState } from './runtime/impl/compilerImpl'
+import { mkErrorMessage } from './cliCommands'
+import { QuintError } from './quintError'
 
 // tunable settings
 export const settings = {
@@ -541,7 +543,7 @@ function tryEval(out: writer, state: ReplState, newInput: string): boolean {
     state.compilationState.sourceMap
   )
   if (parseResult.kind === 'error') {
-    printErrorMessages(out, state, 'syntax error', newInput, parseResult.messages)
+    printErrorMessages(out, state, 'syntax error', newInput, parseResult.errors)
     out('\n') // be nice to external programs
     return false
   }
@@ -617,10 +619,11 @@ function printErrorMessages(
   state: ReplState,
   kind: string,
   inputText: string,
-  messages: ErrorMessage[],
+  errors: QuintError[],
   color: (_text: string) => string = chalk.red
 ) {
   const modulesText = state.moduleHist + inputText
+  const messages = errors.map(mkErrorMessage(state.compilationState.sourceMap))
   // display the error messages and highlight the error places
   messages.forEach(e => {
     const text = e.locs[0]?.source === '<input>' ? inputText : modulesText
diff --git a/quint/src/runtime/compile.ts b/quint/src/runtime/compile.ts
index dacc2d07d..bca471126 100644
--- a/quint/src/runtime/compile.ts
+++ b/quint/src/runtime/compile.ts
@@ -9,25 +9,19 @@
  */
 
 import { Either, left, right } from '@sweet-monads/either'
-import {
-  ErrorMessage,
-  Loc,
-  fromIrErrorMessage,
-  parse,
-  parsePhase3importAndNameResolution,
-} from '../parsing/quintParserFrontend'
+import { SourceMap, parse, parsePhase3importAndNameResolution } from '../parsing/quintParserFrontend'
 import { Computable, ComputableKind, kindName } from './runtime'
 import { ExecutionListener } from './trace'
-import { FlatModule, IrErrorMessage, QuintDeclaration, QuintDef, QuintEx, QuintModule } from '../ir/quintIr'
+import { FlatModule, QuintDeclaration, QuintDef, QuintEx, QuintModule } from '../ir/quintIr'
 import { CompilerVisitor, EvaluationState, newEvaluationState } from './impl/compilerImpl'
 import { walkDefinition } from '../ir/IRVisitor'
 import { LookupTable } from '../names/base'
 import { AnalysisOutput, analyzeInc, analyzeModules } from '../quintAnalyzer'
-import { mkErrorMessage } from '../cliCommands'
 import { IdGenerator, newIdGenerator } from '../idGenerator'
 import { SourceLookupPath } from '../parsing/sourceResolver'
 import { Rng } from '../rng'
 import { flattenModules } from '../flattening/fullFlattener'
+import { QuintError } from '../quintError'
 
 /**
  * The name of the shadow variable that stores the last found trace.
@@ -46,13 +40,13 @@ export interface CompilationContext {
   // the lookup table to query for values and definitions
   lookupTable: LookupTable
   // messages that are produced during parsing
-  syntaxErrors: ErrorMessage[]
+  syntaxErrors: QuintError[]
   // messages that are produced by static analysis
-  analysisErrors: ErrorMessage[]
+  analysisErrors: QuintError[]
   // messages that are produced during compilation
-  compileErrors: ErrorMessage[]
+  compileErrors: QuintError[]
   // messages that get populated as the compiled code is executed
-  getRuntimeErrors: () => ErrorMessage[]
+  getRuntimeErrors: () => QuintError[]
   // The state of pre-compilation phases.
   compilationState: CompilationState
   // The state of the compiler visitor.
@@ -74,7 +68,7 @@ export interface CompilationState {
   // The name of the main module.
   mainName?: string
   // The source map for the compiled code.
-  sourceMap: Map<bigint, Loc>
+  sourceMap: SourceMap
   // The output of the Quint analyzer.
   analysisOutput: AnalysisOutput
 }
@@ -94,17 +88,18 @@ export function newCompilationState(): CompilationState {
   }
 }
 
-export function errorContextFromMessage(listener: ExecutionListener): (errors: ErrorMessage[]) => CompilationContext {
-  const compilationState = newCompilationState()
+export function errorContextFromMessage(
+  listener: ExecutionListener
+): (_: { errors: QuintError[]; sourceMap: SourceMap }) => CompilationContext {
   const evaluationState = newEvaluationState(listener)
-  return (errs: ErrorMessage[]) => {
+  return ({ errors, sourceMap }) => {
     return {
       lookupTable: new Map(),
-      syntaxErrors: errs,
+      syntaxErrors: errors,
       analysisErrors: [],
       compileErrors: [],
       getRuntimeErrors: () => [],
-      compilationState,
+      compilationState: { ...newCompilationState(), sourceMap },
       evaluationState,
     }
   }
@@ -144,7 +139,7 @@ export function compile(
   rand: (bound: bigint) => bigint,
   defs: QuintDef[]
 ): CompilationContext {
-  const { sourceMap, analysisOutput } = compilationState
+  const { analysisOutput } = compilationState
 
   const visitor = new CompilerVisitor(lookupTable, analysisOutput.types, rand, evaluationState)
 
@@ -154,9 +149,9 @@ export function compile(
     lookupTable,
     syntaxErrors: [],
     analysisErrors: [],
-    compileErrors: visitor.getCompileErrors().map(fromIrErrorMessage(sourceMap)),
+    compileErrors: visitor.getCompileErrors(),
     getRuntimeErrors: () => {
-      return visitor.getRuntimeErrors().splice(0).map(fromIrErrorMessage(sourceMap))
+      return visitor.getRuntimeErrors().splice(0)
     },
     compilationState,
     evaluationState: visitor.getEvaluationState(),
@@ -249,11 +244,7 @@ export function compileDecl(
 
       const ctx = compile(newState, evaluationState, flattenedTable, rng.next, defsToCompile)
 
-      const errorLocator = mkErrorMessage(state.sourceMap)
-      return {
-        ...ctx,
-        analysisErrors: Array.from(analysisErrors, errorLocator),
-      }
+      return { ...ctx, analysisErrors }
     }).value // We produce a compilation context in any case
 }
 
@@ -305,22 +296,21 @@ export function compileFromCode(
 
           const main = flattenedModules.find(m => m.name === mainName)
           // when the main module is not found, we will report an error
-          const mainNotFoundError: IrErrorMessage[] = main
+          const mainNotFoundError: QuintError[] = main
             ? []
             : [
                 {
-                  explanation: `Main module ${mainName} not found`,
-                  refs: [],
+                  code: 'QNT405',
+                  message: `Main module ${mainName} not found`,
                 },
               ]
           const defsToCompile = main ? main.declarations : []
           const ctx = compile(compilationState, newEvaluationState(execListener), flattenedTable, rand, defsToCompile)
 
-          const errorLocator = mkErrorMessage(sourceMap)
           return right({
             ...ctx,
-            compileErrors: ctx.compileErrors.concat(mainNotFoundError.map(fromIrErrorMessage(sourceMap))),
-            analysisErrors: Array.from(analysisErrors, errorLocator),
+            compileErrors: ctx.compileErrors.concat(mainNotFoundError),
+            analysisErrors,
           })
         }
         // we produce CompilationContext in any case
diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts
index 7fab0f93b..553f74426 100644
--- a/quint/src/runtime/impl/compilerImpl.ts
+++ b/quint/src/runtime/impl/compilerImpl.ts
@@ -33,7 +33,7 @@ import { ExecutionListener } from '../trace'
 import * as ir from '../../ir/quintIr'
 
 import { RuntimeValue, rv } from './runtimeValue'
-import { ErrorCode } from '../../quintError'
+import { ErrorCode, QuintError } from '../../quintError'
 
 import { inputDefName, lastTraceName } from '../compile'
 import { unreachable } from '../../util'
@@ -83,16 +83,16 @@ export interface EvaluationState {
  */
 export class CompilerErrorTracker {
   // messages that are produced during compilation
-  compileErrors: ir.IrErrorMessage[] = []
+  compileErrors: QuintError[] = []
   // messages that get populated as the compiled code is executed
-  runtimeErrors: ir.IrErrorMessage[] = []
+  runtimeErrors: QuintError[] = []
 
-  addCompileError(id: bigint, msg: string) {
-    this.compileErrors.push({ explanation: msg, refs: [id] })
+  addCompileError(reference: bigint, code: ErrorCode, message: string) {
+    this.compileErrors.push({ code, message, reference })
   }
 
-  addRuntimeError(id: bigint, msg: string) {
-    this.runtimeErrors.push({ explanation: msg, refs: [id] })
+  addRuntimeError(reference: bigint, code: ErrorCode, message: string) {
+    this.runtimeErrors.push({ code, message, reference })
   }
 }
 
@@ -113,7 +113,7 @@ export function newEvaluationState(listener: ExecutionListener): EvaluationState
 
   // Initialize compiler state
   const lastTrace = mkRegister('shadow', lastTraceName, just(rv.mkList([])), () =>
-    state.errorTracker.addRuntimeError(0n, 'q::lastTrace is not set')
+    state.errorTracker.addRuntimeError(0n, 'QNT501', 'q::lastTrace is not set')
   )
   state.shadowVars.push(lastTrace)
   state.context.set(kindName(lastTrace.kind, lastTrace.name), lastTrace)
@@ -218,14 +218,14 @@ export class CompilerVisitor implements IRVisitor {
   /**
    * Get the array of compile errors, which changes as the code gets executed.
    */
-  getCompileErrors(): ir.IrErrorMessage[] {
+  getCompileErrors(): QuintError[] {
     return this.errorTracker.compileErrors
   }
 
   /**
    * Get the array of runtime errors, which changes as the code gets executed.
    */
-  getRuntimeErrors(): ir.IrErrorMessage[] {
+  getRuntimeErrors(): QuintError[] {
     return this.errorTracker.runtimeErrors
   }
 
@@ -239,7 +239,7 @@ export class CompilerVisitor implements IRVisitor {
     // All of them are compiled to callables, which may have zero parameters.
     let boundValue = this.compStack.pop()
     if (boundValue === undefined) {
-      this.errorTracker.addCompileError(opdef.id, `No expression for ${opdef.name} on compStack`)
+      this.errorTracker.addCompileError(opdef.id, 'QNT501', `No expression for ${opdef.name} on compStack`)
       return
     }
 
@@ -310,7 +310,11 @@ export class CompilerVisitor implements IRVisitor {
     // get the expression that is evaluated in the context of let.
     const exprUnderLet = this.compStack.slice(-1).pop()
     if (exprUnderLet === undefined) {
-      this.errorTracker.addCompileError(letDef.opdef.id, `No expression for ${letDef.opdef.name} on compStack`)
+      this.errorTracker.addCompileError(
+        letDef.opdef.id,
+        'QNT501',
+        `No expression for ${letDef.opdef.name} on compStack`
+      )
       return
     }
 
@@ -337,8 +341,8 @@ export class CompilerVisitor implements IRVisitor {
   exitConst(cdef: ir.QuintConst) {
     // all constants should be instantiated before running the simulator
     const code: ErrorCode = 'QNT500'
-    const msg = `${code}: Uninitialized const ${cdef.name}. Use: import <moduleName>(${cdef.name}=<value>).*`
-    this.errorTracker.addCompileError(cdef.id, msg)
+    const msg = `Uninitialized const ${cdef.name}. Use: import <moduleName>(${cdef.name}=<value>).*`
+    this.errorTracker.addCompileError(cdef.id, code, msg)
   }
 
   exitVar(vardef: ir.QuintVar) {
@@ -364,14 +368,14 @@ export class CompilerVisitor implements IRVisitor {
     //  one for the variable, and
     //  one for its next-state version
     const prevRegister = mkRegister('var', varName, none(), () =>
-      this.errorTracker.addRuntimeError(vardef.id, `Variable ${varName} is not set`)
+      this.errorTracker.addRuntimeError(vardef.id, 'QNT502', `Variable ${varName} is not set`)
     )
     this.vars.push(prevRegister)
     // at the moment, we have to refer to variables both via id and name
     this.context.set(kindName('var', varName), prevRegister)
     this.context.set(kindName('var', vardef.id), prevRegister)
     const nextRegister = mkRegister('nextvar', varName, none(), () =>
-      this.errorTracker.addRuntimeError(vardef.id, `${varName}' is not set`)
+      this.errorTracker.addRuntimeError(vardef.id, 'QNT502', `${varName}' is not set`)
     )
     this.nextVars.push(nextRegister)
     // at the moment, we have to refer to variables both via id and name
@@ -412,7 +416,7 @@ export class CompilerVisitor implements IRVisitor {
       this.compStack.push(comp)
     } else {
       // this should not happen, due to the name resolver
-      this.errorTracker.addCompileError(name.id, `Name ${name.name} not found`)
+      this.errorTracker.addCompileError(name.id, 'QNT502', `Name ${name.name} not found`)
       this.compStack.push(fail)
     }
   }
@@ -430,7 +434,7 @@ export class CompilerVisitor implements IRVisitor {
               const nextvar = this.contextGet(name, ['nextvar'])
               this.compStack.push(nextvar ?? fail)
             } else {
-              this.errorTracker.addCompileError(app.id, 'Operator next(...) needs one argument')
+              this.errorTracker.addCompileError(app.id, 'QNT502', 'Operator next(...) needs one argument')
               this.compStack.push(fail)
             }
           }
@@ -507,7 +511,7 @@ export class CompilerVisitor implements IRVisitor {
             if (q.toInt() !== 0n) {
               return just(rv.mkInt(p.toInt() / q.toInt()))
             } else {
-              this.errorTracker.addRuntimeError(app.id, 'Division by zero')
+              this.errorTracker.addRuntimeError(app.id, 'QNT503', 'Division by zero')
               return none()
             }
           })
@@ -520,9 +524,9 @@ export class CompilerVisitor implements IRVisitor {
         case 'ipow':
           this.applyFun(app.id, 2, (p, q) => {
             if (q.toInt() == 0n && p.toInt() == 0n) {
-              this.errorTracker.addRuntimeError(app.id, '0^0 is undefined')
+              this.errorTracker.addRuntimeError(app.id, 'QNT503', '0^0 is undefined')
             } else if (q.toInt() < 0n) {
-              this.errorTracker.addRuntimeError(app.id, 'i^j is undefined for j < 0')
+              this.errorTracker.addRuntimeError(app.id, 'QNT503', 'i^j is undefined for j < 0')
             } else {
               return just(rv.mkInt(p.toInt() ** q.toInt()))
             }
@@ -576,7 +580,7 @@ export class CompilerVisitor implements IRVisitor {
               }
               return just(rv.mkList(arr))
             } else {
-              this.errorTracker.addRuntimeError(app.id, `range(${s}, ${e}) is out of bounds`)
+              this.errorTracker.addRuntimeError(app.id, 'QNT504', `range(${s}, ${e}) is out of bounds`)
               return none()
             }
           })
@@ -603,7 +607,7 @@ export class CompilerVisitor implements IRVisitor {
             if (l.size > 0) {
               return this.sliceList(app.id, l, 1, l.size)
             } else {
-              this.errorTracker.addRuntimeError(app.id, 'Applied tail to an empty list')
+              this.errorTracker.addRuntimeError(app.id, 'QNT505', 'Applied tail to an empty list')
               return none()
             }
           })
@@ -615,7 +619,11 @@ export class CompilerVisitor implements IRVisitor {
             if (s >= 0 && s <= l.size && e <= l.size && e >= s) {
               return this.sliceList(app.id, l, s, e)
             } else {
-              this.errorTracker.addRuntimeError(app.id, `slice(..., ${s}, ${e}) applied to a list of size ${l.size}`)
+              this.errorTracker.addRuntimeError(
+                app.id,
+                'QNT506',
+                `slice(..., ${s}, ${e}) applied to a list of size ${l.size}`
+              )
               return none()
             }
           })
@@ -657,7 +665,7 @@ export class CompilerVisitor implements IRVisitor {
             if (fieldValue) {
               return just(fieldValue)
             } else {
-              this.errorTracker.addRuntimeError(app.id, `Accessing a missing record field ${name}`)
+              this.errorTracker.addRuntimeError(app.id, 'QNT501', `Accessing a missing record field ${name}`)
               return none()
             }
           })
@@ -682,7 +690,7 @@ export class CompilerVisitor implements IRVisitor {
               const newMap = rec.toOrderedMap().set(key, fieldValue)
               return just(rv.mkRecord(newMap))
             } else {
-              this.errorTracker.addRuntimeError(app.id, `Called 'with' with a non-existent key ${key}`)
+              this.errorTracker.addRuntimeError(app.id, 'QNT501', `Called 'with' with a non-existent key ${key}`)
               return none()
             }
           })
@@ -763,7 +771,7 @@ export class CompilerVisitor implements IRVisitor {
               return just(value)
             } else {
               // Should we print the key? It may be a complex expression.
-              this.errorTracker.addRuntimeError(app.id, "Called 'get' with a non-existing key")
+              this.errorTracker.addRuntimeError(app.id, 'QNT507', "Called 'get' with a non-existing key")
               return none()
             }
           })
@@ -778,7 +786,7 @@ export class CompilerVisitor implements IRVisitor {
               const newMap = asMap.set(normalKey, newValue)
               return just(rv.fromMap(newMap))
             } else {
-              this.errorTracker.addRuntimeError(app.id, "Called 'set' with a non-existing key")
+              this.errorTracker.addRuntimeError(app.id, 'QNT507', "Called 'set' with a non-existing key")
               return none()
             }
           })
@@ -806,7 +814,7 @@ export class CompilerVisitor implements IRVisitor {
                 return rv.fromMap(newMap)
               })
             } else {
-              this.errorTracker.addRuntimeError(app.id, "Called 'setBy' with a non-existing key")
+              this.errorTracker.addRuntimeError(app.id, 'QNT507', "Called 'setBy' with a non-existing key")
               return none()
             }
           })
@@ -884,7 +892,7 @@ export class CompilerVisitor implements IRVisitor {
         case 'assert':
           this.applyFun(app.id, 1, cond => {
             if (!cond.toBool()) {
-              this.errorTracker.addRuntimeError(app.id, 'Assertion failed')
+              this.errorTracker.addRuntimeError(app.id, 'QNT508', 'Assertion failed')
               return none()
             }
             return just(cond)
@@ -912,7 +920,11 @@ export class CompilerVisitor implements IRVisitor {
         case 'eventually':
         case 'enabled':
           this.applyFun(app.id, 1, _ => {
-            this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`)
+            this.errorTracker.addRuntimeError(
+              app.id,
+              'QNT501',
+              `Runtime does not support the built-in operator '${app.opcode}'`
+            )
             return none()
           })
           break
@@ -926,7 +938,11 @@ export class CompilerVisitor implements IRVisitor {
         case 'weakFair':
         case 'strongFair':
           this.applyFun(app.id, 2, _ => {
-            this.errorTracker.addRuntimeError(app.id, `Runtime does not support the built-in operator '${app.opcode}'`)
+            this.errorTracker.addRuntimeError(
+              app.id,
+              'QNT501',
+              `Runtime does not support the built-in operator '${app.opcode}'`
+            )
             return none()
           })
           break
@@ -939,7 +955,7 @@ export class CompilerVisitor implements IRVisitor {
 
   private applyUserDefined(app: ir.QuintApp) {
     const onError = (sourceId: bigint, msg: string): void => {
-      this.errorTracker.addCompileError(sourceId, msg)
+      this.errorTracker.addCompileError(sourceId, 'QNT501', msg)
       this.compStack.push(fail)
     }
 
@@ -1034,7 +1050,7 @@ export class CompilerVisitor implements IRVisitor {
         this.context.delete(key)
         registers.push(register)
       } else {
-        this.errorTracker.addCompileError(p.id, `Parameter ${p.name} not found`)
+        this.errorTracker.addCompileError(p.id, 'QNT501', `Parameter ${p.name} not found`)
       }
     })
 
@@ -1042,19 +1058,19 @@ export class CompilerVisitor implements IRVisitor {
     if (lambdaBody) {
       this.compStack.push(mkCallable(registers, lambdaBody))
     } else {
-      this.errorTracker.addCompileError(lam.id, 'Compilation of lambda failed')
+      this.errorTracker.addCompileError(lam.id, 'QNT501', 'Compilation of lambda failed')
     }
   }
 
   private translateAssign(sourceId: bigint): void {
     if (this.compStack.length < 2) {
-      this.errorTracker.addCompileError(sourceId, `Assignment '=' needs two arguments`)
+      this.errorTracker.addCompileError(sourceId, 'QNT501', `Assignment '=' needs two arguments`)
       return
     }
     const [register, rhs] = this.compStack.splice(-2)
     const name = (register as Register).name
     if (name === undefined) {
-      this.errorTracker.addCompileError(sourceId, `Assignment '=' applied to a non-variable`)
+      this.errorTracker.addCompileError(sourceId, 'QNT501', `Assignment '=' applied to a non-variable`)
       this.compStack.push(fail)
       return
     }
@@ -1067,7 +1083,7 @@ export class CompilerVisitor implements IRVisitor {
         return just(rv.mkBool(true))
       })
     } else {
-      this.errorTracker.addCompileError(sourceId, `Undefined next variable in ${name} = ...`)
+      this.errorTracker.addCompileError(sourceId, 'QNT502', `Undefined next variable in ${name} = ...`)
       this.compStack.push(fail)
     }
   }
@@ -1093,7 +1109,7 @@ export class CompilerVisitor implements IRVisitor {
     mapResultAndElems: (_array: Array<[RuntimeValue, RuntimeValue]>) => RuntimeValue
   ): void {
     if (this.compStack.length < 2) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments')
       return
     }
     // lambda translated to Callable
@@ -1114,7 +1130,7 @@ export class CompilerVisitor implements IRVisitor {
    */
   private applyFold(sourceId: bigint, order: 'fwd' | 'rev'): void {
     if (this.compStack.length < 3) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments for fold')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments for fold')
       return
     }
     // extract two arguments from the call stack and keep the set
@@ -1155,7 +1171,7 @@ export class CompilerVisitor implements IRVisitor {
   // push the combined computable value on the stack
   private applyFun(sourceId: bigint, nargs: number, fun: (..._args: RuntimeValue[]) => Maybe<RuntimeValue>) {
     if (this.compStack.length < nargs) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments')
     } else {
       // pop nargs elements of the compStack
       const args = this.compStack.splice(-nargs, nargs)
@@ -1171,7 +1187,7 @@ export class CompilerVisitor implements IRVisitor {
               .join()
           } catch (error) {
             const msg = error instanceof Error ? error.message : 'unknown error'
-            this.errorTracker.addRuntimeError(sourceId, msg)
+            this.errorTracker.addRuntimeError(sourceId, 'QNT501', msg)
             return none()
           }
         },
@@ -1184,7 +1200,7 @@ export class CompilerVisitor implements IRVisitor {
   // as it should not evaluate both arms
   private translateIfThenElse(sourceId: bigint) {
     if (this.compStack.length < 3) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments')
     } else {
       // pop 3 elements of the compStack
       const [cond, thenArm, elseArm] = this.compStack.splice(-3, 3)
@@ -1239,7 +1255,7 @@ export class CompilerVisitor implements IRVisitor {
   // translate all { A, ..., C } or A.then(B)
   private translateAllOrThen(app: ir.QuintApp): void {
     if (this.compStack.length < app.args.length) {
-      this.errorTracker.addCompileError(app.id, `Not enough arguments on stack for "${app.opcode}"`)
+      this.errorTracker.addCompileError(app.id, 'QNT501', `Not enough arguments on stack for "${app.opcode}"`)
       return
     }
     const args = this.compStack.splice(-app.args.length)
@@ -1253,7 +1269,7 @@ export class CompilerVisitor implements IRVisitor {
   // translate n.reps(A)
   private translateReps(app: ir.QuintApp): void {
     if (this.compStack.length < 2) {
-      this.errorTracker.addCompileError(app.id, `Not enough arguments on stack for "${app.opcode}"`)
+      this.errorTracker.addCompileError(app.id, 'QNT501', `Not enough arguments on stack for "${app.opcode}"`)
       return
     }
     const [niterations, action] = this.compStack.splice(-2)
@@ -1290,7 +1306,7 @@ export class CompilerVisitor implements IRVisitor {
     shortCircuit: (no: number, r: boolean) => Maybe<EvalResult>
   ): void {
     if (this.compStack.length < app.args.length) {
-      this.errorTracker.addCompileError(app.id, `Not enough arguments on stack for "${app.opcode}"`)
+      this.errorTracker.addCompileError(app.id, 'QNT501', `Not enough arguments on stack for "${app.opcode}"`)
       return
     }
     const args = this.compStack.splice(-app.args.length)
@@ -1324,7 +1340,7 @@ export class CompilerVisitor implements IRVisitor {
   // translate any { A, ..., C }
   private translateOrAction(app: ir.QuintApp): void {
     if (this.compStack.length < app.args.length) {
-      this.errorTracker.addCompileError(app.id, 'Not enough arguments on stack for "any"')
+      this.errorTracker.addCompileError(app.id, 'QNT501', 'Not enough arguments on stack for "any"')
       return
     }
     const args = this.compStack.splice(-app.args.length)
@@ -1387,7 +1403,7 @@ export class CompilerVisitor implements IRVisitor {
           b
             .map(sz => {
               if (sz === 0n) {
-                this.errorTracker.addRuntimeError(sourceId, `Applied oneOf to an empty set`)
+                this.errorTracker.addRuntimeError(sourceId, 'QNT509', `Applied oneOf to an empty set`)
               }
               return this.rand(sz)
             })
@@ -1406,7 +1422,7 @@ export class CompilerVisitor implements IRVisitor {
 
   private test(sourceId: bigint) {
     if (this.compStack.length < 5) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments on stack for "q::test"')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments on stack for "q::test"')
       return
     }
 
@@ -1416,7 +1432,7 @@ export class CompilerVisitor implements IRVisitor {
 
   private testOnce(sourceId: bigint) {
     if (this.compStack.length < 4) {
-      this.errorTracker.addCompileError(sourceId, 'Not enough arguments on stack for "q::testOnce"')
+      this.errorTracker.addCompileError(sourceId, 'QNT501', 'Not enough arguments on stack for "q::testOnce"')
       return
     }
 
@@ -1610,7 +1626,7 @@ export class CompilerVisitor implements IRVisitor {
       const elem = list.get(Number(idx))
       return elem ? just(elem) : none()
     } else {
-      this.errorTracker.addRuntimeError(sourceId, `Out of bounds, nth(${idx})`)
+      this.errorTracker.addRuntimeError(sourceId, 'QNT510', `Out of bounds, nth(${idx})`)
       return none()
     }
   }
@@ -1620,7 +1636,7 @@ export class CompilerVisitor implements IRVisitor {
     if (idx >= 0n && idx < list.size) {
       return just(rv.mkList(list.set(Number(idx), value)))
     } else {
-      this.errorTracker.addRuntimeError(sourceId, `Out of bounds, replaceAt(..., ${idx}, ...)`)
+      this.errorTracker.addRuntimeError(sourceId, 'QNT510', `Out of bounds, replaceAt(..., ${idx}, ...)`)
       return none()
     }
   }
diff --git a/quint/src/runtime/testing.ts b/quint/src/runtime/testing.ts
index 140779526..d19082578 100644
--- a/quint/src/runtime/testing.ts
+++ b/quint/src/runtime/testing.ts
@@ -8,10 +8,9 @@
  * See License.txt in the project root for license information.
  */
 
-import { Either, left, merge, right } from '@sweet-monads/either'
+import { Either, left, mergeInMany, right } from '@sweet-monads/either'
 import { just } from '@sweet-monads/maybe'
 
-import { ErrorMessage, fromIrErrorMessage } from '../parsing/quintParserFrontend'
 import { QuintEx, QuintOpDef } from '../ir/quintIr'
 
 import { CompilationContext, CompilationState, compile, lastTraceName } from './compile'
@@ -22,6 +21,7 @@ import { ExecutionFrame, newTraceRecorder } from './trace'
 import { Rng } from '../rng'
 import { RuntimeValue, rv } from './impl/runtimeValue'
 import { newEvaluationState } from './impl/compilerImpl'
+import { QuintError } from '../quintError'
 
 /**
  * Various settings to be passed to the testing framework.
@@ -52,9 +52,9 @@ export interface TestResult {
    */
   seed: bigint
   /**
-   * When status === 'failed', errors contain the explanatory error messages.
+   * When status === 'failed', errors contain the explanatory errors.
    */
-  errors: ErrorMessage[]
+  errors: QuintError[]
   /**
    * If the trace was recorded, frames contains the history.
    */
@@ -81,11 +81,11 @@ export function compileAndTest(
   mainName: string,
   lookupTable: LookupTable,
   options: TestOptions
-): Either<ErrorMessage[], TestResult[]> {
+): Either<QuintError[], TestResult[]> {
   const recorder = newTraceRecorder(options.verbosity, options.rng)
   const main = compilationState.modules.find(m => m.name === mainName)
   if (!main) {
-    return left([{ explanation: 'Cannot find main module', locs: [] }])
+    return left([{ code: 'QNT405', message: `Main module ${mainName} not found` }])
   }
 
   const ctx = compile(compilationState, newEvaluationState(recorder), lookupTable, options.rng.next, main.declarations)
@@ -113,7 +113,7 @@ export function compileAndTest(
 
   const testDefs = main.declarations.filter(d => d.kind === 'def' && options.testMatch(d.name)) as QuintOpDef[]
 
-  return merge(
+  return mergeInMany(
     testDefs.map((def, index) => {
       return getComputableForDef(ctx, def).map(comp => {
         const name = def.name
@@ -170,15 +170,16 @@ export function compileAndTest(
 
           if (!ex.value) {
             // if the test returned false, return immediately
-            const e = fromIrErrorMessage(compilationState.sourceMap)({
-              explanation: `${name} returns false`,
-              refs: [def.id],
-            })
+            const error: QuintError = {
+              code: 'QNT511',
+              message: `Test ${name} returned false`,
+              reference: def.id,
+            }
             saveTrace(index, name, 'failed')
             return {
               name,
               status: 'failed',
-              errors: [e],
+              errors: [error],
               seed: seed,
               frames: recorder.getBestTrace().subframes,
               nsamples: nsamples,
@@ -215,11 +216,11 @@ export function compileAndTest(
   )
 }
 
-function getComputableForDef(ctx: CompilationContext, def: QuintOpDef): Either<ErrorMessage[], Computable> {
+function getComputableForDef(ctx: CompilationContext, def: QuintOpDef): Either<QuintError, Computable> {
   const comp = ctx.evaluationState.context.get(kindName('callable', def.id))
   if (comp) {
     return right(comp)
   } else {
-    return left([{ explanation: `Cannot find computable for ${def.name}`, locs: [] }])
+    return left({ code: 'QNT501', message: `Cannot find computable for ${def.name}`, reference: def.id })
   }
 }
diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts
index 8083b7c91..c8cf3eaba 100644
--- a/quint/src/simulation.ts
+++ b/quint/src/simulation.ts
@@ -11,13 +11,13 @@
 import { Either } from '@sweet-monads/either'
 
 import { compileFromCode, contextNameLookup, lastTraceName } from './runtime/compile'
-import { ErrorMessage } from './parsing/quintParserFrontend'
 import { QuintEx } from './ir/quintIr'
 import { Computable } from './runtime/runtime'
 import { ExecutionFrame, newTraceRecorder } from './runtime/trace'
 import { IdGenerator } from './idGenerator'
 import { Rng } from './rng'
 import { SourceLookupPath } from './parsing/sourceResolver'
+import { QuintError } from './quintError'
 
 /**
  * Various settings that have to be passed to the simulator to run.
@@ -42,11 +42,11 @@ export interface SimulatorResult {
   vars: string[]
   states: QuintEx[]
   frames: ExecutionFrame[]
-  errors: ErrorMessage[]
+  errors: QuintError[]
   seed: bigint
 }
 
-function errSimulationResult(status: SimulatorResultStatus, errors: ErrorMessage[]): SimulatorResult {
+function errSimulationResult(status: SimulatorResultStatus, errors: QuintError[]): SimulatorResult {
   return {
     status,
     vars: [],
@@ -111,7 +111,7 @@ export function compileAndRun(
     const evaluationState = ctx.evaluationState
     const res: Either<string, Computable> = contextNameLookup(evaluationState.context, 'q::runResult', 'callable')
     if (res.isLeft()) {
-      const errors = [{ explanation: res.value, locs: [] }] as ErrorMessage[]
+      const errors = [{ code: 'QNT512', message: res.value }] as QuintError[]
       return errSimulationResult('error', errors)
     } else {
       const _ = res.value.eval()
diff --git a/quint/test/errorReporter.test.ts b/quint/test/errorReporter.test.ts
index 8c054cba7..a748e1018 100644
--- a/quint/test/errorReporter.test.ts
+++ b/quint/test/errorReporter.test.ts
@@ -2,7 +2,7 @@ import { describe, it } from 'mocha'
 import { assert } from 'chai'
 import { formatError } from '../src/errorReporter'
 import lineColumn from 'line-column'
-import { ErrorMessage } from '../src'
+import { ErrorMessage } from '../src/ErrorMessage'
 
 describe('errorReporter', () => {
   const text = `module test {
diff --git a/quint/test/flattening/fullFlattener.test.ts b/quint/test/flattening/fullFlattener.test.ts
index 7ed7523bd..7cee6789c 100644
--- a/quint/test/flattening/fullFlattener.test.ts
+++ b/quint/test/flattening/fullFlattener.test.ts
@@ -5,6 +5,7 @@ import { newIdGenerator } from '../../src/idGenerator'
 import { parse, parsePhase3importAndNameResolution } from '../../src/parsing/quintParserFrontend'
 import { SourceLookupPath } from '../../src/parsing/sourceResolver'
 import { analyzeModules } from '../../src/quintAnalyzer'
+import { quintErrorToString } from '../../src'
 
 describe('flattenModules', () => {
   function assertFlattenedModule(text: string) {
@@ -39,7 +40,7 @@ describe('flattenModules', () => {
       })
       .mapLeft(err => {
         it('has no erros', () => {
-          assert.fail(`Expected no error, but got ${err.map(e => e.explanation)}`)
+          assert.fail(`Expected no error, but got ${err.errors.map(quintErrorToString)}`)
         })
       })
   }
diff --git a/quint/test/ir/idRefresher.test.ts b/quint/test/ir/idRefresher.test.ts
index a44acbb72..f1535428d 100644
--- a/quint/test/ir/idRefresher.test.ts
+++ b/quint/test/ir/idRefresher.test.ts
@@ -8,6 +8,7 @@ import { analyzeModules } from '../../src/quintAnalyzer'
 import { collectIds } from '../util'
 import { QuintModule, isDef } from '../../src/ir/quintIr'
 import JSONbig from 'json-bigint'
+import { quintErrorToString } from '../../src'
 
 describe('generateFreshIds', () => {
   // Generate ids starting from 100, so that we can easily distinguish them from
@@ -31,7 +32,9 @@ describe('generateFreshIds', () => {
   const parseResult = parse(idGenerator, 'fake_location', fake_path, quintModules)
   if (parseResult.isLeft()) {
     it('should parse the mocked up module', () => {
-      assert.fail(`Failed to parse mocked up module. Errors: ${parseResult.value.map(e => e.explanation).join('\n')}`)
+      assert.fail(
+        `Failed to parse mocked up module. Errors: ${parseResult.value.errors.map(quintErrorToString).join('\n')}`
+      )
     })
   }
   const { modules, table, sourceMap } = parseResult.unwrap()
diff --git a/quint/test/names/unshadower.test.ts b/quint/test/names/unshadower.test.ts
index 710fdecb1..3e4419748 100644
--- a/quint/test/names/unshadower.test.ts
+++ b/quint/test/names/unshadower.test.ts
@@ -4,7 +4,7 @@ import { newIdGenerator } from '../../src/idGenerator'
 import { SourceLookupPath } from '../../src/parsing/sourceResolver'
 import { parse } from '../../src/parsing/quintParserFrontend'
 import { unshadowNames } from '../../src/names/unshadower'
-import { moduleToString } from '../../src'
+import { moduleToString, quintErrorToString } from '../../src'
 import { dedent } from '../textUtils'
 
 describe('unshadowNames', () => {
@@ -14,7 +14,7 @@ describe('unshadowNames', () => {
 
     const result = parse(idGenerator, 'test_location', fake_path, text)
     if (result.isLeft()) {
-      assert.fail(`Expected no error, but got ${result.value.map(e => e.explanation)}`)
+      assert.fail(`Expected no error, but got ${result.value.errors.map(quintErrorToString)} `)
     }
 
     return result.unwrap()
diff --git a/quint/test/parsing/quintParserFrontend.test.ts b/quint/test/parsing/quintParserFrontend.test.ts
index f604586b8..0a2c09c5d 100644
--- a/quint/test/parsing/quintParserFrontend.test.ts
+++ b/quint/test/parsing/quintParserFrontend.test.ts
@@ -15,6 +15,7 @@ import { right } from '@sweet-monads/either'
 import { newIdGenerator } from '../../src/idGenerator'
 import { collectIds } from '../util'
 import { fileSourceResolver } from '../../src/parsing/sourceResolver'
+import { mkErrorMessage } from '../../src/cliCommands'
 
 // read a Quint file from the test data directory
 function readQuint(name: string): string {
@@ -56,7 +57,7 @@ function parseAndCompare(artifact: string): void {
       err =>
         (outputToCompare = {
           stage: 'parsing',
-          errors: err,
+          errors: err.errors.map(mkErrorMessage(err.sourceMap)),
           warnings: [],
         })
     )
@@ -81,7 +82,7 @@ function parseAndCompare(artifact: string): void {
         err =>
           (outputToCompare = {
             stage: 'parsing',
-            errors: err,
+            errors: err.errors.map(mkErrorMessage(sourceMap)),
             warnings: [],
           })
       )
diff --git a/quint/test/repl.test.ts b/quint/test/repl.test.ts
index 9bef72c16..8b9e3e357 100644
--- a/quint/test/repl.test.ts
+++ b/quint/test/repl.test.ts
@@ -265,7 +265,7 @@ describe('repl ok', () => {
       |[Frame 0]
       |div(2, 0) => none
       |
-      |runtime error: error: Division by zero
+      |runtime error: error: [QNT503] Division by zero
       |div(2, 0)
       |                     ^^^^^
       |
@@ -385,7 +385,7 @@ describe('repl ok', () => {
     )
     const output = dedent(
       `>>> Set(Int)
-      |runtime error: error: Infinite set Int is non-enumerable
+      |runtime error: error: [QNT501] Infinite set Int is non-enumerable
       |Set(Int)
       |^^^^^^^^
       |
diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts
index 1002bac82..259cd8b63 100644
--- a/quint/test/runtime/compile.test.ts
+++ b/quint/test/runtime/compile.test.ts
@@ -20,7 +20,7 @@ import { dedent } from '../textUtils'
 import { newIdGenerator } from '../../src/idGenerator'
 import { Rng, newRng } from '../../src/rng'
 import { SourceLookupPath, stringSourceResolver } from '../../src/parsing/sourceResolver'
-import { analyzeModules, parse, parseExpressionOrDeclaration } from '../../src'
+import { analyzeModules, parse, parseExpressionOrDeclaration, quintErrorToString } from '../../src'
 import { flattenModules } from '../../src/flattening/fullFlattener'
 import { newEvaluationState } from '../../src/runtime/impl/compilerImpl'
 
@@ -34,8 +34,8 @@ function assertResultAsString(input: string, expected: string | undefined) {
   const mockLookupPath = stringSourceResolver(new Map()).lookupPath('/', './mock')
   const context = compileFromCode(idGen, moduleText, '__runtime', mockLookupPath, noExecutionListener, newRng().next)
 
-  assert.isEmpty(context.syntaxErrors, `Syntax errors: ${context.syntaxErrors.map(e => e.explanation).join(', ')}`)
-  assert.isEmpty(context.compileErrors, `Compile errors: ${context.compileErrors.map(e => e.explanation).join(', ')}`)
+  assert.isEmpty(context.syntaxErrors, `Syntax errors: ${context.syntaxErrors.map(quintErrorToString).join(', ')}`)
+  assert.isEmpty(context.compileErrors, `Compile errors: ${context.compileErrors.map(quintErrorToString).join(', ')}`)
 
   assertInputFromContext(context, expected)
 }
@@ -1078,14 +1078,10 @@ describe('incremental compilation', () => {
 
       assert.sameDeepMembers(context.syntaxErrors, [
         {
-          explanation: "[QNT404] Name 'x1' not found",
-          locs: [
-            {
-              source: 'test.qnt',
-              start: { line: 0, col: 9, index: 9 },
-              end: { line: 0, col: 10, index: 10 },
-            },
-          ],
+          code: 'QNT404',
+          message: "Name 'x1' not found",
+          reference: 10n,
+          data: {},
         },
       ])
     })
diff --git a/quint/test/static/callgraph.test.ts b/quint/test/static/callgraph.test.ts
index 0435efb13..9276a03dd 100644
--- a/quint/test/static/callgraph.test.ts
+++ b/quint/test/static/callgraph.test.ts
@@ -9,7 +9,15 @@ import {
   parsePhase3importAndNameResolution,
 } from '../../src/parsing/quintParserFrontend'
 import { SourceLookupPath, fileSourceResolver } from '../../src/parsing/sourceResolver'
-import { LookupTable, QuintDeclaration, QuintExport, QuintImport, QuintInstance, QuintModule } from '../../src'
+import {
+  LookupTable,
+  QuintDeclaration,
+  QuintExport,
+  QuintImport,
+  QuintInstance,
+  QuintModule,
+  quintErrorToString,
+} from '../../src'
 import { CallGraphVisitor, mkCallGraphContext } from '../../src/static/callgraph'
 import { walkModule } from '../../src/ir/IRVisitor'
 
@@ -30,7 +38,7 @@ describe('compute call graph', () => {
       .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data))
 
     if (parseResult.isLeft()) {
-      const msgs = parseResult.value.map(e => e.explanation).join('; ')
+      const msgs = parseResult.value.errors.map(quintErrorToString).join('; ')
       assert.fail(`Failed to parse a mock module: ${msgs}`)
     }
     const { modules, table } = parseResult.unwrap()
diff --git a/quint/testFixture/_0100cyclicDefs.json b/quint/testFixture/_0100cyclicDefs.json
index 4eaebeeab..0d7d791a3 100644
--- a/quint/testFixture/_0100cyclicDefs.json
+++ b/quint/testFixture/_0100cyclicDefs.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":2,"col":2,"index":70},"end":{"line":2,"col":25,"index":93}},{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":3,"col":2,"index":97},"end":{"line":3,"col":25,"index":120}},{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":4,"col":2,"index":124},"end":{"line":4,"col":25,"index":147}}],"explanation":"QNT099: Found cyclic declarations. Use fold and foldl instead of recursion"}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":2,"col":2,"index":70},"end":{"line":2,"col":25,"index":93}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":3,"col":2,"index":97},"end":{"line":3,"col":25,"index":120}}]},{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0100cyclicDefs.qnt","start":{"line":4,"col":2,"index":124},"end":{"line":4,"col":25,"index":147}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_0101noRecursion.json b/quint/testFixture/_0101noRecursion.json
index 69116b772..aa0767347 100644
--- a/quint/testFixture/_0101noRecursion.json
+++ b/quint/testFixture/_0101noRecursion.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"locs":[{"source":"mocked_path/testFixture/_0101noRecursion.qnt","start":{"line":3,"col":2,"index":131},"end":{"line":3,"col":41,"index":170}}],"explanation":"QNT099: Found cyclic declarations. Use fold and foldl instead of recursion"}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT099] Found cyclic declarations. Use fold and foldl instead of recursion","locs":[{"source":"mocked_path/testFixture/_0101noRecursion.qnt","start":{"line":3,"col":2,"index":131},"end":{"line":3,"col":41,"index":170}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1002emptyWithError.json b/quint/testFixture/_1002emptyWithError.json
index 6200352e1..992a9b5db 100644
--- a/quint/testFixture/_1002emptyWithError.json
+++ b/quint/testFixture/_1002emptyWithError.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"extraneous input 'error' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1002emptyWithError.qnt","start":{"line":3,"col":2,"index":74},"end":{"line":3,"col":6,"index":78}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] extraneous input 'error' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1002emptyWithError.qnt","start":{"line":3,"col":2,"index":74},"end":{"line":3,"col":6,"index":78}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1005constRecordsError.json b/quint/testFixture/_1005constRecordsError.json
index ca208ea59..337a2034b 100644
--- a/quint/testFixture/_1005constRecordsError.json
+++ b/quint/testFixture/_1005constRecordsError.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"QNT011: Records in disjoint union have different tag fields: tag and kind","locs":[{"source":"mocked_path/testFixture/_1005constRecordsError.qnt","start":{"line":4,"col":4,"index":127},"end":{"line":5,"col":51,"index":211}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT011] Records in disjoint union have different tag fields: tag and kind","locs":[{"source":"mocked_path/testFixture/_1005constRecordsError.qnt","start":{"line":4,"col":4,"index":127},"end":{"line":5,"col":88,"index":211}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1007unexpectedToken.json b/quint/testFixture/_1007unexpectedToken.json
index ff7cb0d1b..75ad9f208 100644
--- a/quint/testFixture/_1007unexpectedToken.json
+++ b/quint/testFixture/_1007unexpectedToken.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"token recognition error at: '#'","locs":[{"source":"mocked_path/testFixture/_1007unexpectedToken.qnt","start":{"line":2,"col":20,"index":0},"end":{"line":2,"col":20,"index":0}}]},{"explanation":"extraneous input 'name' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1007unexpectedToken.qnt","start":{"line":2,"col":22,"index":77},"end":{"line":2,"col":25,"index":80}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] token recognition error at: '#'","locs":[{"source":"mocked_path/testFixture/_1007unexpectedToken.qnt","start":{"line":2,"col":20,"index":0},"end":{"line":2,"col":20,"index":0}}]},{"explanation":"[QNT000] extraneous input 'name' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1007unexpectedToken.qnt","start":{"line":2,"col":22,"index":77},"end":{"line":2,"col":25,"index":80}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1008unexpectedEq.json b/quint/testFixture/_1008unexpectedEq.json
index 0457f3b89..5687907d2 100644
--- a/quint/testFixture/_1008unexpectedEq.json
+++ b/quint/testFixture/_1008unexpectedEq.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"QNT006: unexpected '=', did you mean '=='?","locs":[{"source":"mocked_path/testFixture/_1008unexpectedEq.qnt","start":{"line":3,"col":0,"index":107},"end":{"line":3,"col":0,"index":107}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT006] unexpected '=', did you mean '=='?","locs":[{"source":"mocked_path/testFixture/_1008unexpectedEq.qnt","start":{"line":3,"col":0,"index":107},"end":{"line":3,"col":0,"index":107}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1009infixFewArgs.json b/quint/testFixture/_1009infixFewArgs.json
index feacab18a..20e8a9dd4 100644
--- a/quint/testFixture/_1009infixFewArgs.json
+++ b/quint/testFixture/_1009infixFewArgs.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"extraneous input 'cardinality' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1009infixFewArgs.qnt","start":{"line":2,"col":17,"index":88},"end":{"line":2,"col":27,"index":98}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] extraneous input 'cardinality' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1009infixFewArgs.qnt","start":{"line":2,"col":17,"index":88},"end":{"line":2,"col":27,"index":98}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1015noToplevelNondet.json b/quint/testFixture/_1015noToplevelNondet.json
index 1f0b437f2..16aa433f7 100644
--- a/quint/testFixture/_1015noToplevelNondet.json
+++ b/quint/testFixture/_1015noToplevelNondet.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input 'nondet' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1015noToplevelNondet.qnt","start":{"line":2,"col":2,"index":101},"end":{"line":2,"col":7,"index":106}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] mismatched input 'nondet' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1015noToplevelNondet.qnt","start":{"line":2,"col":2,"index":101},"end":{"line":2,"col":7,"index":106}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1016nonConstOverride.json b/quint/testFixture/_1016nonConstOverride.json
index d8fc61164..e6d3b580c 100644
--- a/quint/testFixture/_1016nonConstOverride.json
+++ b/quint/testFixture/_1016nonConstOverride.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input 'module' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1016nonConstOverride.qnt","start":{"line":6,"col":2,"index":70},"end":{"line":6,"col":7,"index":75}}]},{"explanation":"mismatched input '=' expecting {'{', '::'}","locs":[{"source":"mocked_path/testFixture/_1016nonConstOverride.qnt","start":{"line":6,"col":12,"index":80},"end":{"line":6,"col":12,"index":80}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] mismatched input 'module' expecting {'}', 'const', 'var', 'assume', 'type', 'val', 'def', 'pure', 'action', 'run', 'temporal', 'import', 'export', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/_1016nonConstOverride.qnt","start":{"line":6,"col":2,"index":70},"end":{"line":6,"col":7,"index":75}}]},{"explanation":"[QNT000] mismatched input '=' expecting {'{', '::'}","locs":[{"source":"mocked_path/testFixture/_1016nonConstOverride.qnt","start":{"line":6,"col":12,"index":80},"end":{"line":6,"col":12,"index":80}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1023importFromUnresolved.json b/quint/testFixture/_1023importFromUnresolved.json
index 56c7123c9..5b8997760 100644
--- a/quint/testFixture/_1023importFromUnresolved.json
+++ b/quint/testFixture/_1023importFromUnresolved.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"import ... from './non-existant-file': could not load","locs":[{"source":"mocked_path/testFixture/_1023importFromUnresolved.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":42,"index":60}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT013] import ... from './non-existant-file': could not load","locs":[{"source":"mocked_path/testFixture/_1023importFromUnresolved.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":42,"index":60}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1024importFromSyntaxError.json b/quint/testFixture/_1024importFromSyntaxError.json
index d89699aae..17376bc1f 100644
--- a/quint/testFixture/_1024importFromSyntaxError.json
+++ b/quint/testFixture/_1024importFromSyntaxError.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input ''' expecting STRING","locs":[{"source":"mocked_path/testFixture/_1024importFromSyntaxError.qnt","start":{"line":1,"col":18,"index":36},"end":{"line":1,"col":18,"index":36}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] mismatched input ''' expecting STRING","locs":[{"source":"mocked_path/testFixture/_1024importFromSyntaxError.qnt","start":{"line":1,"col":18,"index":36},"end":{"line":1,"col":18,"index":36}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1025importeeWithError.json b/quint/testFixture/_1025importeeWithError.json
index 4027490ae..b5fd8d353 100644
--- a/quint/testFixture/_1025importeeWithError.json
+++ b/quint/testFixture/_1025importeeWithError.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"mismatched input '}' expecting {'{', 'nondet', 'val', 'def', 'pure', 'action', 'run', 'temporal', '[', 'all', 'any', 'if', '_', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'Set', 'List', 'Map', 'match', '-', '(', IDENTIFIER}","locs":[{"source":"mocked_path/testFixture/_1025importeeWithError.qnt","start":{"line":3,"col":0,"index":45},"end":{"line":3,"col":0,"index":45}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] mismatched input '}' expecting {'{', 'nondet', 'val', 'def', 'pure', 'action', 'run', 'temporal', '[', 'all', 'any', 'if', '_', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'Set', 'List', 'Map', 'match', '-', '(', IDENTIFIER}","locs":[{"source":"mocked_path/testFixture/_1025importeeWithError.qnt","start":{"line":3,"col":0,"index":45},"end":{"line":3,"col":0,"index":45}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1026importCycleA.json b/quint/testFixture/_1026importCycleA.json
index fceedbf11..fe9ad3304 100644
--- a/quint/testFixture/_1026importCycleA.json
+++ b/quint/testFixture/_1026importCycleA.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"Cyclic imports: 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt'","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt'","locs":[{"source":"mocked_path/testFixture/_1028importCycleC.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1027importCycleB.json b/quint/testFixture/_1027importCycleB.json
index 970dd30a3..02929d6c6 100644
--- a/quint/testFixture/_1027importCycleB.json
+++ b/quint/testFixture/_1027importCycleB.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"Cyclic imports: 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt'","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt'","locs":[{"source":"mocked_path/testFixture/_1026importCycleA.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1028importCycleC.json b/quint/testFixture/_1028importCycleC.json
index a97e476f0..4af7230c9 100644
--- a/quint/testFixture/_1028importCycleC.json
+++ b/quint/testFixture/_1028importCycleC.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"Cyclic imports: 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt'","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT098] Cyclic imports: 'mocked_path/testFixture/_1028importCycleC.qnt' imports 'mocked_path/testFixture/_1026importCycleA.qnt' imports 'mocked_path/testFixture/_1027importCycleB.qnt' imports 'mocked_path/testFixture/_1028importCycleC.qnt'","locs":[{"source":"mocked_path/testFixture/_1027importCycleB.qnt","start":{"line":1,"col":2,"index":20},"end":{"line":1,"col":45,"index":63}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/_1029spreadError.json b/quint/testFixture/_1029spreadError.json
index 99f822de1..d7e62adc9 100644
--- a/quint/testFixture/_1029spreadError.json
+++ b/quint/testFixture/_1029spreadError.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"QNT012: ... may be used once in { ...record, <fields> }","locs":[{"source":"mocked_path/testFixture/_1029spreadError.qnt","start":{"line":3,"col":17,"index":121},"end":{"line":3,"col":34,"index":138}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT012] ... may be used once in { ...record, <fields> ","locs":[{"source":"mocked_path/testFixture/_1029spreadError.qnt","start":{"line":3,"col":17,"index":121},"end":{"line":3,"col":34,"index":138}}]}]}
\ No newline at end of file
diff --git a/quint/testFixture/modulesAndJunk.json b/quint/testFixture/modulesAndJunk.json
index 86c4c5368..ba0ed1bc2 100644
--- a/quint/testFixture/modulesAndJunk.json
+++ b/quint/testFixture/modulesAndJunk.json
@@ -1 +1 @@
-{"stage":"parsing","warnings":[],"errors":[{"explanation":"extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/modulesAndJunk.qnt","start":{"line":8,"col":0,"index":75},"end":{"line":8,"col":2,"index":77}}]}]}
\ No newline at end of file
+{"stage":"parsing","warnings":[],"errors":[{"explanation":"[QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}","locs":[{"source":"mocked_path/testFixture/modulesAndJunk.qnt","start":{"line":8,"col":0,"index":75},"end":{"line":8,"col":2,"index":77}}]}]}
\ No newline at end of file
diff --git a/tutorials/repl/replTestOut.txt b/tutorials/repl/replTestOut.txt
index 56cc7869b..03709b620 100644
--- a/tutorials/repl/replTestOut.txt
+++ b/tutorials/repl/replTestOut.txt
@@ -6,7 +6,7 @@ false
 true
 -40
 104
-runtime error: error: Variable temperature is not set
+runtime error: error: [QNT502] Variable temperature is not set
     var temperature: int
     ^^^^^^^^^^^^^^^^^^^^
 
diff --git a/vscode/quint-vscode/server/src/parsing.ts b/vscode/quint-vscode/server/src/parsing.ts
index 97af22e3c..f8296e403 100644
--- a/vscode/quint-vscode/server/src/parsing.ts
+++ b/vscode/quint-vscode/server/src/parsing.ts
@@ -1,7 +1,6 @@
 import {
   IdGenerator,
   ParserPhase3,
-  QuintError,
   fileSourceResolver,
   parsePhase1fromText,
   parsePhase2sourceResolution,
@@ -10,7 +9,7 @@ import {
 } from '@informalsystems/quint'
 import { basename, dirname } from 'path'
 import { URI } from 'vscode-uri'
-import { assembleDiagnostic } from './reporting'
+import { diagnosticsFromErrors } from './reporting'
 import { TextDocument } from 'vscode-languageserver-textdocument'
 
 export async function parseDocument(idGenerator: IdGenerator, textDocument: TextDocument): Promise<ParserPhase3> {
@@ -32,13 +31,7 @@ export async function parseDocument(idGenerator: IdGenerator, textDocument: Text
       })
       .chain(phase2Data => parsePhase3importAndNameResolution(phase2Data))
       .chain(phase3Data => parsePhase4toposort(phase3Data))
-      .mapLeft(messages =>
-        messages.flatMap(msg => {
-          // TODO: Parse errors should be QuintErrors
-          const error: QuintError = { code: 'QNT000', message: msg.explanation, reference: 0n, data: {} }
-          return msg.locs.map(loc => assembleDiagnostic(error, loc))
-        })
-      )
+      .mapLeft(({ errors, sourceMap }) => diagnosticsFromErrors(errors, sourceMap))
 
     if (result.isRight()) {
       return new Promise((resolve, _reject) => resolve(result.value))
diff --git a/vscode/quint-vscode/server/src/reporting.ts b/vscode/quint-vscode/server/src/reporting.ts
index 24ced46da..c855f89e4 100644
--- a/vscode/quint-vscode/server/src/reporting.ts
+++ b/vscode/quint-vscode/server/src/reporting.ts
@@ -12,7 +12,7 @@
  * @module
  */
 
-import { Loc, QuintError, QuintModule, findExpressionWithId, findTypeWithId } from '@informalsystems/quint'
+import { Loc, QuintError, QuintModule, SourceMap, findExpressionWithId, findTypeWithId } from '@informalsystems/quint'
 import { Diagnostic, DiagnosticSeverity, Position, Range } from 'vscode-languageserver'
 import { compact } from 'lodash'
 
@@ -25,11 +25,11 @@ import { compact } from 'lodash'
  *
  * @returns a list of diagnostics with the proper error messages and locations
  */
-export function diagnosticsFromErrors(errors: [bigint, QuintError][], sourceMap: Map<bigint, Loc>): Diagnostic[] {
-  const diagnostics = errors.map(([id, error]) => {
-    const loc = sourceMap.get(id)!
+export function diagnosticsFromErrors(errors: QuintError[], sourceMap: SourceMap): Diagnostic[] {
+  const diagnostics = errors.map(error => {
+    const loc = sourceMap.get(error.reference!)!
     if (!loc) {
-      console.log(`loc for ${id} not found in source map`)
+      console.log(`loc for ${error} not found in source map`)
     } else {
       return assembleDiagnostic(error, loc)
     }
diff --git a/vscode/quint-vscode/server/test/reporting.test.ts b/vscode/quint-vscode/server/test/reporting.test.ts
index 98f93dfb4..d0ec38483 100644
--- a/vscode/quint-vscode/server/test/reporting.test.ts
+++ b/vscode/quint-vscode/server/test/reporting.test.ts
@@ -12,7 +12,7 @@ import { Position } from 'vscode-languageserver'
 import { parseOrThrow } from './util'
 
 describe('diagnosticsFromErrorMap', () => {
-  const errors: [bigint, QuintError][] = [[1n, { code: 'QNT000', message: 'Message', reference: 0n, data: {} }]]
+  const errors: QuintError[] = [{ code: 'QNT000', message: 'Message', reference: 1n, data: {} }]
 
   const sourceMap = new Map<bigint, Loc>([
     [1n, { start: { col: 1, index: 1, line: 1 }, end: { col: 1, index: 1, line: 1 }, source: 'mocked_path' }],