diff --git a/docs/EXPERIMENTAL_SETUP.md b/docs/EXPERIMENTAL_SETUP.md
index e17fbf83..d4db83c8 100644
--- a/docs/EXPERIMENTAL_SETUP.md
+++ b/docs/EXPERIMENTAL_SETUP.md
@@ -16,6 +16,20 @@ assurance of low-assurance components, mitigate risk in third-party components,
 and maintain the high level of assurance in high-assurance components with lower
 time, effort, and expertise.
 
+- [Experimental Setup](#experimental-setup)
+  - [Red Team Analysis](#red-team-analysis)
+    - [SHAVE Trusted Boot](#shave-trusted-boot)
+    - [Mission Protection System (MPS)](#mission-protection-system-mps)
+    - [pKVM](#pkvm)
+    - [Message Bus](#message-bus)
+    - [Ardupilot](#ardupilot)
+    - [Scenarios](#scenarios)
+  - [Change Events](#change-events)
+    - [Change Event 1: Change SHA to XMSS in Secure boot](#change-event-1-change-sha-to-xmss-in-secure-boot)
+    - [Change event 2: Add network functionality to MPS](#change-event-2-add-network-functionality-to-mps)
+  - [Generate Specifications](#generate-specifications)
+
+
 ## Red Team Analysis
 
 Red Balloon Security will perform a preliminary evaluation of a baseline version
@@ -88,3 +102,18 @@ component and additional notes on how they will be used.
 ## Change Events
 
 The first change event is to modify the HARDENS protection system such that it fits the engine protection domain and runs inside the OpenSUT environment. We will track our change events as we proceed with the development of OpenSUT.
+
+### Change Event 1: Change SHA to XMSS in Secure boot
+
+Tracking issue: [#125](https://github.com/GaloisInc/VERSE-OpenSUT/issues/125)
+
+### Change event 2: Add network functionality to MPS
+
+Tracking issue: [#126](https://github.com/GaloisInc/VERSE-OpenSUT/issues/126)
+
+
+## Generate Specifications
+
+* Used: ChatGPT 4o
+* Prompt:
+    > You are a helpful assistant, and your job is to generate code specifications for C code in a new specification language called CN. CN is similar to Frama-C, and it eliminates undefined behavior from your C program. First, you will need to learn how to write CN specifications from CN tutorial (available online at https://rems-project.github.io/cn-tutorial/) and then I will give some some C code that you will write specifications for.
\ No newline at end of file
diff --git a/docs/ai-experiments/README.md b/docs/ai-experiments/README.md
new file mode 100644
index 00000000..20b43d02
--- /dev/null
+++ b/docs/ai-experiments/README.md
@@ -0,0 +1,155 @@
+# AI experiments with CN
+
+## OpenAI ChatGPT
+
+I attempted to use [OpenAI Assistant API](https://platform.openai.com/docs/assistants/overview) which seems suitable for this task. Ideally, we would add a [custom function call](https://platform.openai.com/docs/guides/function-calling#function-calling-with-structured-outputs) that would call to `cn verify` to test the validity of the output. [openai-quickstart-python](https://github.com/openai/openai-quickstart-python/) has all the components to get started quickly. However, as a first step, I manually interacted with the ChatGPT chat.
+
+I attempted to feed ChatGPT with CN grammar, the tutorial and relevant subset of the tutorial example, hoping that will provide enough data to *fine-tune* the GPT for this task. I used ChatGPT-4o.
+
+After the initial setup, I continued by providing sample C code and the CN error, and asking GPT to provide CN specs for the code that fix the CN errors. I asked both for all specs and only for individual functions, but the result was identical in terms of quality.
+
+The results were following:
+* GPT can learn the language grammar quickly
+* GPT failed to learn various language details, such as how to handle constants in the specs (CN_NULL vs NULL)
+* GPT was unable to generate useful specs with the limited training data I had available
+
+### Examples
+
+
+First take at `client_new()` seemed to correctly identify disjoint return values (NULL vs non NULL),
+but struggled to use correct constants (I believe `CN_NULL` is not a CN constant, and `CS_RECV_KEY_ID` would have to be defined somewhere in the specs). The or `||` operator seems to be incorrect as well, as the CN parser complains with `unexpected token after '||' and before 'take'`:
+
+```C
+struct client* client_new(int fd)
+/*@ requires true;
+    ensures return == CN_NULL || take C = Owned<struct client>(return);
+            if (return != CN_NULL) {
+                C.fd == fd;
+                C.pos == 0u8;
+                C.state == CS_RECV_KEY_ID;
+            };
+@*/
+{
+    struct client* c = malloc(sizeof(struct client));
+    if (c == NULL) {
+        perror("malloc (client_new)");
+        return NULL;
+    }
+    c->fd = fd;
+    c->pos = 0;
+    c->state = CS_RECV_KEY_ID;
+    return c;
+}
+```
+
+ChatGPT was unable to fix the specs even after I provided the error message, so I moved on to `client_read_buffer()`: 
+
+
+```C
+const char* client_read_buffer(struct client* c)
+/*@ requires take C = Owned<struct client>(c);
+    ensures take C_post = Owned<struct client>(c);
+            C == C_post;
+            return == (c->state == CS_RECV_KEY_ID ? c->key_id : 
+                      (c->state == CS_RECV_VALUE ? c->value : CN_NULL));
+@*/
+{
+    switch (c->state) {
+    case CS_RECV_KEY_ID:
+        return c->key_id;
+    case CS_RECV_VALUE:
+        return c->value;
+    default:
+        return NULL;
+    }
+}
+```
+
+In this case the constants were not declared properly in the specs, thus leading to a predicable error:
+
+```
+client.c:68:36: error: the variable `CS_RECV_VALUE' is not declared
+                      (c->state == CS_RECV_VALUE ? c->value : CN_NULL));
+```
+
+I fed ChatGPT with the [style guide](https://rems-project.github.io/cn-tutorial/getting-started/style-guide/#constants) which explains how to use constants, and got a little bit further, but ChatGPT does not understand types so the types of the constants were wrong. After a little bit of back-and-forth I ended up with:
+
+```C
+const char* client_read_buffer(struct client* c)
+/*@ requires take C = Owned<struct client>(c);
+    ensures take C_post = Owned<struct client>(c);
+            C == C_post;
+            return == (c->state == CS_RECV_KEY_ID ? c->key_id : 
+                      (c->state == CS_RECV_VALUE ? c->value : CN_NULL));
+@*/
+{
+    ...
+```
+
+which fails with:
+
+```
+client.c:75:68: error: Type error
+                      (c->state == CS_RECV_VALUE() ? c->response : NULL));
+                                                                   ^
+Expression 'NULL' has type 'pointer'.
+I expected it to have type 'map<u64, u8>' because of client.c:75:54:
+                      (c->state == CS_RECV_VALUE() ? c->response : NULL));
+
+```
+
+
+Then I moved onto a trivial spec for `client_change_state()` which was generated incorrectly (notice the use of the old state, and the superfluous line at the end of the specs):
+
+
+
+```C
+void client_change_state(struct client* c, enum client_state new_state)
+/*@ requires take C = Owned<struct client>(c);
+    ensures take C_post = Owned<struct client>(c);
+            C_post.state == new_state;
+            C.fd == C_post.fd;
+            C.pos == C_post.pos;
+            (C_post.state != C.state implies C == C_post);
+@*/
+{
+    c->state = new_state;
+    c->pos = 0;
+}
+```
+
+At that point I gave up.
+
+### Conclusion
+
+With the limited training and limited examples, I was not able to get meaningful results from ChatGPT. In order to improve the accuracy, I suspect needing to use [fine-tuning](https://platform.openai.com/docs/guides/fine-tuning). Another approach could be using *function calling* to call `cn verify` to provide hints and error messages back to the assistant.
+
+### References
+
+* ChatGPT CN specification writing chat: https://chatgpt.com/share/6747b6e9-8294-8004-93b2-976eea501878
+* Assistant API overview: https://platform.openai.com/docs/assistants/overview
+* Assistant AI deep dive: https://platform.openai.com/docs/assistants/deep-dive
+* Function calling: https://platform.openai.com/docs/guides/function-calling#function-calling-with-structured-outputs
+* Assistants function calling: https://platform.openai.com/docs/assistants/tools/function-calling?context=without-streaming
+* Training data:
+  * Grammar reference (I am assuming the grammar is actually up to date): https://github.com/rems-project/cerberus/blob/master/backend/cn/manual/grammar.md
+  * [CN errors](./sources/examples_errors.md)
+  * [CN specs](./sources/examples_good.md)
+
+
+## Google NotebookLM
+
+Google's NotebookLM consumes sources (web pages, documents, text) and creates a custom model capable of reasoning about those sources. One way to think of it is a search with some contextual understanding. I fed NotebookLM the CN tutorial, the grammar, the CN manual and the training files from the previous example, filling approximately 50% of the NotebookLM's capacity.
+
+The use of such *CN notebook* is faster searching for the right solution, for example you can provide an error message provided by CN and ask for recommendations how to fix it / what it means. NotebookLM will point you to the right solution, but it does not generate new data.
+
+![lm-example](./lm-example.png)
+
+### Summary
+
+The notebook was somewhat useful, and it is good at finding the right source for the user query. It seems to work best over plain text, or with text with minimal formatting. The consumed websites and code were flattened to plain text, thus making the sources harder to read/understand. I expect the notebook to be much more useful if it supported code snippets and other more advanced text formatting.
+
+### References
+
+* [CN NotebookLM link](https://notebooklm.google.com/notebook/50eea5e0-7a66-4e81-962e-59501249a415?pli=1) - NOTE it can be shared only within Galois workspace
+* more info: https://notebooklm.google.com/
diff --git a/docs/ai-experiments/lm-example.png b/docs/ai-experiments/lm-example.png
new file mode 100644
index 00000000..abc5a8fc
Binary files /dev/null and b/docs/ai-experiments/lm-example.png differ
diff --git a/docs/ai-experiments/sources/examples_errors.md b/docs/ai-experiments/sources/examples_errors.md
new file mode 100644
index 00000000..5343392a
--- /dev/null
+++ b/docs/ai-experiments/sources/examples_errors.md
@@ -0,0 +1,244 @@
+# Example CN errors and solutions
+
+## Array Load
+
+Broken file:
+
+```C
+int read (int *p, int n, int i)
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
+             0i32 <= i && i < n; 
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
+{
+  return p[i];
+}
+```
+
+Error:
+```
+array_load.broken.c:2:19: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                  ^
+array_load.broken.c:5:18: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                 ^
+[1/1]: read -- fail
+array_load.broken.c:9:10: error: `&p[(u64)i]` out of bounds
+  return p[i];
+         ^~~~ 
+(UB missing short message): UB_CERB004_unspecified__pointer_add
+```
+
+Fix #1:
+```C
+int read (int *p, int n, int i)
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
+             0i32 <= i && i < n; 
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
+{
+  /*@ extract Owned<int>, i; @*/
+  return p[i];
+}
+```
+
+Fix #2:
+```
+int read (int *p, int n, int i)
+/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+             0i32 <= i && i < n;
+    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+            a1 == a2;
+            return == a1[i];
+@*/
+{
+  /*@ extract Owned<int>, i; @*/
+  return p[i];
+}
+```
+
+## Read
+
+Broken file:
+
+```C
+int read (int *p)
+/*@ requires take v1 = Owned<int>(p); @*/
+{
+  return *p;
+}
+
+```
+
+Error:
+```
+[1/1]: read -- fail
+read.broken.c:4:3: error: Left-over unused resource 'Owned<signed int>(p)(v1)'
+  return *p;
+  ^~~~~~~~~~ 
+
+```
+
+Fix #1:
+```C
+int read (int *p)
+
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
+@*/
+
+{
+  return *p;
+}
+
+```
+
+Fix #2:
+```C
+int read (int *p)
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
+            return == P;
+            P_post == P;
+@*/
+{
+  return *p;
+}
+
+```
+
+## Signed Increment
+
+Broken file:
+
+```C
+void incr (int *p)
+/*@ requires take v1 = Block<int>(p);
+    ensures take v2 = Owned<int>(p);
+            v2 == v1+1i32; @*/
+{
+  int n = *p;
+  int m = n+1;
+  *p = m;
+}
+
+```
+
+Error:
+```
+[1/1]: incr -- fail
+slf0_incr.broken.c:8:11: error: Missing resource for reading
+  int n = *p;
+          ^~ 
+Resource needed: Owned<signed int>(p)
+```
+
+Fix #1:
+```C
+void incr (int *p)
+/*@ requires take v1 = Owned<int>(p);
+    requires let N = (i64) v1;
+             (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32();
+             (i64)MINi32() <= N + N; N + N <= (i64)MAXi32();
+    ensures take v2 = Owned<int>(p);
+            v2 == v1+1i32; @*/
+{
+  int n = *p;
+  int m = n+1;
+  *p = m;
+}
+
+```
+
+
+## Transpose
+
+Broken file:
+
+```C
+struct point { int x; int y; };
+
+void transpose (struct point *p) 
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
+@*/
+{
+  int temp_x = p->x;
+  int temp_y = p->y;
+  /*@ assert(false); @*/
+  p->x = temp_y;
+  p->y = temp_x;
+}
+
+```
+
+Error:
+```
+[1/1]: transpose -- fail
+transpose.broken.c:12:7: error: Unprovable constraint
+  /*@ assert(false); @*/
+      ^~~~~~~~~~~~~~ 
+Constraint from transpose.broken.c:12:7:
+  /*@ assert(false); @*/
+      ^~~~~~~~~~~~~~ 
+
+```
+
+Fix #1:
+```C
+struct point { int x; int y; };
+
+void transpose (struct point *p) 
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
+@*/
+{
+  int temp_x = p->x;
+  int temp_y = p->y;
+  p->x = temp_y;
+  p->y = temp_x;
+}
+
+```
+
+
+Fix #2:
+```C
+void swap (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
+@*/
+{
+  unsigned int m = *p;
+  unsigned int n = *q;
+  *p = n;
+  *q = m;
+}
+
+struct upoint { unsigned int x; unsigned int y; };
+
+void transpose2 (struct upoint *p)
+
+/*@ requires take P = Owned<struct upoint>(p);
+    ensures take P_post = Owned<struct upoint>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
+@*/
+
+{
+  swap(&p->x, &p->y);
+}
+
+```
\ No newline at end of file
diff --git a/docs/ai-experiments/sources/examples_good.md b/docs/ai-experiments/sources/examples_good.md
new file mode 100644
index 00000000..5ac587a5
--- /dev/null
+++ b/docs/ai-experiments/sources/examples_good.md
@@ -0,0 +1,832 @@
+# Example CN programs
+
+File abs.c
+
+```C
+int abs (int x)
+
+/*@ requires MINi32() < x;
+    ensures return == ((x >= 0i32) ? x : (0i32-x));
+@*/
+
+{
+  if (x >= 0) {
+    return x;
+  } else {
+    return -x;
+  }
+}
+```
+
+File abs_mem.c
+
+```C
+int abs_mem (int *p)
+
+/*@ requires take x = Owned<int>(p);
+             MINi32() < x;
+    ensures take x_post = Owned<int>(p);
+            x == x_post;
+            return == ((x >= 0i32) ? x : (0i32-x));
+@*/
+
+{
+  int x = *p;
+  if (x >= 0) {
+    return x;
+  }
+  else {
+    return -x;
+  }
+}
+```
+
+File abs_mem_struct.c
+
+```C
+int abs_mem (int *p)
+
+/*@ requires take x = Owned<int>(p);
+             MINi32() < x;
+    ensures take x2 = Owned<int>(p);
+            x == x2;
+            return == ((x >= 0i32) ? x : (0i32-x));
+@*/
+
+{
+  int x = *p;
+  if (x >= 0) {
+    return x;
+  }
+  else {
+    return -x;
+  }
+}
+
+
+
+struct tuple {
+  int x;
+  int y;
+};
+
+
+int abs_y (struct tuple *p)
+/*@ requires take s = Owned(p);
+             MINi32() < s.y;
+    ensures  take s2 = Owned(p);
+             s == s2;
+             return == ((s.y >= 0i32) ? s.y : (0i32-s.y));
+@*/
+{
+  return abs_mem(&p->y);
+}
+```
+
+File add_0.c
+
+```C
+int add(int x, int y)
+
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/
+
+{
+  return x+y;
+}
+```
+
+File add_1.c
+
+```C
+int add(int x, int y)
+
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64;
+    ensures return == (i32) Sum;
+@*/
+
+{
+  return x+y;
+}
+```
+
+File add_2.c
+
+```C
+int add(int x, int y)
+
+/*@ requires let Sum = (i64) x + (i64) y;
+             (i64)MINi32() <= Sum; Sum <= (i64)MAXi32();
+    ensures return == (i32) Sum;
+@*/
+
+{
+  return x+y;
+}
+```
+
+File add_read.c
+
+```C
+unsigned int add (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P == P_post && Q == Q_post;
+            return == P + Q;
+@*/
+{
+  unsigned int m = *p;
+  unsigned int n = *q;
+  return m+n;
+}
+```
+
+File add_two_array.c
+
+```C
+unsigned int array_read_two (unsigned int *p, int n, int i, int j)
+
+/*@ requires take A = each(i32 k; 0i32 <= k && k < n) { 
+                        Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+             0i32 <= i && i < n;
+             0i32 <= j && j < n;
+             j != i;
+    ensures take A_post = each(i32 k; 0i32 <= k && k < n) { 
+                            Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+            A == A_post;
+            return == A[i] + A[j];
+@*/
+
+{
+
+  /*@ extract Owned<unsigned int>, i; @*/
+
+  unsigned int tmp1 = p[i];
+
+  /*@ extract Owned<unsigned int>, j; @*/
+
+  unsigned int tmp2 = p[j];
+  return (tmp1 + tmp2);
+}
+```
+
+File bcp_framerule.c
+
+```C
+void incr_first (unsigned int *p, unsigned int *q)
+/*@ requires take pv = Owned<unsigned int>(p);
+    ensures take pv_ = Owned<unsigned int>(p);
+            pv_ == pv + 1u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+}
+
+void incr_first_frame (unsigned int *p, unsigned int *q)
+/*@ requires take pv = Owned<unsigned int>(p);
+             take qv = Owned<unsigned int>(q);
+    ensures take pv_ = Owned<unsigned int>(p);
+            take qv_ = Owned<unsigned int>(q);
+            pv_ == pv + 1u32;
+            qv_ == qv;
+@*/
+{
+  incr_first(p, q);
+}
+```
+
+File const_example.c
+
+```C
+#define CONST 1
+    /*@ function (i32) CONST () @*/
+    static int c_CONST() /*@ cn_function CONST; @*/ { return CONST; }
+
+int foo (int x)
+/*@
+  requires true;
+  ensures return == CONST();
+@*/
+{
+  return CONST;
+}
+```
+
+File const_example_lessgood.c
+
+```C
+#define CONST 1
+/*@ function (i32) CONST () { 1i32 } @*/
+```
+
+File init_array2.c
+
+```C
+void init_array2 (char *p, unsigned int n)
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
+@*/
+{
+  unsigned int j = 0;
+  while (j < n)
+
+  /*@ inv take Al = each(u32 i; i < j) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; j <= i && i < n) { 
+                      Block<char>( array_shift<char>(p, i)) };
+          {p} unchanged; {n} unchanged;
+          j <= n;
+  @*/
+
+  {
+
+    /*@ extract Block<char>, j; @*/
+    /*@ extract Owned<char>, j; @*/
+
+    p[j] = 0;
+    j++;
+  }
+}
+```
+
+File init_array.c
+
+```C
+void init_array (char *p, unsigned int n)
+/*@ requires take A = each(u32 i; i < n) { 
+                         Owned<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
+@*/
+{
+  unsigned int j = 0;
+  while (j < n)
+
+  /*@ inv take Ai = each(u32 i; i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          {p} unchanged; 
+          {n} unchanged;
+  @*/
+
+  {
+
+    /*@ extract Owned<char>, j; @*/
+
+    p[j] = 0;
+    j++;
+  }
+}
+```
+
+File init_array_rev.c
+
+```C
+void init_array_rev (char *p, unsigned int n)
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
+    n > 0u32;
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
+@*/
+{
+  unsigned int j = 0;
+  while (j < n)
+
+  /*@ inv take Al = each(u32 i; i < n-j) { 
+                      Block<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; n-j <= i && i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          {p} unchanged; {n} unchanged;
+          0u32 <= j && j <= n;
+  @*/
+
+  {
+
+    /*@ extract Block<char>, n-(j+1u32); @*/
+    /*@ extract Owned<char>, n-(j+1u32); @*/
+
+    p[n-(j+1)] = 0;
+    j++;
+  }
+}
+```
+
+File init_point.c
+
+```C
+void zero (int *coord) 
+/*@ requires take Coord = Block<int>(coord);
+    ensures take Coord_post = Owned<int>(coord);
+            Coord_post == 0i32; @*/
+{
+  *coord = 0;
+}
+
+struct point { int x; int y; };
+
+void init_point(struct point *p) 
+/*@ requires take P = Block<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == 0i32;
+            P_post.y == 0i32;
+@*/
+{
+  zero(&p->x);
+  zero(&p->y);
+}
+```
+
+File slf10_basic_ref.c
+
+```C
+extern unsigned int *refUnsignedInt (unsigned int v);
+/*@ spec refUnsignedInt(u32 v);
+    requires true;
+    ensures take vr = Owned(return);
+            vr == v;
+@*/
+
+```
+
+File slf11_basic_ref_greater.c
+
+```C
+#include "slf10_basic_ref.c"
+
+unsigned int *ref_greater (unsigned int *p)
+
+/*@ requires take n1 = Owned(p);
+    ensures  take n2 = Owned(p);
+             take m2 = Owned(return);
+             n2 == n1;
+             m2 == n1 + 1u32;
+@*/
+
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  return refUnsignedInt(m);
+}
+```
+
+File slf12_basic_ref_greater_abstract.c
+
+```C
+#include "slf10_basic_ref.c"
+
+unsigned int *ref_greater (unsigned int *p)
+
+/*@ requires take n1 = Owned(p);
+             n1 < n1 + 1u32;
+    ensures  take n2 = Owned(p);
+             take m2 = Owned(return);
+             n2 == n1;
+             m2 > n1;
+@*/
+
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  return refUnsignedInt(m);
+}
+```
+
+File slf15_basic_succ_using_incr_attempt_.c
+
+```C
+/* triple_succ_using_incr_attempt'  cannot be expressed in CN */
+
+```
+
+File slf16_basic_succ_using_incr.c
+
+```C
+#include "free.h"
+#include "ref.h"
+#include "slf0_basic_incr.c"
+
+unsigned int succ_using_incr (unsigned int n)
+/*@ ensures return == n + 1u32; @*/
+{
+  unsigned int *p = refUnsignedInt(n);
+  incr(p);
+  unsigned int x = *p;
+  freeUnsignedInt(p);
+  return x;
+}
+```
+
+File slf17_get_and_free.c
+
+```C
+#include "free.h"
+
+unsigned int get_and_free (unsigned int *p)
+/*@ requires take P = Owned(p);
+    ensures return == P; 
+@*/
+{
+  unsigned int v = *p;
+  freeUnsignedInt (p);
+  return v;
+}
+```
+
+File slf18_two_dice.c
+
+```C
+unsigned int val_rand (unsigned int n);
+/*@ spec val_rand(u32 n);
+    requires n > 0u32;
+    ensures 0u32 <= return && return < n;
+@*/
+
+unsigned int two_dice ()
+/*@ ensures 2u32 <= return && return <= 12u32; @*/
+{
+  unsigned int n1 = val_rand (6);
+  unsigned int n2 = val_rand (6);
+  unsigned int s = n1 + n2;
+  return s + 2;
+}
+```
+
+File slf1_basic_example_let.c
+
+```C
+unsigned int example_let (unsigned int n) 
+/*@ ensures return == 2u32 * n;
+@*/
+{
+  unsigned int a = n+1;
+  unsigned int b = n-1;
+  return a+b;
+}
+
+
+```
+
+File slf1_basic_example_let.signed.c
+
+```C
+int doubled (int n)
+
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32();
+             (i64)MINi32() <= N + N; N + N <= (i64)MAXi32();
+    ensures return == n * 2i32;
+@*/
+
+{
+  int a = n+1;
+  int b = n-1;
+  return a+b;
+}
+```
+
+File slf2_basic_quadruple.c
+
+```C
+unsigned int quadruple (unsigned int n)
+/*@ ensures return == 4u32 * n; @*/
+{
+  unsigned int m = n + n;
+  return m + m;
+}
+```
+
+File slf2_basic_quadruple.signed.c
+
+```C
+int quadruple (int n)
+
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32();
+    ensures return == 4i32 * n;
+ @*/
+
+{
+  int m = n + n;
+  return m + m;
+}
+```
+
+File slf3_basic_inplace_double.c
+
+```C
+void inplace_double (int *p)
+
+/*@ requires take P = Owned<int>(p);
+             let M = 2i64 * ((i64) P);
+             (i64) MINi32() <= M; M <= (i64) MAXi32();
+    ensures  take P_post = Owned<int>(p);
+             P_post == (i32) M;
+@*/
+
+{
+  int n = *p;
+  int m = n + n;
+  *p = m;
+}
+```
+
+File slf7_basic_incr_first.c
+
+```C
+#include "slf0_basic_incr.c"
+
+void incr_first(unsigned int *p, unsigned int *q)
+/*@ requires take n1 = Owned(p);
+             take m1 = Owned(q);
+    ensures  take n2 = Owned(p);
+             take m2 = Owned(q);
+             n2 == n1 + 1u32;
+             m2 == m1;
+@*/
+{
+  incr(p);
+}
+
+
+void incr_first_(unsigned int *p, unsigned int *q)
+/*@ requires take n1 = Owned(p);
+    ensures  take n2 = Owned(p);
+             n2 == n1 + 1u32;
+@*/
+{
+  incr(p);
+}
+```
+
+File slf8_basic_transfer.c
+
+```C
+void transfer (unsigned int *p, unsigned int *q)
+
+/*@ requires take P = Owned(p);
+             take Q = Owned(q);
+    ensures  take P_post = Owned(p);
+             take Q_post = Owned(q);
+             P_post == P + Q;
+             Q_post == 0u32;
+@*/
+
+{
+  unsigned int n = *p;
+  unsigned int m = *q;
+  unsigned int s = n + m;
+  *p = s;
+  *q = 0;
+}
+```
+
+File slf9_basic_transfer_aliased.c
+
+```C
+void transfer (unsigned int *p, unsigned int *q)
+/*@ requires take n1 = Owned(p);
+             ptr_eq(p,q);
+    ensures  take n2 = Owned(p);
+             n2 == 0u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = *q;
+  unsigned int s = n + m;
+  *p = s;
+  *q = 0;
+}
+```
+
+File slf_incr2_alias.c
+
+```C
+// Increment two different pointers (same as above)
+void incr2a (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+  n = *q;
+  m = n+1;
+  *q = m;
+}
+
+// Increment the same pointer twice
+void incr2b (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             ptr_eq(q,p);
+    ensures take P_post = Owned<unsigned int>(p);
+            ptr_eq(q,p);
+            P_post == P + 2u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+  n = *q;
+  m = n+1;
+  *q = m;
+}
+
+void call_both (unsigned int *p, unsigned int *q)
+/*@ requires take pv = Owned<unsigned int>(p);
+             take qv = Owned<unsigned int>(q);
+    ensures take pv_ = Owned<unsigned int>(p);
+            take qv_ = Owned<unsigned int>(q);
+            pv_ == pv + 3u32;
+            qv_ == qv + 1u32;
+@*/
+{
+  incr2a(p, q);   // increment two different pointers
+  incr2b(p, p);   // increment the same pointer twice
+}
+```
+
+File slf_incr2.c
+
+```C
+/*@
+predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q)
+{
+  if (ptr_eq(p,q)) {
+    take PX = Owned<unsigned int>(p);
+    return {P: PX, Q: PX};
+  }
+  else {
+    take PX = Owned<unsigned int>(p);
+    take QX = Owned<unsigned int>(q);
+    return {P: PX, Q: QX};
+  }
+}
+@*/
+
+void incr2(unsigned int *p, unsigned int *q)
+/*@ requires take PQ = BothOwned(p,q);
+    ensures take PQ_post = BothOwned(p,q);
+            PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1u32) : (PQ.P + 2u32));
+            PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1u32) : PQ_post.P);
+@*/
+{
+  /*@ split_case ptr_eq(p,q); @*/
+  unsigned int n = *p;
+  unsigned int m = n + 1;
+  *p = m;
+  n = *q;
+  m = n + 1;
+  *q = m;
+}
+
+void call_both_better(unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+             !ptr_eq(p,q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 3u32;
+            Q_post == Q + 1u32;
+@*/
+{
+  incr2(p, q);
+  incr2(p, p);
+}
+```
+
+File slf_incr2_noalias.c
+
+```C
+void incr2a (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+  n = *q;
+  m = n+1;
+  *q = m;
+}
+
+```
+
+File slf_quadruple_mem.c
+
+```C
+int quadruple_mem (int *p)
+
+/*@ requires take P = Owned<int>(p);
+             let P64 = (i64) P;
+             (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32();
+    ensures take P_post = Owned<int>(p);
+            P_post == P;
+            return == 4i32 * P;
+ @*/
+
+{
+  int m = *p + *p;
+  return m + m;
+}
+```
+
+File slf_ref_greater.c
+
+```C
+#include "malloc.h"
+
+unsigned int *ref_greater_abstract (unsigned int *p)
+
+/*@ requires take P = Owned<unsigned int>(p);
+             P < 4294967295u32;
+    ensures take P_post = Owned<unsigned int>(p);
+            take R = Owned<unsigned int>(return);
+            P == P_post;
+            P <= R;
+@*/
+
+{
+  unsigned int* q = mallocUnsignedInt();
+  *q = *p + 1;
+  return q;
+}
+```
+
+File swap_array.c
+
+```C
+void swap_array (int *p, int n, int i, int j)
+
+/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+             0i32 <= i && i < n;
+             0i32 <= j && j < n;
+             j != i;
+    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+            a2 == a1[i: a1[j], j: a1[i]];
+@*/
+
+{
+
+  /*@ extract Owned<int>, i; @*/
+
+  int tmp = p[i];
+
+  /*@ extract Owned<int>, j; @*/
+
+  p[i] = p[j];
+  p[j] = tmp;
+}
+```
+
+File swap.c
+
+```C
+void swap (unsigned int *p, unsigned int *q)
+
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
+@*/
+
+{
+  unsigned int m = *p;
+  unsigned int n = *q;
+  *p = n;
+  *q = m;
+}
+```
+
+File zero.c
+
+```C
+void zero (int *p)
+
+/*@ requires take P = Block<int>(p);
+    ensures take P_post = Owned<int>(p);
+            P_post == 0i32;
+@*/
+
+{
+  *p = 0;
+}
+```
+