diff --git a/col/src/main/java/vct/col/ast/Node.scala b/col/src/main/java/vct/col/ast/Node.scala
index 488e09bf82..f5b1cf9f17 100644
--- a/col/src/main/java/vct/col/ast/Node.scala
+++ b/col/src/main/java/vct/col/ast/Node.scala
@@ -58,10 +58,11 @@ import vct.col.ast.statement.composite._
 import vct.col.ast.statement.exceptional._
 import vct.col.ast.statement.nonexecutable._
 import vct.col.ast.statement.terminal._
+import vct.col.ast.statement.veymont.VeyMontCommImpl
 import vct.col.ast.util.Declarator
 import vct.col.debug._
 import vct.col.origin._
-import vct.col.ref.Ref
+import vct.col.ref.{DirectRef, Ref}
 import vct.col.resolve._
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.JavaAnnotationData
@@ -127,6 +128,8 @@ final case class TZFraction[G]()(implicit val o: Origin = DiagnosticOrigin) exte
 sealed trait DeclaredType[G] extends Type[G] with DeclaredTypeImpl[G]
 final case class TModel[G](model: Ref[G, Model[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TModelImpl[G]
 final case class TClass[G](cls: Ref[G, Class[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TClassImpl[G]
+final case class TSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TSeqProgImpl[G]
+final case class TVeyMontThread[G](cls: Ref[G, VeyMontThread[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TVeyMontThreadImpl[G]
 final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAnyClassImpl[G]
 final case class TAxiomatic[G](adt: Ref[G, AxiomaticDataType[G]], args: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAxiomaticImpl[G]
 final case class TEnum[G](enum: Ref[G, Enum[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G]
@@ -212,6 +215,8 @@ sealed trait GlobalDeclaration[G] extends Declaration[G] with GlobalDeclarationI
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
 final class AxiomaticDataType[G](val decls: Seq[ADTDeclaration[G]], val typeArgs: Seq[Variable[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with AxiomaticDataTypeImpl[G]
 final class Class[G](val declarations: Seq[ClassDeclaration[G]], val supports: Seq[Ref[G, Class[G]]], val intrinsicLockInvariant: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with ClassImpl[G]
+final class VeyMontSeqProg[G](val contract: ApplicableContract[G], val progArgs : Seq[Variable[G]], val threads: Seq[VeyMontThread[G]], val runMethod: ClassDeclaration[G], val methods: Seq[ClassDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with VeyMontSeqProgImpl[G]
+final class VeyMontThread[G](val threadType: Type[G], val args: Seq[Expr[G]])(implicit val o: Origin) extends Declaration[G]
 final class Model[G](val declarations: Seq[ModelDeclaration[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with Declarator[G] with ModelImpl[G]
 final class Function[G](val returnType: Type[G], val args: Seq[Variable[G]], val typeArgs: Seq[Variable[G]],
                val body: Option[Expr[G]], val contract: ApplicableContract[G], val inline: Boolean = false, val threadLocal: Boolean = false)
@@ -405,6 +410,7 @@ final case class AmbiguousThis[G]()(implicit val o: Origin) extends Expr[G] with
 
 final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with ThisObjectImpl[G]
 final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends Expr[G] with ThisModelImpl[G]
+final case class ThisSeqProg[G](cls: Ref[G, VeyMontSeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
 
 final case class AmbiguousResult[G]()(implicit val o: Origin) extends Expr[G] with AmbiguousResultImpl[G] {
   var ref: Option[ResultTarget[G]] = None
@@ -445,6 +451,7 @@ sealed trait HeapDeref[G] extends Expr[G] with HeapDerefImpl[G]
 final case class Deref[G](obj: Expr[G], ref: Ref[G, InstanceField[G]])(val blame: Blame[InsufficientPermission])(implicit val o: Origin) extends Expr[G] with HeapDeref[G] with DerefImpl[G]
 final case class ModelDeref[G](obj: Expr[G], ref: Ref[G, ModelField[G]])(val blame: Blame[ModelInsufficientPermission])(implicit val o: Origin) extends Expr[G] with ModelDerefImpl[G]
 final case class DerefPointer[G](pointer: Expr[G])(val blame: Blame[PointerDerefError])(implicit val o: Origin) extends Expr[G] with DerefPointerImpl[G]
+final case class DerefVeyMontThread[G](ref: Ref[G,VeyMontThread[G]])(implicit val o: Origin) extends Expr[G] with DerefVeyMontThreadImpl[G]
 final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(val blame: Blame[PointerAddError])(implicit val o: Origin) extends Expr[G] with PointerAddImpl[G]
 final case class AddrOf[G](e: Expr[G])(implicit val o: Origin) extends Expr[G] with AddrOfImpl[G]
 final case class FunctionOf[G](binding: Ref[G, Variable[G]], vars: Seq[Ref[G, Variable[G]]])(implicit val o: Origin) extends Expr[G] with FunctionOfImpl[G]
@@ -522,6 +529,7 @@ final case class Star[G](left: Expr[G], right: Expr[G])(implicit val o: Origin)
 final case class Wand[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends Expr[G] with WandImpl[G]
 final case class Scale[G](scale: Expr[G], res: Expr[G])(val blame: Blame[ScaleNegative])(implicit val o: Origin) extends Expr[G] with ScaleImpl[G]
 final case class ScaleByParBlock[G](block: Ref[G, ParBlockDecl[G]], res: Expr[G])(implicit val o: Origin) extends Expr[G] with ScaleByParBlockImpl[G]
+final case class VeyMontCondition[G](condition: Seq[(Ref[G,VeyMontThread[G]],Expr[G])])(implicit val o: Origin) extends Expr[G] with VeyMontConditionImpl[G]
 final case class PolarityDependent[G](onInhale: Expr[G], onExhale: Expr[G])(implicit val o: Origin) extends Expr[G] with PolarityDependentImpl[G]
 
 final case class Unfolding[G](res: Expr[G], body: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends Expr[G] with UnfoldingImpl[G]
@@ -647,6 +655,8 @@ final case class SuperType[G](left: Expr[G], right: Expr[G])(implicit val o: Ori
 final case class IndeterminateInteger[G](min: Expr[G], max: Expr[G])(implicit val o: Origin) extends Expr[G] with IndeterminateIntegerImpl[G]
 
 sealed trait AssignExpression[G] extends Expr[G] with AssignExpressionImpl[G]
+final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
+final case class VeyMontAssignExpression[G](thread : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G]
 final case class PreAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PreAssignExpressionImpl[G]
 final case class PostAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PostAssignExpressionImpl[G]
 
diff --git a/col/src/main/java/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala b/col/src/main/java/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala
new file mode 100644
index 0000000000..64079cd150
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala
@@ -0,0 +1,11 @@
+package vct.col.ast.declaration.global
+
+import vct.col.ast.{Class, Declaration, VeyMontSeqProg}
+import vct.col.ast.util.Declarator
+import vct.col.check.{CheckContext, CheckError}
+import vct.col.origin.Origin
+
+trait VeyMontSeqProgImpl[G] extends Declarator[G] { this: VeyMontSeqProg[G] =>
+  def members: Seq[Declaration[G]] = threads ++ Seq(runMethod) ++ methods
+  override def declarations: Seq[Declaration[G]] = progArgs ++ members
+}
diff --git a/col/src/main/java/vct/col/ast/expr/context/ThisSeqProgImpl.scala b/col/src/main/java/vct/col/ast/expr/context/ThisSeqProgImpl.scala
new file mode 100644
index 0000000000..614f8c7f54
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/expr/context/ThisSeqProgImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.expr.context
+
+import vct.col.ast.{TAnyClass, TSeqProg, ThisSeqProg, Type}
+
+trait ThisSeqProgImpl[G] { this: ThisSeqProg[G] =>
+  override def t: Type[G] = TSeqProg(cls)
+}
\ No newline at end of file
diff --git a/col/src/main/java/vct/col/ast/expr/heap/read/DerefVeyMontThreadImpl.scala b/col/src/main/java/vct/col/ast/expr/heap/read/DerefVeyMontThreadImpl.scala
new file mode 100644
index 0000000000..eec36b6bfe
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/expr/heap/read/DerefVeyMontThreadImpl.scala
@@ -0,0 +1,8 @@
+package vct.col.ast.expr.heap.read
+
+import vct.col.ast.{DerefVeyMontThread, Type}
+
+trait DerefVeyMontThreadImpl[G] {
+  this: DerefVeyMontThread[G] =>
+  override def t: Type[G] = ref.decl.threadType
+}
diff --git a/col/src/main/java/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala b/col/src/main/java/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala
new file mode 100644
index 0000000000..8ca782c4ef
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/expr/op/bool/VeyMontConditionImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.expr.op.bool
+
+import vct.col.ast.{TBool, Type, VeyMontCondition}
+
+trait VeyMontConditionImpl[G] { this: VeyMontCondition[G] =>
+  override def t: Type[G] = TBool()
+}
diff --git a/col/src/main/java/vct/col/ast/lang/PVLLocalImpl.scala b/col/src/main/java/vct/col/ast/lang/PVLLocalImpl.scala
index 3c1f25daa3..8beb75c22a 100644
--- a/col/src/main/java/vct/col/ast/lang/PVLLocalImpl.scala
+++ b/col/src/main/java/vct/col/ast/lang/PVLLocalImpl.scala
@@ -12,5 +12,6 @@ trait PVLLocalImpl[G] { this: PVLLocal[G] =>
     case ref: RefClass[G] => Types.notAValue(ref)
     case ref: RefField[G] => ref.decl.t
     case ref: RefModelField[G] => ref.decl.t
+    case ref: RefVeyMontThread[G] => ref.decl.threadType
   }
 }
\ No newline at end of file
diff --git a/col/src/main/java/vct/col/ast/statement/veymont/VeyMontCommImpl.scala b/col/src/main/java/vct/col/ast/statement/veymont/VeyMontCommImpl.scala
new file mode 100644
index 0000000000..5765b3c4f2
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/statement/veymont/VeyMontCommImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.statement.veymont
+
+import vct.col.ast.{VeyMontCommExpression}
+
+trait VeyMontCommImpl[G] { this: VeyMontCommExpression[G] =>
+
+}
diff --git a/col/src/main/java/vct/col/ast/type/TSeqProgImpl.scala b/col/src/main/java/vct/col/ast/type/TSeqProgImpl.scala
new file mode 100644
index 0000000000..ff52fbc57c
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/type/TSeqProgImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TSeqProg
+
+trait TSeqProgImpl[G] { this: TSeqProg[G] =>
+
+}
diff --git a/col/src/main/java/vct/col/ast/type/TVeyMontThreadImpl.scala b/col/src/main/java/vct/col/ast/type/TVeyMontThreadImpl.scala
new file mode 100644
index 0000000000..7f1c0510cc
--- /dev/null
+++ b/col/src/main/java/vct/col/ast/type/TVeyMontThreadImpl.scala
@@ -0,0 +1,7 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TVeyMontThread
+
+trait TVeyMontThreadImpl[G] { this: TVeyMontThread[G] =>
+
+}
diff --git a/col/src/main/java/vct/col/print/Printer.scala b/col/src/main/java/vct/col/print/Printer.scala
index 0aa892c40f..4738c51191 100644
--- a/col/src/main/java/vct/col/print/Printer.scala
+++ b/col/src/main/java/vct/col/print/Printer.scala
@@ -454,6 +454,10 @@ case class Printer(out: Appendable,
       statement("return", space, result)
     case Assign(target, value) =>
       statement(target, space, "=", space, value)
+    case va: VeyMontAssignExpression[_] =>
+      statement(va.assign.asInstanceOf[Assign[_]].target, space, "=", space, va.assign.asInstanceOf[Assign[_]].value)
+    case vc: VeyMontCommExpression[_] =>
+      statement(vc.assign.asInstanceOf[Assign[_]].target, space, "=", space, vc.assign.asInstanceOf[Assign[_]].value)
     case block: Block[_] =>
       printBlock(block, newline = true)
     case Scope(locals, body) =>
@@ -465,7 +469,11 @@ case class Printer(out: Appendable,
     case Branch(branches) =>
       val `if` = (phrase("if (", branches.head._1, ")"), branches.head._2)
       val others = branches.tail.map {
-        case (cond, impl) => (phrase("else if (", cond, ")"), impl)
+        case (cond, impl) =>
+          if(cond match{ case BooleanValue(value) => value}) { //if cond == true
+            (phrase("else"),impl)
+          } else
+            (phrase("else if(", cond, ")"), impl) //never reached since the two branches in else { if(cond) statement } are mapped separately
       }
       controls(`if` +: others)
     case Switch(expr, body) =>
@@ -473,7 +481,9 @@ case class Printer(out: Appendable,
     case Loop(Block(Nil), cond, Block(Nil), invariant, body) =>
       control(phrase(printLoopInvariant(invariant), newline, "while (", cond, ")"), body)
     case Loop(init, cond, update, invariant, body) =>
-      control(phrase(printLoopInvariant(invariant), newline, "for (", statement_no_semicolon(init), "; ", cond, "; ", statement_no_semicolon(update), ")"), body)
+      if(isSkip(init) && isSkip(update))
+        control(phrase(printLoopInvariant(invariant), newline, "while(", cond, ")"), body)
+      else control(phrase(printLoopInvariant(invariant), newline, "for(", init, "; ", cond, "; ", statement_no_semicolon(update), ")"), body)
     case TryCatchFinally(body, after, catches) =>
       controls(
         Seq((phrase("try"), body)) ++
@@ -735,6 +745,11 @@ case class Printer(out: Appendable,
       phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")")
   }
 
+  private def isSkip(st: Statement[_]): Boolean = st match {
+    case Block(stmts) => stmts.isEmpty
+    case _ => false
+  }
+
   def printExpr(e: Expr[_]): Unit =
     say(expr(e)._1)
 
@@ -833,6 +848,8 @@ case class Printer(out: Appendable,
       (phrase("running", "(", thread, ")"), 100)
     case Starall(bindings, triggers, body) =>
       (phrase("(", "\\forall*", space, commas(bindings.map(NodePhrase)), "; true; ", body, ")"), 120)
+    case VeyMontCondition(c) =>
+      (phrase(intersperse(" && ", c.map{case (t,e) => e})),40)
     case Star(left, right) =>
       (phrase(assoc(40, left), space, "**", space, assoc(40, right)), 40)
     case Wand(left, right) =>
@@ -927,6 +944,7 @@ case class Printer(out: Appendable,
       (phrase(name(ref.decl)), 110)
     case Deref(obj, ref) =>
       (phrase(assoc(100, obj), ".", name(ref.decl)), 100)
+    case DerefVeyMontThread(ref) => (phrase(name(ref.decl)), 110)
     case ModelDeref(obj, ref) =>
       (phrase(assoc(100, obj), ".", name(ref.decl)), 100)
     case DerefPointer(pointer) =>
@@ -946,7 +964,10 @@ case class Printer(out: Appendable,
     case FunctionInvocation(ref, args, typeArgs, givenMap, yields) =>
       (phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
     case MethodInvocation(obj, ref, args, outArgs, typeArgs, givenMap, yields) =>
-      (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+      obj match {
+        case o:ThisSeqProg[_] => (phrase(name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+        case _ => (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
+      }
     case InstanceFunctionInvocation(obj, ref, args, typeArgs, givenMap, yields) =>
       (phrase(assoc(100, obj), ".", name(ref.decl), "(", commas(args.map(NodePhrase)), ")"), 100)
     case UMinus(arg) =>
@@ -1005,12 +1026,16 @@ case class Printer(out: Appendable,
       (phrase(bind(60, left), space, ">", space, bind(60, right)), 60)
     case Less(left, right) =>
       (phrase(bind(60, left), space, "<", space, bind(60, right)), 60)
+    case AmbiguousLess(left, right) =>
+      (phrase(bind(60, left), space, "<", space, bind(60, right)), 60)
     case AmbiguousGreaterEq(left, right) =>
       (phrase(bind(60, left), space, ">=", space, bind(60, right)), 60)
     case GreaterEq(left, right) =>
       (phrase(bind(60, left), space, ">=", space, bind(60, right)), 60)
     case LessEq(left, right) =>
       (phrase(bind(60, left), space, "<=", space, bind(60, right)), 60)
+    case AmbiguousLessEq(left, right) =>
+      (phrase(bind(60, left), space, "<=", space, bind(60, right)), 60)
     case SubSet(left, right) =>
       ???
     case SubSetEq(left, right) =>
@@ -1377,6 +1402,21 @@ case class Printer(out: Appendable,
       ???
     case field: ModelField[_] =>
       ???
+    case seqprog: VeyMontSeqProg[_] => phrase(
+      doubleline,
+      seqprog.contract, newline,
+      "seq_program", space, name(seqprog),"(",commas(seqprog.progArgs.map(NodePhrase)) ,")", space, "{",
+      indent(phrase(seqprog.members.map(NodePhrase): _*)),
+      "}",
+      doubleline)
+    case thread: VeyMontThread[_] => phrase(newline,"thread",space,name(thread),space,"=",space,thread.threadType,"(",commas(thread.args.map(NodePhrase)),")",newline)
+    case runMethod : RunMethod[_] => {
+      val header = phrase(runMethod.contract,"run")
+      runMethod.body match {
+        case Some(body) => control(header, body)
+        case None => phrase(doubleline, header, ";", doubleline)
+      }
+    }
   })
 
   def printApplicableContract(node: ApplicableContract[_]): Unit =
diff --git a/col/src/main/java/vct/col/resolve/ctx/Referrable.scala b/col/src/main/java/vct/col/resolve/ctx/Referrable.scala
index c6727b34a2..9a463d3cb3 100644
--- a/col/src/main/java/vct/col/resolve/ctx/Referrable.scala
+++ b/col/src/main/java/vct/col/resolve/ctx/Referrable.scala
@@ -56,6 +56,8 @@ sealed trait Referrable[G] {
     case RefModelField(decl) => Referrable.originName(decl)
     case RefModelProcess(decl) => Referrable.originName(decl)
     case RefModelAction(decl) => Referrable.originName(decl)
+    case RefSeqProg(decl) => Referrable.originName(decl)
+    case RefVeyMontThread(decl) => Referrable.originName(decl)
     case BuiltinField(_) => ""
     case BuiltinInstanceMethod(_) => ""
     case RefPVLConstructor(decl) => ""
@@ -119,6 +121,8 @@ case object Referrable {
     case decl: CLocalDeclaration[G] => return decl.decl.inits.indices.map(RefCLocalDeclaration(decl, _))
     case decl: JavaLocalDeclaration[G] => return decl.decls.indices.map(RefJavaLocalDeclaration(decl, _))
     case decl: PVLConstructor[G] => RefPVLConstructor(decl)
+    case decl: VeyMontSeqProg[G] => RefSeqProg(decl)
+    case decl: VeyMontThread[G] => RefVeyMontThread(decl)
     case decl: JavaBipGlueContainer[G] => RefJavaBipGlueContainer()
   })
 
@@ -218,6 +222,9 @@ case class RefJavaBipStatePredicate[G](state: String, decl: JavaAnnotation[G]) e
 case class RefJavaBipGuard[G](decl: JavaMethod[G]) extends Referrable[G] with JavaNameTarget[G]
 case class RefJavaBipGlueContainer[G]() extends Referrable[G] // Bip glue jobs are not actually referrable
 
+case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G]
+case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G]
+
 case class BuiltinField[G](f: Expr[G] => Expr[G]) extends Referrable[G] with SpecDerefTarget[G]
 case class BuiltinInstanceMethod[G](f: Expr[G] => Seq[Expr[G]] => Expr[G]) extends Referrable[G] with SpecInvocationTarget[G]
 
diff --git a/col/src/main/java/vct/col/typerules/CoercingRewriter.scala b/col/src/main/java/vct/col/typerules/CoercingRewriter.scala
index ca2fff4d25..1ef7bdc0e7 100644
--- a/col/src/main/java/vct/col/typerules/CoercingRewriter.scala
+++ b/col/src/main/java/vct/col/typerules/CoercingRewriter.scala
@@ -841,10 +841,13 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         CurPerm(loc)
       case CurrentThreadId() =>
         CurrentThreadId()
+      //case deref @ DerefVeyMontThread(ref) =>
+        //DerefVeyMontThread( TVeyMontThread[Pre](ref))
       case deref @ Deref(obj, ref) =>
         Deref(cls(obj), ref)(deref.blame)
       case deref @ DerefPointer(p) =>
         DerefPointer(pointer(p)._1)(deref.blame)
+      case deref @ DerefVeyMontThread(ref) => deref
       case div @ Div(left, right) =>
         firstOk(e, s"Expected both operands to be rational.",
           // PB: horrible hack: Div ends up being silver.PermDiv, which expects an integer divisor. In other cases,
@@ -1022,7 +1025,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case MatrixSum(indices, mat) =>
         MatrixSum(coerce(indices, TSeq[Pre](TInt())), coerce(mat, TSeq[Pre](TRational())))
       case inv @ MethodInvocation(obj, ref, args, outArgs, typeArgs, givenMap, yields) =>
-        MethodInvocation(cls(obj), ref, coerceArgs(args, ref.decl, typeArgs), outArgs, typeArgs, coerceGiven(givenMap), coerceYields(yields, inv))(inv.blame)
+        MethodInvocation(obj, ref, coerceArgs(args, ref.decl, typeArgs), outArgs, typeArgs, coerceGiven(givenMap), coerceYields(yields, inv))(inv.blame)
       case Minus(left, right) =>
         firstOk(e, s"Expected both operands to be numeric, but got ${left.t} and ${right.t}.",
           Minus(int(left), int(right)),
@@ -1265,6 +1268,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         Then(value, post)
       case ThisModel(ref) =>
         ThisModel(ref)
+      case ThisSeqProg(ref) =>
+        ThisSeqProg(ref)
       case ThisObject(ref) =>
         ThisObject(ref)
       case TupGet(tup, index) =>
@@ -1318,6 +1323,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         With(pre, value)
       case WritePerm() =>
         WritePerm()
+      case VeyMontCondition(c) => VeyMontCondition(c)
       case localIncoming: BipLocalIncomingData[Pre] => localIncoming
       case glue: JavaBipGlue[Pre] => glue
     }
@@ -1391,6 +1397,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case w @ Wait(obj) => Wait(cls(obj))(w.blame)
       case w @ WandApply(assn) => WandApply(res(assn))(w.blame)
       case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
+      case VeyMontAssignExpression(t,a) => VeyMontAssignExpression(t,a)
+      case VeyMontCommExpression(r,s,a) => VeyMontCommExpression(r,s,a)
     }
   }
 
@@ -1493,6 +1501,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
           case JavaVariableDeclaration(name, dims, Some(v)) =>
             JavaVariableDeclaration(name, dims, Some(coerce(v, FuncTools.repeat[Type[Pre]](TArray(_), dims, declaration.t))))
         })
+      case seqProg: VeyMontSeqProg[Pre] => seqProg
+      case thread: VeyMontThread[Pre] => thread
       case bc: BipComponent[Pre] =>
         new BipComponent(bc.fqn, bc.constructors, res(bc.invariant), bc.initial)
       case bsp: BipStatePredicate[Pre] =>
diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/examples/technical/veymont-seq-progs/veymont-swap.pvl
new file mode 100644
index 0000000000..72e1c70988
--- /dev/null
+++ b/examples/technical/veymont-seq-progs/veymont-swap.pvl
@@ -0,0 +1,65 @@
+class Storage {
+  int v, temp;
+
+  constructor(int v) {
+    this.v = v;
+  }
+  
+  void inc() {
+  	v = v+1;
+  }
+  
+  int num() {
+  	return 2;
+  }
+  
+  void bla(int b) {}
+}
+
+
+requires x >= 0;
+seq_program SeqProgram(int x, int y) {
+   thread s1 = Storage(x);
+   thread s2 = Storage(y);
+
+  int num() {}
+  
+  void foo() {
+     s1.temp = 5;
+  }
+  
+  void bar(int a) {}
+
+  run {
+    if(s1.v == 5 && s2.v == 6) {
+    	s1.temp = s1.num();
+ //     s1.temp = num();
+ //       s1.temp = s1.v + s2.v;
+ 
+    } else if(s1.v == 0 && s2.v == 0) {
+    	while(s1.temp == 1 && s2.v == 3) {
+    	  s1.temp = 5;
+    	}
+    }
+    for(s1.temp = 0; s1.temp > 10 && s2.v == 6; s1.v = s1.v+1) {
+    	s2.temp = 6;
+    }
+//    if(s1.temp > 10 && s1.v == 6) {
+    	s2.v = 2;
+//    }
+    s1.temp = s1.v;
+    s2.temp = s2.v;
+    foo();
+    //bar(1);
+    s1.inc();
+    s1.bla(s1.temp);
+    // s1.bla(s2.temp);
+    s1.v = s2.temp;
+    s2.v = s1.temp;
+    assert s1.v == \old(s2.v);
+    assert s2.v == \old(s1.v);
+  }
+  
+  
+}
+
diff --git a/parsers/lib/antlr4/LangPVLLexer.g4 b/parsers/lib/antlr4/LangPVLLexer.g4
index 92b6a866a3..0dbc74136b 100644
--- a/parsers/lib/antlr4/LangPVLLexer.g4
+++ b/parsers/lib/antlr4/LangPVLLexer.g4
@@ -48,11 +48,13 @@ CONS: '::';
 
 ENUM: 'enum';
 CLASS: 'class';
+SEQ_PROGRAM: 'seq_program';
 KERNEL: 'kernel';
 BARRIER: 'barrier';
 INVARIANT: 'invariant';
 CONSTRUCTOR: 'constructor';
 RUN: 'run';
+THREAD: 'thread';
 
 IF: 'if';
 ELSE: 'else';
diff --git a/parsers/lib/antlr4/LangPVLParser.g4 b/parsers/lib/antlr4/LangPVLParser.g4
index 5afce9c6d4..e822538302 100644
--- a/parsers/lib/antlr4/LangPVLParser.g4
+++ b/parsers/lib/antlr4/LangPVLParser.g4
@@ -6,7 +6,7 @@ parser grammar LangPVLParser;
 
 program  : programDecl* EOF EOF ;
 
-programDecl : valGlobalDeclaration | declClass | enumDecl | method;
+programDecl : valGlobalDeclaration | declClass | enumDecl | method | declVeyMontSeqProg;
 
 enumDecl : 'enum' identifier '{' identifierList? ','? '}' ;
 
@@ -14,6 +14,14 @@ declClass
  : contract 'class' identifier '{' classDecl* '}'
  ;
 
+declVeyMontSeqProg : contract 'seq_program' identifier '(' args? ')' '{' seqProgDecl* '}';
+
+seqProgDecl
+ : 'thread' identifier '=' type '(' exprList? ')' ';' # seqProgThread
+ | runMethod # seqProgRunMethod
+ | method # seqProgMethod
+ ;
+
 applicableReference
  : identifier '.' identifier # pvlAdtFunctionRef
  | identifier                # pvlFunctionRef
diff --git a/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala b/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala
index aa53a57622..5fe14ba033 100644
--- a/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala
+++ b/parsers/src/main/java/vct/parsers/transform/PVLToCol.scala
@@ -28,6 +28,7 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
     case ProgramDecl1(cls) => Seq(convert(cls))
     case ProgramDecl2(enum) => Seq(convert(enum))
     case ProgramDecl3(method) => Seq(convertProcedure(method))
+    case ProgramDecl4(seqProg) => Seq(convertVeyMontProg(seqProg))
   }
 
   def convert(implicit enum: EnumDeclContext): Enum[G] = enum match {
@@ -40,6 +41,35 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
     case IdentifierList1(id, _, tail) => new vct.col.ast.EnumConstant[G]()(SourceNameOrigin(convert(id), origin(identifierList))) +: convertConstants(tail)
   }
 
+  def convert(implicit decl: SeqProgDeclContext): Declaration[G] = decl match {
+    case SeqProgMethod(methods) => convert(methods)
+    case SeqProgRunMethod(runMethod) => convert(runMethod).head
+    case SeqProgThread(_, threadId, _, threadType, _, args, _, _) => new VeyMontThread(convert(threadType), args.map(convert(_)).getOrElse(Nil))(SourceNameOrigin(convert(threadId), origin(decl)))
+  }
+
+  def convertVeyMontProg(implicit cls: DeclVeyMontSeqProgContext): VeyMontSeqProg[G] = cls match {
+    case DeclVeyMontSeqProg0(contract, _, name, _, args, _, _, decls, _) =>
+      val seqargs = args.map(convert(_)).getOrElse(Nil)
+      val declseq: Seq[Declaration[G]] = decls.map(convert(_))
+      val runMethod = declseq.collectFirst {
+        case x: RunMethod[G] => x
+      }.getOrElse(throw new RuntimeException("A seq_prog needs to have a run method, but none was found!"))
+      val methods = declseq.collect {
+        case m: InstanceMethod[G] => m
+      }
+      val threads = declseq.collect {
+        case v: VeyMontThread[G] => v
+      }
+      withContract(contract, contract => {
+        new VeyMontSeqProg(
+          contract.consumeApplicableContract(blame(cls)),
+          seqargs,
+          threads,
+          runMethod,
+          methods)(SourceNameOrigin(convert(name), origin(cls)))
+      })
+  }
+
   def convertProcedure(implicit method: MethodContext): Procedure[G] = method match {
     case Method0(contract, modifiers, returnType, name, _, args, _, body) =>
       withModifiers(modifiers, mods => withContract(contract, contract => {
diff --git a/project/ColDefs.scala b/project/ColDefs.scala
index 7ace482605..9c5c89626d 100644
--- a/project/ColDefs.scala
+++ b/project/ColDefs.scala
@@ -37,6 +37,7 @@ object ColDefs {
     "CLocalDeclaration",
     "CParam",
     "JavaLocalDeclaration",
+    "VeyMontThread",
     "JavaParam",
   )
 
@@ -85,6 +86,7 @@ object ColDefs {
       "JavaConstructor", "JavaMethod",
       "Scope",
     ),
+    "VeyMontThread" -> Seq("VeyMontSeqProg"),
     "JavaParam" -> Seq("JavaMethod", "JavaAnnotationMethod", "JavaConstructor"),
   )
 
diff --git a/project/ColHelperDeserialize.scala b/project/ColHelperDeserialize.scala
index 54259a4c0f..ab5b25a54d 100644
--- a/project/ColHelperDeserialize.scala
+++ b/project/ColHelperDeserialize.scala
@@ -29,26 +29,28 @@ case class ColHelperDeserialize(info: ColDescription, proto: ColProto) extends C
       })
     """)
 
-  def deserializeTerm(term: Term, typ: proto.Typ): Term =
+  def lastTypeArg(t: Type): Type = t.asInstanceOf[Type.Apply].args.last
+
+  def deserializeTerm(term: Term, typ: proto.Typ, scalaTyp: Type): Term =
     proto.primitivize(typ) match {
       case proto.TName("ExpectedErrors") => q"Nil"
 
       case proto.TBool => term
-      case r @ proto.TRef() => q"ref[${r.scalaArg}]($term.index)"
+      case r @ proto.TRef() => q"ref[${lastTypeArg(scalaTyp)}]($term.index)"
       case proto.TInt => term
       case proto.TBigInt => q"BigInt(new java.math.BigInteger($term.data.toByteArray()))"
-      case proto.TBigDecimal => q"BigDecimal(${deserializeTerm(q"$term.unscaledValue", proto.TBigInt)}, $term.scale)"
+      case proto.TBigDecimal => q"BigDecimal(${deserializeTerm(q"$term.unscaledValue", proto.TBigInt, null)}, $term.scale)"
       case proto.TString => term
-      case proto.TOption(t) => q"$term.map(e => ${deserializeTerm(q"e", t)})"
-      case proto.TSeq(t) => q"$term.map(e => ${deserializeTerm(q"e", t)})"
-      case proto.TSet(t) => q"$term.map(e => ${deserializeTerm(q"e", t)}).toSet"
+      case proto.TOption(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))})"
+      case proto.TSeq(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))})"
+      case proto.TSet(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))}).toSet"
       case typ @ proto.TName(name) if proto.boxedTypeFamily.contains(typ) => q"deserialize($term)"
-      case typ @ proto.TName(name) if proto.boxedTypeForward.contains(typ) => deserializeTerm(q"$term.v", proto.boxedTypeForward(typ))
+      case typ @ proto.TName(name) if proto.boxedTypeForward.contains(typ) => deserializeTerm(q"$term.v", proto.boxedTypeForward(typ), scalaTyp)
       case typ @ proto.TName(name) if proto.boxedTypeTuple.contains(typ) =>
         q"""(..${
           val ts = proto.boxedTypeTuple(typ).ts
           ts.zipWithIndex.map {
-            case (typ, i) => deserializeTerm(Term.Select(term, Term.Name(s"v${i+1}")), typ)
+            case (typ, i) => deserializeTerm(Term.Select(term, Term.Name(s"v${i+1}")), typ, scalaTyp.asInstanceOf[Type.Tuple].args(i))
           }.toList
         })"""
       case _ => ColHelperUtil.fail(s"Unknown type $typ")
@@ -58,7 +60,7 @@ case class ColHelperDeserialize(info: ColDescription, proto: ColProto) extends C
   // contextEverywhere (Node.scala) -> context_everywhere (proto) -> contextEverywhere (scalapb)
   // context_everywhere (Node.scala; poor style) -> context_everywhere (proto) -> contextEverywhere (scalapb)
   def deserializeParam(defn: ClassDef)(param: Term.Param): Term =
-    deserializeTerm(q"node.${Term.Name(proto.Name(param.name.value).camel)}", proto.getType(param.decltpe.get))
+    deserializeTerm(q"node.${Term.Name(proto.Name(param.name.value).camel)}", proto.getType(param.decltpe.get), param.decltpe.get)
 
   def makeNodeDeserialize(defn: ClassDef): List[Stat] = List(q"""
     def ${Term.Name("deserialize" + defn.baseName)}(node: ${serType(defn.baseName)}): ${defn.typ}[G] =
diff --git a/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala b/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
index e08728f43f..09468bddad 100644
--- a/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
+++ b/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
@@ -8,7 +8,7 @@ import vct.col.util.AstBuildHelpers._
 import vct.col.ast.RewriteHelpers._
 import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
 import vct.col.ref.Ref
-import vct.col.resolve.ctx.{BuiltinField, BuiltinInstanceMethod, ImplicitDefaultPVLConstructor, PVLBuiltinInstanceMethod, RefADTFunction, RefAxiomaticDataType, RefClass, RefEnum, RefEnumConstant, RefField, RefFunction, RefInstanceFunction, RefInstanceMethod, RefInstancePredicate, RefModel, RefModelAction, RefModelField, RefModelProcess, RefPVLConstructor, RefPredicate, RefProcedure, RefVariable}
+import vct.col.resolve.ctx.{BuiltinField, BuiltinInstanceMethod, ImplicitDefaultPVLConstructor, PVLBuiltinInstanceMethod, RefADTFunction, RefAxiomaticDataType, RefClass, RefEnum, RefEnumConstant, RefField, RefFunction, RefInstanceFunction, RefInstanceMethod, RefInstancePredicate, RefModel, RefModelAction, RefModelField, RefModelProcess, RefPVLConstructor, RefPredicate, RefProcedure, RefVariable, RefVeyMontThread}
 import vct.col.util.{AstBuildHelpers, SuccessionMap}
 
 case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends LazyLogging {
@@ -80,6 +80,7 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
       case RefModelField(decl) => ModelDeref[Post](rw.currentThis.top, rw.succ(decl))(local.blame)
       case RefClass(decl) => throw NotAValue(local)
       case RefField(decl) => Deref[Post](rw.currentThis.top, rw.succ(decl))(local.blame)
+      case RefVeyMontThread(decl) => DerefVeyMontThread[Post](rw.succ(decl))
     }
   }
 
diff --git a/rewrite/src/main/java/vct/col/rewrite/lang/LangSpecificToCol.scala b/rewrite/src/main/java/vct/col/rewrite/lang/LangSpecificToCol.scala
index 9ef4c000d4..969977afcb 100644
--- a/rewrite/src/main/java/vct/col/rewrite/lang/LangSpecificToCol.scala
+++ b/rewrite/src/main/java/vct/col/rewrite/lang/LangSpecificToCol.scala
@@ -47,6 +47,11 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
       currentThis.having(ThisModel[Post](succ(model))) {
         globalDeclarations.succeed(model, model.rewrite())
       }
+    case seqProg: VeyMontSeqProg[Pre] =>
+      implicit val o: Origin = seqProg.o
+      currentThis.having(ThisSeqProg[Post](succ(seqProg))) {
+        globalDeclarations.succeed(seqProg, seqProg.rewrite())
+      }
 
     case ns: JavaNamespace[Pre] => java.rewriteNamespace(ns)
     case cls: JavaClassOrInterface[Pre] => java.rewriteClass(cls)
diff --git a/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontAssignmentNodes.scala b/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontAssignmentNodes.scala
new file mode 100644
index 0000000000..f3c19ff228
--- /dev/null
+++ b/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontAssignmentNodes.scala
@@ -0,0 +1,103 @@
+package vct.col.rewrite.veymont
+
+import hre.util.ScopedStack
+import vct.col.ast.{Assign, Declaration, Deref, DerefVeyMontThread, Expr, MethodInvocation, Node, ProcedureInvocation, RunMethod, Statement, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
+import vct.col.ref.Ref
+import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{AddVeyMontAssignmentError, getDerefsFromExpr, getThreadDeref}
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+import vct.result.VerificationError.UserError
+
+object AddVeyMontAssignmentNodes extends RewriterBuilder {
+
+  override def key: String = "addVeyMontAssignmentNodes"
+
+  override def desc: String = "Add nodes for VeyMont assignments"
+
+  case class AddVeyMontAssignmentError(node : Node[_], msg: String) extends UserError {
+    override def code: String = "addVeyMontAssignmentError"
+
+    override def text: String = node.o.messageInContext(msg)
+  }
+
+  /**
+   * Utility function to extract all derefs from an expression
+   * @param exp
+   * @tparam Pre
+   * @return
+   */
+  def getDerefsFromExpr[Pre](exp : Expr[Pre]): Seq[Deref[Pre]] = {
+    exp.collect { case d@Deref(_, _) => d }.distinct
+  }
+
+  /**
+   * Utility function to get VeyMontThread from a Deref, and throw error err in case of other dereferences
+   * @param deref to be matched
+   * @param err to be thrown if match unsuccessful
+   * @tparam Pre type of expression
+   * @return list of threads that are dereferenced in the expression
+   */
+  def getThreadDeref[Pre](deref: Deref[Pre], err: UserError) : VeyMontThread[Pre] = deref.obj match {
+    case DerefVeyMontThread(threadref) => threadref.decl
+    case _ => throw err
+  }
+
+}
+case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre] {
+
+  val inSeqProg: ScopedStack[Unit] = ScopedStack()
+
+  override def dispatch(decl: Declaration[Pre]): Unit =
+    decl match {
+      case dcl: VeyMontSeqProg[Pre] => inSeqProg.having(()) {
+        rewriteDefault(dcl)
+      }
+      case _ => rewriteDefault(decl)
+    }
+
+  override def dispatch(st: Statement[Pre]): Statement[Post] = st match {
+      case a@Assign(target, value) =>
+        if(inSeqProg.nonEmpty) {
+          val receiver = getAssignmentReceiver(target)
+          checkAssignmentMethodCalls(value)
+          createVeyMontAssignNode(receiver,a)
+        } else rewriteDefault(st)
+      case _ => rewriteDefault(st)
+    }
+
+  def getAssignmentReceiver(target: Expr[Pre]): VeyMontThread[Pre] = target match {
+    case Deref(obj, _) => obj match {
+      case DerefVeyMontThread(ref) =>  ref.decl//target is correct ref to thread
+      case _ => throw AddVeyMontAssignmentError(target, "The target of this assignment must refer to a thread")
+    }
+    case _ => throw AddVeyMontAssignmentError(target, "The target of this assignment must be a dereference to a thread, e.g. someThread.someField")
+  }
+
+  /**
+   *
+   * @param value is the expression to be checked on occurring method calls.
+   * @return Whether all method calls of the assignment are method calls on thread objects
+   */
+  private def checkAssignmentMethodCalls(value: Expr[Pre]): Boolean = {
+    !value.exists {
+      case m: ProcedureInvocation[Pre] => throw AddVeyMontAssignmentError(m, "Cannot call non-thread method in assignment!")
+      case m: MethodInvocation[Pre] => m.obj match {
+        case t: DerefVeyMontThread[Pre] => false
+        case m => throw AddVeyMontAssignmentError(m, "Cannot call non-thread method in assignment!")
+      }
+    }
+  }
+
+  def createVeyMontAssignNode(receiver: VeyMontThread[Pre], a: Assign[Pre]): Statement[Post] = {
+    val derefs = getDerefsFromExpr(a.value)
+    if (derefs.isEmpty)
+      new VeyMontAssignExpression[Post](succ(receiver), rewriteDefault(a))(a.o)
+    else if (derefs.size == 1) {
+      val sender = getAssignmentSender(derefs.head)
+      new VeyMontCommExpression[Post](succ(receiver), succ(sender), rewriteDefault(a))(a.o)
+    } else throw AddVeyMontAssignmentError(a.value, "The value of this assignment is not allowed to refer to multiple threads!")
+  }
+
+  def getAssignmentSender(deref : Deref[Pre]): VeyMontThread[Pre] =
+    getThreadDeref(deref,AddVeyMontAssignmentError (deref, "Object identifiers in the value of this assignment can only refer to a thread!") )
+
+}
diff --git a/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontConditionNodes.scala b/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontConditionNodes.scala
new file mode 100644
index 0000000000..5b8d55a9b8
--- /dev/null
+++ b/rewrite/src/main/java/vct/col/rewrite/veymont/AddVeyMontConditionNodes.scala
@@ -0,0 +1,108 @@
+package vct.col.rewrite.veymont
+
+
+import hre.util.ScopedStack
+import vct.col.ast.{And, Block, BooleanValue, Branch, Declaration, Expr, Loop, Node, Statement, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ref.Ref
+import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{getDerefsFromExpr, getThreadDeref}
+import vct.col.rewrite.veymont.AddVeyMontConditionNodes.AddVeyMontConditionError
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+import vct.result.VerificationError.UserError
+
+import scala.reflect.internal.util.TriState.True
+
+object AddVeyMontConditionNodes  extends RewriterBuilder {
+  override def key: String = "addVeyMontConditionNodes"
+
+  override def desc: String = "Add nodes for VeyMont conditions"
+
+  case class AddVeyMontConditionError(node : Node[_], msg: String) extends UserError {
+    override def code: String = "addVeyMontConditionError"
+
+    override def text: String = node.o.messageInContext(msg)
+  }
+}
+
+case class AddVeyMontConditionNodes[Pre <: Generation]() extends Rewriter[Pre] {
+
+  val inSeqProg: ScopedStack[Int] = ScopedStack()
+
+  override def dispatch(decl: Declaration[Pre]): Unit =
+    decl match {
+      case dcl: VeyMontSeqProg[Pre] =>
+        inSeqProg.push(dcl.threads.size)
+        try {
+          rewriteDefault(dcl)
+        } finally {
+          inSeqProg.pop()
+        }
+      case _ => rewriteDefault(decl)
+    }
+
+  override def dispatch(st: Statement[Pre]): Statement[Post] = {
+    if(inSeqProg.nonEmpty) {
+      st match {
+      case Branch(branches) => {
+        val postbranches = branches.map{case (c,s) => rewriteBranch(c,s)}
+        Branch(postbranches)(st.o)
+      }
+      case l: Loop[Pre] =>
+          rewriteLoop(l)
+      case _ => rewriteDefault(st)
+      }
+    } else rewriteDefault(st)
+  }
+
+  private def rewriteBranch(cond: Expr[Pre], st: Statement[Pre]) : (Expr[Post],Statement[Post]) = {
+    val condMap = checkConditionAndGetConditionMap(cond)
+    if(condMap.isEmpty) //in case of else statement
+      (dispatch(cond),dispatch(st))
+    else (VeyMontCondition[Post](condMap.toList)(st.o), dispatch(st))
+  }
+
+  private def rewriteLoop(l: Loop[Pre]): Loop[Post] = {
+    val condMap = checkConditionAndGetConditionMap(l.cond)
+    if (condMap.isEmpty)
+      throw AddVeyMontConditionError(l.cond, "Conditions of loops cannot be `true'!")
+    else  Loop(rewriteDefault(l.init),
+      VeyMontCondition[Post](condMap.toList)(l.cond.o),
+      rewriteDefault(l.update),
+      rewriteDefault(l.contract),
+      dispatch(l.body))(l.o)
+  }
+
+  private def checkConditionAndGetConditionMap(e: Expr[Pre]): Map[Ref[Post, VeyMontThread[Post]], Expr[Post]] = {
+    if (isTrue(e))
+      Map.empty
+    else {
+      val condEls = collectConditionElements(e)
+      val m = getConditionMap(condEls,e)
+      if(m.keys.toSet.size == inSeqProg.top) {
+        m
+      } else throw AddVeyMontConditionError(e, "Conditions of if/while need to reference each thread exactly once!")
+    }
+  }
+
+  private def getConditionMap(condEls: List[Expr[Pre]], e : Expr[Pre]): Map[Ref[Post, VeyMontThread[Post]], Expr[Post]] = {
+    val derefs = condEls.map(el => (getDerefsFromExpr(el), el))
+    derefs.foldRight(Map.empty[Ref[Post, VeyMontThread[Post]], Expr[Post]]) { case ((d, el), m) =>
+      if (d.size != 1)
+        throw AddVeyMontConditionError(e, "Conditions of if/while need to reference each thread exactly once!")
+      else {
+        val thread = getThreadDeref(d.head, AddVeyMontConditionError(e, "Conditions of if/while can only reference threads, so nothing else!"))
+        m + (succ(thread) -> dispatch(el))
+      }
+    }
+  }
+
+  private def isTrue(e : Expr[Pre]) = e match {
+    case BooleanValue(value) => value
+    case _ => false
+  }
+
+  private def collectConditionElements(e: Expr[Pre]) : List[Expr[Pre]] = e match {
+    case And(left,right) => collectConditionElements(left) ++ collectConditionElements(right)
+    case _ => List(e)
+  }
+
+}
diff --git a/rewrite/src/main/java/vct/col/rewrite/veymont/StructureCheck.scala b/rewrite/src/main/java/vct/col/rewrite/veymont/StructureCheck.scala
new file mode 100644
index 0000000000..897517f779
--- /dev/null
+++ b/rewrite/src/main/java/vct/col/rewrite/veymont/StructureCheck.scala
@@ -0,0 +1,83 @@
+package vct.col.rewrite.veymont
+
+import hre.util.ScopedStack
+import vct.col.ast._
+import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.{getDerefsFromExpr,getThreadDeref}
+import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+import vct.result.VerificationError.UserError
+
+object StructureCheck extends RewriterBuilder {
+
+  override def key: String = "structureCheck"
+
+  override def desc: String = "Check if program adheres to syntax of VeyMont input program"
+
+  case class VeyMontStructCheckError(node : Node[_], msg: String) extends UserError { //SystemErrir fir unreachable errros
+    override def code: String = "veyMontStructCheckError"
+
+    override def text: String = node.o.messageInContext(msg)
+  }
+
+}
+
+case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
+
+  val inSeqProg: ScopedStack[Unit] = ScopedStack()
+
+  override def dispatch(decl: Declaration[Pre]): Unit =
+    decl match {
+      case dcl: VeyMontSeqProg[Pre] => inSeqProg.having(()) {
+        rewriteDefault(dcl)
+      }
+      case _ => rewriteDefault(decl)
+    }
+
+  override def dispatch(prog : Program[Pre]) : Program[Post] = {
+    if(!prog.declarations.exists {
+      case dcl: VeyMontSeqProg[Pre] =>
+        if(dcl.threads.isEmpty)
+          throw VeyMontStructCheckError(dcl,"A seq_program needs to have at least 1 thread, but none was found!")
+        else true
+      case _ => false
+    })
+      throw VeyMontStructCheckError(prog,"VeyMont requires a seq_program, but none was found!")
+    else rewriteDefault(prog)
+  }
+
+  override def dispatch(st : Statement[Pre]) : Statement[Post] = {
+    if(inSeqProg.nonEmpty)
+      st match {
+        case VeyMontCommExpression(_,_,_) => rewriteDefault(st)
+        case VeyMontAssignExpression(_,_) => rewriteDefault (st)
+        case Assign(_,_) => rewriteDefault (st)
+        case Branch(_) => rewriteDefault(st)
+        case Loop(_,_,_,_,_) => rewriteDefault(st)
+        case Scope(_,_) => rewriteDefault(st)
+        case Block(_) => rewriteDefault(st)
+        case Eval(expr) => checkMethodCall(st, expr)
+        case Assert(_) => rewriteDefault(st)
+        case _ => throw VeyMontStructCheckError(st,"Statement not allowed in seq_program")
+      }
+    else rewriteDefault(st)
+  }
+
+
+  private def checkMethodCall(st: Statement[Pre], expr: Expr[Pre]): Statement[Post] = {
+    expr match {
+      case MethodInvocation(obj, _, args, _, _, _, _) => obj match {
+        case ThisSeqProg(_) =>
+          if (args.isEmpty) rewriteDefault(st)
+          else throw VeyMontStructCheckError(st, "Calls to methods in seq_program cannot have any arguments!")
+        case DerefVeyMontThread(thread) =>
+          val argderefs = args.flatMap(getDerefsFromExpr)
+          val argthreads = argderefs.map(d => getThreadDeref(d,
+            VeyMontStructCheckError(st, "A method call on a thread object may only refer to a thread in its arguments!")))
+          if (argthreads.forall(_ == thread.decl))
+            rewriteDefault(st)
+          else throw VeyMontStructCheckError(st, "A method call on a thread object may only refer to same thread in its arguments!")
+        case _ => throw VeyMontStructCheckError(st, "This kind of method call is not allowed in seq_program")
+      }
+    }
+  }
+}
diff --git a/src/main/java/vct/main/Main.scala b/src/main/java/vct/main/Main.scala
index 641e409a4c..fd76dbddc0 100644
--- a/src/main/java/vct/main/Main.scala
+++ b/src/main/java/vct/main/Main.scala
@@ -8,6 +8,7 @@ import org.slf4j.LoggerFactory
 import scopt.OParser
 import vct.col.ast.Node
 import vct.main.modes.Verify
+import vct.main.modes.VeyMont
 import vct.main.modes.Transform
 import vct.main.stages.Transformation
 import vct.options.types.{Mode, Verbosity}
@@ -92,7 +93,7 @@ case object Main extends LazyLogging {
             logger.info(s"    ${pass.desc}")
           }
           EXIT_CODE_SUCCESS
-        case Mode.VeyMont => ???
+        case Mode.VeyMont => VeyMont.runOptions(options)
         case Mode.VeSUV =>
           logger.info("Starting transformation")
           Transform.runOptions(options)
diff --git a/src/main/java/vct/main/modes/VeyMont.scala b/src/main/java/vct/main/modes/VeyMont.scala
new file mode 100644
index 0000000000..c9405ebe20
--- /dev/null
+++ b/src/main/java/vct/main/modes/VeyMont.scala
@@ -0,0 +1,31 @@
+package vct.main.modes
+
+import com.typesafe.scalalogging.LazyLogging
+import vct.col.origin.BlameCollector
+import vct.main.Main.{EXIT_CODE_ERROR, EXIT_CODE_SUCCESS, EXIT_CODE_VERIFICATION_FAILURE}
+import vct.main.modes.Verify.logger
+import vct.main.stages.Stages
+import vct.options.Options
+import vct.options.types.PathOrStd
+import vct.parsers.transform.ConstantBlameProvider
+import viper.carbon.boogie.Implicits.lift
+
+object VeyMont extends LazyLogging {
+
+  def verifyWithOptions(options: Options, inputs: Seq[PathOrStd]) = {
+    val collector = BlameCollector()
+    val stages = Stages.veymontOfOptions(options, ConstantBlameProvider(collector))
+    logger.debug("Stages: " ++ stages.flatNames.map(_._1).mkString(", "))
+    stages.run(inputs) match {
+      case Left(value) => logger.error(value.text)
+      case Right(()) => logger.info("VeyMont terminated successfully.")
+    }
+
+  }
+
+  def runOptions(options: Options): Int = {
+    verifyWithOptions(options, options.inputs)
+    0
+  }
+
+}
diff --git a/src/main/java/vct/main/stages/SaveStage.scala b/src/main/java/vct/main/stages/SaveStage.scala
new file mode 100644
index 0000000000..e5323d856b
--- /dev/null
+++ b/src/main/java/vct/main/stages/SaveStage.scala
@@ -0,0 +1,27 @@
+package vct.main.stages
+
+import hre.io.Writeable
+import hre.stages.Stage
+import vct.col.ast.Verification
+import vct.col.print.Printer
+import vct.col.rewrite.Generation
+import vct.options.Options
+
+case class SaveStage(writeable : Writeable) extends Stage[Verification[_<: Generation], Unit] {
+  override def friendlyName: String = "Saving File..."
+
+  override def progressWeight: Int = 1
+
+  override def run(in: Verification[_ <: Generation]): Unit = {
+    writeable.write(w => {
+      val printer = Printer(w)
+      printer.print(in.tasks.head.program)
+    })
+  }
+}
+
+object SaveStage {
+  def ofOptions(options: Options): Stage[Verification[_ <: Generation], Unit] = {
+    SaveStage(options.veymontOutput)
+  }
+}
diff --git a/src/main/java/vct/main/stages/Stages.scala b/src/main/java/vct/main/stages/Stages.scala
index 82941615bf..01c409d70e 100644
--- a/src/main/java/vct/main/stages/Stages.scala
+++ b/src/main/java/vct/main/stages/Stages.scala
@@ -1,7 +1,7 @@
 package vct.main.stages
 
 import hre.progress.Progress
-import vct.col.ast.{BipTransition, Program}
+import vct.col.ast.{Program, Verification, BipTransition}
 import vct.col.rewrite.Generation
 import vct.options.Options
 import vct.parsers.transform.BlameProvider
@@ -58,6 +58,13 @@ case object Stages {
       .thenRun(ExpectedErrors.ofOptions(options))
   }
 
+  def veymontOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
+    Parsing.ofOptions(options, blameProvider)
+      .thenRun(Resolution.ofOptions(options, blameProvider))
+      .thenRun(Transformation.veymontOfOptions(options))
+      .thenRun(SaveStage.ofOptions(options))
+  }
+
   def vesuvOfOptions(options: Options, blameProvider: BlameProvider) : Stages[Seq[Readable], Unit] = {
     Parsing.ofOptions(options, blameProvider)
       .thenRun(Output.ofOptions(options, blameProvider))
diff --git a/src/main/java/vct/main/stages/Transformation.scala b/src/main/java/vct/main/stages/Transformation.scala
index 121f8a85e8..402360dcd7 100644
--- a/src/main/java/vct/main/stages/Transformation.scala
+++ b/src/main/java/vct/main/stages/Transformation.scala
@@ -14,6 +14,7 @@ import vct.col.rewrite.adt._
 import vct.col.rewrite.lang.NoSupportSelfLoop
 import vct.col.origin.{ExpectedError, FileSpanningOrigin}
 import vct.col.print.Printer
+import vct.col.rewrite.veymont.{AddVeyMontAssignmentNodes, AddVeyMontConditionNodes, StructureCheck}
 import vct.col.rewrite.bip.{BIP, ComputeBipGlue, EncodeBip, EncodeBipPermissions, InstantiateBipSynchronizations}
 import vct.col.rewrite.{Generation, InitialGeneration, RewriterBuilder}
 import vct.importer.{PathAdtImporter, Util}
@@ -65,6 +66,15 @@ object Transformation {
           splitVerificationByProcedure = options.devSplitVerificationByProcedure,
         )
     }
+
+  def veymontOfOptions(options: Options): Transformation =
+    options.backend match {
+      case Backend.Silicon | Backend.Carbon =>
+        VeyMontTransformation(
+          onBeforePassKey = writeOutFunctions(options.outputBeforePass),
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass)
+        )
+    }
 }
 
 /**
@@ -277,3 +287,12 @@ case class SilverTransformation
 
     Explode.withArg(splitVerificationByProcedure),
   ))
+
+case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil)
+  extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
+    AddVeyMontAssignmentNodes,
+    AddVeyMontConditionNodes,
+    StructureCheck
+  ))
+
diff --git a/src/test/scala/vct/test/integration/helper/ExampleFiles.scala b/src/test/scala/vct/test/integration/helper/ExampleFiles.scala
index fe19699b07..6e6bc76000 100644
--- a/src/test/scala/vct/test/integration/helper/ExampleFiles.scala
+++ b/src/test/scala/vct/test/integration/helper/ExampleFiles.scala
@@ -8,6 +8,7 @@ case object ExampleFiles {
     "examples/private/",
     "examples/archive/",
     "examples/technical/veymont-check/",
+    "examples/technical/veymont-seq-progs/",
   ).map(_.replaceAll("/", File.separator))
 
   val IGNORE_EXTS: Seq[String] = Seq(