diff --git a/WIP/Terverak/verify.sh b/WIP/Terverak/verify.sh
index 846d1461..45ff387a 100644
--- a/WIP/Terverak/verify.sh
+++ b/WIP/Terverak/verify.sh
@@ -1,3 +1,3 @@
 #!/bin/bash
 
-stainless-dotty src/main/scala/terverak/**/*.scala "$@"
+stainless-dotty src/main/scala/terverak/**/*.scala "$@" $1
diff --git a/caching/CachedFunction.scala b/caching/CachedFunction.scala
index 241e737d..5d9f1f0e 100644
--- a/caching/CachedFunction.scala
+++ b/caching/CachedFunction.scala
@@ -1,4 +1,4 @@
-import ch.epfl.chassot.*
+import ch.epfl.map.*
 import stainless.lang.StaticChecks.*
 import stainless.annotation.*
 import stainless.lang.{ghost => ghostExpr, _}
diff --git a/caching/verify.sh b/caching/verify.sh
index a489cf14..fbfa8244 100755
--- a/caching/verify.sh
+++ b/caching/verify.sh
@@ -1,8 +1,9 @@
 stainless-dotty\
  CachedFunction.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala \
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala\
- ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala\
- --config-file=stainless.conf --functions=CachedFunction._    
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala \
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala\
+ ../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/iMutableMaps.scala\
+ --config-file=stainless.conf --functions=CachedFunction._\
+  $1
diff --git a/data-structures/bitstream_esa/verify.sh b/data-structures/bitstream_esa/verify.sh
index f81a2718..7ef39f58 100755
--- a/data-structures/bitstream_esa/verify.sh
+++ b/data-structures/bitstream_esa/verify.sh
@@ -4,4 +4,5 @@ asn1jvm_Verification.scala  \
 asn1jvm_Helper.scala \
 asn1jvm_Bitstream.scala \
 --config-file=stainless.conf \
--D-parallel=5
+-D-parallel=5 \
+$1
\ No newline at end of file
diff --git a/data-structures/maps/mutablemaps/README.md b/data-structures/maps/mutablemaps/README.md
index 7db5d877..e42cd7e4 100644
--- a/data-structures/maps/mutablemaps/README.md
+++ b/data-structures/maps/mutablemaps/README.md
@@ -58,4 +58,4 @@ The SMT queries generated by Stainless during the verification of the `MutableLo
 
 To run the main class, run in `sbt`
 
-```$ runMain ch.epfl.chassot.Main```
\ No newline at end of file
+```$ runMain ch.epfl.map.Main```
diff --git a/data-structures/maps/mutablemaps/build.sbt b/data-structures/maps/mutablemaps/build.sbt
index 81ebe50e..1a04d209 100644
--- a/data-structures/maps/mutablemaps/build.sbt
+++ b/data-structures/maps/mutablemaps/build.sbt
@@ -1,6 +1,6 @@
 name := "MutableMaps"
 version := "0.1.0-SNAPSHOT"
-scalaVersion :="3.3.3" 
+scalaVersion :="3.5.0" 
 
 run / fork := true
 
diff --git a/data-structures/maps/mutablemaps/generate_smt_queries.py b/data-structures/maps/mutablemaps/generate_smt_queries.py
index 1759c4e8..de282210 100644
--- a/data-structures/maps/mutablemaps/generate_smt_queries.py
+++ b/data-structures/maps/mutablemaps/generate_smt_queries.py
@@ -72,7 +72,7 @@ def main():
         shutil.rmtree("./smt-sessions")
     except OSError as e:
         print("Error: %s - %s." % (e.filename, e.strerror))
-    files = ["./src/main/scala/ch/epfl/chassot/ListLongMap.scala", "./src/main/scala/ch/epfl/chassot/MutableLongMap.scala"]
+    files = ["./src/main/scala/ch/epfl/map/ListLongMap.scala", "./src/main/scala/ch/epfl/map/MutableLongMap.scala"]
     res = verify(files)
     table = extract_table_from_res(res)
     today_date = time.strftime("%Y-%m-%d--%H-%M-%S")
diff --git a/data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala b/data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala
index a05d7c86..f6f57b41 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala
@@ -5,15 +5,15 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.chassot.MutableLongMap
+import ch.epfl.map.MutableLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.chassot.EfficientFill
-import ch.epfl.chassot.MutableHashMap
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.Hashable
-import ch.epfl.chassot.ListMap
-import ch.epfl.chassot.Ordering
+import ch.epfl.map.EfficientFill
+import ch.epfl.map.MutableHashMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.Hashable
+import ch.epfl.map.ListMap
+import ch.epfl.map.Ordering
 
 
 @State(Scope.Benchmark)
diff --git a/data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala b/data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala
index 2c06a91e..2fbb430f 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala
@@ -5,14 +5,14 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.MutableLongMapOpti
-import ch.epfl.chassot.ListLongMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.MutableLongMapOpti
+import ch.epfl.map.ListLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.chassot.MutableLongMapOpti.LongMapOpti
+import ch.epfl.map.MutableLongMapOpti.LongMapOpti
 import benchmark.BenchmarkUtil.getHashMapEmptyBuffer
-import ch.epfl.chassot.EfficientFill
+import ch.epfl.map.EfficientFill
 
 @State(Scope.Benchmark)
 class ArrayFillBenchmark {
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/BuggyNewMaskComputation.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/BuggyNewMaskComputation.scala
similarity index 100%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/BuggyNewMaskComputation.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/BuggyNewMaskComputation.scala
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/EfficientFill.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/EfficientFill.scala
similarity index 95%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/EfficientFill.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/EfficientFill.scala
index 8d56e031..a82e38bf 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/EfficientFill.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/EfficientFill.scala
@@ -1,7 +1,7 @@
 /** This file contains implementations of a "fill" function for Array, used as benchmark.
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import MutableLongMap.*
 
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap-onlyCode.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap-onlyCode.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap-onlyCode.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap-onlyCode.scala
index 8412283a..a1e260c8 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap-onlyCode.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap-onlyCode.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot Contains only the code of the ListLongMap, without specification nor proof, for line counting purposes.
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
index 346f6924..735d2146 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
similarity index 90%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
index 13ca7888..34515fe6 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -19,7 +19,9 @@ import scala.collection.mutable
 case class ListMap[K, B](toList: List[(K, B)]) {
   require(TupleListOpsGenK.invariantList(toList))
 
-  def isEmpty: Boolean = toList.isEmpty
+  def isEmpty: Boolean = {
+    toList.isEmpty
+  }.ensuring(res => toList.size >= Int.MaxValue || res == (size == 0))
 
   def eq(other: ListMap[K, B]): Boolean = toList.content == other.toList.content
 
@@ -48,10 +50,16 @@ case class ListMap[K, B](toList: List[(K, B)]) {
     val res = TupleListOpsGenK.containsKey(toList, key)
     if (res) {
       TupleListOpsGenK.lemmaContainsKeyImpliesGetValueByKeyDefined(toList, key)
+      TupleListOpsGenK.lemmaInListThenGetKeysListContains(toList, key)
+    } else {
+      if(this.keys().contains(key)){
+        TupleListOpsGenK.lemmaInGetKeysListThenContainsKey(toList, key)
+        check(false)
+      }
     }
     res
 
-  }.ensuring(res => !res || this.get(key).isDefined)
+  }.ensuring(res => (!res && !this.keys().contains(key)) || (this.get(key).isDefined && this.keys().contains(key)))
 
   @inline
   def get(key: K): Option[B] = {
@@ -65,7 +73,12 @@ case class ListMap[K, B](toList: List[(K, B)]) {
 
   def keys(): List[K] = {
     TupleListOpsGenK.getKeysList(toList)
-  }
+  }.ensuring(res => 
+    noDuplicate(res) 
+    && res.length == this.toList.length 
+    && res.forall(k => TupleListOpsGenK.containsKey(this.toList, k)) 
+    && res.content == this.toList.map(_._1).content
+    )
 
   def apply(key: K): B = {
     require(contains(key))
@@ -98,7 +111,9 @@ case class ListMap[K, B](toList: List[(K, B)]) {
   }
   def -(key: K): ListMap[K, B] = {
     ListMap(TupleListOpsGenK.removePresrvNoDuplicatedKeys(toList, key))
-  }.ensuring(res => !res.contains(key))
+  }.ensuring(res => 
+    !res.contains(key)
+    && this.keys().content - key == res.keys().content )
 
   def --(keys: List[K]): ListMap[K, B] = {
     decreases(keys)
@@ -141,7 +156,12 @@ object TupleListOpsGenK {
         Cons(head._1, getKeysList(tl))
       case Nil() => Nil[K]()
     }
-  }.ensuring(res => noDuplicate(res) && res.length == l.length && res.forall(k => containsKey(l, k)))
+  }.ensuring(res => 
+    noDuplicate(res) 
+    && res.length == l.length 
+    && res.forall(k => containsKey(l, k)) 
+    && res.content == l.map(_._1).content
+    )
 
   @pure
   def intSizeKeys[K](l: List[K]): Int = {
@@ -162,13 +182,13 @@ object TupleListOpsGenK {
         if (s1 < Integer.MAX_VALUE) {
           1 + s1
         } else {
-          0
+          Integer.MAX_VALUE
         }
       }
 
       case Nil() => 0
     }
-  }.ensuring(res => res >= 0)
+  }.ensuring(res => res >= 0 && (l.isEmpty == (res == 0)))
 
   def getKeysOf[K, B](l: List[(K, B)], value: B): List[K] = {
     require(invariantList(l))
@@ -349,6 +369,96 @@ object TupleListOpsGenK {
 
   // ----------- LEMMAS -----------------------------------------------------
 
+  /**
+   * Wow this one was generated by copilot, I just had to adjust the postcondition as it wrote it in the wrong
+   * direction.
+   * But Impressive!
+   **/
+  @opaque
+  @inlineOnce 
+  def lemmaRemoveFromListThenKeysSetRemove[K, B](l: List[(K, B)], key: K): Unit = {
+    require(invariantList(l))
+    decreases(l)
+    l match {
+      case Cons(head, tl) if (head._1 == key) => 
+        if(containsKey(l, key)){
+          val h = (key, getValueByKey(l, key).get)
+          assert(l.head == (key, getValueByKey(l, key).get))
+          if(tl.contains(h)){
+            lemmaContainsTupleThenContainsKey(tl, h._1, h._2)
+            check(false)
+          }
+          assert(!tl.contains(head))
+          check(tl.content == l.content - (key, getValueByKey(l, key).get))
+        } else {
+          check(tl.content == l.content)
+        }
+      case Cons(head, tl) if (head._1 != key) =>
+        lemmaRemoveFromListThenKeysSetRemove(tl, key)
+        if(getKeysList(tl).contains(head._1)){
+          lemmaInGetKeysListThenContainsKey(tl, head._1) 
+          check(false)
+        }
+        if(containsKey(removePresrvNoDuplicatedKeys(tl, key), head._1)){
+          lemmaInListThenGetKeysListContains(removePresrvNoDuplicatedKeys(tl, key), head._1)
+          check(false)
+        }
+      case Nil() => ()
+    }
+  }.ensuring(_ => getKeysList(l).content - key == getKeysList(removePresrvNoDuplicatedKeys(l, key)).content)
+  
+  @opaque 
+  @inlineOnce
+  def lemmaEqMapSameKeysSet[K, B](lm1: ListMap[K, B], lm2: ListMap[K, B]): Unit = {
+    require(lm1.eq(lm2))
+    assert(lm1.toList.content == lm2.toList.content)
+    ListSpecs.subsetRefl(lm1.toList)
+    ListSpecs.subsetRefl(lm2.toList)
+    lemmaSubsetThenKeysSubset(lm1.toList, lm2.toList)
+    lemmaSubsetThenKeysSubset(lm2.toList, lm1.toList)
+    assert(lm1.keys().content.subsetOf(lm2.keys().content))
+    assert(lm2.keys().content.subsetOf(lm1.keys().content))
+  }.ensuring(_ => lm1.keys().content == lm2.keys().content)
+
+  @opaque
+  @inlineOnce
+  def lemmaSubsetThenKeysSubset[K, B](l1: List[(K, B)], l2: List[(K, B)]): Unit = {
+    require(invariantList(l1))
+    require(invariantList(l2))
+    require(l1.content.subsetOf(l2.content))
+    decreases(l1)
+    l1 match
+      case Cons(hd, tl) => 
+        lemmaSubsetThenKeysSubset(tl, l2)
+        assert(getKeysList(tl).content.subsetOf(getKeysList(l2).content))
+        assert(l2.contains(hd))
+        lemmaMapFirstElmtContains(l2, hd)
+        assert(l2.map(_._1).contains(hd._1))
+        assert(getKeysList(l2).contains(hd._1))
+        assert(!containsKey(tl, hd._1))
+        if(getKeysList(tl).contains(hd._1)){
+          lemmaInGetKeysListThenContainsKey(tl, hd._1)
+          check(false)
+        }
+        assert(!getKeysList(tl).contains(hd._1))
+      case Nil() => ()
+    
+
+  }.ensuring(_ => getKeysList(l1).content.subsetOf(getKeysList(l2).content))
+
+  @opaque
+  @inlineOnce
+  def lemmaMapFirstElmtContains[K, B](l: List[(K, B)], p: (K, B)): Unit = {
+      require(invariantList(l))
+      require(l.contains(p))
+      decreases(l)
+      l match {
+        case Cons(head, tl) if (head != p) =>
+          lemmaMapFirstElmtContains(tl, p)
+        case _ => ()
+      }
+    }.ensuring(_ => l.map(_._1).contains(p._1))
+
   @opaque
   @inlineOnce
   def lemmainsertNoDuplicatedKeysPreservesForall[K, B](
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/Main.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/Main.scala
similarity index 80%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/Main.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/Main.scala
index 0cb10de0..69560c93 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/Main.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/Main.scala
@@ -1,13 +1,13 @@
-package ch.epfl.chassot
+package ch.epfl.map
 
-import ch.epfl.chassot.MutableLongMap
-import ch.epfl.chassot.ListLongMap
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.ListLongMap
 import stainless.collection.List
 import benchmark.BenchmarkUtil.*
 import benchmark.Key
-import ch.epfl.chassot.MutableHashMap.*
-import ch.epfl.chassot.MutableLongMap.ValueCellFull
-import ch.epfl.chassot.MutableLongMap.EmptyCell
+import ch.epfl.map.MutableHashMap.*
+import ch.epfl.map.MutableLongMap.ValueCellFull
+import ch.epfl.map.MutableLongMap.EmptyCell
 import scala.collection.mutable.HashMap
 object Main {
   def main(args: Array[String]): Unit = {
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
index 229bd874..4ec56b9c 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection.{ListMap => ListMapStainless, ListMapLemmas => ListMapLemmasStainless, _}
@@ -15,7 +15,7 @@ import LongMapFixedSize.validMask
 import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
 // import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
 
-import MutableMapInterface.iMHashMap
+import MutableMapInterface.MutableMap
 
 trait Hashable[K] {
   @pure
@@ -41,7 +41,7 @@ object MutableHashMap {
       val hashF: Hashable[K],
       var _size: Int,
       val defaultValue: K => V
-  ) extends iMHashMap[K, V] {
+  ) extends MutableMap[K, V] {
 
     @pure
     override def defaultEntry: K => V = this.defaultValue
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
index c2af75ce..4938f12e 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -13,7 +13,7 @@ import stainless.lang.Cell
 import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
 // import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
 
-import MutableMapInterface.iMLongMap
+import MutableMapInterface.MutLongMap
 
 object MutableLongMap {
   import LongMapFixedSize.validMask
@@ -44,7 +44,7 @@ object MutableLongMap {
   @mutable
   final case class LongMap[V](
       val underlying: Cell[LongMapFixedSize[V]]
-  ) extends iMLongMap[V] {
+  ) extends MutLongMap[V] {
 
     @pure
     override def defaultEntry: Long => V = underlying.v.defaultEntry
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMapOpti.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMapOpti.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMapOpti.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMapOpti.scala
index e176e95e..5d527c39 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMapOpti.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMapOpti.scala
@@ -4,7 +4,7 @@
   *
   * It comes without proof or specification, and is used for benchmarking purposes.
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
similarity index 96%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
index 3d8e4a7a..fef66172 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -14,7 +14,7 @@ import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsu
 
 object MutableMapInterface{
   @mutable
-  trait iMLongMap[V] {
+  trait MutLongMap[V] {
     /**
      * Invariant for the datastructure
      */
@@ -67,8 +67,8 @@ object MutableMapInterface{
   }
 
   @mutable
-  trait iMHashMap[K, V] {
-    import ch.epfl.chassot.ListMap
+  trait MutableMap[K, V] {
+    import ch.epfl.map.ListMap
     /**
      * Invariant for the datastructure
      */
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OptimisedChecks.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OptimisedChecks.scala
similarity index 91%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OptimisedChecks.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OptimisedChecks.scala
index 39fb0cda..dffc6769 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OptimisedChecks.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OptimisedChecks.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 object OptimisedChecks {
   extension [T](inline value: T) inline def.ensuring(condition: T => Boolean): T = value
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OrderedListMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OrderedListMap.scala
similarity index 99%
rename from data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OrderedListMap.scala
rename to data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OrderedListMap.scala
index c9d07792..3149ea4e 100644
--- a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/OrderedListMap.scala
+++ b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OrderedListMap.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.map
 
 import stainless.annotation._
 import stainless.collection._
diff --git a/data-structures/maps/mutablemaps/verify.sh b/data-structures/maps/mutablemaps/verify.sh
index b13601d4..2e08dd98 100755
--- a/data-structures/maps/mutablemaps/verify.sh
+++ b/data-structures/maps/mutablemaps/verify.sh
@@ -1,7 +1,7 @@
 stainless-dotty\
- ./src/main/scala/ch/epfl/chassot/ListMap.scala\
- ./src/main/scala/ch/epfl/chassot/ListLongMap.scala\
- ./src/main/scala/ch/epfl/chassot/MutableLongMap.scala\
- ./src/main/scala/ch/epfl/chassot/MutableHashMap.scala\
- ./src/main/scala/ch/epfl/chassot/iMutableMaps.scala\
+ ./src/main/scala/ch/epfl/map/ListMap.scala\
+ ./src/main/scala/ch/epfl/map/ListLongMap.scala\
+ ./src/main/scala/ch/epfl/map/MutableLongMap.scala\
+ ./src/main/scala/ch/epfl/map/MutableHashMap.scala\
+ ./src/main/scala/ch/epfl/map/MutableMapsInterface.scala\
   --config-file=stainless.conf -Dparallel=6 $1
diff --git a/data-structures/sets/mutablesets/.gitignore b/data-structures/sets/mutablesets/.gitignore
new file mode 100644
index 00000000..9c145aa4
--- /dev/null
+++ b/data-structures/sets/mutablesets/.gitignore
@@ -0,0 +1,38 @@
+# macOS
+.DS_Store
+
+# sbt specific
+dist/*
+target/
+lib_managed/
+src_managed/
+project/boot/
+project/plugins/project/
+project/local-plugins.sbt
+.history
+.ensime
+.ensime_cache/
+.sbt-scripted/
+local.sbt
+
+# Bloop
+.bsp
+
+# VS Code
+.vscode/
+
+# Metals
+.bloop/
+.metals/
+metals.sbt
+
+# IDEA
+.idea
+.idea_modules
+/.worksheet/
+
+**/*.jar
+**/.jvmopts
+
+
+stainless
diff --git a/data-structures/sets/mutablesets/.scalafmt.conf b/data-structures/sets/mutablesets/.scalafmt.conf
new file mode 100644
index 00000000..e679074a
--- /dev/null
+++ b/data-structures/sets/mutablesets/.scalafmt.conf
@@ -0,0 +1,3 @@
+version = "3.7.14"
+runner.dialect = scala3
+maxColumn = 200
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/build.sbt b/data-structures/sets/mutablesets/build.sbt
new file mode 100644
index 00000000..a49a2dc0
--- /dev/null
+++ b/data-structures/sets/mutablesets/build.sbt
@@ -0,0 +1,9 @@
+name := "MutableSets"
+version := "0.1.0-SNAPSHOT"
+scalaVersion :="3.5.0" 
+
+// run / fork := true
+
+stainlessEnabled := false
+
+enablePlugins(StainlessPlugin, JmhPlugin)
diff --git a/data-structures/sets/mutablesets/project/build.properties b/data-structures/sets/mutablesets/project/build.properties
new file mode 100644
index 00000000..27430827
--- /dev/null
+++ b/data-structures/sets/mutablesets/project/build.properties
@@ -0,0 +1 @@
+sbt.version=1.9.6
diff --git a/data-structures/sets/mutablesets/project/plugins.sbt b/data-structures/sets/mutablesets/project/plugins.sbt
new file mode 100644
index 00000000..42535658
--- /dev/null
+++ b/data-structures/sets/mutablesets/project/plugins.sbt
@@ -0,0 +1 @@
+addSbtPlugin("pl.project13.scala" % "sbt-jmh" % "0.4.3")
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListLongMap.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListLongMap.scala
new file mode 120000
index 00000000..6f86782d
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListLongMap.scala
@@ -0,0 +1 @@
+../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListMap.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListMap.scala
new file mode 120000
index 00000000..51963129
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListMap.scala
@@ -0,0 +1 @@
+../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableHashMap.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableHashMap.scala
new file mode 120000
index 00000000..db3db9f0
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableHashMap.scala
@@ -0,0 +1 @@
+../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableLongMap.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableLongMap.scala
new file mode 120000
index 00000000..c8af5a54
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableLongMap.scala
@@ -0,0 +1 @@
+../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableMapsInterface.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
new file mode 120000
index 00000000..71f203ab
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
@@ -0,0 +1 @@
+../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/Main.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/Main.scala
new file mode 100644
index 00000000..a8539ca4
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/Main.scala
@@ -0,0 +1,22 @@
+package ch.epfl.set
+
+import ch.epfl.map.MutableLongMap
+import ch.epfl.map.ListLongMap
+import ch.epfl.map.Hashable
+import ch.epfl.set.MutableHashSet
+
+object Main {
+  def main(args: Array[String]): Unit = {
+    val set = MutableHashSet.getEmptyHashSet[Int](IntHashable())
+    set.update(1)
+    set.update(2)
+    println(f"Set.contains(1): ${set.contains(1)}")
+    println(f"Set.contains(2): ${set.contains(2)}")
+    println(f"Set.contains(3): ${set.contains(3)}")
+  }
+
+  case class IntHashable() extends Hashable[Int] {
+    def hash(x: Int): Long = x.toLong
+  }
+
+}
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableHashSet.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableHashSet.scala
new file mode 100644
index 00000000..bbefcf63
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableHashSet.scala
@@ -0,0 +1,86 @@
+package ch.epfl.set
+
+import stainless.annotation.*
+import stainless.collection.*
+import stainless.lang.{ghost => ghostExpr, *}
+import stainless.proof.check
+
+import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
+
+import ch.epfl.map.MutableMapInterface.MutableMap
+import ch.epfl.map.MutableHashMap
+import ch.epfl.map.Hashable
+import ch.epfl.map.ListMap
+import ch.epfl.map.TupleListOpsGenK
+
+object MutableHashSet {
+  /** Helper method to create a new empty HashSet
+    *
+    * @param hashF: Hash function for the keys
+    * @return
+    */
+  def getEmptyHashSet[K](hashF: Hashable[K]): MutableHashSet[K] = {
+    MutableHashSet(MutableHashMap.getEmptyHashMap[K, Unit]((k: K) => (), hashF))
+  }.ensuring (res => res.valid && res.size == 0)
+}
+
+@mutable
+final case class MutableHashSet[V](private val underlying: MutableMap[V, Unit]) extends MutableSetInterface.MutableSet[V]:
+    @pure 
+    @ghost
+    override def valid: Boolean = {
+      underlying.valid
+    }
+
+    override def size: Int = {
+      underlying.size
+    }
+
+    override def contains(v: V): Boolean = {
+      require(valid)
+      underlying.contains(v)
+    }.ensuring(res => valid && (res == abstractSet.contains(v)))
+
+    override def update(v: V): Boolean = {
+      require(valid)
+      @ghost val oldAbstractMap = underlying.abstractMap
+      @ghost val oldAbstractSet = abstractSet
+      val res = underlying.update(v, ())
+      ghostExpr({
+        if (res) {
+          TupleListOpsGenK.lemmaEqMapSameKeysSet(underlying.abstractMap, oldAbstractMap + (v, ()))
+        } else {
+          TupleListOpsGenK.lemmaEqMapSameKeysSet(underlying.abstractMap, oldAbstractMap)
+        }
+      })
+      res
+    }.ensuring(res => valid && (if (res) then abstractSet.contains(v) && (abstractSet == old(this).abstractSet + v) else abstractSet == old(this).abstractSet))
+
+    override def remove(v: V): Boolean = {
+      require(valid)
+      @ghost val oldAbstractMap = underlying.abstractMap
+      @ghost val oldAbstractSet = abstractSet
+      val res = underlying.remove(v)
+      ghostExpr({
+        if(!res){
+          TupleListOpsGenK.lemmaEqMapSameKeysSet(underlying.abstractMap, oldAbstractMap)
+        } else {
+          TupleListOpsGenK.lemmaEqMapSameKeysSet(underlying.abstractMap, oldAbstractMap - v)
+        }
+      })
+      res
+    }.ensuring(res => valid && (if (res) then abstractSet == old(this).abstractSet - v else abstractSet == old(this).abstractSet))
+
+    override def isEmpty: Boolean = {
+      require(valid)
+      underlying.isEmpty
+    }
+
+    @ghost
+    @pure
+    override  def abstractSet: Set[V] = {
+      require(valid)
+      underlying.abstractMap.keys().content
+    }
+
+end MutableHashSet
\ No newline at end of file
diff --git a/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableSetsInterface.scala b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableSetsInterface.scala
new file mode 100644
index 00000000..accc3289
--- /dev/null
+++ b/data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableSetsInterface.scala
@@ -0,0 +1,57 @@
+/** Author: Samuel Chassot
+  */
+package ch.epfl.set
+
+import stainless.annotation.*
+import stainless.collection.*
+import stainless.lang.*
+
+import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
+
+object MutableSetInterface{
+  @mutable
+  trait MutableSet[V] {
+    /**
+     * Invariant for the datastructure
+     */
+    @pure 
+    @ghost
+    def valid: Boolean
+
+    /**
+     * @return an instance of the executable specification of the Set
+     * This is an instance stainless.lang.Set
+     */
+    @ghost
+    @pure
+    def abstractSet: Set[V] = {
+      require(valid)
+      ??? : Set[V]
+    }
+
+    @pure
+    def size: Int
+
+    @pure
+    def isEmpty: Boolean = {
+      require(valid)
+      ??? : Boolean
+    }
+
+    @pure
+    def contains(v: V): Boolean = {
+    require(valid)
+    ??? : Boolean
+    }.ensuring(res => valid && (res == abstractSet.contains(v)))
+
+    def update(v: V): Boolean = {
+      require(valid)
+      ??? : Boolean
+    }.ensuring(res => valid && (if (res) then abstractSet.contains(v) && (abstractSet == old(this).abstractSet + v) else abstractSet == old(this).abstractSet))
+    
+    def remove(v: V): Boolean = {
+      require(valid)
+      ??? : Boolean
+    }.ensuring(res => valid && (if (res) then abstractSet == old(this).abstractSet - v else abstractSet == old(this).abstractSet))
+  }
+}
diff --git a/data-structures/sets/mutablesets/stainless.conf b/data-structures/sets/mutablesets/stainless.conf
new file mode 100644
index 00000000..ef9b3403
--- /dev/null
+++ b/data-structures/sets/mutablesets/stainless.conf
@@ -0,0 +1,16 @@
+
+# The settings below correspond to the various
+# options listed by `stainless --help`
+
+vc-cache            = true
+# debug               = ["verification", "smt"]
+timeout             = 20
+check-models        = false
+print-ids           = false
+print-types         = false
+batched             = true
+strict-arithmetic   = false
+solvers             = "smt-cvc5,smt-z3,smt-cvc4"
+check-measures      = yes
+infer-measures      = true
+simplifier           = "ol"
diff --git a/data-structures/sets/mutablesets/verify.sh b/data-structures/sets/mutablesets/verify.sh
new file mode 100755
index 00000000..7f5dd97d
--- /dev/null
+++ b/data-structures/sets/mutablesets/verify.sh
@@ -0,0 +1,9 @@
+stainless-dotty\
+ ./src/main/scala/ch/epfl/set/MutableSetsInterface.scala\
+ ./src/main/scala/ch/epfl/set/MutableHashSet.scala\
+ ./src/main/scala/ch/epfl/map/MutableMapsInterface.scala\
+ ./src/main/scala/ch/epfl/map/MutableHashMap.scala\
+ ./src/main/scala/ch/epfl/map/MutableLongMap.scala\
+ ./src/main/scala/ch/epfl/map/ListMap.scala\
+ ./src/main/scala/ch/epfl/map/ListLongMap.scala\
+  --config-file=stainless.conf -Dparallel=6 --functions=MutableSet._,MutableMapInterface._ $1
diff --git a/lexers/regex/verifiedlexer/build.sbt b/lexers/regex/verifiedlexer/build.sbt
index c64b8f37..7c99167e 100644
--- a/lexers/regex/verifiedlexer/build.sbt
+++ b/lexers/regex/verifiedlexer/build.sbt
@@ -1,6 +1,6 @@
 name := "VerifiedLexer"
 version := "0.1.0-SNAPSHOT"
-scalaVersion :="3.3.3" 
+scalaVersion :="3.5.0" 
 
 run / fork := true
 
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/benchmark/Utils.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/benchmark/Utils.scala
index c3a5e339..14e84d4d 100644
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/benchmark/Utils.scala
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/benchmark/Utils.scala
@@ -9,7 +9,7 @@ import stainless.proof.check
 import stainless.lang.StaticChecks.*
 import stainless.collection._
 
-import ch.epfl.chassot.Hashable
+import ch.epfl.map.Hashable
 import ch.epfl.lexer.VerifiedRegex._
 
 
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListLongMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListLongMap.scala
deleted file mode 120000
index 47da45f9..00000000
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListLongMap.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListLongMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListMap.scala
deleted file mode 120000
index 5b929f60..00000000
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/ListMap.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/ListMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableHashMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableHashMap.scala
deleted file mode 120000
index 333efe6a..00000000
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableHashMap.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableHashMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableLongMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableLongMap.scala
deleted file mode 120000
index 345ac4c1..00000000
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/MutableLongMap.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/MutableLongMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/iMutableMaps.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/iMutableMaps.scala
deleted file mode 120000
index 8fe7da3c..00000000
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/chassot/iMutableMaps.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/chassot/iMutableMaps.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Main.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Main.scala
index d61ab010..ba78a05f 100644
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Main.scala
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/Main.scala
@@ -1,6 +1,6 @@
 package ch.epfl.lexer
 
-import ch.epfl.chassot.MutableHashMap
+import ch.epfl.map.MutableHashMap
 import ch.epfl.lexer.VerifiedRegex._
 import ch.epfl.lexer.VerifiedRegexMatcher._
 import ch.epfl.lexer.Memoisation._
@@ -8,7 +8,7 @@ import ch.epfl.benchmark.RegexUtils._
 import stainless.annotation._
 import stainless.lang._
 import stainless.collection._
-import ch.epfl.chassot.Hashable
+import ch.epfl.map.Hashable
 import ch.epfl.lexer.RegexBenchmark.testSimp
 import scala.collection.View.Empty
 
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/OptimisedChecks.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/OptimisedChecks.scala
index 39fb0cda..407b7c8b 100644
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/OptimisedChecks.scala
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/OptimisedChecks.scala
@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.chassot
+package ch.epfl.lexer
 
 object OptimisedChecks {
   extension [T](inline value: T) inline def.ensuring(condition: T => Boolean): T = value
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala
index daa87e15..4fcb5b5e 100644
--- a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/lexer/VerifiedRegex.scala
@@ -8,17 +8,17 @@ import stainless.lang.{ghost => ghostExpr, *}
 import stainless.collection._
 import stainless.annotation._
 import stainless.proof._
-import ch.epfl.chassot.MutableLongMap._
-import ch.epfl.chassot.ListLongMap
-import ch.epfl.chassot.ListMap
-import ch.epfl.chassot.TupleListOpsGenK
-import ch.epfl.chassot.MutableHashMap._
-import ch.epfl.chassot.Hashable
-import ch.epfl.chassot.TupleListOpsGenK.invariantList
-import ch.epfl.chassot.MutableHashMap
+import ch.epfl.map.MutableLongMap._
+import ch.epfl.map.ListLongMap
+import ch.epfl.map.ListMap
+import ch.epfl.map.TupleListOpsGenK
+import ch.epfl.map.MutableHashMap._
+import ch.epfl.map.Hashable
+import ch.epfl.map.TupleListOpsGenK.invariantList
+import ch.epfl.map.MutableHashMap
 
 import stainless.lang.StaticChecks._
-// import ch.epfl.chassot.OptimisedChecks.*
+// import ch.epfl.map.OptimisedChecks.*
 
 object Memoisation {
   import VerifiedRegex._
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListLongMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListLongMap.scala
new file mode 120000
index 00000000..5f611526
--- /dev/null
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListLongMap.scala
@@ -0,0 +1 @@
+../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListMap.scala
new file mode 120000
index 00000000..41a6f75a
--- /dev/null
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/ListMap.scala
@@ -0,0 +1 @@
+../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableHashMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableHashMap.scala
new file mode 120000
index 00000000..bdd1e0d3
--- /dev/null
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableHashMap.scala
@@ -0,0 +1 @@
+../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableLongMap.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableLongMap.scala
new file mode 120000
index 00000000..300d0bfa
--- /dev/null
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableLongMap.scala
@@ -0,0 +1 @@
+../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableMapsInterface.scala b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
new file mode 120000
index 00000000..f855424c
--- /dev/null
+++ b/lexers/regex/verifiedlexer/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
@@ -0,0 +1 @@
+../../../../../../../../../data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
\ No newline at end of file
diff --git a/lexers/regex/verifiedlexer/verify.sh b/lexers/regex/verifiedlexer/verify.sh
index d144894a..b281ce09 100755
--- a/lexers/regex/verifiedlexer/verify.sh
+++ b/lexers/regex/verifiedlexer/verify.sh
@@ -2,6 +2,7 @@ stainless-dotty\
  src/main/scala/ch/epfl/lexer/VerifiedRegex.scala\
  src/main/scala/ch/epfl/lexer/VerifiedLexer.scala\
  src/main/scala/ch/epfl/lexer/ListUtils.scala\
- src/main/scala/ch/epfl/chassot/*\
+ src/main/scala/ch/epfl/map/*\
  --config-file=stainless.conf\
- -D-parallel=12 --functions=Memoisation._,VerifiedRegex_,VerifiedRegexMatcher._,VerifiedLexer._,ListUtils._
+ -D-parallel=12 --functions=Memoisation._,VerifiedRegex_,VerifiedRegexMatcher._,VerifiedLexer._,ListUtils._\
+ $1
diff --git a/lexers/regex/verifiedlexer/verify_dev.sh b/lexers/regex/verifiedlexer/verify_dev.sh
index 8d6857e8..04aabbed 100755
--- a/lexers/regex/verifiedlexer/verify_dev.sh
+++ b/lexers/regex/verifiedlexer/verify_dev.sh
@@ -1 +1 @@
-stainless-dotty --config-file=stainless.conf --watch -D-parallel=12 src/main/scala/ch/epfl/lexer/VerifiedRegex.scala src/main/scala/ch/epfl/lexer/ListUtils.scala src/main/scala/ch/epfl/chassot/* $1
+stainless-dotty --config-file=stainless.conf --watch -D-parallel=12 src/main/scala/ch/epfl/lexer/VerifiedRegex.scala src/main/scala/ch/epfl/lexer/ListUtils.scala src/main/scala/ch/epfl/map/* $1
diff --git a/qoi/verify.sh b/qoi/verify.sh
index 887a60f1..b3b1c097 100755
--- a/qoi/verify.sh
+++ b/qoi/verify.sh
@@ -3,4 +3,4 @@
 # kill subprocesses on exit or kill
 trap '[ -n "$(jobs -pr)" ] && kill -9 $(jobs -pr)' SIGINT SIGTERM EXIT
 
-stainless-dotty verified/common.scala verified/encoder.scala verified/decoder.scala -J-Xms10G -J-Xss20M "$@"
\ No newline at end of file
+stainless-dotty verified/common.scala verified/encoder.scala verified/decoder.scala -J-Xms10G -J-Xss20M "$@" $1
\ No newline at end of file
diff --git a/run-one-test.sh b/run-one-test.sh
index f67ce2cd..7445fa7d 100755
--- a/run-one-test.sh
+++ b/run-one-test.sh
@@ -22,27 +22,31 @@ function run_tests {
   echo "------------------------------------------------------------------------------------------"
   # Check if there is a verify.sh file in the project folder
   # If yes, then echo a message saying we run it and its content, then run it, other run the command X
+  status=-1
   if [ -f "$project/verify.sh" ]; then
     echo "Running verify.sh script in bolts project: $project..."
     cd "$project"
     echo "$ cat ./verify.sh"
     cat "./verify.sh"
     echo ""
-    bash "./verify.sh" "--admit-vcs=true"
+    if [ "$ADMIT_VCS" = true ]; then
+      bash "./verify.sh" "--compact" "--admit-vcs=true"
+    else
+      bash "./verify.sh" "--compact"
+    fi
     status=$?
     cd -
   else
     echo "Running '$STAINLESS --config-file=$conf $@' on bolts project: $project..."
     echo "$ find $project -name '*.scala' -exec $STAINLESS --config-file=$conf $@ {} +"
     if [ "$ADMIT_VCS" = true ]; then
-      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "--admit-vcs=true" "$@" {} +
+      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "--compact" "--admit-vcs=true" "$@" {} +
     else
       find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "$@" {} +
     fi
+    status=$?
   fi
 
-  status=$?
-
   if [ $ADMIT_VCS = true ]; then
     if [ $status -eq 0 ] || [ $status -eq 1 ]; then
       echo "Stainless accepted project: $project."
diff --git a/run-tests.sh b/run-tests.sh
index 867b32d6..d656aff5 100755
--- a/run-tests.sh
+++ b/run-tests.sh
@@ -25,4 +25,5 @@ for project in $TC_TESTS; do
   if [ $status -ne 0 ]; then
     exit $status
   fi
-done
\ No newline at end of file
+done
+echo "************* Verifying bolts projects was successful! *************"
\ No newline at end of file
diff --git a/tctests.txt b/tctests.txt
index 19074160..0ecd4205 100644
--- a/tctests.txt
+++ b/tctests.txt
@@ -7,6 +7,7 @@ algorithms/reachabilityChecker
 data-structures/amortized-queue1
 data-structures/amortized-queue2
 data-structures/maps/mutablemaps
+data-structures/sets/mutablesets
 data-structures/lisp
 data-structures/sorted-array
 data-structures/trees/concrope
diff --git a/tutorials/const-fold/ConstFold.scala b/tutorials/const-fold/ConstFold.scala
index 0d52f266..1f5e2ca7 100644
--- a/tutorials/const-fold/ConstFold.scala
+++ b/tutorials/const-fold/ConstFold.scala
@@ -1,5 +1,5 @@
 import stainless.annotation.*
-import stainless.lang.*
+import stainless.lang.{ghost => ghostExpr, *}
 object ConstFold:
 
   sealed abstract class Expr
@@ -54,7 +54,11 @@ object ConstFold:
     e match
       case Add(Number(n1), Number(n2))   => Number(n1 + n2)
       case Minus(Number(n1), Number(n2)) => Number(n1 - n2)
-      case Mul(Number(n1), Number(n2))   => Number(n1 * n2)
+      case Mul(Number(n1), Number(n2))   => 
+        ghostExpr(unfold(evaluate(anyCtx,e)))
+        ghostExpr(unfold(evaluate(anyCtx,Number(n1))))
+        ghostExpr(unfold(evaluate(anyCtx,Number(n2))))
+        Number(n1 * n2)
       case e                             => e
   }.ensuring(evaluate(anyCtx,_) == evaluate(anyCtx,e))
 
diff --git a/verify_all.sh b/verify_all.sh
new file mode 100755
index 00000000..ef337919
--- /dev/null
+++ b/verify_all.sh
@@ -0,0 +1,32 @@
+#!/bin/bash
+
+# Find all files named "verify.sh" starting from the current directory
+find . -type f -name "verify.sh" | while read -r script; do
+  # Get the directory containing the script
+  script_dir=$(dirname "$script")
+
+  # Check if the script path contains WIP and if so, skip it
+  if [[ "$script_dir" == *"WIP"* ]]; then
+    echo "Skipping $script_dir"
+    continue
+  fi
+
+  # Change to the script's directory
+  cd "$script_dir" || exit
+
+  echo "Verifying $script_dir"
+
+  # Execute the "verify.sh" script
+  # ./verify.sh
+
+  # Check the exit code of the script, and if it is not 0, print an error message and exit with the same code
+  if [ $? -ne 0 ]; then
+    echo "Verifying $script_dir failed!!!!!!!!!"
+    exit 1
+  fi
+
+  echo "----------------------------------------------------------------------------------------------------------------------------------------------------------------"
+
+  # Return to the original directory
+  cd - > /dev/null || exit
+done
\ No newline at end of file