diff --git a/CHANGELOG.md b/CHANGELOG.md
index f73892a6..289fb73e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,10 +8,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Added
-- Add Callgraph: PR [#185](https://github.com/nowarp/misti/pull/185)
+- `ExitCodeUsage` detector: PR [#207](https://github.com/nowarp/misti/pull/207)
 - `EtaLikeSimplifications` detector: PR [#198](https://github.com/nowarp/misti/pull/198)
 - `ShortCircuitCondition` detector: PR [#202](https://github.com/nowarp/misti/pull/202)
-### Changed 
+- Add Callgraph: PR [#185](https://github.com/nowarp/misti/pull/185)
+
+### Changed
 - `SuspiciousMessageMode` detector now suggests using SendDefaultMode instead of 0 for mode: PR [#199](https://github.com/nowarp/misti/pull/199/)
 
 ## [0.5.0] - 2024-10-31
diff --git a/cspell.json b/cspell.json
index 78552d0c..272b05d6 100644
--- a/cspell.json
+++ b/cspell.json
@@ -102,7 +102,9 @@
     "consteval",
     "Georgiy",
     "Komarov",
-    "callgraph"
+    "callgraph",
+    "nums",
+    "extremal"
   ],
   "flagWords": [],
   "ignorePaths": [
diff --git a/src/cli/driver.ts b/src/cli/driver.ts
index b5b69b68..5efeb0b9 100644
--- a/src/cli/driver.ts
+++ b/src/cli/driver.ts
@@ -618,7 +618,9 @@ export class Driver {
         );
         return [];
       }
-      this.ctx.logger.debug(`${cu.projectName}: Running ${detector.id}`);
+      this.ctx.logger.debug(
+        `${cu.projectName}: Running ${detector.id} for ${cu.projectName}`,
+      );
       try {
         const warnings = await Promise.race([
           detector.check(cu),
@@ -630,7 +632,21 @@ export class Driver {
         ]);
         this.ctx.logger.debug(`${cu.projectName}: Finished ${detector.id}`);
         return warnings;
-      } catch (error) {
+      } catch (err) {
+        let error: string = "";
+        if (err instanceof Error) {
+          const result = [] as string[];
+          result.push(err.message);
+          if (
+            err.stack !== undefined &&
+            this.ctx.config.verbosity === "debug"
+          ) {
+            result.push(err.stack);
+          }
+          error = result.join("\n");
+        } else {
+          error = `${err}`;
+        }
         this.ctx.logger.error(
           `${cu.projectName}: Error in ${detector.id}: ${error}`,
         );
diff --git a/src/detectors/builtin/exitCodeUsage.ts b/src/detectors/builtin/exitCodeUsage.ts
new file mode 100644
index 00000000..890e11fe
--- /dev/null
+++ b/src/detectors/builtin/exitCodeUsage.ts
@@ -0,0 +1,301 @@
+import { InternalException } from "../../internals/exceptions";
+import { CFG, BasicBlock, CompilationUnit } from "../../internals/ir";
+import {
+  IntervalJoinSemiLattice,
+  JoinSemilattice,
+  WideningLattice,
+} from "../../internals/lattice";
+import { Interval, Num } from "../../internals/numbers";
+import { WideningWorklistSolver } from "../../internals/solver";
+import { findInExpressions } from "../../internals/tact/iterators";
+import { Transfer } from "../../internals/transfer";
+import { MistiTactWarning, Severity } from "../../internals/warnings";
+import { DataflowDetector } from "../detector";
+import {
+  AstStatement,
+  AstId,
+  idText,
+  AstExpression,
+  AstStatementAssign,
+  AstStatementLet,
+  AstNumber,
+} from "@tact-lang/compiler/dist/grammar/ast";
+
+type Variable = string & { readonly __brand: unique symbol };
+
+type VariableState = Map<Variable, Interval>;
+
+class ExitCodeLattice
+  implements JoinSemilattice<VariableState>, WideningLattice<VariableState>
+{
+  private intervalLattice;
+  private widenCount = new Map<Variable, number>();
+  private readonly WIDENING_THRESHOLD = 3;
+
+  constructor() {
+    this.intervalLattice = new IntervalJoinSemiLattice();
+  }
+
+  bottom(): VariableState {
+    return new Map();
+  }
+
+  join(a: VariableState, b: VariableState): VariableState {
+    const result = new Map<Variable, Interval>();
+    const variables = new Set([...a.keys(), ...b.keys()]);
+    for (const variable of variables) {
+      const intervalA = a.get(variable) || this.intervalLattice.bottom();
+      const intervalB = b.get(variable) || this.intervalLattice.bottom();
+      const joinedInterval = this.intervalLattice.join(intervalA, intervalB);
+      result.set(variable, joinedInterval);
+    }
+    return result;
+  }
+
+  leq(a: VariableState, b: VariableState): boolean {
+    for (const [variable, intervalA] of a.entries()) {
+      const intervalB = b.get(variable) || this.intervalLattice.bottom();
+      if (!this.intervalLattice.leq(intervalA, intervalB)) {
+        return false;
+      }
+    }
+    return true;
+  }
+
+  widen(oldState: VariableState, newState: VariableState): VariableState {
+    const result = new Map<Variable, Interval>();
+    const variables = new Set([...oldState.keys(), ...newState.keys()]);
+
+    for (const variable of variables) {
+      // Track widening iterations per variable
+      const count = (this.widenCount.get(variable) || 0) + 1;
+      this.widenCount.set(variable, count);
+      const intervalOld =
+        oldState.get(variable) || this.intervalLattice.bottom();
+      const intervalNew =
+        newState.get(variable) || this.intervalLattice.bottom();
+
+      // If we've widened too many times, jump straight to ±∞
+      let widenedInterval: Interval;
+      if (count > this.WIDENING_THRESHOLD) {
+        widenedInterval = IntervalJoinSemiLattice.topValue;
+      } else {
+        widenedInterval = this.intervalLattice.widen(intervalOld, intervalNew);
+      }
+
+      result.set(variable, widenedInterval);
+    }
+    return result;
+  }
+}
+
+class ExitCodeTransfer implements Transfer<VariableState> {
+  transfer(
+    inState: VariableState,
+    _bb: BasicBlock,
+    stmt: AstStatement,
+  ): VariableState {
+    const outState = new Map(inState);
+
+    if (stmt.kind === "statement_assign") {
+      const assignStmt = stmt as AstStatementAssign;
+      const varName = this.extractVariableName(assignStmt.path);
+      if (varName) {
+        const exprInterval = this.evaluateExpression(
+          assignStmt.expression,
+          inState,
+        );
+        outState.set(varName as Variable, exprInterval);
+      }
+    } else if (stmt.kind === "statement_let") {
+      const letStmt = stmt as AstStatementLet;
+      const varName = idText(letStmt.name);
+      const exprInterval = this.evaluateExpression(letStmt.expression, inState);
+      outState.set(varName as Variable, exprInterval);
+    }
+
+    return outState;
+  }
+
+  private extractVariableName(expr: AstExpression): string | null {
+    return expr.kind === "id" ? idText(expr) : null;
+  }
+
+  private evaluateExpression(
+    expr: AstExpression,
+    state: VariableState,
+  ): Interval {
+    if (expr.kind === "number") {
+      const exprNum = expr as AstNumber;
+      const value = BigInt(exprNum.value);
+      return Interval.fromNum(value);
+    } else if (expr.kind === "id") {
+      const varName = idText(expr) as Variable;
+      return state.get(varName) || IntervalJoinSemiLattice.topValue;
+    } else if (expr.kind === "op_binary") {
+      const leftInterval = this.evaluateExpression(expr.left, state);
+      const rightInterval = this.evaluateExpression(expr.right, state);
+      switch (expr.op) {
+        case "+":
+          return leftInterval.plus(rightInterval);
+        case "-":
+          return leftInterval.minus(rightInterval);
+        case "*":
+          return leftInterval.times(rightInterval);
+        case "/":
+          return leftInterval.div(rightInterval);
+        default:
+          return IntervalJoinSemiLattice.topValue;
+      }
+    }
+    return IntervalJoinSemiLattice.topValue;
+  }
+}
+
+/**
+ * A detector that identifies improper use of exit codes outside the developer-allowed range.
+ *
+ * ## Why is it bad?
+ * In the TON blockchain, exit codes are divided into specific ranges: 0 to 127
+ * are reserved for the TVM or FunC, and 128 to 255 are reserved for Tact. This
+ * structure leaves the range from 256 to 65535 for developers to define custom
+ * exit codes.
+ *
+ * When exit codes are defined outside this allowed range, it may lead to
+ * conflicts with existing reserved codes, causing unintended behavior or
+ * errors in the contract.
+ *
+ * ## Example
+ * ```tact
+ * contract Foo {
+ *     receive("foobar") {
+ *         // Bad: exit code defined in the reserved range for Tact
+ *         let code: Int = 128;
+ *         nativeThrowUnless(code, sender() == self.owner);
+ *     }
+ * }
+ * ```
+ *
+ * Use instead:
+ * ```tact
+ * contract Foo {
+ *     receive("foobar") {
+ *         // OK: using exit code from the allowed range
+ *         let code: Int = 256;
+ *         nativeThrowUnless(code, sender() == self.owner);
+ *     }
+ * }
+ * ```
+ *
+ * ## Resources
+ * 1. [Exit Codes | Tact Docs](https://docs.tact-lang.org/book/exit-codes)
+ */
+export class ExitCodeUsage extends DataflowDetector {
+  severity = Severity.HIGH;
+
+  async check(cu: CompilationUnit): Promise<MistiTactWarning[]> {
+    const warnings: MistiTactWarning[] = [];
+
+    cu.forEachCFG(
+      (cfg: CFG) => {
+        const node = cu.ast.getFunction(cfg.id);
+        if (node === undefined) {
+          return;
+        }
+        const lattice = new ExitCodeLattice();
+        const transfer = new ExitCodeTransfer();
+        const solver = new WideningWorklistSolver<VariableState>(
+          cu,
+          cfg,
+          transfer,
+          lattice,
+          "forward",
+          5,
+        );
+        const results = solver.solve();
+        for (const bb of cfg.nodes) {
+          const state = results.getState(bb.idx);
+          if (state) {
+            this.checkStateForWarnings(cu, state, bb, warnings);
+          }
+        }
+      },
+      { includeStdlib: false },
+    );
+    return warnings;
+  }
+
+  private checkStateForWarnings(
+    cu: CompilationUnit,
+    state: VariableState,
+    bb: BasicBlock,
+    warnings: MistiTactWarning[],
+  ): void {
+    const stmt = cu.ast.getStatement(bb.stmtID);
+    if (!stmt) {
+      throw InternalException.make(`Cannot find a statement for BB #${bb.idx}`);
+    }
+    // TODO: Handle direct cases e.g. throw(128)
+    const exitVariable = this.findExitVariable(stmt);
+    if (exitVariable === null) {
+      return;
+    }
+    const exitVariableName = idText(exitVariable);
+    for (const [varName, interval] of state.entries()) {
+      if (
+        exitVariableName === varName &&
+        this.isOutsideAllowedRange(interval)
+      ) {
+        warnings.push(
+          this.makeWarning(
+            `Exit code variable "${varName}" has value outside allowed range`,
+            exitVariable.loc,
+            {
+              extraDescription: `Exit codes 0-255 are reserved. Variable value: ${interval.toString()}`,
+              suggestion: "Use a value between 256 and 65535",
+            },
+          ),
+        );
+      }
+    }
+  }
+
+  private isOutsideAllowedRange(interval: Interval): boolean {
+    const lowerBound = interval.low;
+    const upperBound = interval.high;
+
+    // Developer-allowed range is 256 to 65535
+    const belowMin = Num.compare(upperBound, Num.int(256n)) < 0;
+    const aboveMax = Num.compare(lowerBound, Num.int(65535n)) > 0;
+
+    return belowMin || aboveMax;
+  }
+
+  /**
+   * Finds a local variable used as an exit code.
+   */
+  private findExitVariable(stmt: AstStatement): AstId | null {
+    let result: AstId | null = null;
+    // The first argument of these functions is an exit code:
+    // https://docs.tact-lang.org/ref/core-debug/#throw
+    const throwFunctions = new Set([
+      "throw",
+      "nativeThrow",
+      "nativeThrowIf",
+      "nativeThrowUnless",
+    ]);
+    findInExpressions(stmt, (expr) => {
+      if (
+        expr.kind === "static_call" &&
+        expr.args.length > 0 &&
+        throwFunctions.has(idText(expr.function)) &&
+        expr.args[0].kind === "id"
+      ) {
+        result = expr.args[0];
+        return true;
+      }
+      return false;
+    });
+    return result;
+  }
+}
diff --git a/src/detectors/detector.ts b/src/detectors/detector.ts
index eb720dc5..006c0ec3 100644
--- a/src/detectors/detector.ts
+++ b/src/detectors/detector.ts
@@ -392,6 +392,13 @@ export const BuiltInDetectors: Record<string, DetectorEntry> = {
       ),
     enabledByDefault: true,
   },
+  ExitCodeUsage: {
+    loader: (ctx: MistiContext) =>
+      import("./builtin/exitCodeUsage").then(
+        (module) => new module.ExitCodeUsage(ctx),
+      ),
+    enabledByDefault: true,
+  },
 };
 
 /**
diff --git a/src/index.ts b/src/index.ts
index 9e861ab0..a900c54c 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -7,6 +7,7 @@ export * from "./internals/transfer";
 export * from "./internals/tact";
 export * from "./internals/logger";
 export * from "./internals/lattice";
+export * from "./internals/numbers";
 export * from "./internals/exceptions";
 export * from "./internals/config";
 export * from "./internals/context";
diff --git a/src/internals/context.ts b/src/internals/context.ts
index 530df2b2..108e72d9 100644
--- a/src/internals/context.ts
+++ b/src/internals/context.ts
@@ -8,8 +8,8 @@ import { execSync } from "child_process";
  * Represents the context for a Misti run.
  */
 export class MistiContext {
-  logger: Logger;
-  config: MistiConfig;
+  public logger: Logger;
+  public config: MistiConfig;
 
   /**
    * Indicates whether a Souffle binary is available.
diff --git a/src/internals/lattice.ts b/src/internals/lattice/common.ts
similarity index 85%
rename from src/internals/lattice.ts
rename to src/internals/lattice/common.ts
index 21d402f1..e610da0d 100644
--- a/src/internals/lattice.ts
+++ b/src/internals/lattice/common.ts
@@ -1,8 +1,9 @@
 /**
  * Interface for a join semilattice that introduces the join operation.
+ *
  * @template T The type of elements in the semilattice.
  */
-export interface JoinSemilattice<T> {
+export interface JoinSemilattice<T> extends Semilattice<T> {
   /**
    * Represents the bottom element of the lattice.
    * @returns The bottom element.
@@ -30,7 +31,7 @@ export interface JoinSemilattice<T> {
  * Interface for a meet semilattice that introduces the meet operation.
  * @template T The type of elements in the semilattice.
  */
-export interface MeetSemilattice<T> {
+export interface MeetSemilattice<T> extends Semilattice<T> {
   /**
    * Represents the top element of the lattice.
    * @returns The top element.
@@ -54,13 +55,19 @@ export interface MeetSemilattice<T> {
   leq(a: T, b: T): boolean;
 }
 
-/**
- * Union type representing either a join or meet semilattice.
- */
-export type Semilattice<T> = JoinSemilattice<T> | MeetSemilattice<T>;
+export interface Semilattice<T> {
+  /**
+   * Determines if one element in the semilattice is less than or equal to another element.
+   * @param a The element to compare.
+   * @param b The element to compare against.
+   * @returns `true` if `a` is less than or equal to `b`, otherwise `false`.
+   */
+  leq(a: T, b: T): boolean;
+}
 
 /**
  * Implementation of a join semilattice for sets.
+ *
  * @template T The type of elements in the sets.
  */
 export class SetJoinSemilattice<T> implements JoinSemilattice<Set<T>> {
@@ -88,6 +95,7 @@ export class SetJoinSemilattice<T> implements JoinSemilattice<Set<T>> {
 
 /**
  * Implementation of a meet semilattice for sets.
+ *
  * @template T The type of elements in the sets.
  */
 export class SetMeetSemilattice<T> implements MeetSemilattice<Set<T>> {
diff --git a/src/internals/lattice/index.ts b/src/internals/lattice/index.ts
new file mode 100644
index 00000000..dcb668d7
--- /dev/null
+++ b/src/internals/lattice/index.ts
@@ -0,0 +1,3 @@
+export * from "./common";
+export * from "./interval";
+export * from "./widening";
diff --git a/src/internals/lattice/interval.ts b/src/internals/lattice/interval.ts
new file mode 100644
index 00000000..7ea160ec
--- /dev/null
+++ b/src/internals/lattice/interval.ts
@@ -0,0 +1,69 @@
+import { JoinSemilattice } from "./common";
+import { Num, NumImpl, Interval } from "../numbers";
+import { WideningLattice } from "./widening";
+
+/**
+ * Infinite-length join semilattice lattice representing interval of numbers
+ * with abstract interpretation operations over intervals.
+ */
+export class IntervalJoinSemiLattice
+  implements JoinSemilattice<Interval>, WideningLattice<Interval>
+{
+  static bottomValue: Interval = Interval.EMPTY;
+  static topValue: Interval = Interval.FULL;
+
+  constructor() {}
+
+  bottom(): Interval {
+    return IntervalJoinSemiLattice.bottomValue;
+  }
+
+  top(): Interval {
+    return IntervalJoinSemiLattice.topValue;
+  }
+
+  /**
+   * Joins two elements, returning the least upper bound (lub) of the two
+   * intervals.
+   */
+  join(x: Interval, y: Interval): Interval {
+    if (x.isFull() || y.isFull()) {
+      return Interval.FULL;
+    }
+    if (x.isEmpty()) return y;
+    if (y.isEmpty()) return x;
+    return new Interval(Num.min(x.low, y.low), Num.max(x.high, y.high));
+  }
+
+  /**
+   * Implements the widening operator (∇) for intervals to ensure termination
+   * of fixed point computations.
+   *
+   * @param a First interval operand
+   * @param b Second interval operand (typically the newer value)
+   * @returns Widened interval that over-approximates both inputs
+   */
+  widen(a: Interval, b: Interval): Interval {
+    if (a.isEmpty()) return b;
+    if (b.isEmpty()) return a;
+    if (a.isFull() || b.isFull()) return Interval.FULL;
+    const lower = this.widenNum(a.low, b.low, true);
+    const upper = this.widenNum(a.high, b.high, false);
+    return new Interval(lower, upper);
+  }
+
+  private widenNum(a: NumImpl, b: NumImpl, isLower: boolean): NumImpl {
+    if (Num.compare(a, b) === 0n) {
+      return a;
+    }
+    if (isLower) {
+      return Num.compare(b, a) < 0 ? b : Num.m();
+    } else {
+      return Num.compare(b, a) > 0 ? b : Num.p();
+    }
+  }
+
+  leq(x: Interval, y: Interval): boolean {
+    return x.leq(y);
+  }
+}
diff --git a/src/internals/lattice/widening.ts b/src/internals/lattice/widening.ts
new file mode 100644
index 00000000..a83d4022
--- /dev/null
+++ b/src/internals/lattice/widening.ts
@@ -0,0 +1,11 @@
+import { Semilattice } from "./common";
+
+export interface WideningLattice<T> extends Semilattice<T> {
+  /**
+   * Applies the widening operation to accelerate convergence.
+   * @param oldState The previous state.
+   * @param newState The newly computed state.
+   * @returns The widened state.
+   */
+  widen(oldState: T, newState: T): T;
+}
diff --git a/src/internals/numbers/index.ts b/src/internals/numbers/index.ts
new file mode 100644
index 00000000..478add43
--- /dev/null
+++ b/src/internals/numbers/index.ts
@@ -0,0 +1,2 @@
+export * from "./num";
+export * from "./interval";
diff --git a/src/internals/numbers/interval.ts b/src/internals/numbers/interval.ts
new file mode 100644
index 00000000..d4c24c8d
--- /dev/null
+++ b/src/internals/numbers/interval.ts
@@ -0,0 +1,133 @@
+import { Num, NumImpl } from "./num";
+
+/**
+ * Represents a numeric interval [low, high] in abstract interpretation.
+ * Supports basic arithmetic operations and comparisons on intervals.
+ *
+ * Special cases:
+ * - FULL: (-∞, +∞) represents the interval containing all numbers
+ * - EMPTY: Empty interval (∅) represents an invalid or undefined interval
+ *
+ * @remarks
+ * This class implements interval arithmetic for abstract interpretation,
+ * following standard interval arithmetic rules for operations like
+ * addition, multiplication, division etc.
+ *
+ * @throws Error when performing division by an interval containing zero
+ */
+export class Interval {
+  constructor(
+    public readonly low: NumImpl,
+    public readonly high: NumImpl,
+  ) {}
+
+  static FULL = new Interval(Num.m(), Num.p());
+  static EMPTY = new Interval(Num.p(), Num.m());
+
+  static fromNum(i: bigint | number): Interval {
+    const n = Num.int(i);
+    return new Interval(n, n);
+  }
+
+  isFull(): boolean {
+    return this.low.kind === "MInf" && this.high.kind === "PInf";
+  }
+
+  isEmpty(): boolean {
+    return this.low.kind === "PInf" && this.high.kind === "MInf";
+  }
+
+  /**
+   * Checks if this interval is less than or equal to other interval.
+   */
+  leq(other: Interval): boolean {
+    if (this.isEmpty()) return true; // empty interval is less than everything
+    if (other.isEmpty()) return false; // nothing is less than empty (except empty)
+    if (other.isFull()) return true; // everything is less than full interval
+    if (this.isFull()) return false; // full interval is not less than anything (except full)
+    return (
+      Num.compare(this.low, other.low) <= 0 &&
+      Num.compare(this.high, other.high) <= 0
+    );
+  }
+
+  eq(other: Interval): boolean {
+    return (
+      Num.compare(this.low, other.low) == 0n &&
+      Num.compare(this.high, other.high) == 0n
+    );
+  }
+
+  plus(other: Interval): Interval {
+    return new Interval(
+      Num.add(this.low, other.low),
+      Num.add(this.high, other.high),
+    );
+  }
+
+  inv(): Interval {
+    return new Interval(Num.negate(this.high), Num.negate(this.low));
+  }
+
+  minus(other: Interval): Interval {
+    return this.plus(other.inv());
+  }
+
+  times(other: Interval): Interval {
+    const products = [
+      Num.multiply(this.low, other.low),
+      Num.multiply(this.low, other.high),
+      Num.multiply(this.high, other.low),
+      Num.multiply(this.high, other.high),
+    ];
+    return new Interval(Num.min(...products), Num.max(...products));
+  }
+
+  /**
+   * Abstract division.
+   *
+   * @returns A division result or a full interval if attempting to divide by zero.
+   */
+  div(other: Interval): Interval {
+    if (other.containsZero()) {
+      return Interval.FULL;
+    }
+    const quotients = [
+      Num.divide(this.low, other.low),
+      Num.divide(this.low, other.high),
+      Num.divide(this.high, other.low),
+      Num.divide(this.high, other.high),
+    ];
+    return new Interval(Num.min(...quotients), Num.max(...quotients));
+  }
+
+  containsZero(): boolean {
+    return (
+      Num.compare(this.low, Num.int(0)) <= 0 &&
+      Num.compare(this.high, Num.int(0)) >= 0
+    );
+  }
+
+  equals(other: Interval): Interval {
+    if (this.isFull() || other.isFull()) {
+      return Interval.FULL;
+    }
+    if (
+      this.low.kind === "IntNum" &&
+      this.low === this.high &&
+      other.low.kind === "IntNum" &&
+      other.low === other.high &&
+      this.low.value === other.low.value
+    ) {
+      return Interval.fromNum(1);
+    }
+    return new Interval(Num.int(0), Num.int(1));
+  }
+
+  toString(): string {
+    if (this.isFull()) return "(-∞, +∞)";
+    if (this.isEmpty()) return "∅";
+    if (Num.compare(this.low, this.high) === 0n) return Num.toString(this.low);
+    return `(${Num.toString(this.low)}, ${Num.toString(this.high)})`;
+  }
+}
diff --git a/src/internals/numbers/num.ts b/src/internals/numbers/num.ts
new file mode 100644
index 00000000..ac6d3125
--- /dev/null
+++ b/src/internals/numbers/num.ts
@@ -0,0 +1,230 @@
+/**
+ * Numbers that could include positive and negative infinity.
+ *
+ * We use these instead of `bigint` to distinguish infinities.
+ * positive and negative infinities.
+ *
+ * @packageDocumentation
+ */
+
+import { ExecutionException, InternalException } from "../exceptions";
+
+export type NumImpl = IntNum | PInf | MInf;
+
+export interface IntNum {
+  kind: "IntNum";
+  value: bigint;
+}
+
+/**
+ * Positive infinity.
+ */
+export interface PInf {
+  kind: "PInf";
+}
+
+/**
+ * Negative infinity.
+ */
+export interface MInf {
+  kind: "MInf";
+}
+
+/**
+ * Utility class for working with extended number types that include infinities.
+ */
+export class Num {
+  /**
+   * Creates an integer number representation.
+   * @param value The numeric value to wrap
+   * @returns An IntNum object
+   */
+  static int(value: bigint | number): IntNum {
+    const bigIntValue = typeof value === "number" ? BigInt(value) : value;
+    return { kind: "IntNum", value: bigIntValue };
+  }
+
+  /**
+   * Creates a positive infinity representation.
+   * @returns A PInf object
+   */
+  static p(): PInf {
+    return { kind: "PInf" };
+  }
+
+  /**
+   * Creates a negative infinity representation.
+   * @returns An MInf object
+   */
+  static m(): MInf {
+    return { kind: "MInf" };
+  }
+
+  /**
+   * Adds two numbers, handling infinite values appropriately.
+   * @throws {ExecutionException} When attempting to add +inf and -inf
+   * @throws {InternalException} When given invalid NumImpl types
+   */
+  static add(a: NumImpl, b: NumImpl): NumImpl {
+    if (a.kind === "IntNum" && b.kind === "IntNum") {
+      return this.int(a.value + b.value);
+    }
+    if (
+      (a.kind === "PInf" && b.kind === "MInf") ||
+      (a.kind === "MInf" && b.kind === "PInf")
+    ) {
+      throw ExecutionException.make("Cannot add +inf and -inf");
+    }
+    if (a.kind === "PInf" || b.kind === "PInf") {
+      return this.p();
+    }
+    if (a.kind === "MInf" || b.kind === "MInf") {
+      return this.m();
+    }
+    throw InternalException.make("Invalid NumImpl types for addition");
+  }
+
+  /**
+   * Compares two numbers, returning:
+   * - negative if a < b
+   * - zero if a = b
+   * - positive if a > b
+   */
+  static compare(a: NumImpl, b: NumImpl): bigint {
+    if (a.kind === "IntNum" && b.kind === "IntNum") {
+      return a.value - b.value;
+    } else if (a.kind === b.kind) {
+      return 0n;
+    } else if (a.kind === "MInf" || b.kind === "PInf") {
+      return -1n;
+    } else {
+      return 1n;
+    }
+  }
+
+  /**
+   * Returns the arithmetic negation of a number.
+   * @throws {Error} When given an invalid NumImpl type
+   */
+  static negate(n: NumImpl): NumImpl {
+    if (n.kind === "IntNum") {
+      return this.int(-n.value);
+    } else if (n.kind === "PInf") {
+      return this.m();
+    } else if (n.kind === "MInf") {
+      return this.p();
+    } else {
+      throw new Error("Invalid NumImpl type for negation");
+    }
+  }
+
+  static isZero(n: NumImpl): boolean {
+    return n.kind === "IntNum" && n.value === 0n;
+  }
+
+  static divide(a: NumImpl, b: NumImpl): NumImpl {
+    if (this.isZero(b)) {
+      throw ExecutionException.make("Division by zero");
+    }
+    if (a.kind === "IntNum" && b.kind === "IntNum") {
+      return this.int(a.value / b.value);
+    }
+    if (a.kind === "IntNum") {
+      if (b.kind === "PInf" || b.kind === "MInf") {
+        return this.int(0n);
+      }
+    }
+    if (b.kind === "IntNum") {
+      if (b.value > 0) {
+        if (a.kind === "PInf" || a.kind === "MInf") {
+          return a;
+        }
+      } else if (b.value < 0) {
+        if (a.kind === "PInf") {
+          return this.m();
+        }
+        if (a.kind === "MInf") {
+          return this.p();
+        }
+      }
+    }
+    if (a.kind === b.kind) {
+      return this.int(1n);
+    }
+    if (
+      (a.kind === "PInf" && b.kind === "MInf") ||
+      (a.kind === "MInf" && b.kind === "PInf")
+    ) {
+      return this.int(-1n);
+    }
+    throw InternalException.make("Invalid NumImpl types for division");
+  }
+
+  static multiply(a: NumImpl, b: NumImpl): NumImpl {
+    if (a.kind === "IntNum" && b.kind === "IntNum") {
+      return this.int(a.value * b.value);
+    }
+    if (this.isZero(a) || this.isZero(b)) {
+      return this.int(0n);
+    }
+    if (
+      (a.kind === "PInf" || a.kind === "MInf") &&
+      (b.kind === "PInf" || b.kind === "MInf")
+    ) {
+      if (a.kind === b.kind) {
+        return this.p();
+      } else {
+        return this.m();
+      }
+    }
+    if (a.kind === "IntNum") {
+      if (
+        (a.value > 0 && b.kind === "PInf") ||
+        (a.value < 0 && b.kind === "MInf")
+      ) {
+        return this.p();
+      }
+      if (
+        (a.value > 0 && b.kind === "MInf") ||
+        (a.value < 0 && b.kind === "PInf")
+      ) {
+        return this.m();
+      }
+      if (a.value === 0n) {
+        return this.int(0n);
+      }
+    }
+    if (b.kind === "IntNum") {
+      return this.multiply(b, a);
+    }
+    throw new Error("Invalid NumImpl types for multiplication");
+  }
+
+  /**
+   * Returns the minimum of the given numbers.
+   * @param nums Array of numbers to compare
+   */
+  static min(...nums: NumImpl[]): NumImpl {
+    return nums.reduce((a, b) => (this.compare(a, b) <= 0 ? a : b));
+  }
+
+  /**
+   * Returns the maximum of the given numbers.
+   * @param nums Array of numbers to compare
+   */
+  static max(...nums: NumImpl[]): NumImpl {
+    return nums.reduce((a, b) => (this.compare(a, b) >= 0 ? a : b));
+  }
+
+  static toString(n: NumImpl): string {
+    if (n.kind === "IntNum") {
+      return n.value.toString();
+    } else if (n.kind === "PInf") {
+      return "+∞";
+    } else if (n.kind === "MInf") {
+      return "-∞";
+    } else {
+      return "unknown";
+    }
+  }
+}
diff --git a/src/internals/solver/index.ts b/src/internals/solver/index.ts
index 9c7cc710..c3caeebe 100644
--- a/src/internals/solver/index.ts
+++ b/src/internals/solver/index.ts
@@ -1,4 +1,4 @@
 export { SouffleSolver, SouffleMapper } from "./souffle";
 export { Solver } from "./solver";
-export { WorklistSolver, AnalysisKind } from "./worklist";
+export * from "./worklist";
 export { SolverResults } from "./results";
diff --git a/src/internals/solver/worklist.ts b/src/internals/solver/worklist.ts
index 2527cd38..da547802 100644
--- a/src/internals/solver/worklist.ts
+++ b/src/internals/solver/worklist.ts
@@ -8,7 +8,13 @@ import {
   getPredecessors,
   getSuccessors,
 } from "../ir";
-import { Semilattice, JoinSemilattice, MeetSemilattice } from "../lattice";
+import {
+  Semilattice,
+  JoinSemilattice,
+  MeetSemilattice,
+  WideningLattice,
+} from "../lattice";
+import { Num } from "../numbers/";
 import { Transfer } from "../transfer";
 
 /**
@@ -26,12 +32,12 @@ export type AnalysisKind = "forward" | "backward";
  * This class encapsulates the control flow graph (CFG), node state transformations,
  * and lattice properties necessary for the computation of fixpoints in dataflow equations.
  */
-export class WorklistSolver<State> implements Solver<State> {
-  private readonly cu: CompilationUnit;
-  private readonly cfg: CFG;
-  private transfer: Transfer<State>;
-  private readonly lattice: Semilattice<State>;
-  private readonly kind: AnalysisKind;
+export abstract class AbstractWorklistSolver<State> implements Solver<State> {
+  protected readonly cu: CompilationUnit;
+  protected readonly cfg: CFG;
+  protected transfer: Transfer<State>;
+  protected readonly lattice: Semilattice<State>;
+  protected readonly kind: AnalysisKind;
 
   /**
    * @param transfer An object that defines the transfer operation for a node and its state.
@@ -52,18 +58,32 @@ export class WorklistSolver<State> implements Solver<State> {
     this.kind = kind;
   }
 
+  /**
+   * Abstract method to update the state of a node.
+   *
+   * @param oldState The previous state of the node.
+   * @param newState The newly computed state of the node.
+   * @param iterations The number of times the node has been processed.
+   * @returns The updated state after applying join/meet/widening/narrowing.
+   */
+  protected abstract updateState(
+    oldState: State,
+    newState: State,
+    iterations: number,
+  ): State;
+
   /**
    * Finds a fixpoint using the worklist algorithm.
    * @returns The results of solving the dataflow problem.
    */
   public findFixpoint(): SolverResults<State> {
+    // Track results and how many times we've visited each node
     const results = new SolverResults<State>();
-    const worklist: BasicBlock[] = [...this.cfg.nodes];
-
-    const bbs: BasicBlock[] = this.cfg.nodes;
+    const iterationCounts: Map<number, number> = new Map();
 
-    // Initialize all node states
-    bbs.forEach((bb) => {
+    // Initialize each block with lattice extremal value (⊥ for join, ⊤ for meet)
+    const worklist: BasicBlock[] = [...this.cfg.nodes];
+    worklist.forEach((bb) => {
       if (this.isJoinSemilattice(this.lattice)) {
         results.setState(bb.idx, this.lattice.bottom());
       } else if (this.isMeetSemilattice(this.lattice)) {
@@ -71,20 +91,22 @@ export class WorklistSolver<State> implements Solver<State> {
       } else {
         throw InternalException.make("Unsupported semilattice type");
       }
+      iterationCounts.set(bb.idx, 0);
     });
 
     while (worklist.length > 0) {
-      const bb = worklist.pop()!;
-      const neighbors =
+      const bb = worklist.shift()!;
+
+      // Compute input state by combining states from predecessors/successors
+      // depending on analysis direction (forward/backward)
+      let inState: State;
+      const neighborStates = (
         this.kind === "forward"
           ? getPredecessors(this.cfg, bb)
-          : getSuccessors(this.cfg, bb);
-
-      const neighborStates = neighbors.map(
-        (neighbor) => results.getState(neighbor.idx)!,
-      );
+          : getSuccessors(this.cfg, bb)
+      ).map((neighbor) => results.getState(neighbor.idx)!);
 
-      let inState: State;
+      // Apply lattice operation (join/meet) to combine neighbor states
       if (this.isJoinSemilattice(this.lattice)) {
         const joinLattice = this.lattice as JoinSemilattice<State>;
         inState = neighborStates.reduce((acc, state) => {
@@ -99,17 +121,28 @@ export class WorklistSolver<State> implements Solver<State> {
         throw InternalException.make("Unsupported semilattice type");
       }
 
+      // Fetch and validate the AST statement for this basic block
       const stmt = this.cu.ast.getStatement(bb.stmtID);
       if (stmt === undefined) {
         throw InternalException.make(
           `Cannot find statement #${bb.stmtID} defined within node #${bb.idx}`,
         );
       }
-      const outState = this.transfer.transfer(inState, bb, stmt);
 
-      if (!this.lattice.leq(outState, results.getState(bb.idx)!)) {
-        results.setState(bb.idx, outState);
-        // Push successors or predecessors based on the analysis kind
+      // Apply transfer function and get previous state for comparison
+      let currentOut = this.transfer.transfer(inState, bb, stmt);
+      const previousOut = results.getState(bb.idx)!;
+
+      // Track visits to handle widening/narrowing in derived classes
+      const iterations = iterationCounts.get(bb.idx)! + 1;
+      iterationCounts.set(bb.idx, iterations);
+
+      // Let derived solver classes apply their state update strategy
+      currentOut = this.updateState(previousOut, currentOut, iterations);
+
+      // If state changed (not less than or equal), update and propagate
+      if (!this.lattice.leq(currentOut, previousOut)) {
+        results.setState(bb.idx, currentOut);
         worklist.push(
           ...(this.kind === "forward"
             ? getSuccessors(this.cfg, bb)
@@ -125,15 +158,94 @@ export class WorklistSolver<State> implements Solver<State> {
     return this.findFixpoint();
   }
 
-  private isJoinSemilattice(
+  protected isJoinSemilattice(
     lattice: Semilattice<State>,
   ): lattice is JoinSemilattice<State> {
-    return (lattice as JoinSemilattice<State>).join !== undefined;
+    return "join" in lattice && typeof lattice.join === "function";
   }
 
-  private isMeetSemilattice(
+  protected isMeetSemilattice(
     lattice: Semilattice<State>,
   ): lattice is MeetSemilattice<State> {
-    return (lattice as MeetSemilattice<State>).meet !== undefined;
+    return "meet" in lattice && typeof lattice.meet === "function";
+  }
+}
+
+/**
+ * WorklistSolver performs a standard worklist-based iterative analysis relying
+ * solely on the lattice's join or meet operation to update states.
+ *
+ * @template State The type representing the state in the analysis.
+ */
+export class WorklistSolver<State> extends AbstractWorklistSolver<State> {
+  protected updateState(
+    _oldState: State,
+    newState: State,
+    _iterations: number,
+  ): State {
+    return newState;
+  }
+}
+
+/**
+ * WideningWorklistSolver performs a worklist-based iterative analysis using
+ * widening to accelerate convergence when a specified iteration threshold is
+ * reached.
+ *
+ * @template State The type representing the state in the analysis.
+ */
+export class WideningWorklistSolver<
+  State,
+> extends AbstractWorklistSolver<State> {
+  private readonly maxIterations: number;
+
+  /**
+   * @param maxIterations Number of iterations after which widening is applied.
+   */
+  constructor(
+    cu: CompilationUnit,
+    cfg: CFG,
+    transfer: Transfer<State>,
+    lattice: WideningLattice<State>,
+    kind: AnalysisKind,
+    maxIterations: number = 5,
+  ) {
+    super(cu, cfg, transfer, lattice, kind);
+    this.maxIterations = maxIterations;
+  }
+
+  protected updateState(
+    oldState: State,
+    newState: State,
+    iterations: number,
+  ): State {
+    if (iterations >= this.maxIterations) {
+      // Apply widening
+      return (this.lattice as WideningLattice<State>).widen(oldState, newState);
+    } else {
+      // Use standard join or meet
+      if (this.isJoinSemilattice(this.lattice)) {
+        const joinLattice = this.lattice as JoinSemilattice<State>;
+        return joinLattice.join(oldState, newState);
+      } else if (this.isMeetSemilattice(this.lattice)) {
+        const meetLattice = this.lattice as MeetSemilattice<State>;
+        return meetLattice.meet(oldState, newState);
+      } else {
+        throw InternalException.make("Unsupported semilattice type");
+      }
+    }
+  }
+
+  /**
+   * Type guard to check if the value is a numeric type.
+   * @param n The value to check.
+   * @returns True if the value is a Num, false otherwise.
+   */
+  private isNum(n: any): n is Num {
+    return (
+      typeof n === "object" &&
+      "kind" in n &&
+      (n.kind === "IntNum" || n.kind === "PInf" || n.kind === "MInf")
+    );
   }
 }
diff --git a/test/detectors/ExitCodeUsage.expected.out b/test/detectors/ExitCodeUsage.expected.out
new file mode 100644
index 00000000..f31b41b9
--- /dev/null
+++ b/test/detectors/ExitCodeUsage.expected.out
@@ -0,0 +1,19 @@
+[HIGH] ExitCodeUsage: Exit code variable "code1" has value outside allowed range
+test/detectors/ExitCodeUsage.tact:15:28:
+  14 |          let code1: Int = 128;
+> 15 |          nativeThrowUnless(code1, sender() == self.owner);
+                                  ^
+  16 | 
+Exit codes 0-255 are reserved. Variable value: 128
+Help: Use a value between 256 and 65535
+See: https://nowarp.io/tools/misti/docs/detectors/ExitCodeUsage
+
+[HIGH] ExitCodeUsage: Exit code variable "code2" has value outside allowed range
+test/detectors/ExitCodeUsage.tact:20:28:
+  19 |          code2 = code2 - 10;
+> 20 |          nativeThrowUnless(code2, sender() == self.owner);
+                                  ^
+  21 | 
+Exit codes 0-255 are reserved. Variable value: 246
+Help: Use a value between 256 and 65535
+See: https://nowarp.io/tools/misti/docs/detectors/ExitCodeUsage
\ No newline at end of file
diff --git a/test/detectors/ExitCodeUsage.tact b/test/detectors/ExitCodeUsage.tact
new file mode 100644
index 00000000..a07c4094
--- /dev/null
+++ b/test/detectors/ExitCodeUsage.tact
@@ -0,0 +1,26 @@
+ contract C {
+     owner: Address;
+     init() { self.owner = sender(); }
+
+     fun testDivByZero(unknown: Int) {
+         // OK: No exception
+         let a: Int = 128;
+         let b: Int = a / unknown;
+         nativeThrowUnless(b, sender() == self.owner);
+     }
+
+     receive("test") {
+         // Bad
+         let code1: Int = 128;
+         nativeThrowUnless(code1, sender() == self.owner);
+
+         // Bad
+         let code2: Int = 256;
+         code2 = code2 - 10;
+         nativeThrowUnless(code2, sender() == self.owner);
+
+         // OK: No false positive
+         let code3: Int = 257;
+         nativeThrowUnless(code3, sender() == self.owner);
+     }
+ }