diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index a581bffe6..1742eebab 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -145,13 +145,8 @@ interface TestedStage extends LoadedStage {
   ignored: string[]
 }
 
-interface SimulatorStage extends LoadedStage {
-  status: 'ok' | 'violation' | 'failure'
-  trace?: QuintEx[]
-}
-
-interface VerifiedStage extends LoadedStage {
-  status: 'ok' | 'violation' | 'failure'
+// Data resulting from stages that can produce a trace
+interface TracingStage extends LoadedStage {
   trace?: QuintEx[]
 }
 
@@ -301,10 +296,9 @@ export async function runRepl(_argv: any) {
  * @param typedStage the procedure stage produced by `typecheck`
  */
 export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<TestedStage>> {
-  // TODO: Logic should be consistent with runSimulator?
-  const verbosityLevel = !prev.args.out ? prev.args.verbosity : 0
-  const mainName = guessMainModule(prev)
   const testing = { ...prev, stage: 'testing' as stage }
+  const verbosityLevel = deriveVerbosity(prev.args)
+  const mainName = guessMainModule(prev)
 
   const rngOrError = mkRng(prev.args.seed)
   if (rngOrError.isLeft()) {
@@ -519,10 +513,10 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra
  *
  * @param prev the procedure stage produced by `typecheck`
  */
-export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<SimulatorStage>> {
-  const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0
-  const mainName = guessMainModule(prev)
+export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
   const simulator = { ...prev, stage: 'running' as stage }
+  const verbosityLevel = deriveVerbosity(prev.args)
+  const mainName = guessMainModule(prev)
 
   const rngOrError = mkRng(prev.args.seed)
   if (rngOrError.isLeft()) {
@@ -553,53 +547,60 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   const mainEnd = prev.sourceMap.get(mainId)!.end!.index
   const result = compileAndRun(newIdGenerator(), mainText, mainStart, mainEnd, mainName, mainPath, options)
 
-  if (result.status !== 'error') {
-    if (verbosity.hasResults(verbosityLevel)) {
-      const elapsedMs = Date.now() - startMs
+  const elapsedMs = Date.now() - startMs
+
+  switch (result.outcome.status) {
+    case 'error':
+      return cliErr('Runtime error', {
+        ...simulator,
+        status: result.outcome.status,
+        trace: result.states,
+        errors: result.outcome.errors.map(mkErrorMessage(prev.sourceMap)),
+      })
+
+    case 'ok':
       maybePrintCounterExample(verbosityLevel, result.states, result.frames)
-      if (result.status === 'ok') {
+      if (verbosity.hasResults(verbosityLevel)) {
         console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
         console.log(chalk.gray(`Use --seed=0x${result.seed.toString(16)} to reproduce.`))
         if (verbosity.hasHints(options.verbosity)) {
           console.log(chalk.gray('You may increase --max-samples and --max-steps.'))
           console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
         }
-      } else {
-        console.log(chalk.red(`[${result.status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
+      }
+      return right({
+        ...simulator,
+        status: result.outcome.status,
+        trace: result.states,
+      })
+
+    case 'violation':
+      maybePrintCounterExample(verbosityLevel, result.states, result.frames)
+      if (verbosity.hasResults(verbosityLevel)) {
+        console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
         console.log(chalk.gray(`Use --seed=0x${result.seed.toString(16)} to reproduce.`))
 
         if (verbosity.hasHints(options.verbosity)) {
           console.log(chalk.gray('Use --verbosity=3 to show executions.'))
         }
       }
-    }
 
-    if (prev.args.outItf) {
-      const trace = toItf(result.vars, result.states)
-      if (trace.isRight()) {
-        const jsonObj = addItfHeader(prev.args.input, result.status, trace.value)
-        writeToJson(prev.args.outItf, jsonObj)
-      } else {
-        const newStage = { ...simulator, errors: result.errors.map(mkErrorMessage(prev.sourceMap)) }
-        return cliErr(`ITF conversion failed: ${trace.value}`, newStage)
+      if (prev.args.outItf) {
+        const trace = toItf(result.vars, result.states)
+        if (trace.isRight()) {
+          const jsonObj = addItfHeader(prev.args.input, result.outcome.status, trace.value)
+          writeToJson(prev.args.outItf, jsonObj)
+        } else {
+          return cliErr(`ITF conversion failed: ${trace.value}`, { ...simulator, errors: [] })
+        }
       }
-    }
-  }
 
-  if (result.status === 'ok') {
-    return right({
-      ...simulator,
-      status: result.status,
-      trace: result.states,
-    })
-  } else {
-    const msg = result.status === 'violation' ? 'Invariant violated' : 'Runtime error'
-    return cliErr(msg, {
-      ...simulator,
-      status: result.status,
-      trace: result.states,
-      errors: result.errors.map(mkErrorMessage(prev.sourceMap)),
-    })
+      return cliErr('Invariant violated', {
+        ...simulator,
+        status: result.outcome.status,
+        trace: result.states,
+        errors: [],
+      })
   }
 }
 
@@ -608,9 +609,11 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
  *
  * @param prev the procedure stage produced by `typecheck`
  */
-export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<VerifiedStage>> {
+export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
   const verifying = { ...prev, stage: 'verifying' as stage }
   const args = verifying.args
+  const verbosityLevel = deriveVerbosity(args)
+
   let loadedConfig: any = {}
   try {
     if (args.apalacheConfig) {
@@ -696,7 +699,6 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
 
   const startMs = Date.now()
 
-  const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0
   return verify(config, verbosityLevel).then(res => {
     const elapsedMs = Date.now() - startMs
     return res
@@ -708,7 +710,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
             console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
           }
         }
-        return { ...verifying, status: 'ok', errors: [] } as VerifiedStage
+        return { ...verifying, status: 'ok', errors: [] } as TracingStage
       })
       .mapLeft(err => {
         const trace: QuintEx[] | undefined = err.traces ? ofItf(err.traces[0]) : undefined
@@ -881,3 +883,8 @@ function isMatchingTest(match: string | undefined, name: string) {
     return name.endsWith('Test')
   }
 }
+
+// Derive the verbosity for simulation and verification routines
+function deriveVerbosity(args: { out: string | undefined; outItf: string | undefined; verbosity: number }): number {
+  return !args.out && !args.outItf ? args.verbosity : 0
+}
diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts
index a2061b9bc..49ab3374e 100644
--- a/quint/src/simulation.ts
+++ b/quint/src/simulation.ts
@@ -20,6 +20,7 @@ import { SourceLookupPath } from './parsing/sourceResolver'
 import { QuintError } from './quintError'
 import { mkErrorMessage } from './cliCommands'
 import { createFinders, formatError } from './errorReporter'
+import assert from 'assert'
 
 /**
  * Various settings that have to be passed to the simulator to run.
@@ -34,27 +35,30 @@ export interface SimulatorOptions {
   verbosity: number
 }
 
-export type SimulatorResultStatus = 'ok' | 'violation' | 'failure' | 'error'
+/** The outcome of a simulation
+ */
+export type Outcome =
+  | { status: 'ok' } /** Simulation succeeded */
+  | { status: 'violation' } /** Simulation found an invariant violation */
+  | { status: 'error'; errors: QuintError[] } /** An error occurred during simulation  */
 
 /**
  * A result returned by the simulator.
  */
 export interface SimulatorResult {
-  status: SimulatorResultStatus
+  outcome: Outcome
   vars: string[]
   states: QuintEx[]
   frames: ExecutionFrame[]
-  errors: QuintError[]
   seed: bigint
 }
 
-function errSimulationResult(status: SimulatorResultStatus, errors: QuintError[]): SimulatorResult {
+function errSimulationResult(errors: QuintError[]): SimulatorResult {
   return {
-    status,
+    outcome: { status: 'error', errors },
     vars: [],
     states: [],
     frames: [],
-    errors: errors,
     seed: 0n,
   }
 }
@@ -105,65 +109,73 @@ export function compileAndRun(
   const recorder = newTraceRecorder(options.verbosity, options.rng)
   const ctx = compileFromCode(idGen, codeWithExtraDefs, mainName, mainPath, recorder, options.rng.next)
 
-  if (ctx.compileErrors.length > 0 || ctx.syntaxErrors.length > 0 || ctx.analysisErrors.length > 0) {
-    const errors = ctx.syntaxErrors.concat(ctx.analysisErrors).concat(ctx.compileErrors)
-    return errSimulationResult('error', errors)
-  } else {
-    // evaluate q::runResult, which triggers the simulator
-    const evaluationState = ctx.evaluationState
-    const res: Either<string, Computable> = contextNameLookup(evaluationState.context, 'q::runResult', 'callable')
-    if (res.isLeft()) {
-      const errors = [{ code: 'QNT512', message: res.value }] as QuintError[]
-      return errSimulationResult('error', errors)
-    } else {
-      const _ = res.value.eval()
-    }
-
-    const topFrame = recorder.getBestTrace()
-    let status: SimulatorResultStatus = 'failure'
-    if (topFrame.result.isJust()) {
-      const ex = topFrame.result.unwrap().toQuintEx(idGen)
-      if (ex.kind === 'bool') {
-        status = ex.value ? 'ok' : 'violation'
-      }
-    } else {
-      // This should not happen. But if it does, give a debugging hint.
-      console.error('No trace recorded')
-    }
+  const compilationErrors = ctx.syntaxErrors.concat(ctx.analysisErrors).concat(ctx.compileErrors)
+  if (compilationErrors.length > 0) {
+    return errSimulationResult(compilationErrors)
+  }
 
-    let errors = ctx.getRuntimeErrors()
-    if (errors.length > 0) {
-      // FIXME(#1052) we shouldn't need to do this if the error id was not some non-sense generated in `compileFromCode`
-      // The evaluated code source is not included in the context, so we crete a version with it for the error reporter
-      const code = new Map([...ctx.compilationState.sourceCode.entries(), [mainPath.normalizedPath, codeWithExtraDefs]])
-      const finders = createFinders(code)
-
-      errors = errors.map(error => ({
-        code: error.code,
-        // Include the location information (locs) in the error message - this
-        // is the hacky part, as it should only be included at the CLI level
-        message: formatError(code, finders, {
-          // This will create the `locs` attribute and an explanation
-          ...mkErrorMessage(ctx.compilationState.sourceMap)(error),
-          // We override the explanation to keep the original one to avoid
-          // duplication, since `mkErrorMessage` will be called again at the CLI
-          // level. `locs` won't be touched then because this error doesn't
-          // include a `reference` field
-          explanation: error.message,
-        }),
-      }))
-
-      // This should be kept after the hack is removed
-      status = 'error'
-    }
+  // evaluate q::runResult, which triggers the simulator
+  const evaluationState = ctx.evaluationState
+  const res: Either<string, Computable> = contextNameLookup(evaluationState.context, 'q::runResult', 'callable')
+  if (res.isLeft()) {
+    const errors = [{ code: 'QNT512', message: res.value }] as QuintError[]
+    return errSimulationResult(errors)
+  } else {
+    res.value.eval()
+  }
 
+  const topFrame: ExecutionFrame = recorder.getBestTrace()
+
+  // Validate required outcome of correct simulation
+  const maybeEvalResult = topFrame.result
+  assert(maybeEvalResult.isJust(), 'invalid simulation failed to produce a result')
+  const quintExResult = maybeEvalResult.value.toQuintEx(idGen)
+  assert(quintExResult.kind === 'bool', 'invalid simulation produced non-boolean value ')
+  const simulationSucceeded = quintExResult.value
+
+  const vars = evaluationState.vars.map(v => v.name)
+  const states = topFrame.args.map(e => e.toQuintEx(idGen))
+  const frames = topFrame.subframes
+  const seed = recorder.getBestTraceSeed()
+
+  const runtimeErrors = ctx.getRuntimeErrors()
+  if (runtimeErrors.length > 0) {
+    // FIXME(#1052) we shouldn't need to do this if the error id was not some non-sense generated in `compileFromCode`
+    // The evaluated code source is not included in the context, so we crete a version with it for the error reporter
+    const code = new Map([...ctx.compilationState.sourceCode.entries(), [mainPath.normalizedPath, codeWithExtraDefs]])
+    const finders = createFinders(code)
+
+    const locatedErrors = runtimeErrors.map(error => ({
+      code: error.code,
+      // Include the location information (locs) in the error message - this
+      // is the hacky part, as it should only be included at the CLI level
+      message: formatError(code, finders, {
+        // This will create the `locs` attribute and an explanation
+        ...mkErrorMessage(ctx.compilationState.sourceMap)(error),
+        // We override the explanation to keep the original one to avoid
+        // duplication, since `mkErrorMessage` will be called again at the CLI
+        // level. `locs` won't be touched then because this error doesn't
+        // include a `reference` field
+        explanation: error.message,
+      }),
+    }))
+
+    // This should be kept after the hack is removed
     return {
-      status: status,
-      vars: evaluationState.vars.map(v => v.name),
-      states: topFrame.args.map(e => e.toQuintEx(idGen)),
-      frames: topFrame.subframes,
-      errors: errors,
-      seed: recorder.getBestTraceSeed(),
+      vars,
+      states,
+      frames,
+      seed,
+      outcome: { status: 'error', errors: locatedErrors },
     }
   }
+
+  const status = simulationSucceeded ? 'ok' : 'violation'
+  return {
+    vars,
+    states,
+    frames,
+    seed,
+    outcome: { status },
+  }
 }