List proofs and signoff (#194)

16 files changed, 1737 insertions, 59 deletions

diff --git a/FreeRTOS/Test/VeriFast/Makefile b/FreeRTOS/Test/VeriFast/Makefile
index 9e774f61a..3d9fb4800 100644
--- a/FreeRTOS/Test/VeriFast/Makefile
+++ b/FreeRTOS/Test/VeriFast/Makefile
@@ -14,28 +14,37 @@ check_coverage = perl -pe \
    $$status=/$1 statements verified/ ? 0 : 1;'
 endif
 
-all: queue
+all: queue list
 
 .PHONY: queue
 queue:
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,317)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvCopyDataFromQueue.c      | $(call check_coverage,301)
-	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c        | $(call check_coverage,329)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueEmpty.c           | $(call check_coverage,282)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueFull.c            | $(call check_coverage,282)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvLockQueue.c              | $(call check_coverage,283)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvUnlockQueue.c            | $(call check_coverage,297)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueMessagesWaiting.c    | $(call check_coverage,285)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueSpacesAvailable.c    | $(call check_coverage,283)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/vQueueDelete.c              | $(call check_coverage,280)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueGenericSend.c         | $(call check_coverage,328)
-	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c  | $(call check_coverage,310)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,280)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueFullFromISR.c  | $(call check_coverage,280)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeek.c                | $(call check_coverage,328)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeekFromISR.c         | $(call check_coverage,293)
-	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueReceive.c             | $(call check_coverage,330)
-	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c      | $(call check_coverage,307)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/create.c                    | $(call check_coverage,324)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvCopyDataFromQueue.c      | $(call check_coverage,308)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c        | $(call check_coverage,336)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueEmpty.c           | $(call check_coverage,289)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvIsQueueFull.c            | $(call check_coverage,289)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvLockQueue.c              | $(call check_coverage,290)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/prvUnlockQueue.c            | $(call check_coverage,304)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueMessagesWaiting.c    | $(call check_coverage,292)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/uxQueueSpacesAvailable.c    | $(call check_coverage,290)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/vQueueDelete.c              | $(call check_coverage,287)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueGenericSend.c         | $(call check_coverage,335)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c  | $(call check_coverage,317)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,287)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueIsQueueFullFromISR.c  | $(call check_coverage,287)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeek.c                | $(call check_coverage,335)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueuePeekFromISR.c         | $(call check_coverage,300)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         queue/xQueueReceive.c             | $(call check_coverage,337)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c      | $(call check_coverage,314)
+
+.PHONY: list
+list:
+	@$(VERIFAST) $(VERIFAST_ARGS)                         list/listLIST_IS_EMPTY.c   | $(call check_coverage,314)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         list/uxListRemove.c        | $(call check_coverage,440)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialise.c     | $(call check_coverage,325)
+	@$(VERIFAST) $(VERIFAST_ARGS)                         list/vListInitialiseItem.c | $(call check_coverage,316)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsertEnd.c      | $(call check_coverage,410)
+	@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsert.c         | $(call check_coverage,456)
 
 .PHONY: proof_changes
 proof_changes:
@@ -43,10 +52,13 @@ proof_changes:
 
 GIT?=git
 NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
-NO_CHANGE_EXPECTED_HASH=587a83d6476
+NO_CHANGE_EXPECTED_HASH_QUEUE=587a83d6476
+NO_CHANGE_EXPECTED_HASH_LIST=bb1c4293787
 .PHONY: synced_with_source_check
 synced_with_source_check:
 	@rm -rf $(NO_CHANGE_CHECKOUT_DIR)
 	@$(GIT) clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git $(NO_CHANGE_CHECKOUT_DIR)
-	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) queue.c
-	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) include/queue.h
+	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) queue.c
+	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) include/queue.h
+	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) list.c
+	@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) include/list.h
diff --git a/FreeRTOS/Test/VeriFast/README.md b/FreeRTOS/Test/VeriFast/README.md
index f0deecdfc..5d472692f 100644
--- a/FreeRTOS/Test/VeriFast/README.md
+++ b/FreeRTOS/Test/VeriFast/README.md
@@ -1,8 +1,19 @@
 # FreeRTOS VeriFast proofs
 
-This directory contains automated functional correctness proofs of the FreeRTOS
-kernel queue data structure. These properties are proven with the
-[VeriFast](https://github.com/verifast/verifast) verifier.
+This directory contains unbounded proofs of the FreeRTOS kernel queue and list
+data structures. Unbounded proofs mean that these results hold independent of
+the length of the queue or list.
+
+Informally, the queue proofs demonstrate that the queue implementation is
+memory safe (does not access invalid memory), thread safe (properly
+synchronizes accesses) and functionally correct (behaves like a queue) under
+any arbitrary number of tasks or ISRs. The list proofs demonstrate that the
+list implementation is memory safe and functionally correct.
+
+These properties are proven with the
+[VeriFast](https://github.com/verifast/verifast) verifier. See the proof
+[signoff](docs/signoff.md) document for more on the proof properties,
+assumptions, and simplifications.
 
 ## Proof directory structure
 
@@ -14,6 +25,7 @@ predicates, functions and lemmas used by all proofs is maintained in the
 `include/proof` directory.
 
   - `queue`: proofs for the FreeRTOS queue data structure
+  - `list`: proofs for the FreeRTOS list data structure
 
 The following figure gives the callgraph of the queue proofs. Green=Proven
 functions, Blue=Functions modeled by lock invariants (underlying implementation
@@ -49,7 +61,7 @@ and uncheck `Check arithmetic overflow`).
   - `queue/xQueueReceiveFromISR.c`
 
 A successful proof results in the top banner turning green with a statement
-similar to: `0 errors found (328 statements verified)`.
+similar to: `0 errors found (335 statements verified)`.
 
 ## Proof checking a single proof at the command-line
 
@@ -65,7 +77,7 @@ A successful proof results in output similar to:
 
 ```
 queue/xQueueGenericSend.c
-0 errors found (328 statements verified)
+0 errors found (335 statements verified)
 ```
 
 ## Running proof regression
@@ -87,7 +99,8 @@ $ VERIFAST=/path/to/verifast NO_COVERAGE=1 make
 ## Annotation burden
 
 VeriFast can emit statistics about the number of source code lines and
-annotations. These range from .3-2x annotations per line of source code.
+annotations. These range from .3-2x annotations per line of source code for the
+queue proofs and up to 7x for the list proofs.
 
 ```
 $ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
@@ -96,15 +109,12 @@ $ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
 ## Reading a VeriFast proof
 
 VeriFast is a modular deductive verifier using separation logic. A quick
-introduction is given by [Jacobs and
-Piessens](https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf).
-In particular, Section 1 Introduction, gives a high-level overview of the proof
-technique, which uses forward symbolic execution over a symbolic heap.
+introduction is given by [Jacobs and Piessens][1]. In particular, Section 1
+Introduction, gives a high-level overview of the proof technique, which uses
+forward symbolic execution over a symbolic heap.
 
-Learning how to use VeriFast will help you read and understand the proofs. 
-The VeriFast
-[tutorial](https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf) is
-a good guide. You will need to understand:
+Learning how to use VeriFast will help you read and understand the proofs. The
+VeriFast [tutorial][2] is a good guide. You will need to understand:
 
   - Sec 4. Functions and Contracts
   - Sec 5. Patterns
@@ -115,8 +125,12 @@ a good guide. You will need to understand:
   - Sec 10. Inductive Datatypes
   - Sec 11. Lemmas
 
+[1]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf
+[2]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf
+
 ## Contributors
 
-We acknowledge and thank the following contributors, listed alphabetically:
+We acknowledge and thank the following contributors:
 
   - Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/
+  - Aalok Thakkar, University of Pennsylvania, https://aalok-thakkar.github.io/
diff --git a/FreeRTOS/Test/VeriFast/docs/signoff.md b/FreeRTOS/Test/VeriFast/docs/signoff.md
new file mode 100644
index 000000000..71af7ddbf
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/docs/signoff.md
@@ -0,0 +1,144 @@
+# FreeRTOS VeriFast Proof Signoff
+
+Verification tool: VeriFast (code-level proof)
+
+Proofs: `queue/` and `list`
+
+Implementation: Kernel queue data structure (`queue.c`) and list data structure (`list.c`)
+
+Specification / Properties:
+  - *Memory safety*: the implementation only accesses valid memory. In the case
+    of the queue, this is true under any arbitrary number of tasks or ISRs.
+  - *Thread safety*: in the case of the queue, tasks and ISRs only update
+    objects that they own via proper synchronization.
+  - *Functional correctness*: the queue and list implementations behave like an
+    abstract queue and list. In the case of the queue, this is true under any
+    arbitrary number of tasks or ISRs.
+
+## Queue proof assumptions
+
+Generally, we assume well-behaved clients; the correctness of underlying
+primitives (memory allocation, task scheduling, scheduler suspension); and
+assumptions about the system.
+
+  - Well-behaved client: all client tasks and ISRs use the queue API in a
+    manner that adheres to the specification. A badly-behaved client can
+    invalidate the proven properties. For example, a client that reads or
+    writes to the queue storage directly, without masking interrupts, is racy
+    and no longer thread safe. The specification forbids this behavior by
+    the definition of `queuehandle`, which is a handle to acquire ownership of
+    the queue through interrupt masking, but we cannot, in general, enforce
+    this behavior since we do not verify client code.
+
+  - Memory safety, thread safety and function contracts for the following
+    primitives. For the list and task functions we give a contract that is
+    maximal in terms of the queue objects that can be updated, but we do not
+    model their function effect (e.g., task blocking and the moving of task
+    control blocks between scheduler lists).
+
+        pvPortMalloc
+        vPortFree
+        memcpy
+        vListInitialise
+        xTaskRemoveFromEventList
+        vTaskMissedYield
+        xTaskCheckForTimeOut
+        vTaskInternalSetTimeOutState
+        vTaskPlaceOnEventList
+
+  - We assume interrupt masking gives strong isolation between tasks and ISRs.
+    See Appendix. We further assume the system is configured as required by
+    `configASSERT`. For example, interrupts with a priority greater than the
+    maximum system call priority must not call queue API functions, otherwise
+    the strong isolation guarantee is not maintained.
+
+## List proof assumptions
+
+The list proofs are sequential. We assume the caller of the list API functions
+has taken appropriate synchronization steps to avoid races.
+
+## Simplifications
+
+A list of changes to the source code required for the proofs can be generated:
+
+```
+make proof_changes
+```
+
+A side-by-side diff with respect to the source code can be generated. See
+![`scripts/diff_files.md`](../scripts/diff_files.md).
+
+The main queue changes are:
+
+  - merge cTxLock and cRxLock critical regions: under approximate queue
+	unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
+    single critical region instead of two separate critical regions. In
+	practice, this is not an issue since no ISR function reads-from both
+    cTxLock and cRxLock.
+  - model single malloc of struct and buffer: split the single malloc of the
+    queue struct and storage into two separate mallocs.
+  - xQueueGenericReset happens-before concurrent behavior: assume that queue
+    initialisation is not concurrent.
+  - do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
+    the list structs of the queue implementation
+
+The main list changes are:
+
+  - change `MiniList_t` to `ListItem_t`: simplifying assumption on the list
+    structure.
+  - over-approximate list insert loop: replace a loop in the insert function
+    that finds the insertion point with an over-approximating function call.
+
+The following minor changes due to the stricter typing and parser of VeriFast:
+
+  - replacing a union declaration with a struct
+  - const pointer declaration
+  - stricter casting
+  - void cast of unused return value
+  - void cast of unused var
+
+The following minor changes due to the modeling of interrupts and scheduler
+suspension in the proofs as ghost state.
+
+  - ghost action
+  - leak ghost state on deletion
+
+## Configuration
+
+We do not verify across the full configuration space of FreeRTOS. In
+particular, the queue proofs do not apply when the following options are
+enabled:
+
+  - `configUSE_QUEUE_SETS`
+  - `configSUPPORT_STATIC_ALLOCATION`
+
+For both the queue and list proofs we assume that coverage and tracing
+macros are no-ops.
+
+## Trusted computing base
+
+  - Soundness of verification tools: VeriFast, Redux prover
+  - C Compiler, because the verification is at the C code-level and the
+    properties proved may not be preserved by compilation.
+
+## References
+
+[N1570] ISO/IEC. Programming languages – C. International standard 9899:201x,
+2011
+
+## Appendix
+
+Assumption on strong isolation induced by interrupt masking and scheduler
+suspension for queue proofs. Informally, we need the following:
+
+```
+// Initially *data == 0
+// Task 1
+taskENTER_CRITICAL()
+*data = 1;
+*data = 2;
+taskEXIT_CRITICAL()
+
+// ISR or Task 2
+r0 = *data; //< guaranteed to read 0 or 2, never 1
+```
diff --git a/FreeRTOS/Test/VeriFast/include/proof/common.gh b/FreeRTOS/Test/VeriFast/include/proof/common.gh
index c3b064939..f8acfdddc 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/common.gh
+++ b/FreeRTOS/Test/VeriFast/include/proof/common.gh
@@ -191,6 +191,45 @@ lemma_auto void mod_range(int x, int n)
   div_rem_nonneg(x, n);
 }
 
+lemma void head_append<t>(list<t> xs, list<t> ys)
+  requires 0 < length(xs);
+  ensures head(append(xs, ys)) == head(xs);
+{
+  switch(xs)
+  {
+    case cons(c, cs):
+    case nil:
+  }
+}
+
+lemma void drop_take_singleton<t>(int i, list<t> xs)
+  requires 0 < i && i < length(xs);
+  ensures drop(i-1, take(i, xs)) == singleton(nth(i-1, xs));
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (i == 1) {
+    } else {
+      drop_take_singleton(i-1, xs0);
+    }
+  }
+}
+
+lemma void take_singleton<t>(int i, list<t> xs)
+  requires 0 <= i && i < length(xs);
+  ensures append(take(i, xs), singleton(nth(i, xs))) == take(i+1, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (i == 0) {
+    } else {
+      take_singleton(i-1, xs0);
+    }
+  }
+}
+
 lemma void drop_update_le<t>(int i, int j, t x, list<t> xs)
   requires 0 <= i && i <= j && j < length(xs);
   ensures drop(i, update(j, x, xs)) == update(j - i, x, drop(i, xs));
@@ -298,21 +337,17 @@ lemma void take_take<t>(int m, int n, list<t> xs)
   }
 }
 
-lemma void index_of_distinct<t>(list<t> xs, t x1, t x2)
-  requires mem(x1, xs) == true &*& mem(x2, xs) == true &*& x1 != x2;
-  ensures index_of(x1, xs) != index_of(x2, xs);
+lemma_auto void take_head<t>(list<t> xs)
+  requires 0 < length(xs);
+  ensures take(1, xs) == singleton(head(xs));
 {
-  switch (xs) {
+  switch(xs) {
   case nil:
-  case cons(h, tl):
-    if (h == x1 || h == x2) {
-      /* trivial */
-    } else {
-      index_of_distinct(tl, x1, x2);
-    }
+  case cons(x0, xs0):
   }
 }
 
+/* Following lemma from `verifast/bin/rt/_list.java` */
 lemma void remove_remove_nth<t>(list<t> xs, t x)
   requires mem(x, xs) == true;
   ensures remove(x, xs) == remove_nth(index_of(x, xs), xs);
@@ -328,6 +363,18 @@ lemma void remove_remove_nth<t>(list<t> xs, t x)
   }
 }
 
+lemma void mem_take_false<t>(t x, int n, list<t> xs)
+    requires mem(x, xs) == false;
+    ensures mem(x, take(n, xs)) == false;
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+      if (x0 != x && n != 0)
+          mem_take_false(x, n - 1, xs0);
+  }
+}
+
 /* Following lemma from `verifast/bin/rt/_list.java`. Renamed to
 avoid clash with listex.c's nth_drop lemma. */
 lemma void nth_drop2<t>(list<t> vs, int i)
@@ -536,12 +583,12 @@ lemma void update_rewrite<t>(list<t> vs, t v, int pos)
   ensures update(pos, v, vs) == append(take(pos, vs), cons(v, (drop(pos+1, vs))));
 {
   switch(vs) {
-    case nil:
-    case cons(h, t):
-      if(pos == 0) {
-      } else {
-        update_rewrite(t, v, pos - 1);
-      }
+  case nil:
+  case cons(h, t):
+    if (pos == 0) {
+    } else {
+      update_rewrite(t, v, pos - 1);
+    }
   }
 }
 
diff --git a/FreeRTOS/Test/VeriFast/include/proof/list.h b/FreeRTOS/Test/VeriFast/include/proof/list.h
new file mode 100644
index 000000000..21f9b42b0
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/include/proof/list.h
@@ -0,0 +1,368 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#ifndef LIST_H
+#define LIST_H
+
+#define VERIFAST
+#include <stdlib.h>
+#include <stdint.h>
+//@#include "common.gh"
+
+typedef size_t TickType_t;
+typedef size_t UBaseType_t;
+typedef ssize_t BaseType_t;
+
+#define pdTRUE 1
+#define pdFALSE 0
+
+/* Empty/no-op macros */
+#define mtCOVERAGE_TEST_MARKER()
+#define mtCOVERAGE_TEST_DELAY()
+#define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )
+#define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )
+#define listTEST_LIST_INTEGRITY( pxList )
+#define listTEST_LIST_ITEM_INTEGRITY( pxListItem )
+#define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
+#define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
+
+/* Max value stored in sentinel xListEnd element */
+#define portMAX_DELAY UINT_MAX
+
+struct xLIST;
+
+struct xLIST_ITEM {
+	TickType_t xItemValue;
+	struct xLIST_ITEM * pxNext;
+	struct xLIST_ITEM * pxPrevious;
+	void * pvOwner;
+	struct xLIST *pxContainer;
+};
+typedef struct xLIST_ITEM ListItem_t;
+
+typedef struct xLIST {
+	UBaseType_t uxNumberOfItems;
+	struct xLIST_ITEM *pxIndex;
+#ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
+	struct xLIST_ITEM xListEnd;
+#else
+	MiniListItem_t xListEnd;
+#endif
+} List_t;
+
+/*@
+predicate xLIST_ITEM(
+	struct xLIST_ITEM *n,
+	TickType_t xItemValue,
+	struct xLIST_ITEM *pxNext,
+	struct xLIST_ITEM *pxPrevious,
+	struct xLIST *pxContainer;) =
+	n->xItemValue |-> xItemValue &*&
+	n->pxNext |-> pxNext &*&
+	n->pxPrevious |-> pxPrevious &*&
+	n->pvOwner |-> _ &*&
+	n->pxContainer |-> pxContainer;
+@*/
+
+/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
+/*@
+predicate DLS(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells,
+	list<TickType_t > vals,
+	struct xLIST *pxContainer) =
+	n == m
+		? cells == cons(n, nil) &*&
+			vals == cons(?v, nil) &*&
+			xLIST_ITEM(n, v, mnext, nprev, pxContainer)
+		: cells == cons(n, ?cells0) &*&
+			vals == cons(?v, ?vals0) &*&
+			xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
+
+lemma void dls_star_item(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *m,
+	struct xLIST_ITEM *o)
+requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2);
+ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
+{
+	open DLS(n, nprev, mnext, m, cells, vals, l);
+	if (n == m) {
+		assert xLIST_ITEM(n, _, _, _, _);
+		open xLIST_ITEM(n, _, _, _, _);
+		open xLIST_ITEM(o, _, _, _, _);
+		assert n != o;
+		close xLIST_ITEM(o, _, _, _, _);
+		close xLIST_ITEM(n, _, _, _, _);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	}
+	else {
+		assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
+		dls_star_item(nnext, m, o);
+		open xLIST_ITEM(n, _, _, _, _);
+		open xLIST_ITEM(o, _, _, _, _);
+		assert n != o;
+		close xLIST_ITEM(o, _, _, _, _);
+		close xLIST_ITEM(n, _, _, _, _);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	}
+}
+
+lemma void dls_distinct(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells)
+requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
+ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
+{
+	if (n == m) {
+		open DLS(n, nprev, mnext, m, cells, vals, l);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	} else {
+		open DLS(n, nprev, mnext, m, cells, vals, l);
+		assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
+		dls_distinct(nnext, n, mnext, m, tail(cells));
+		dls_star_item(nnext, m, n);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	}
+}
+
+predicate xLIST(
+	struct xLIST *l,
+	int uxNumberOfItems,
+	struct xLIST_ITEM *pxIndex,
+	struct xLIST_ITEM *xListEnd,
+	list<struct xLIST_ITEM *>cells,
+	list<TickType_t >vals) =
+	l->uxNumberOfItems |-> uxNumberOfItems &*&
+	l->pxIndex |-> pxIndex &*&
+	mem(pxIndex, cells) == true &*&
+	xListEnd == &(l->xListEnd) &*&
+	xListEnd == head(cells) &*&
+	portMAX_DELAY == head(vals) &*&
+	struct_xLIST_ITEM_padding(&l->xListEnd) &*&
+	length(cells) == length(vals) &*&
+	uxNumberOfItems + 1 == length(cells) &*&
+	DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
+
+lemma void xLIST_distinct_cells(struct xLIST *l)
+requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
+ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
+{
+	open xLIST(l, n, idx, end, cells, vals);
+	assert DLS(end, ?endprev, end, _, cells, vals, l);
+	dls_distinct(end, endprev, end, endprev, cells);
+	close xLIST(l, n, idx, end, cells, vals);
+}
+
+lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
+requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2);
+ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false;
+{
+	open xLIST(l, n, idx, end, cells, vals);
+	assert DLS(end, ?endprev, end, _, cells, vals, l);
+	dls_distinct(end, endprev, end, endprev, cells);
+	dls_star_item(end, endprev, x);
+	close xLIST(l, n, idx, end, cells, vals);
+}
+
+lemma void dls_first_mem(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells)
+requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
+ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
+{
+	open DLS(n, nprev, mnext, m, cells, vals, l);
+	if (n == m) {
+		assert cells == cons(n, nil);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	} else {
+		assert cells == cons(n, ?tail);
+		close DLS(n, nprev, mnext, m, cells, vals, l);
+	}
+}
+
+lemma void dls_not_empty(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells,
+	struct xLIST_ITEM *x)
+requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n;
+ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
+{
+	open DLS(n, m, n, m, cells, vals, l);
+	close DLS(n, m, n, m, cells, vals, l);
+}
+
+lemma void dls_last_mem(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells)
+requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
+ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
+{
+	open DLS(n, nprev, mnext, m, cells, vals, l);
+	if (n == m) {
+		// trivial
+	} else {
+		open xLIST_ITEM(n, _, ?nnext, _, l);
+		assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l);
+		dls_last_mem(o, n, mnext, m, tail(cells));
+		close xLIST_ITEM(n, _, nnext, _, l);
+	}
+	close DLS(n, nprev, mnext, m, cells, vals, l);
+}
+
+lemma void split(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells,
+	list<TickType_t > vals,
+	struct xLIST_ITEM *x,
+	int i)
+requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
+ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), l) &*& xprev == nth(i-1, cells);
+{
+	open DLS(n, nprev, mnext, m, cells, vals, l);
+	assert n != m;
+	assert xLIST_ITEM(n, ?v, ?nnext, _, _);
+	assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
+	if (nnext == x) {
+		close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
+		open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
+		open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
+		close xLIST_ITEM(x, _, xnext, xprev, l);
+		close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
+	} else {
+		assert nnext != x;
+		split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
+		assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
+		dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
+		dls_star_item(nnext, xprev, n);
+		dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
+		assert n != xprev;
+		close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
+	}
+}
+
+lemma void join(
+	struct xLIST_ITEM *n1,
+	struct xLIST_ITEM *nprev1,
+	struct xLIST_ITEM *mnext1,
+	struct xLIST_ITEM *m1,
+	list<struct xLIST_ITEM * > cells1,
+	list<TickType_t > vals1,
+	struct xLIST_ITEM *n2,
+	struct xLIST_ITEM *nprev2,
+	struct xLIST_ITEM *mnext2,
+	struct xLIST_ITEM *m2,
+	list<struct xLIST_ITEM * > cells2,
+	list<TickType_t > vals2)
+requires
+	DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
+	DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
+	mnext1 == n2 &*& m1 == nprev2;
+ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
+{
+	if (n1 == m1) {
+		dls_first_mem(n1, nprev1, mnext1, m1, cells1);
+		dls_last_mem(n2, nprev2, mnext2, m2, cells2);
+		open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
+		dls_star_item(n2, m2, n1);
+		close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
+	} else {
+		open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
+		assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
+		join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
+			n2, nprev2, mnext2, m2, cells2, vals2);
+		assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
+		dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
+		dls_star_item(o, m2, n1);
+		close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
+	}
+}
+
+lemma void idx_remains_in_list<t>(
+	list<t> cells,
+	t idx,
+	t x,
+	int ix)
+requires
+	idx != x &*&
+	mem(idx, cells) == true &*&
+	mem(x, cells) == true &*&
+	index_of(x, cells) == ix;
+ensures mem(idx, remove_nth(ix, cells)) == true;
+{
+	neq_mem_remove(idx, x, cells);
+	remove_remove_nth(cells, x);
+}
+@*/
+
+/* Following lemma from `verifast/examples/shared_boxes/concurrentqueue.c`.
+Used in the uxListRemove proof to show that the item to remove `x` must
+have value `nth(i, vals)` where `i == index_of(x, cells)`. */
+/*@
+lemma void drop_nth_index_of<t>(list<t> vs, int i)
+requires
+	0 <= i && i < length(vs);
+ensures
+	head(drop(i , vs)) == nth(i, vs);
+{
+	switch(vs) {
+		case nil:
+		case cons(h, t):
+		if (i == 0) {
+			// trivial
+		} else {
+			drop_nth_index_of(t, i - 1);
+		}
+	}
+}
+@*/
+
+/*@
+lemma void remove_append<t>(t x, list<t> l1, list<t> l2)
+	requires mem(x, l1) == false;
+	ensures remove(x, append(l1, l2)) == append(l1, remove(x, l2));
+{
+	switch(l1) {
+		case nil:
+		case cons(h1, t1):
+			remove_append(x, t1, l2);
+	}
+}
+@*/
+
+#endif /* LIST_H */
diff --git a/FreeRTOS/Test/VeriFast/include/proof/queue.h b/FreeRTOS/Test/VeriFast/include/proof/queue.h
index 610bc03d9..a05b327f7 100644
--- a/FreeRTOS/Test/VeriFast/include/proof/queue.h
+++ b/FreeRTOS/Test/VeriFast/include/proof/queue.h
@@ -305,7 +305,6 @@ ensures
         }
         drop_drop(1, j, elements);
         nth_drop2(elements, i);
-        open buffer(buffer + (i+1) * M, (N-1-i), M, _);
     }
 }
 
diff --git a/FreeRTOS/Test/VeriFast/list/README.md b/FreeRTOS/Test/VeriFast/list/README.md
new file mode 100644
index 000000000..b9385b920
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/README.md
@@ -0,0 +1,69 @@
+# FreeRTOS list proofs
+
+The list predicates and proofs are inspired by and based on the work from
+Ferreira et al. (STTT'14).
+
+The main shape predicate is a doubly-linked list segment (DLS), as defined
+by Ferreira et al. in Fig 15. A DLS is defined by two `xLIST_ITEM` struct
+pointers `n` and `m` (possibly pointing to the same item) which are the start
+and end of the segment. We track the item pointers and values within the DLS in
+the lists `cells` and `vals`, respectively. Therefore `n` and `m` are the first
+and last items of `cells`.
+
+```
+          +--+     +--+
+ -----n-> |*n| ... |*m| -mnext->
+ <-nprev- |  |     |  | <-m-----
+          +--+     +--+
+          ^-----------^
+           DLS(n, nprev, mnext, m)
+```
+
+With base case: `n == m` (single item case)
+
+```
+          +--+
+ -----n-> |*n| -mnext->
+ <-nprev- |  | <-n-----
+          +--+
+          ^--^
+          xLIST_ITEM
+          DLS(n, nprev, mnext, n)
+```
+
+Cons case:
+
+```
+          +--+      +--+     +--+
+ -----n-> |*n| -o-> |*o| ... |*m| -mnext->
+ <-nprev- |  | <-n- |  |     |  | <-m-----
+          +--+      +--+     +--+
+          ^--^      ^-----------^
+          xLIST_ITEM DLS(o, n, mnext, m)
+
+          ^---------------------^
+          DLS(n, nprev, mnext, m)
+```
+
+A DLS can be made into a well-formed list by joining `n` and `m` into a cycle.
+Note that unlike Ferreira et al.'s list shape predicate, we always start with
+the sentinel end item to avoid a top-level case-split. So in the following
+diagram the start and end of the DLS are `end` and the item-before-end
+`endprev`.
+
+```
+ .-----------------------------------.
+ |     +--------+     +--------+     |
+  `--> |*end    | ... |*endprev| ----'
+ .---- |        |     |        | <---.
+ |     +--------+     +--------+     |
+  `----------------------------------'
+       ^-----------------------^
+        DLS(end, endprev, end, endprev)
+```
+
+## References
+
+- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK\
+  João F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin\
+  https://joaoff.com/publication/2014/sttt/
diff --git a/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c b/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c
new file mode 100644
index 000000000..ab6e12b4a
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c
@@ -0,0 +1,36 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+/* Wrap the macro in a function call so we can give a function contract */
+#define listLIST_IS_EMPTY( pxList )                       ( ( ( pxList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? pdTRUE : pdFALSE )
+
+BaseType_t wrapper_listLIST_IS_EMPTY( List_t * pxList )
+/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals);@*/
+/*@ensures xLIST(pxList, len, idx, end, cells, vals) &*&
+    result == ((len == 0) ? pdTRUE : pdFALSE); @*/
+{
+    /*@open xLIST(pxList, len, _, _, _, _);@*/
+    return listLIST_IS_EMPTY( pxList );
+    /*@close xLIST(pxList, len, _, _, cells, vals);@*/
+}
diff --git a/FreeRTOS/Test/VeriFast/list/uxListRemove.c b/FreeRTOS/Test/VeriFast/list/uxListRemove.c
new file mode 100644
index 000000000..1d244bc06
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/uxListRemove.c
@@ -0,0 +1,306 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
+/*@requires
+    exists<struct xLIST * >(?l) &*&
+    xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    end != pxItemToRemove &*&
+    mem(pxItemToRemove, cells) == true;@*/
+/*@ensures
+    result == len-1 &*&
+    xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, NULL) &*&
+    pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*&
+    xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx,  end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals));@*/
+{
+    /* For brevity we alias x to pxItemToRemove */
+    /*@struct xLIST_ITEM *x = pxItemToRemove;@*/
+
+    /* Start by establishing that the list must be non-empty since x != end */
+    /*@open xLIST(l, len, idx, end, cells, vals);@*/
+    /*@assert DLS(end, ?endprev, end, _, cells, vals, l);@*/
+    /*@assert vals == cons(portMAX_DELAY, _);@*/
+    /*@dls_not_empty(end, endprev, cells, x);@*/
+
+    /* We know the xLIST is a DLS: end...endprev
+    Split this into DLS1:end...xprev and DLS2:x...endprev */
+    /*@int i = index_of(x, cells);@*/
+    /*@split(end, endprev, end, endprev, cells, vals, x, i);@*/
+    /*@list<struct xLIST_ITEM *> ys = take(i, cells);@*/
+    /*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
+    /*@list<TickType_t> vs = take(i, vals);@*/
+    /*@list<TickType_t> ws = drop(i, vals);@*/
+    /*@assert length(ys) == length(vs);@*/
+    /*@assert length(zs) == length(ws);@*/
+    /*@assert DLS(end, endprev, x, ?xprev, ys, vs, l);@*/ /*< DLS1 (ys, vs) */
+    /*@assert DLS(x, xprev, end, endprev, zs, ws, l);@*/  /*< DLS2 (zs, ws) */
+
+    /* Now case split to open DLS1 and DLS2 appropriately */
+    /*@
+    if (end == xprev)
+    {
+        if (x == endprev)
+        {
+            //Case A
+            //DLS1: extract end=prev=next
+            open DLS(end, endprev, x, xprev, ys, vs, l);
+            open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
+            //DLS2: extract x
+            open DLS(x, xprev, end, endprev, zs, ws, l);
+            //Lengths
+            assert length(ys) == 1;
+            assert length(zs) == 1;
+        }
+        else
+        {
+            //Case B
+            //DLS1: extract end=prev
+            open DLS(end, endprev, x, xprev, ys, vs, l);
+            open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
+            //DLS2: extract next and x
+            open DLS(x, end, end, endprev, zs, ws, l);
+            assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), l);
+            open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
+            open xLIST_ITEM(xnext, _, _, x, l);
+            //Lengths
+            assert length(ys) == 1;
+        }
+    }
+    else
+    {
+        if (x == endprev)
+        {
+            //Case C
+            //DLS1: extract end=next and prev
+            dls_last_mem(end, endprev, x, xprev, ys);
+            assert mem(xprev, ys) == true;
+            open DLS(end, endprev, x, xprev, ys, vs, l);
+            open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
+            if (endnext == xprev)
+            {
+                open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
+                open xLIST_ITEM(xprev, _, x, _, l);
+            }
+            else
+            {
+                assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
+                int k = index_of(xprev, tail(ys));
+                dls_last_mem(endnext, end, x, xprev, tail(ys));
+                split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
+                open DLS(xprev, _, x, xprev, _, _, l);
+                open xLIST_ITEM(xprev, _, x, _, l);
+            }
+            //DLS2: extract x
+            open DLS(x, xprev, end, endprev, zs, ws, l);
+            //Lengths
+            assert length(zs) == 1;
+        }
+        else
+        {
+            //Case D
+            //DLS1: extract prev
+            dls_last_mem(end, endprev, x, xprev, ys);
+            int j = index_of(xprev, ys);
+            open DLS(end, endprev, x, xprev, ys, vs, l);
+            open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
+            if (endnext == xprev)
+            {
+                open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
+                assert tail(ys) == singleton(xprev);
+                open xLIST_ITEM(xprev, _, x, _, l);
+            }
+            else
+            {
+                assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
+                int k = index_of(xprev, tail(ys));
+                dls_last_mem(endnext, end, x, xprev, tail(ys));
+                split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
+                open DLS(xprev, _, x, xprev, _, _, l);
+                open xLIST_ITEM(xprev, _, x, _, l);
+            }
+            //DLS2: extract next and x
+            open DLS(x, xprev, end, endprev, zs, ws, l);
+            assert xLIST_ITEM(x, _, ?xnext, _, l);
+            open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
+            open xLIST_ITEM(xnext, _, _, x, l);
+        }
+    }
+    @*/
+    /*@drop_nth_index_of(vals, i);@*/
+    /*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, l);@*/
+
+/* The list item knows which list it is in.  Obtain the list from the list
+ * item. */
+#ifdef VERIFAST /*< const pointer declaration */
+    List_t * pxList = pxItemToRemove->pxContainer;
+#else
+    List_t * const pxList = pxItemToRemove->pxContainer;
+#endif
+
+    pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
+    pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
+
+    /* Only used during decision coverage testing. */
+    mtCOVERAGE_TEST_DELAY();
+
+    /* Make sure the index is left pointing to a valid item. */
+    if( pxList->pxIndex == pxItemToRemove )
+    {
+        pxList->pxIndex = pxItemToRemove->pxPrevious;
+    }
+    else
+    {
+        mtCOVERAGE_TEST_MARKER();
+    }
+
+    pxItemToRemove->pxContainer = NULL;
+    ( pxList->uxNumberOfItems )--;
+
+    return pxList->uxNumberOfItems;
+
+    /*@
+    // Reassemble DLS1 and a modified DLS2, which no longer includes x
+    if (end == xprev)
+    {
+        if (x == endprev)
+        {
+            //Case A
+            close xLIST_ITEM(end, portMAX_DELAY, _, _, _);
+            close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), l);
+        }
+        else
+        {
+            //Case B
+            close xLIST_ITEM(xprev, _, xnext, endprev, l);
+            close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), l);
+            close xLIST_ITEM(xnext, _, _, xprev, l);
+            close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
+            join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY),
+                 xnext, xprev, end, endprev, tail(zs), tail(ws));
+        }
+    }
+    else
+    {
+        if (x == endprev)
+        {
+            //Case C
+            close xLIST_ITEM(end, _, ?endnext, xprev, l);
+            close xLIST_ITEM(xprev, ?xprev_val, end, _, l);
+            if (endnext == xprev)
+            {
+                close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), l);
+                close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), l);
+            }
+            else
+            {
+                close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
+                assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
+                join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
+                     xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
+                close DLS(end, xprev, end, xprev, ys, vs, l);
+            }
+        }
+        else
+        {
+            //Case D
+            close xLIST_ITEM(xnext, _, ?xnextnext, xprev, l);
+            close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
+            close xLIST_ITEM(end, _, ?endnext, endprev, l);
+            close xLIST_ITEM(xprev, ?xprev_val, xnext, _, l);
+            if (endnext == xprev)
+            {
+                close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
+                close DLS(end, endprev, xnext, xprev, ys, vs, l);
+                join(end, endprev, xnext, xprev, ys, vs,
+                     xnext, xprev, end, endprev, tail(zs), tail(ws));
+            }
+            else
+            {
+                close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
+                assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
+                join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
+                     xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
+                close DLS(end, endprev, xnext, xprev, ys, vs, l);
+                join(end, endprev, xnext, xprev, ys, vs,
+                     xnext, xprev, end, endprev, tail(zs), tail(ws));
+            }
+        }
+    }
+    @*/
+    /*@remove_remove_nth(cells, x);@*/
+    /*@
+    if (idx == x)
+    {
+        close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)));
+    }
+    else
+    {
+        idx_remains_in_list(cells, idx, x, i);
+        close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)));
+    }
+    @*/
+    /*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, NULL);@*/
+}
+
+ListItem_t * client_example( List_t * l )
+/*@requires
+    xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    idx != end &*&
+    cells == cons(end, cons(idx, ?cells_tl)) &*&
+    vals == cons(portMAX_DELAY, cons(42, ?vals_tl));@*/
+/*@ensures
+    xLIST(l, len - 1, _, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
+    xLIST_ITEM(result, 42, _, _, NULL);@*/
+{
+    /*@open xLIST(l, len, idx, end, cells, vals);@*/
+    ListItem_t *index = l->pxIndex;
+    /*@close xLIST(l, len, idx, end, cells, vals);@*/
+    /*@close exists(l);@*/
+    uxListRemove( index );
+    return index;
+}
+
+void client_example2( List_t * l )
+/*@requires
+    xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    cells == cons(end, cons(?x1, cons(?x2, ?cells_tl))) &*&
+    idx == x2 &*&
+    vals == cons(portMAX_DELAY, cons(1, cons(2, ?vals_tl)));@*/
+/*@ensures
+    xLIST(l, len-2, end, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
+    xLIST_ITEM(_, 1, _, _, NULL) &*&
+    xLIST_ITEM(_, 2, _, _, NULL);@*/
+{
+    /*@xLIST_distinct_cells(l);@*/
+    /*@open xLIST(l, len, idx, end, cells, vals);@*/
+    ListItem_t *index = l->pxIndex;
+    /*@close xLIST(l, len, idx, end, cells, vals);@*/
+    /*@close exists(l);@*/
+    uxListRemove( index );
+    /*@open xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
+    index = l->pxIndex;
+    /*@close xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
+    /*@close exists(l);@*/
+    uxListRemove( index );
+}
diff --git a/FreeRTOS/Test/VeriFast/list/vListInitialise.c b/FreeRTOS/Test/VeriFast/list/vListInitialise.c
new file mode 100644
index 000000000..6ea02e6af
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/vListInitialise.c
@@ -0,0 +1,71 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+/*@
+predicate xLIST_uninitialised(struct xLIST *l) =
+    l->uxNumberOfItems |-> _ &*&
+    l->pxIndex |-> _ &*&
+    l->xListEnd.xItemValue |-> _ &*&
+    l->xListEnd.pxNext |-> _ &*&
+    l->xListEnd.pxPrevious |-> _ &*&
+    l->xListEnd.pvOwner |-> _ &*&
+    l->xListEnd.pxContainer |-> _ &*&
+    struct_xLIST_ITEM_padding(&l->xListEnd);
+@*/
+
+void vListInitialise( List_t * const pxList )
+/*@requires xLIST_uninitialised(pxList);@*/
+/*@ensures xLIST(pxList, 0, ?end, end, singleton(end), singleton(portMAX_DELAY));@*/
+{
+    /*@open xLIST_uninitialised(pxList);@*/
+
+    /* The list structure contains a list item which is used to mark the
+     * end of the list.  To initialise the list the list end is inserted
+     * as the only list entry. */
+    pxList->pxIndex = ( ListItem_t * ) &( pxList->xListEnd ); /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM.  This is checked and valid. */
+
+    /* The list end value is the highest possible value in the list to
+     * ensure it remains at the end of the list. */
+    pxList->xListEnd.xItemValue = portMAX_DELAY;
+
+    /* The list end next and previous pointers point to itself so we know
+     * when the list is empty. */
+    pxList->xListEnd.pxNext = ( ListItem_t * ) &( pxList->xListEnd );     /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM.  This is checked and valid. */
+    pxList->xListEnd.pxPrevious = ( ListItem_t * ) &( pxList->xListEnd ); /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM.  This is checked and valid. */
+
+    pxList->uxNumberOfItems = ( UBaseType_t ) 0U;
+
+    /* Write known values into the list if
+     * configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+    listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList );
+    listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList );
+
+#ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
+    pxList->xListEnd.pxContainer = pxList;
+#endif
+    /*@ListItem_t *end = &(pxList->xListEnd);@*/
+    /*@close xLIST_ITEM(end, portMAX_DELAY, _, _, pxList);@*/
+    /*@close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), pxList);@*/
+    /*@close xLIST(pxList, 0, end, end, singleton(end), singleton(portMAX_DELAY));@*/
+}
diff --git a/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c b/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c
new file mode 100644
index 000000000..d744f5f28
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c
@@ -0,0 +1,37 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+void vListInitialiseItem( ListItem_t * const pxItem )
+/*@requires xLIST_ITEM(pxItem, _, _, _, _);@*/
+/*@ensures xLIST_ITEM(pxItem, _, _, _, NULL);@*/
+{
+    /* Make sure the list item is not recorded as being on a list. */
+    pxItem->pxContainer = NULL;
+
+    /* Write known values into the list item if
+     * configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
+    listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem );
+    listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem );
+    /*@close xLIST_ITEM(pxItem, _, _, _, NULL);@*/
+}
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsert.c b/FreeRTOS/Test/VeriFast/list/vListInsert.c
new file mode 100644
index 000000000..96e333832
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/vListInsert.c
@@ -0,0 +1,316 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+
+ListItem_t * choose(List_t * list);
+/*@ requires DLS(&(list->xListEnd), ?endprev, &(list->xListEnd), endprev, ?cells, ?vals, ?container);@*/
+/*@ ensures DLS(&(list->xListEnd), endprev, &(list->xListEnd), endprev, cells, vals, container) &*&
+    mem(result, cells) == true;@*/
+
+void vListInsert( List_t * const pxList,
+                  ListItem_t * const pxNewListItem )
+/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/
+/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
+    remove(pxNewListItem, new_cells) == cells
+;@*/
+{
+    /*@xLIST_star_item(pxList, pxNewListItem);@*/
+    /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
+    /*@open xLIST(pxList, len, idx, end, cells, vals);@*/
+    /*@assert DLS(end, ?endprev, end, endprev, cells, vals, pxList);@*/
+    ListItem_t * pxIterator;
+    const TickType_t xValueOfInsertion = pxNewListItem->xItemValue;
+
+    /* Only effective when configASSERT() is also defined, these tests may catch
+     * the list data structures being overwritten in memory.  They will not catch
+     * data errors caused by incorrect configuration or use of FreeRTOS. */
+    listTEST_LIST_INTEGRITY( pxList );
+    listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );
+
+    /* Insert the new list item into the list, sorted in xItemValue order.
+     *
+     * If the list already contains a list item with the same item value then the
+     * new list item should be placed after it.  This ensures that TCBs which are
+     * stored in ready lists (all of which have the same xItemValue value) get a
+     * share of the CPU.  However, if the xItemValue is the same as the back marker
+     * the iteration loop below will not end.  Therefore the value is checked
+     * first, and the algorithm slightly modified if necessary. */
+    if( xValueOfInsertion == portMAX_DELAY )
+    {
+        /*@open DLS(end, endprev, end, endprev, cells, vals, pxList);@*/
+        /*@open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);@*/
+        /*@
+        if (end != endprev)
+        {
+            assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
+            if (endnext == endprev)
+            {
+                // done
+            }
+            else
+            {
+                dls_last_mem(endnext, end, end, endprev, tail(cells));
+                split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
+            }
+            open DLS(endprev, _, _, _, _, _, _);
+            open xLIST_ITEM(endprev, _, _, _, _);
+        }
+        @*/
+        pxIterator = pxList->xListEnd.pxPrevious;
+    }
+    else
+    {
+        /* *** NOTE ***********************************************************
+        *  If you find your application is crashing here then likely causes are
+        *  listed below.  In addition see https://www.freertos.org/FAQHelp.html for
+        *  more tips, and ensure configASSERT() is defined!
+        *  https://www.freertos.org/a00110.html#configASSERT
+        *
+        *   1) Stack overflow -
+        *      see https://www.freertos.org/Stacks-and-stack-overflow-checking.html
+        *   2) Incorrect interrupt priority assignment, especially on Cortex-M
+        *      parts where numerically high priority values denote low actual
+        *      interrupt priorities, which can seem counter intuitive.  See
+        *      https://www.freertos.org/RTOS-Cortex-M3-M4.html and the definition
+        *      of configMAX_SYSCALL_INTERRUPT_PRIORITY on
+        *      https://www.freertos.org/a00110.html
+        *   3) Calling an API function from within a critical section or when
+        *      the scheduler is suspended, or calling an API function that does
+        *      not end in "FromISR" from an interrupt.
+        *   4) Using a queue or semaphore before it has been initialised or
+        *      before the scheduler has been started (are interrupts firing
+        *      before vTaskStartScheduler() has been called?).
+        **********************************************************************/
+
+#ifdef VERIFAST /*< ***over-approximate list insert loop*** */
+        pxIterator = choose(pxList);
+#else
+        for( pxIterator = ( ListItem_t * ) &( pxList->xListEnd ); pxIterator->pxNext->xItemValue <= xValueOfInsertion; pxIterator = pxIterator->pxNext ) /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM.  This is checked and valid. *//*lint !e440 The iterator moves to a different value, not xValueOfInsertion. */
+        {
+            /* There is nothing to do here, just iterating to the wanted
+             * insertion position. */
+        }
+#endif
+        /*@int i = index_of(pxIterator, cells);@*/
+        /*@
+        if (pxIterator == end)
+        {
+            open DLS(end, endprev, end, endprev, cells, vals, pxList);
+            open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
+            if (end != endprev)
+            {
+                assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
+                open DLS(endnext, _, _, _, _, _, _);
+                open xLIST_ITEM(endnext, _, _, _, _);
+            }
+        }
+        else
+        {
+            assert DLS(end, endprev, end, endprev, cells, vals, pxList);
+            dls_first_mem(end, endprev, end, endprev, cells);
+            assert pxIterator != end;
+            assert index_of(end, cells) == 0;
+            split(end, endprev, end, endprev, cells, vals, pxIterator, i);
+            assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList);
+            assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
+            open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
+            open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList);
+            if (pxIterator == endprev)
+            {
+                open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
+                take_take(1, i, vals);
+                assert xLIST_ITEM(end, portMAX_DELAY, _, _, _);
+                open xLIST_ITEM(iternext, _, _, pxIterator, _);
+            }
+            else
+            {
+                open DLS(iternext, pxIterator, end, endprev, _, _, _);
+                open xLIST_ITEM(iternext, _, _, pxIterator, _);
+            }
+        }@*/
+    }
+
+    pxNewListItem->pxNext = pxIterator->pxNext;
+    pxNewListItem->pxNext->pxPrevious = pxNewListItem;
+    pxNewListItem->pxPrevious = pxIterator;
+    pxIterator->pxNext = pxNewListItem;
+
+    /* Remember which list the item is in.  This allows fast removal of the
+     * item later. */
+    pxNewListItem->pxContainer = pxList;
+
+    ( pxList->uxNumberOfItems )++;
+
+    /*@close xLIST_ITEM(pxNewListItem, val, ?iternext, pxIterator, pxList);@*/
+    /*@close xLIST_ITEM(pxIterator, ?iterval, pxNewListItem, ?iterprev, pxList);@*/
+    /*@
+    if( xValueOfInsertion == portMAX_DELAY )
+    {
+        assert iternext == end;
+        assert pxIterator == endprev;
+        if (end == endprev)
+        {
+            close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
+            close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
+            join(end, pxNewListItem, pxNewListItem, end, cells, vals,
+                pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+            close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+        }
+        else
+        {
+            close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
+            close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
+            if (endnext == endprev)
+            {
+                assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList);
+                close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList);
+                close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList);
+                join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY),
+                    endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval));
+                assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList);
+            }
+            else
+            {
+                assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
+                assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells));
+                assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1;
+                assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells));
+                assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList);
+                close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
+                dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev);
+                dls_star_item(endnext, endprevprev, end);
+                close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList);
+                join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev),
+                    endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
+                assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
+
+            }
+            join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
+                pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+            remove_append(pxNewListItem, cells, singleton(pxNewListItem));
+            close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+        }
+    }
+    else
+    {
+        if (pxIterator == end)
+        {
+            if (iternext == end)
+            {
+                close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
+                close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
+                join(end, pxNewListItem, pxNewListItem, end, cells, vals,
+                    pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+                close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+            }
+            else
+            {
+                close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
+                if (iternext == endprev)
+                {
+                    close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
+                    dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext));
+                }
+                else
+                {
+                    assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList);
+                    close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList);
+                    dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev));
+                }
+                close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
+                assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList);
+                dls_star_item(iternext, endprev, pxNewListItem);
+                close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList);
+                join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY),
+                    pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev));
+                close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev)));
+            }
+        }
+        else
+        {
+            close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
+            if (pxIterator == endprev)
+            {
+                if (iterprev == end)
+                {
+                    close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList);
+                }
+                else
+                {
+                    assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _);
+                    close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList);
+                }
+                int i = index_of(pxIterator, cells);
+                assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
+                close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList);
+                close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
+                join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals),
+                    pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals));
+                join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals,
+                    pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+                close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+                remove_append(pxNewListItem, cells, singleton(pxNewListItem));
+            }
+            else
+            {
+                int i = index_of(pxIterator, cells);
+                if (iternext == endprev)
+                {
+                    close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
+                }
+                else
+                {
+                    assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList);
+                    dls_star_item(end, iterprev, iternext);
+                    close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList);
+                }
+                drop_drop(1, i, cells);
+                drop_drop(1, i, vals);
+                assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList);
+                assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
+                dls_star_item(iternext, endprev, pxNewListItem);
+                dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells));
+                close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList);
+                close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList);
+                join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals),
+                    pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))));
+                list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
+                list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
+                head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
+                take_head(take(i, cells));
+                take_take(1, i, cells);
+                assert( end == head(new_cells) );
+                head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
+                take_head(take(i, vals));
+                take_take(1, i, vals);
+                assert( portMAX_DELAY == head(new_vals) );
+                append_take_drop_n(cells, index_of(pxIterator, cells));
+                close xLIST(pxList, len+1, idx, end, append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))), append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))));
+                mem_take_false(pxNewListItem, i, cells);
+                remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
+            }
+        }
+    }@*/
+}
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c b/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c
new file mode 100644
index 000000000..063eeb7a6
--- /dev/null
+++ b/FreeRTOS/Test/VeriFast/list/vListInsertEnd.c
@@ -0,0 +1,234 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include "proof/list.h"
+
+void vListInsertEnd( List_t * const pxList,
+                     ListItem_t * const pxNewListItem )
+/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/
+/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
+    idx == end
+        ? (new_cells == append(cells, singleton(pxNewListItem)) &*&
+            new_vals == append(vals, singleton(val)))
+        : (new_cells == append(take(index_of(idx, cells), cells), append(singleton(pxNewListItem), drop(index_of(idx, cells), cells))) &*&
+            new_vals == append(take(index_of(idx, cells), vals), append(singleton(val), drop(index_of(idx, cells), vals))));@*/
+{
+    /*@xLIST_star_item(pxList, pxNewListItem);@*/
+    /*@assert mem(pxNewListItem, cells) == false;@*/
+    /*@open xLIST(pxList, len, idx, end, cells, vals);@*/
+#ifdef VERIFAST /*< const pointer declaration */
+    ListItem_t * pxIndex = pxList->pxIndex;
+#else
+    ListItem_t * const pxIndex = pxList->pxIndex;
+
+    /* Only effective when configASSERT() is also defined, these tests may catch
+     * the list data structures being overwritten in memory.  They will not catch
+     * data errors caused by incorrect configuration or use of FreeRTOS. */
+    listTEST_LIST_INTEGRITY( pxList );
+    listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );
+#endif
+
+    /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
+    /*@assert DLS(end, ?endprev, end, _, cells, vals, pxList);@*/
+    /*@dls_first_mem(end, endprev, end, endprev, cells);@*/
+    /*@dls_last_mem(end, endprev, end, endprev, cells);@*/
+    /*@
+    if (end == idx)
+    {
+        open DLS(end, endprev, end, endprev, cells, vals, pxList);
+        open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
+        if (end == endprev)
+        {
+            // Case A (singleton): idx==end==endprev
+        }
+        else
+        {
+            assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
+            if (endnext == endprev)
+            {
+                // Case B (two): idx==end and endnext==endprev
+                open DLS(endnext, end, end, endnext, _, _, _);
+                open xLIST_ITEM(endnext, _, _, _, _);
+            }
+            else
+            {
+                // Case C: idx==end and DLS:endnext...endprev
+                split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
+                open DLS(endprev, _, _, _, _, _, _);
+                open xLIST_ITEM(endprev, _, _, _, _);
+            }
+        }
+    }
+    else
+    {
+        int i = index_of(idx, cells);
+        split(end, endprev, end, endprev, cells, vals, idx, i);
+        assert DLS(end, endprev, idx, ?idxprev, take(i, cells), take(i, vals), pxList);
+        assert DLS(idx, idxprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
+        open DLS(idx, idxprev, end, endprev, _, _, _);
+        open xLIST_ITEM(idx, _, _, _, _);
+        if (end == idxprev)
+        {
+            // Case D: end==idxprev and DLS:idx...endprev
+            take_take(1, i, vals);
+            take_head(vals);
+            open DLS(end, endprev, idx, idxprev, take(i, cells), take(i, vals), pxList);
+            open xLIST_ITEM(end, portMAX_DELAY, _, _, _);
+            assert length(take(i, cells)) == 1;
+        }
+        else
+        {
+            // Case E: DLS:end...idxprev and DLS:idx...endprev
+            dls_last_mem(end, endprev, idx, idxprev, take(i, cells));
+            split(end, endprev, idx, idxprev, take(i, cells), take(i, vals), idxprev, index_of(idxprev, take(i, cells)));
+            open DLS(idxprev, _, _, idxprev, _, _, _);
+            length_take(i, cells);
+            drop_take_singleton(i, vals);
+            open xLIST_ITEM(idxprev, nth(i-1, vals), _, _, _);
+        }
+    }
+    @*/
+
+    /* Insert a new list item into pxList, but rather than sort the list,
+     * makes the new list item the last item to be removed by a call to
+     * listGET_OWNER_OF_NEXT_ENTRY(). */
+    pxNewListItem->pxNext = pxIndex;
+    pxNewListItem->pxPrevious = pxIndex->pxPrevious;
+
+    /* Only used during decision coverage testing. */
+    mtCOVERAGE_TEST_DELAY();
+
+    pxIndex->pxPrevious->pxNext = pxNewListItem;
+    pxIndex->pxPrevious = pxNewListItem;
+
+    /* Remember which list the item is in. */
+    pxNewListItem->pxContainer = pxList;
+
+    ( pxList->uxNumberOfItems )++;
+
+    /*@
+    if (end == idx)
+    {
+        close xLIST_ITEM(pxNewListItem, val, end, endprev, pxList);
+        close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
+        close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
+        if (end == endprev)
+        {
+            // Case A (singleton): idx==end==endprev
+            close DLS(end, pxNewListItem, endnext, end, cells, vals, pxList);
+            join(end, pxNewListItem, endnext, end, cells, vals,
+                pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+            close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+        }
+        else
+        {
+            close xLIST_ITEM(endprev, ?endprevval, pxNewListItem, ?endprevprev, _);
+            if (endnext == endprev)
+            {
+                // Case B (two): idx==end and endnext==endprev
+                close DLS(endprev, end, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
+                close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
+                join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
+                    pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+                close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+            }
+            else
+            {
+                // Case C: idx==end and DLS:endnext...endprev
+                close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
+                assert DLS(endnext, end, endprev, endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
+                join(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev, vals_endnext_to_endprevprev,
+                     endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
+                close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
+                join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
+                     pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
+                close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
+            }
+        }
+    }
+    else
+    {
+        // Case D: end==idxprev and DLS:idx...endprev
+        // Case E: DLS:end...idxprev and DLS:idx...endprev
+        int i = index_of(idx, cells);
+        close xLIST_ITEM(pxNewListItem, val, idx, ?idxprev, pxList);
+        close xLIST_ITEM(idx, ?idxval, ?idxnext, pxNewListItem, pxList);
+        nth_drop2(vals, i);
+        assert idxval == nth(i, vals);
+        close xLIST_ITEM(idxprev, ?idxprevval, pxNewListItem, ?idxprevprev, pxList);
+
+        if (end == idxprev)
+        {
+            close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
+        }
+        else
+        {
+            length_take(i, cells);
+            take_take(i-1, i, vals);
+            take_singleton(i-1, vals);
+            take_singleton(i, vals);
+            assert DLS(end, endprev, idxprev, idxprevprev, ?cells_end_to_idxprevprev, take(i-1, vals), pxList);
+            close DLS(idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval), pxList);
+            join(end, endprev, idxprev, idxprevprev, cells_end_to_idxprevprev, take(i-1, vals),
+                 idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval));
+        }
+
+        if (idx == endprev)
+        {
+            close DLS(idx, pxNewListItem, end, idx, singleton(idx), singleton(idxval), pxList);
+        }
+        else
+        {
+            assert DLS(end, endprev, pxNewListItem, idxprev, ?cells_end_to_idxprev, ?vals_end_to_idxprev, pxList);
+            close DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList);
+        }
+
+        assert DLS(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), pxList);
+        assert DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList);
+        assert xLIST_ITEM(pxNewListItem, val, idx, idxprev, pxList);
+        dls_star_item(idx, endprev, pxNewListItem);
+        close DLS(pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)), pxList);
+        join(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals),
+             pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)));
+        assert DLS(end, endprev, end, endprev, ?cells_new, ?vals_new, pxList);
+        assert cells_new == append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells)));
+        assert vals_new == append(take(i, vals) , append(singleton(val), drop(i, vals)));
+        head_append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells)));
+        take_take(1, i, cells);
+        head_append(take(i, vals), append(singleton(val), drop(i, vals)));
+        take_take(1, i, vals);
+        close xLIST(pxList, len+1, idx, end, cells_new, vals_new);
+    }
+    @*/
+}
+
+void client_example1( List_t * const l, ListItem_t * const pxNewListItem )
+/*@requires
+    xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
+    xLIST_ITEM(pxNewListItem, ?val, _, _, _) &*&
+    idx == end;@*/
+/*@ensures
+    xLIST(l, len + 1, idx, end, _, append(vals, singleton(val)));@*/
+{
+    vListInsertEnd(l, pxNewListItem);
+}
diff --git a/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh b/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh
index 3384ea1aa..b49fc84bc 100755
--- a/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh
+++ b/FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh
@@ -1,3 +1,3 @@
 #!/bin/bash -eu
 
-NO_COVERAGE=1 EXTRA_VERIFAST_ARGS=-stats make queue | grep overhead: | sort | uniq
+NO_COVERAGE=1 EXTRA_VERIFAST_ARGS=-stats make queue list | grep overhead: | sort | uniq
diff --git a/FreeRTOS/Test/VeriFast/scripts/diff_files.md b/FreeRTOS/Test/VeriFast/scripts/diff_files.md
index 59f62d364..cfc2fb7de 100644
--- a/FreeRTOS/Test/VeriFast/scripts/diff_files.md
+++ b/FreeRTOS/Test/VeriFast/scripts/diff_files.md
@@ -16,7 +16,7 @@ implementation and the proof directory.
 ```
 cd scripts
 ./generate_diff_files.sh
-# will extract to ./FreeRTOS-Kernel/generated and ./queue/generated
+# will extract to ./FreeRTOS-Kernel/generated and ./queue/generated and ./list/generated
 ```
 
 Then use `diff` for a side-by-side comparison.  Note that the `--color=always`
@@ -24,12 +24,14 @@ flag needs v3.4+:
 
 ```
 diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated queue/generated | less -r
+diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated list/generated | less -r
 ```
 
 Or generate a html report using `diff2html`:
 
 ```
 diff -u FreeRTOS-Kernel/generated queue/generated | diff2html -i stdin
+diff -u FreeRTOS-Kernel/generated list/generated | diff2html -i stdin
 ```
 
 The expectation is that the proofs make minimal changes to the original source
diff --git a/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh
index 55f9cfbd2..db4d9469a 100755
--- a/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh
+++ b/FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh
@@ -1,6 +1,6 @@
 #!/bin/bash -eu
 
-FUNCS=(
+QUEUE_FUNCS=(
   prvCopyDataFromQueue
   prvCopyDataToQueue
   prvInitialiseNewQueue
@@ -22,6 +22,14 @@ FUNCS=(
   xQueueReceiveFromISR
 )
 
+LIST_FUNCS=(
+  uxListRemove
+  vListInitialise
+  vListInitialiseItem
+  vListInsertEnd
+  vListInsert
+)
+
 if [ ! -d "FreeRTOS-Kernel" ]; then
     git clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git
 fi
@@ -29,7 +37,11 @@ pushd FreeRTOS-Kernel > /dev/null
 rm -rf tags generated
 ctags --excmd=number queue.c
 mkdir generated
-for f in ${FUNCS[@]}; do
+for f in ${QUEUE_FUNCS[@]}; do
+  ../extract.py tags $f > generated/$f.c
+done
+ctags --excmd=number list.c
+for f in ${LIST_FUNCS[@]}; do
   ../extract.py tags $f > generated/$f.c
 done
 popd > /dev/null
@@ -40,8 +52,19 @@ pushd queue > /dev/null
 rm -rf tags generated
 ctags --excmd=number *.c
 mkdir generated
-for f in ${FUNCS[@]}; do
+for f in ${QUEUE_FUNCS[@]}; do
   ../scripts/extract.py tags $f > generated/$f.c
 done
 popd > /dev/null
 echo "created: queue/generated"
+
+ln -fs ../list .
+pushd list > /dev/null
+rm -rf tags generated
+ctags --excmd=number *.c
+mkdir generated
+for f in ${LIST_FUNCS[@]}; do
+  ../scripts/extract.py tags $f > generated/$f.c
+done
+popd > /dev/null
+echo "created: list/generated"