diff --git a/src/org/sosy_lab/common/collect/PackageSanityTest.java b/src/org/sosy_lab/common/collect/PackageSanityTest.java
index d349efcf9..877ce29e1 100644
--- a/src/org/sosy_lab/common/collect/PackageSanityTest.java
+++ b/src/org/sosy_lab/common/collect/PackageSanityTest.java
@@ -16,6 +16,8 @@ public class PackageSanityTest extends AbstractPackageSanityTests {
   {
     setDistinctValues(
         PersistentLinkedList.class, PersistentLinkedList.of(), PersistentLinkedList.of("test"));
+    setDistinctValues(
+        PersistentLinkedStack.class, PersistentLinkedStack.of(), PersistentLinkedStack.of("test"));
     @SuppressWarnings("unchecked")
     OurSortedMap<String, String> singletonMap =
         (PathCopyingPersistentTreeMap<String, String>)
diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedList.java b/src/org/sosy_lab/common/collect/PersistentLinkedList.java
index c0bbc5f23..b5de8f002 100644
--- a/src/org/sosy_lab/common/collect/PersistentLinkedList.java
+++ b/src/org/sosy_lab/common/collect/PersistentLinkedList.java
@@ -9,9 +9,9 @@
 package org.sosy_lab.common.collect;
 
 import static com.google.common.base.Preconditions.checkNotNull;
+import static com.google.common.base.Preconditions.checkPositionIndex;
 import static com.google.common.base.Preconditions.checkState;
 
-import com.google.common.collect.FluentIterable;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Lists;
 import com.google.common.collect.UnmodifiableListIterator;
@@ -20,221 +20,158 @@
 import com.google.errorprone.annotations.InlineMe;
 import com.google.errorprone.annotations.Var;
 import java.util.AbstractSequentialList;
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Comparator;
-import java.util.EnumSet;
 import java.util.Iterator;
 import java.util.List;
 import java.util.ListIterator;
 import java.util.NoSuchElementException;
-import java.util.Objects;
-import java.util.Set;
-import java.util.function.BiConsumer;
-import java.util.function.BinaryOperator;
-import java.util.function.Function;
-import java.util.function.Supplier;
 import java.util.function.UnaryOperator;
 import java.util.stream.Collector;
+import java.util.stream.Collectors;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
- * A single-linked-list implementation of {@link PersistentList}. Null values are not supported
- * (similarly to {@link ImmutableList}).
+ * A {@link PersistentList} backed by a {@link PersistentLinkedStack}. List order is top-to-bottom
+ * stack order. Null elements are not supported.
  *
- * <p>Adding to the front of the list needs only O(1) time and memory.
+ * <p>Prepending, head access, tail access, and size take O(1) time. Updates share unchanged stack
+ * nodes.
  *
- * <p>This implementation supports almost all operations, except for the {@link
- * ListIterator#hasPrevious()} and {@link ListIterator#previous()} methods of its list iterator.
- * This means you cannot traverse this list in reverse order.
+ * <p>List iterators support forward traversal only; {@link ListIterator#hasPrevious()} and {@link
+ * ListIterator#previous()} are unsupported.
  *
- * <p>All instances of this class are fully-thread safe. However, note that each modifying operation
- * allocates a new instance whose reference needs to be published safely in order to be usable by
- * other threads. Two concurrent accesses to a modifying operation on the same instance will create
- * two new maps, each reflecting exactly the operation executed by the current thread, and not
- * reflecting the operation executed by the other thread.
+ * <p>The list structure is immutable and thread-safe. Elements are not copied; iterator instances
+ * have no thread-safety guarantee.
+ *
+ * @param <T> the type of elements
  */
 @Immutable(containerOf = "T")
 @SuppressWarnings({
   "deprecation", // javac complains about deprecated methods from PersistentList
-  "Immutable", // AbstractList.modCount is mutable but safe
+  "Immutable", // AbstractList.modCount is mutable but unused
 })
 public final class PersistentLinkedList<T> extends AbstractSequentialList<T>
     implements PersistentList<T> {
 
-  private final @Nullable T head; // only null for the empty list
-  private final @Nullable PersistentLinkedList<T> tail; // only null for the empty list
+  private static final PersistentLinkedList<?> EMPTY =
+      new PersistentLinkedList<>(PersistentLinkedStack.of());
 
-  private PersistentLinkedList(@Nullable T head, @Nullable PersistentLinkedList<T> tail) {
-    this.head = head;
-    this.tail = tail;
-  }
+  private final PersistentStack<T> stack;
 
-  @SuppressWarnings("rawtypes")
-  private static final PersistentLinkedList EMPTY = makeEmpty();
+  private PersistentLinkedList(PersistentStack<T> pStack) {
+    stack = checkNotNull(pStack);
+  }
 
-  @SuppressWarnings({"rawtypes", "unchecked"})
-  private static PersistentLinkedList makeEmpty() {
-    return new PersistentLinkedList(null, null);
+  private static <T> PersistentLinkedList<T> fromStack(PersistentStack<T> stack) {
+    return stack.isEmpty() ? of() : new PersistentLinkedList<>(stack);
   }
 
-  /**
-   * Returns the empty list.
-   *
-   * @return The empty list
-   */
-  @SuppressWarnings("unchecked")
+  /** Returns the empty list. */
+  @SuppressWarnings("unchecked") // The empty list contains no elements.
   public static <T> PersistentLinkedList<T> of() {
-    return EMPTY;
+    return (PersistentLinkedList<T>) EMPTY;
   }
 
-  /**
-   * Returns a list containing the specified value.
-   *
-   * @return A list containing the specified value
-   */
+  /** Returns a list containing the given element. */
   public static <T> PersistentLinkedList<T> of(T value) {
-    checkNotNull(value);
-    return new PersistentLinkedList<>(value, PersistentLinkedList.<T>of());
+    return new PersistentLinkedList<>(PersistentLinkedStack.of(value));
   }
 
-  /**
-   * Returns a list containing the specified values.
-   *
-   * @return A list containing the specified values
-   */
+  /** Returns a list containing the given elements in argument order. */
   public static <T> PersistentLinkedList<T> of(T v1, T v2) {
     return of(v2).with(v1);
   }
 
-  /**
-   * Returns a list containing the specified values.
-   *
-   * @return A list containing the specified values
-   */
+  /** Returns a list containing the given elements in argument order. */
   public static <T> PersistentLinkedList<T> of(T v1, T v2, T v3) {
     return of(v3).with(v2).with(v1);
   }
 
-  /**
-   * Returns a list containing the specified values.
-   *
-   * @return A list containing the specified values
-   */
-  @SuppressWarnings("unchecked")
+  /** Returns a list containing the given elements in argument order. */
+  @SafeVarargs
+  @SuppressWarnings("varargs") // The array is only read and is not retained.
   public static <T> PersistentLinkedList<T> of(T v1, T... values) {
     return copyOf(values).with(v1);
   }
 
-  /**
-   * Returns a list containing the specified values.
-   *
-   * @return A list containing the specified values
-   */
-  @SuppressWarnings("unchecked")
+  /** Returns a list containing the given elements in array order. */
+  @SafeVarargs
+  @SuppressWarnings("varargs") // The array is only read and is not retained.
   public static <T> PersistentLinkedList<T> copyOf(T... values) {
     return copyOf(Arrays.asList(values));
   }
 
   /**
-   * Returns A new list with the values from the Iterable.
-   *
-   * @return A new list with the values from the Iterable
+   * Returns a list in iteration order, reusing {@code values} if it is a {@code
+   * PersistentLinkedList}.
    */
   public static <T> PersistentLinkedList<T> copyOf(List<T> values) {
-    if (values instanceof PersistentLinkedList<?>) {
-      return (PersistentLinkedList<T>) values;
-    }
-    @Var PersistentLinkedList<T> result = PersistentLinkedList.<T>of();
-    for (T value : Lists.reverse(values)) {
-      result = result.with(value);
+    if (values instanceof PersistentLinkedList<T> list) {
+      return list;
     }
-    return result;
+    return PersistentLinkedList.<T>of().withAll(values);
   }
 
   /**
-   * Returns the value at the start of the list for non-empty lists.
+   * Returns the first element.
    *
-   * @throws NoSuchElementException if the list is empty.
-   * @return The value at the start of the list
+   * @throws NoSuchElementException if this list is empty
    */
   public T head() {
-    if (isEmpty()) {
-      throw new NoSuchElementException();
-    } else {
-      return head;
-    }
+    return stack.peek();
   }
 
   /**
-   * Returns the remainder of the list without the first element for non-empty lists.
+   * Returns the list without its first element, sharing the remaining stack nodes.
    *
-   * @throws IllegalStateException if the list is empty.
-   * @return The remainder of the list without the first element
+   * @throws IllegalStateException if this list is empty
    */
   public PersistentLinkedList<T> tail() {
     checkState(!isEmpty());
-    return tail;
+    return fromStack(stack.popAndCopy());
   }
 
-  /**
-   * Returns a new list with value as the head and the old list as the tail.
-   *
-   * @return A new list with value as the head and the old list as the tail
-   */
+  /** Returns a list with {@code value} prepended in O(1) time and space. */
   @Override
   public PersistentLinkedList<T> with(T value) {
-    checkNotNull(value);
-    return new PersistentLinkedList<>(value, this);
+    return fromStack(stack.pushAndCopy(value));
   }
 
-  /**
-   * Returns a new list with values as the head and the old list as the tail.
-   *
-   * @return A new list with value sas the head and the old list as the tail
-   */
+  /** Returns a list with {@code values} prepended in their iteration order. */
   @Override
-  public PersistentLinkedList<T> withAll(@Var List<T> values) {
-    @Var PersistentLinkedList<T> result = this;
-    if (values instanceof PersistentLinkedList<?>) {
-      // does not support listIterator() and thus fails on Lists.reverse()
-      values = ImmutableList.copyOf(values);
+  public PersistentLinkedList<T> withAll(List<T> values) {
+    if (values.isEmpty()) {
+      return this;
     }
-    for (T value : Lists.reverse(values)) {
-      result = result.with(value);
+    @Var PersistentStack<T> result = stack;
+    // A snapshot also supports inputs whose list iterators cannot traverse backwards.
+    for (T value : ImmutableList.copyOf(values).reverse()) {
+      result = result.pushAndCopy(value);
     }
-    return result;
+    return fromStack(result);
   }
 
-  /**
-   * Returns a new list omitting the specified value. Note: O(N)
-   *
-   * @return A new list omitting the specified value
-   */
+  /** Returns a list without the first occurrence of {@code value}, or this list if absent. */
   @Override
   public PersistentLinkedList<T> without(@Nullable T value) {
-    @Var PersistentLinkedList<T> suffix = of(); // remainder of list after value
-
-    // find position of value and update suffix
-    @Var int pos = 0;
-    for (PersistentLinkedList<T> list = this; !list.isEmpty(); list = list.tail) {
-      if (Objects.equals(value, list.head)) {
-        suffix = list.tail;
-        break;
-      }
-      pos++;
+    int index = indexOf(value);
+    if (index < 0) {
+      return this;
     }
 
-    // get start of list until value
-    // into a separate list so we can iterate in reverse
-    ImmutableList<T> prefix = FluentIterable.from(this).limit(pos).toList();
-
-    // concatenate prefix and suffix
-    @Var PersistentLinkedList<T> result = suffix;
-    for (T v : prefix.reverse()) {
-      result = result.with(v);
+    List<T> prefix = new ArrayList<>(index);
+    @Var PersistentStack<T> result = stack;
+    for (int i = 0; i < index; i++) {
+      prefix.add(result.peek());
+      result = result.popAndCopy();
     }
-
-    return result;
+    result = result.popAndCopy();
+    for (T element : Lists.reverse(prefix)) {
+      result = result.pushAndCopy(element);
+    }
+    return fromStack(result);
   }
 
   @Override
@@ -242,82 +179,90 @@ public PersistentLinkedList<T> empty() {
     return of();
   }
 
-  /**
-   * Returns the number of elements in the list. Note: O(N)
-   *
-   * @return The number of elements in the list
-   */
+  /** Returns the number of elements in O(1) time. */
   @Override
   public int size() {
-    @Var int size = 0;
-    for (PersistentLinkedList<T> list = this; !list.isEmpty(); list = list.tail) {
-      ++size;
-    }
-    return size;
+    return stack.size();
   }
 
   @Override
-  @SuppressWarnings("ReferenceEquality") // singleton instance
   public boolean isEmpty() {
-    return this == EMPTY;
+    return stack.isEmpty();
   }
 
-  /**
-   * Returns a new list with the elements in the reverse order. This operation runs in O(n).
-   *
-   * @return A new list with the elements in the reverse order
-   */
+  /** Returns a list in reverse order in O(n) time and space. */
   @Override
   public PersistentLinkedList<T> reversed() {
-    @Var PersistentLinkedList<T> result = empty();
-    for (PersistentLinkedList<T> p = this; !p.isEmpty(); p = p.tail) {
-      result = result.with(p.head);
-    }
-    return result;
+    return fromStack(PersistentLinkedStack.copyOf(stack.asTopDownIterable()));
   }
 
   @Override
   public Iterator<T> iterator() {
-    return new Iter<>(this);
+    return stack.asTopDownIterable().iterator();
   }
 
   @Override
   public ListIterator<T> listIterator(int index) {
-    if (index < 0) {
-      throw new IndexOutOfBoundsException();
-    }
-    ListIterator<T> it = new Iter<>(this);
+    checkPositionIndex(index, size());
+    ListIterator<T> result = new Iter<>(iterator());
     for (int i = 0; i < index; i++) {
-      if (!it.hasNext()) {
-        throw new IndexOutOfBoundsException();
-      }
-      it.next();
+      result.next();
     }
-    return it;
+    return result;
+  }
+
+  /** Returns a collector that collects elements in reverse encounter order. */
+  @SuppressWarnings("NoFunctionalReturnType")
+  public static <T> Collector<T, ?, PersistentLinkedList<T>> toPersistentLinkedList() {
+    return Collectors.collectingAndThen(
+        PersistentLinkedStack.<T>toPersistentLinkedStack(), PersistentLinkedList::fromStack);
+  }
+
+  /**
+   * Returns a collector that collects elements in reverse encounter order.
+   *
+   * @deprecated use {@link #toPersistentLinkedList()}
+   */
+  @Deprecated
+  @InlineMe(
+      replacement = "PersistentLinkedList.toPersistentLinkedList()",
+      imports = "org.sosy_lab.common.collect.PersistentLinkedList")
+  public static <T> Collector<T, ?, PersistentLinkedList<T>> collector() {
+    return toPersistentLinkedList();
+  }
+
+  @Deprecated
+  @Override
+  @DoNotCall
+  public void replaceAll(UnaryOperator<T> pOperator) {
+    throw new UnsupportedOperationException();
+  }
+
+  @Deprecated
+  @Override
+  @DoNotCall
+  public void sort(Comparator<? super T> pComparator) {
+    throw new UnsupportedOperationException();
   }
 
   private static final class Iter<T> extends UnmodifiableListIterator<T> {
 
-    private PersistentLinkedList<T> list;
+    private final Iterator<T> delegate;
     private int nextIndex = 0;
 
-    private Iter(PersistentLinkedList<T> list) {
-      this.list = list;
+    private Iter(Iterator<T> pDelegate) {
+      delegate = pDelegate;
     }
 
     @Override
     public boolean hasNext() {
-      return !list.isEmpty();
+      return delegate.hasNext();
     }
 
     @Override
     public T next() {
-      if (list.isEmpty()) {
-        throw new NoSuchElementException();
-      }
+      T result = delegate.next();
       nextIndex++;
-      T result = list.head;
-      list = list.tail;
       return result;
     }
 
@@ -341,83 +286,4 @@ public T previous() {
       throw new UnsupportedOperationException();
     }
   }
-
-  /**
-   * Return a {@link Collector} that creates PersistentLinkedLists and can be used in {@link
-   * java.util.stream.Stream#collect(Collector)}. The returned collector does not support parallel
-   * streams.
-   */
-  @SuppressWarnings("NoFunctionalReturnType")
-  public static <T> Collector<T, ?, PersistentLinkedList<T>> toPersistentLinkedList() {
-    return new Collector<T, PersistentLinkedListBuilder<T>, PersistentLinkedList<T>>() {
-
-      @Override
-      public Supplier<PersistentLinkedListBuilder<T>> supplier() {
-        return PersistentLinkedListBuilder::new;
-      }
-
-      @Override
-      public BiConsumer<PersistentLinkedListBuilder<T>, T> accumulator() {
-        return PersistentLinkedListBuilder::add;
-      }
-
-      @Override
-      public BinaryOperator<PersistentLinkedListBuilder<T>> combiner() {
-        return (a, b) -> {
-          throw new UnsupportedOperationException("Should be used sequentially");
-        };
-      }
-
-      @Override
-      public Function<PersistentLinkedListBuilder<T>, PersistentLinkedList<T>> finisher() {
-        return PersistentLinkedListBuilder::build;
-      }
-
-      @Override
-      public Set<Characteristics> characteristics() {
-        return EnumSet.noneOf(Characteristics.class);
-      }
-    };
-  }
-
-  /**
-   * Return a {@link Collector} that creates PersistentLinkedLists and can be used in {@link
-   * java.util.stream.Stream#collect(Collector)}. The returned collector does not support parallel
-   * streams.
-   *
-   * @deprecated renamed to {@link #toPersistentLinkedList()} to conform with Guava's naming
-   */
-  @Deprecated
-  @InlineMe(
-      replacement = "PersistentLinkedList.toPersistentLinkedList()",
-      imports = "org.sosy_lab.common.collect.PersistentLinkedList")
-  public static <T> Collector<T, ?, PersistentLinkedList<T>> collector() {
-    return toPersistentLinkedList();
-  }
-
-  private static final class PersistentLinkedListBuilder<T> {
-    private PersistentLinkedList<T> list = PersistentLinkedList.of();
-
-    void add(T e) {
-      list = list.with(e);
-    }
-
-    PersistentLinkedList<T> build() {
-      return list;
-    }
-  }
-
-  @Deprecated
-  @Override
-  @DoNotCall
-  public void replaceAll(UnaryOperator<T> pOperator) {
-    throw new UnsupportedOperationException();
-  }
-
-  @Deprecated
-  @Override
-  @DoNotCall
-  public void sort(Comparator<? super T> pC) {
-    throw new UnsupportedOperationException();
-  }
 }
diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStack.java b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java
new file mode 100644
index 000000000..a337fd33a
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/PersistentLinkedStack.java
@@ -0,0 +1,316 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+import static com.google.common.base.Preconditions.checkPositionIndex;
+
+import com.google.common.base.Joiner;
+import com.google.common.collect.AbstractIterator;
+import com.google.common.collect.ImmutableList;
+import com.google.errorprone.annotations.Immutable;
+import com.google.errorprone.annotations.Var;
+import java.io.InvalidObjectException;
+import java.io.ObjectInputStream;
+import java.io.Serial;
+import java.io.Serializable;
+import java.util.NoSuchElementException;
+import java.util.stream.Collector;
+import java.util.stream.Collectors;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+/**
+ * A persistent stack. Pushes structurally share the complete previous stack, and pops return the
+ * existing tail without copying, while leaving the original stack unchanged. Thus {@link
+ * #pushAndCopy(Object)}, {@link #popAndCopy()}, {@link #peek()}, {@link #empty()}, {@link
+ * #isEmpty()}, and {@link #size()} run in O(1) time. Iteration, {@link #equals(Object)}, {@link
+ * #hashCode()}, and {@link #toString()} have O(n) worst-case stack-traversal overhead. When two
+ * equal-size {@link PersistentLinkedStack} instances share a tail, {@code equals} traverses only
+ * the k nodes preceding that tail and thus has O(k) traversal overhead. These bounds exclude work
+ * performed by element methods.
+ *
+ * <p>All structural state is final and correctly constructed, so the immutable stack structure may
+ * be accessed concurrently without synchronization. Publishing or updating a shared reference to a
+ * stack version still requires coordination, and compound updates require synchronization or an
+ * atomic operation. Each traversal has an independent iterator; a single iterator instance has no
+ * thread-safety guarantee. Values are stored by reference and are not copied or made immutable or
+ * thread-safe.
+ *
+ * <p>Null values are not supported.
+ *
+ * <p><b>Serialization:</b> Serialization and deserialization have O(n) stack-traversal overhead and
+ * use O(n) temporary memory, excluding the processing of element object graphs. A flattened proxy
+ * stores the logical values in top-to-bottom order instead of serializing the linked nodes. This
+ * avoids recursive traversal of long stacks and keeps node and cache fields out of the serialized
+ * form. Deserialization rejects null proxy data and rebuilds the stack from bottom to top while
+ * validating each value, thereby preserving order and restoring the canonical empty instance.
+ * Because each stack is flattened independently, distinct, structurally related stacks serialized
+ * together have their shared non-empty tails reconstructed independently; {@link #popAndCopy()} on
+ * a deserialized stack nevertheless returns its existing tail. Element object graphs must not
+ * contain references back to the containing stack because proxy replacement cannot restore such
+ * cycles. Persisted data remains readable only while the proxy and element serialized forms remain
+ * compatible.
+ *
+ * @param <T> the type of values
+ */
+@Immutable(containerOf = "T")
+public final class PersistentLinkedStack<T> implements PersistentStack<T> {
+
+  @Serial private static final long serialVersionUID = -4286928240765960519L;
+
+  private static final PersistentLinkedStack<?> EMPTY = new PersistentLinkedStack<>();
+
+  /** The top value, null exactly for the empty singleton. */
+  @SuppressWarnings("serial") // writeReplace prevents direct serialization of this field.
+  private final @Nullable T top;
+
+  /** The linked tail, null exactly for the empty singleton. */
+  private final @Nullable PersistentLinkedStack<T> tail;
+
+  /**
+   * The size, cached for O(1) access. It is zero exactly for the empty stack and otherwise equals
+   * {@code tail.size + 1}. The cache is one logical 4-byte {@code int}; its actual footprint
+   * depends on JVM object layout and alignment. It often fits into padding with compressed
+   * references and 8-byte alignment, but may add an alignment unit otherwise.
+   */
+  private final int size;
+
+  private PersistentLinkedStack() {
+    top = null;
+    tail = null;
+    size = 0;
+  }
+
+  private PersistentLinkedStack(T pTop, PersistentLinkedStack<T> pTail) {
+    top = checkNotNull(pTop);
+    tail = checkNotNull(pTail);
+    size = pTail.size + 1;
+  }
+
+  /** Returns an empty stack. */
+  @SuppressWarnings("unchecked")
+  public static <T> PersistentLinkedStack<T> of() {
+    return (PersistentLinkedStack<T>) EMPTY;
+  }
+
+  /**
+   * Returns a stack containing {@code value}.
+   *
+   * @throws NullPointerException if {@code value} is null
+   */
+  public static <T> PersistentLinkedStack<T> of(T value) {
+    return new PersistentLinkedStack<>(value, PersistentLinkedStack.of());
+  }
+
+  @Override
+  public PersistentLinkedStack<T> pushAndCopy(T value) {
+    return new PersistentLinkedStack<>(value, this);
+  }
+
+  @Override
+  public PersistentLinkedStack<T> popAndCopy() {
+    if (isEmpty()) {
+      throw new NoSuchElementException();
+    }
+    return checkNotNull(tail);
+  }
+
+  @Override
+  public T peek() {
+    if (isEmpty()) {
+      throw new NoSuchElementException();
+    }
+    return checkNotNull(top);
+  }
+
+  @Override
+  public PersistentLinkedStack<T> empty() {
+    return of();
+  }
+
+  @Override
+  public boolean isEmpty() {
+    return size == 0;
+  }
+
+  @Override
+  public int size() {
+    return size;
+  }
+
+  @Override
+  public Iterable<T> asTopDownIterable() {
+    return () -> new StackIterator<>(this);
+  }
+
+  @Override
+  public ImmutableList<T> copyToList() {
+    return ImmutableList.copyOf(asTopDownIterable()).reverse();
+  }
+
+  @Override
+  @SuppressWarnings("ReferenceEquality") // Identical tails need no further comparison.
+  public boolean equals(@Nullable Object obj) {
+    if (obj == this) {
+      return true;
+    }
+    if (!(obj instanceof PersistentStack<?> other) || size != other.size()) {
+      return false;
+    }
+
+    @Var PersistentStack<?> left = this;
+    @Var PersistentStack<?> right = other;
+    while (!left.isEmpty()) {
+      if (left == right) {
+        return true;
+      }
+      if (!left.peek().equals(right.peek())) {
+        return false;
+      }
+      left = left.popAndCopy();
+      right = right.popAndCopy();
+    }
+    return true;
+  }
+
+  @Override
+  public int hashCode() {
+    @Var int hash = 1;
+    for (T value : asTopDownIterable()) {
+      hash = 31 * hash + value.hashCode();
+    }
+    return hash;
+  }
+
+  /**
+   * Returns the values in top-to-bottom order, separated by {@code ", "} and enclosed in square
+   * brackets: {@code [top, ..., bottom]}. The empty stack is represented as {@code []}.
+   */
+  @Override
+  public String toString() {
+    return "[" + Joiner.on(", ").join(asTopDownIterable()) + "]";
+  }
+
+  @Override
+  public PersistentLinkedStack<T> takeBottom(int count) {
+    checkPositionIndex(count, size);
+    if (count == 0) {
+      return of();
+    }
+
+    @Var PersistentLinkedStack<T> result = this;
+    while (result.size > count) {
+      result = result.popAndCopy();
+    }
+    return result;
+  }
+
+  /**
+   * Returns a stack by pushing the arguments from left to right. The last argument is on top.
+   *
+   * @throws NullPointerException if an element or the varargs array is null
+   */
+  @SafeVarargs
+  public static <T> PersistentLinkedStack<T> of(T first, T second, T... remaining) {
+    @Var PersistentLinkedStack<T> result = of(first).pushAndCopy(second);
+    for (T value : remaining) {
+      result = result.pushAndCopy(value);
+    }
+    return result;
+  }
+
+  /**
+   * Returns a stack by pushing the elements in iteration order. The last element is on top.
+   *
+   * @throws NullPointerException if {@code values} or an element is null
+   */
+  public static <T> PersistentLinkedStack<T> copyOf(Iterable<? extends T> values) {
+    checkNotNull(values);
+    @Var PersistentLinkedStack<T> result = of();
+    for (T value : values) {
+      result = result.pushAndCopy(value);
+    }
+    return result;
+  }
+
+  /** Returns a collector that pushes elements in encounter order, with the last element on top. */
+  @SuppressWarnings("NoFunctionalReturnType")
+  public static <T> Collector<T, ?, PersistentLinkedStack<T>> toPersistentLinkedStack() {
+    return Collectors.collectingAndThen(
+        ImmutableList.<T>toImmutableList(), PersistentLinkedStack::copyOf);
+  }
+
+  @Serial
+  private Object writeReplace() {
+    return new SerializationProxy(this);
+  }
+
+  @Serial
+  @SuppressWarnings("unused") // Serialization hook prevents bypassing the proxy.
+  private void readObject(ObjectInputStream pInputStream) throws InvalidObjectException {
+    throw new InvalidObjectException("Serialization proxy required");
+  }
+
+  /** Flat serialized form containing the logical values in top-to-bottom order. */
+  private static final class SerializationProxy implements Serializable {
+
+    @Serial private static final long serialVersionUID = 2702329958583141147L;
+
+    /** Nullable only to model malformed serialized input, which {@link #readResolve()} rejects. */
+    @SuppressWarnings("serial") // ObjectOutputStream checks each element graph at runtime.
+    private final @Nullable Object @Nullable [] values;
+
+    private SerializationProxy(PersistentLinkedStack<?> stack) {
+      values = new Object[stack.size];
+      @Var int index = 0;
+      for (Object value : stack.asTopDownIterable()) {
+        values[index] = value;
+        index++;
+      }
+    }
+
+    @Serial
+    private Object readResolve() throws InvalidObjectException {
+      @Nullable Object @Nullable [] serializedValues = values;
+      if (serializedValues == null) {
+        throw new InvalidObjectException("Stack values must not be null");
+      }
+
+      @Var PersistentLinkedStack<Object> stack = PersistentLinkedStack.of();
+      // The serialized order is top-to-bottom; push in the opposite direction.
+      for (@Var int index = serializedValues.length - 1; index >= 0; index--) {
+        @Nullable Object value = serializedValues[index];
+        if (value == null) {
+          throw new InvalidObjectException("Stack values must not contain null");
+        }
+        stack = stack.pushAndCopy(value);
+      }
+      return stack;
+    }
+  }
+
+  private static final class StackIterator<T> extends AbstractIterator<T> {
+
+    private PersistentLinkedStack<T> remaining;
+
+    private StackIterator(PersistentLinkedStack<T> stack) {
+      remaining = stack;
+    }
+
+    @Override
+    protected @Nullable T computeNext() {
+      if (remaining.isEmpty()) {
+        return endOfData();
+      }
+      T result = remaining.peek();
+      remaining = remaining.popAndCopy();
+      return result;
+    }
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java
new file mode 100644
index 000000000..e22bbbba4
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/PersistentLinkedStackTest.java
@@ -0,0 +1,249 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import static com.google.common.truth.Truth.assertThat;
+import static org.junit.Assert.assertThrows;
+
+import com.google.common.testing.EqualsTester;
+import com.google.common.testing.SerializableTester;
+import com.google.errorprone.annotations.Var;
+import java.math.BigInteger;
+import java.util.Iterator;
+import java.util.NoSuchElementException;
+import org.junit.Test;
+
+public class PersistentLinkedStackTest {
+
+  @Test
+  public void testEmptyFactory() {
+    PersistentStack<String> stack = PersistentLinkedStack.of();
+
+    assertThat(stack.isEmpty()).isTrue();
+  }
+
+  @Test
+  public void testSingletonFactory() {
+    PersistentStack<String> stack = PersistentLinkedStack.of("value");
+
+    assertThat(stack.isEmpty()).isFalse();
+    assertThat(stack.asTopDownIterable()).containsExactly("value");
+  }
+
+  @Test
+  public void testPushAndCopy() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+    PersistentStack<String> stack = empty.pushAndCopy("value");
+
+    assertThat(stack.peek()).isEqualTo("value");
+    assertThat(empty.asTopDownIterable()).isEmpty();
+    assertThat(empty.isEmpty()).isTrue();
+  }
+
+  @Test
+  public void testDuplicateEmptyStrings() {
+    PersistentStack<String> stack =
+        PersistentLinkedStack.<String>of().pushAndCopy("").pushAndCopy("");
+
+    assertThat(stack.size()).isEqualTo(2);
+    assertThat(stack.peek()).isEmpty();
+    PersistentStack<String> popped = stack.popAndCopy();
+    assertThat(popped.size()).isEqualTo(1);
+    assertThat(popped.peek()).isEqualTo(stack.peek());
+  }
+
+  @Test
+  public void testIntegerValues() {
+    PersistentStack<Integer> stack =
+        PersistentLinkedStack.<Integer>of().pushAndCopy(1).pushAndCopy(2);
+
+    assertThat(stack.size()).isEqualTo(2);
+    assertThat(stack.peek()).isEqualTo(2);
+    PersistentStack<Integer> popped = stack.popAndCopy();
+    assertThat(popped.size()).isEqualTo(1);
+    assertThat(popped.peek()).isEqualTo(1);
+  }
+
+  @Test
+  public void testBigIntegerValueEqualityAndIdentity() {
+    BigInteger sharedValue = new BigInteger("123456789012345678901234567890");
+    BigInteger equalValue = new BigInteger("123456789012345678901234567890");
+    PersistentStack<BigInteger> first = PersistentLinkedStack.of(sharedValue);
+    PersistentStack<BigInteger> sameReference = PersistentLinkedStack.of(sharedValue);
+    PersistentStack<BigInteger> equalReference = PersistentLinkedStack.of(equalValue);
+
+    assertThat(first).isNotSameInstanceAs(sameReference);
+    assertThat(first).isEqualTo(sameReference);
+    assertThat(first.peek()).isSameInstanceAs(sharedValue);
+    assertThat(sameReference.peek()).isSameInstanceAs(sharedValue);
+
+    assertThat(equalValue).isNotSameInstanceAs(sharedValue);
+    assertThat(equalValue).isEqualTo(sharedValue);
+    assertThat(first).isEqualTo(equalReference);
+    assertThat(equalReference.peek()).isSameInstanceAs(equalValue);
+    assertThat(equalReference.peek()).isNotSameInstanceAs(sharedValue);
+  }
+
+  @Test
+  public void testPopReturnsSamePredecessor() {
+    PersistentStack<String> predecessor =
+        PersistentLinkedStack.<String>of().pushAndCopy("bottom").pushAndCopy("middle");
+    PersistentStack<String> stack = predecessor.pushAndCopy("top");
+
+    assertThat(stack.popAndCopy()).isSameInstanceAs(predecessor);
+  }
+
+  @Test
+  public void testPeekEmptyThrows() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+
+    assertThrows(NoSuchElementException.class, empty::peek);
+  }
+
+  @Test
+  public void testPopEmptyThrows() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+
+    assertThrows(NoSuchElementException.class, empty::popAndCopy);
+  }
+
+  @Test
+  public void testSizeAcrossPersistentVersions() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+    PersistentStack<String> one = empty.pushAndCopy("one");
+    PersistentStack<String> two = one.pushAndCopy("two");
+
+    assertThat(empty.size()).isEqualTo(0);
+    assertThat(one.size()).isEqualTo(1);
+    assertThat(two.size()).isEqualTo(2);
+    assertThat(two.popAndCopy().size()).isEqualTo(1);
+    assertThat(empty.size()).isEqualTo(0);
+    assertThat(one.size()).isEqualTo(1);
+    assertThat(two.size()).isEqualTo(2);
+  }
+
+  @Test
+  public void testCanonicalEmpty() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+    PersistentStack<String> singleton = PersistentLinkedStack.of("value");
+
+    assertThat(PersistentLinkedStack.<String>of()).isSameInstanceAs(empty);
+    assertThat(singleton.empty()).isSameInstanceAs(empty);
+    assertThat(singleton.popAndCopy()).isSameInstanceAs(empty);
+  }
+
+  @Test
+  public void testRejectsNull() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+
+    assertThrows(NullPointerException.class, () -> PersistentLinkedStack.of((String) null));
+    assertThrows(NullPointerException.class, () -> empty.pushAndCopy(null));
+    assertThrows(
+        NullPointerException.class, () -> PersistentLinkedStack.of("value").pushAndCopy(null));
+  }
+
+  @Test
+  public void testIteratorOrderIsTopToBottom() {
+    PersistentStack<String> stack =
+        PersistentLinkedStack.<String>of()
+            .pushAndCopy("bottom")
+            .pushAndCopy("middle")
+            .pushAndCopy("top");
+
+    assertThat(stack.asTopDownIterable()).containsExactly("top", "middle", "bottom").inOrder();
+  }
+
+  @Test
+  public void testIteratorExhaustion() {
+    Iterator<String> iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator();
+
+    assertThat(iterator.next()).isEqualTo("value");
+    assertThrows(NoSuchElementException.class, iterator::next);
+  }
+
+  @Test
+  public void testIteratorRemoveRejected() {
+    Iterator<String> iterator = PersistentLinkedStack.of("value").asTopDownIterable().iterator();
+
+    assertThrows(UnsupportedOperationException.class, iterator::remove);
+  }
+
+  @Test
+  public void testEquality() {
+    PersistentStack<String> stack =
+        PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top");
+    PersistentStack<String> independentlyBuilt =
+        PersistentLinkedStack.<String>of()
+            .pushAndCopy("bottom")
+            .pushAndCopy("middle")
+            .pushAndCopy("top");
+    PersistentStack<String> differentOrder =
+        PersistentLinkedStack.of("top").pushAndCopy("middle").pushAndCopy("bottom");
+    PersistentStack<String> differentMiddle =
+        PersistentLinkedStack.of("bottom").pushAndCopy("other").pushAndCopy("top");
+    PersistentStack<String> differentBottom =
+        PersistentLinkedStack.of("other").pushAndCopy("middle").pushAndCopy("top");
+    PersistentStack<String> shorter = PersistentLinkedStack.of("middle").pushAndCopy("top");
+
+    new EqualsTester()
+        .addEqualityGroup(stack, independentlyBuilt)
+        .addEqualityGroup(differentOrder)
+        .addEqualityGroup(differentMiddle)
+        .addEqualityGroup(differentBottom)
+        .addEqualityGroup(shorter)
+        .testEquals();
+  }
+
+  @Test
+  public void testEqualityWithSharedTail() {
+    PersistentLinkedStack<String> sharedTail =
+        PersistentLinkedStack.of("bottom").pushAndCopy("shared");
+    PersistentStack<String> stack = sharedTail.pushAndCopy("middle").pushAndCopy("top");
+    PersistentStack<String> equal = sharedTail.pushAndCopy("middle").pushAndCopy("top");
+    PersistentStack<String> different = sharedTail.pushAndCopy("other").pushAndCopy("top");
+
+    new EqualsTester().addEqualityGroup(stack, equal).addEqualityGroup(different).testEquals();
+  }
+
+  @Test
+  public void testToString() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+    PersistentStack<String> stack =
+        PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top");
+
+    assertThat(empty.toString()).isEqualTo("[]");
+    assertThat(stack.toString()).isEqualTo("[top, middle, bottom]");
+  }
+
+  @Test
+  public void testSerializationRoundTrip() {
+    PersistentStack<String> stack =
+        PersistentLinkedStack.of("bottom").pushAndCopy("middle").pushAndCopy("top");
+
+    SerializableTester.reserializeAndAssert(stack);
+  }
+
+  @Test
+  public void testEmptySerializationReturnsCanonicalInstance() {
+    PersistentStack<String> empty = PersistentLinkedStack.of();
+
+    assertThat(SerializableTester.reserialize(empty)).isSameInstanceAs(empty);
+  }
+
+  @Test
+  public void testLongStackSerializationRoundTrip() {
+    int length = 10_000;
+    @Var PersistentStack<Integer> stack = PersistentLinkedStack.of();
+    for (int i = 0; i < length; i++) {
+      stack = stack.pushAndCopy(i);
+    }
+
+    assertThat(SerializableTester.reserialize(stack)).isEqualTo(stack);
+  }
+}
diff --git a/src/org/sosy_lab/common/collect/PersistentStack.java b/src/org/sosy_lab/common/collect/PersistentStack.java
new file mode 100644
index 000000000..be8b1b2f2
--- /dev/null
+++ b/src/org/sosy_lab/common/collect/PersistentStack.java
@@ -0,0 +1,116 @@
+// This file is part of SoSy-Lab Common,
+// a library of useful utilities:
+// https://github.com/sosy-lab/java-common-lib
+//
+// SPDX-FileCopyrightText: 2007-2026 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.common.collect;
+
+import com.google.errorprone.annotations.CheckReturnValue;
+import com.google.errorprone.annotations.Immutable;
+import java.io.Serializable;
+import java.util.List;
+import java.util.NoSuchElementException;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+/**
+ * Interface for persistent stacks. A persistent data structure is structurally immutable, but
+ * provides cheap copy-and-write operations. Operations that conceptually modify the stack return
+ * another stack while leaving the current instance unchanged.
+ *
+ * <p>Implementations are expected to provide {@link #pushAndCopy(Object)}, {@link #popAndCopy()},
+ * {@link #peek()}, {@link #empty()}, {@link #isEmpty()}, and {@link #size()} in O(1) time.
+ * Iteration proceeds from the top of the stack to the bottom.
+ *
+ * <p>Null values are not supported.
+ *
+ * <p>Instances and their views are thread-safe; iterator instances have no thread-safety guarantee.
+ * Elements are not copied, and their own thread-safety requirements still apply.
+ *
+ * <p>Stacks are serializable when their elements are serializable.
+ *
+ * <p>Values are stored by reference: they are not copied or made immutable or thread-safe.
+ *
+ * @param <T> The type of values.
+ */
+@Immutable(containerOf = "T")
+public interface PersistentStack<T> extends Serializable {
+
+  /**
+   * Returns a stack with {@code value} on top, leaving this stack unchanged.
+   *
+   * @throws NullPointerException if {@code value} is null
+   */
+  @CheckReturnValue
+  PersistentStack<T> pushAndCopy(T value);
+
+  /**
+   * Returns a stack without this stack's top value, leaving this stack unchanged.
+   *
+   * @throws NoSuchElementException if this stack is empty
+   */
+  @CheckReturnValue
+  PersistentStack<T> popAndCopy();
+
+  /**
+   * Returns this stack's top value without modifying the stack.
+   *
+   * @throws NoSuchElementException if this stack is empty
+   */
+  T peek();
+
+  /** Returns an empty stack of the same implementation. */
+  @CheckReturnValue
+  PersistentStack<T> empty();
+
+  /** Returns whether this stack contains no values. */
+  boolean isEmpty();
+
+  /** Returns the number of values in this stack. */
+  int size();
+
+  /**
+   * Returns an unmodifiable top-to-bottom view in O(1) time. Each iterator traverses this stack
+   * version independently.
+   */
+  Iterable<T> asTopDownIterable();
+
+  /** Returns an unmodifiable bottom-to-top list in O(n) time and space. */
+  List<T> copyToList();
+
+  /**
+   * Returns a stack containing the bottom {@code count} elements.
+   *
+   * @throws IndexOutOfBoundsException if {@code count} is outside {@code [0, size()]}
+   */
+  @CheckReturnValue
+  PersistentStack<T> takeBottom(int count);
+
+  /**
+   * Returns {@code true} if and only if {@code obj} is a {@link PersistentStack} with the same
+   * number of elements and equal corresponding elements in top-to-bottom order. Elements are
+   * compared using {@link Object#equals(Object)}.
+   *
+   * <p>Equality is independent of the concrete implementation and structural sharing. All empty
+   * stacks are equal.
+   *
+   * @param obj the object to compare with this stack
+   * @return whether the object is equal to this stack
+   */
+  @Override
+  boolean equals(@Nullable Object obj);
+
+  /**
+   * Returns the hash code of this stack.
+   *
+   * <p>The hash code is computed starting with {@code hash = 1} and applying {@code hash = 31 *
+   * hash + element.hashCode()} to each element in top-to-bottom order, using Java {@code int}
+   * arithmetic. The hash code of an empty stack is {@code 1}.
+   *
+   * @return the hash code of this stack
+   */
+  @Override
+  int hashCode();
+}