diff --git a/docs/gen.log b/docs/gen.log
new file mode 100644
index 0000000000..2ec4141d83
--- /dev/null
+++ b/docs/gen.log
@@ -0,0 +1,1062 @@
+[
+  {
+    "here": "",
+    "title": "Reach",
+    "isBook": true,
+    "rank": 0
+  },
+  {
+    "here": "build",
+    "title": "Reach is for Builders",
+    "isBook": false,
+    "rank": 5
+  },
+  {
+    "here": "cout",
+    "title": "Compiled Output",
+    "isBook": false,
+    "rank": 60
+  },
+  {
+    "here": "frontend",
+    "title": "Frontends",
+    "isBook": false,
+    "rank": 70
+  },
+  {
+    "here": "changelog",
+    "title": "Changelog",
+    "isBook": false,
+    "rank": 120
+  },
+  {
+    "here": "index",
+    "title": "Index",
+    "isBook": false,
+    "rank": 140
+  },
+  {
+    "here": "model",
+    "title": "Model",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "networks",
+    "title": "Networks",
+    "isBook": false,
+    "rank": 80
+  },
+  {
+    "here": "search",
+    "title": "Search",
+    "isBook": false,
+    "rank": 130
+  },
+  {
+    "here": "tool",
+    "title": "Tool",
+    "isBook": false,
+    "rank": 40
+  },
+  {
+    "here": "rsh",
+    "title": "Language",
+    "isBook": false,
+    "rank": 50
+  },
+  {
+    "here": "tut",
+    "title": "Tutorials",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "trouble",
+    "title": "Troubleshooting",
+    "isBook": false,
+    "rank": 115
+  },
+  {
+    "here": "quickstart",
+    "title": "Quickstart",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "guide",
+    "title": "Guide",
+    "isBook": true,
+    "rank": 110
+  },
+  {
+    "here": "rpc",
+    "title": "RPC Server",
+    "isBook": true,
+    "rank": 90
+  },
+  {
+    "here": "workshop",
+    "title": "Workshops",
+    "isBook": true,
+    "rank": 100
+  },
+  {
+    "here": "rsh/appinit",
+    "title": "Application Initialization",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "rsh/module",
+    "title": "Modules",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "rsh/consensus",
+    "title": "Consensus Steps",
+    "isBook": false,
+    "rank": 50
+  },
+  {
+    "here": "rsh/local",
+    "title": "Local Steps",
+    "isBook": false,
+    "rank": 40
+  },
+  {
+    "here": "rsh/step",
+    "title": "Steps",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "rsh/compute",
+    "title": "Computations",
+    "isBook": false,
+    "rank": 60
+  },
+  {
+    "here": "rsh/errors",
+    "title": "Error Codes",
+    "isBook": false,
+    "rank": 70
+  },
+  {
+    "here": "tut/rsvp",
+    "title": "Répondez S'il Vous Plaît",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "tut/overview",
+    "title": "Overview",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "tut/wfs",
+    "title": "Wisdom For Sale",
+    "isBook": false,
+    "rank": 18
+  },
+  {
+    "here": "tut/rps",
+    "title": "Rock, Paper, Scissors!",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "guide/editor-support",
+    "title": "IDE/Text Editor Support",
+    "isBook": false,
+    "rank": 150
+  },
+  {
+    "here": "guide/ctransfers",
+    "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?",
+    "isBook": false,
+    "rank": 70
+  },
+  {
+    "here": "guide/logging",
+    "title": "How do I add tracing logs to my Reach program?",
+    "isBook": false,
+    "rank": 50
+  },
+  {
+    "here": "guide/loop-invs",
+    "title": "Finding and using loop invariants",
+    "isBook": false,
+    "rank": 90
+  },
+  {
+    "here": "guide/assert",
+    "title": "How and what to verify",
+    "isBook": false,
+    "rank": 80
+  },
+  {
+    "here": "guide/determ",
+    "title": "Determinism, simultaneity, and choice in decentralized applications",
+    "isBook": false,
+    "rank": 110
+  },
+  {
+    "here": "guide/ganache",
+    "title": "How to use Ganache with Reach",
+    "isBook": false,
+    "rank": 140
+  },
+  {
+    "here": "guide/limits",
+    "title": "What are Reach's limitations?",
+    "isBook": false,
+    "rank": 180
+  },
+  {
+    "here": "guide/race",
+    "title": "Racing non-determinism in decentralized applications",
+    "isBook": false,
+    "rank": 120
+  },
+  {
+    "here": "guide/nntoks",
+    "title": "How do network and non-network tokens differ?",
+    "isBook": false,
+    "rank": 60
+  },
+  {
+    "here": "guide/reach",
+    "title": "How does Reach work?",
+    "isBook": false,
+    "rank": 170
+  },
+  {
+    "here": "guide/packages",
+    "title": "Sharing and discovering shared Reach packages",
+    "isBook": false,
+    "rank": 160
+  },
+  {
+    "here": "guide/roadmap",
+    "title": "Reach's Roadmap",
+    "isBook": false,
+    "rank": 190
+  },
+  {
+    "here": "guide/staking",
+    "title": "Example: Staking and Unstaking Tokens",
+    "isBook": false,
+    "rank": 135
+  },
+  {
+    "here": "guide/lifecycle",
+    "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps",
+    "isBook": false,
+    "rank": 35
+  },
+  {
+    "here": "guide/invariants",
+    "title": "Writing Invariants",
+    "isBook": false,
+    "rank": 95
+  },
+  {
+    "here": "guide/solidity",
+    "title": "How does Reach development compare to Solidity development?",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "guide/windows",
+    "title": "Using Reach on Windows",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "guide/timeout",
+    "title": "Non-participation: What it is and how to protect against it",
+    "isBook": false,
+    "rank": 100
+  },
+  {
+    "here": "guide/abstract",
+    "title": "Building decentralized abstractions",
+    "isBook": false,
+    "rank": 130
+  },
+  {
+    "here": "rpc/go",
+    "title": "Go",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "rpc/cs",
+    "title": "C#",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "rpc/proto",
+    "title": "Specification",
+    "isBook": false,
+    "rank": 50
+  },
+  {
+    "here": "rpc/py",
+    "title": "Python",
+    "isBook": false,
+    "rank": 40
+  },
+  {
+    "here": "rpc/client",
+    "title": "Client Walkthrough",
+    "isBook": false,
+    "rank": 60
+  },
+  {
+    "here": "guide/versions",
+    "title": "How does Reach use version numbers?",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "guide/rpc",
+    "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?",
+    "isBook": false,
+    "rank": 40
+  },
+  {
+    "here": "guide/testing",
+    "title": "How should I test a DApp?",
+    "isBook": false,
+    "rank": 51
+  },
+  {
+    "here": "rpc/js",
+    "title": "JavaScript",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "workshop/hash-lock",
+    "title": "Hash Lock",
+    "isBook": false,
+    "rank": 10
+  },
+  {
+    "here": "workshop/relay",
+    "title": "Relay Account",
+    "isBook": false,
+    "rank": 20
+  },
+  {
+    "here": "workshop/fomo",
+    "title": "Fear of Missing Out",
+    "isBook": false,
+    "rank": 40
+  },
+  {
+    "here": "workshop/fomo-generalized",
+    "title": "Fear of Missing Out+",
+    "isBook": false,
+    "rank": 50
+  },
+  {
+    "here": "workshop/trust-fund",
+    "title": "Trust Fund",
+    "isBook": false,
+    "rank": 30
+  },
+  {
+    "here": "tut/rps/7-rpc",
+    "title": "Rock, Paper, Scissors in Python",
+    "isBook": false,
+    "rank": 10
+  }
+]
+{
+  "path": [],
+  "children": {
+    "build": {
+      "path": [
+        "build"
+      ],
+      "children": {},
+      "here": "build",
+      "title": "Reach is for Builders",
+      "isBook": false,
+      "rank": 5
+    },
+    "cout": {
+      "path": [
+        "cout"
+      ],
+      "children": {},
+      "here": "cout",
+      "title": "Compiled Output",
+      "isBook": false,
+      "rank": 60
+    },
+    "frontend": {
+      "path": [
+        "frontend"
+      ],
+      "children": {},
+      "here": "frontend",
+      "title": "Frontends",
+      "isBook": false,
+      "rank": 70
+    },
+    "changelog": {
+      "path": [
+        "changelog"
+      ],
+      "children": {},
+      "here": "changelog",
+      "title": "Changelog",
+      "isBook": false,
+      "rank": 120
+    },
+    "index": {
+      "path": [
+        "index"
+      ],
+      "children": {},
+      "here": "index",
+      "title": "Index",
+      "isBook": false,
+      "rank": 140
+    },
+    "model": {
+      "path": [
+        "model"
+      ],
+      "children": {},
+      "here": "model",
+      "title": "Model",
+      "isBook": false,
+      "rank": 30
+    },
+    "networks": {
+      "path": [
+        "networks"
+      ],
+      "children": {},
+      "here": "networks",
+      "title": "Networks",
+      "isBook": false,
+      "rank": 80
+    },
+    "search": {
+      "path": [
+        "search"
+      ],
+      "children": {},
+      "here": "search",
+      "title": "Search",
+      "isBook": false,
+      "rank": 130
+    },
+    "tool": {
+      "path": [
+        "tool"
+      ],
+      "children": {},
+      "here": "tool",
+      "title": "Tool",
+      "isBook": false,
+      "rank": 40
+    },
+    "rsh": {
+      "path": [
+        "rsh"
+      ],
+      "children": {
+        "appinit": {
+          "path": [
+            "rsh",
+            "appinit"
+          ],
+          "children": {},
+          "here": "rsh/appinit",
+          "title": "Application Initialization",
+          "isBook": false,
+          "rank": 20
+        },
+        "module": {
+          "path": [
+            "rsh",
+            "module"
+          ],
+          "children": {},
+          "here": "rsh/module",
+          "title": "Modules",
+          "isBook": false,
+          "rank": 10
+        },
+        "consensus": {
+          "path": [
+            "rsh",
+            "consensus"
+          ],
+          "children": {},
+          "here": "rsh/consensus",
+          "title": "Consensus Steps",
+          "isBook": false,
+          "rank": 50
+        },
+        "local": {
+          "path": [
+            "rsh",
+            "local"
+          ],
+          "children": {},
+          "here": "rsh/local",
+          "title": "Local Steps",
+          "isBook": false,
+          "rank": 40
+        },
+        "step": {
+          "path": [
+            "rsh",
+            "step"
+          ],
+          "children": {},
+          "here": "rsh/step",
+          "title": "Steps",
+          "isBook": false,
+          "rank": 30
+        },
+        "compute": {
+          "path": [
+            "rsh",
+            "compute"
+          ],
+          "children": {},
+          "here": "rsh/compute",
+          "title": "Computations",
+          "isBook": false,
+          "rank": 60
+        },
+        "errors": {
+          "path": [
+            "rsh",
+            "errors"
+          ],
+          "children": {},
+          "here": "rsh/errors",
+          "title": "Error Codes",
+          "isBook": false,
+          "rank": 70
+        }
+      },
+      "here": "rsh",
+      "title": "Language",
+      "isBook": false,
+      "rank": 50
+    },
+    "tut": {
+      "path": [
+        "tut"
+      ],
+      "children": {
+        "rsvp": {
+          "path": [
+            "tut",
+            "rsvp"
+          ],
+          "children": {},
+          "here": "tut/rsvp",
+          "title": "Répondez S'il Vous Plaît",
+          "isBook": false,
+          "rank": 30
+        },
+        "overview": {
+          "path": [
+            "tut",
+            "overview"
+          ],
+          "children": {},
+          "here": "tut/overview",
+          "title": "Overview",
+          "isBook": false,
+          "rank": 10
+        },
+        "wfs": {
+          "path": [
+            "tut",
+            "wfs"
+          ],
+          "children": {},
+          "here": "tut/wfs",
+          "title": "Wisdom For Sale",
+          "isBook": false,
+          "rank": 18
+        },
+        "rps": {
+          "path": [
+            "tut",
+            "rps"
+          ],
+          "children": {
+            "7-rpc": {
+              "path": [
+                "tut",
+                "rps",
+                "7-rpc"
+              ],
+              "children": {},
+              "here": "tut/rps/7-rpc",
+              "title": "Rock, Paper, Scissors in Python",
+              "isBook": false,
+              "rank": 10
+            }
+          },
+          "here": "tut/rps",
+          "title": "Rock, Paper, Scissors!",
+          "isBook": false,
+          "rank": 20
+        }
+      },
+      "here": "tut",
+      "title": "Tutorials",
+      "isBook": false,
+      "rank": 20
+    },
+    "trouble": {
+      "path": [
+        "trouble"
+      ],
+      "children": {},
+      "here": "trouble",
+      "title": "Troubleshooting",
+      "isBook": false,
+      "rank": 115
+    },
+    "quickstart": {
+      "path": [
+        "quickstart"
+      ],
+      "children": {},
+      "here": "quickstart",
+      "title": "Quickstart",
+      "isBook": false,
+      "rank": 10
+    },
+    "guide": {
+      "path": [
+        "guide"
+      ],
+      "children": {
+        "editor-support": {
+          "path": [
+            "guide",
+            "editor-support"
+          ],
+          "children": {},
+          "here": "guide/editor-support",
+          "title": "IDE/Text Editor Support",
+          "isBook": false,
+          "rank": 150
+        },
+        "ctransfers": {
+          "path": [
+            "guide",
+            "ctransfers"
+          ],
+          "children": {},
+          "here": "guide/ctransfers",
+          "title": "What do the different kinds of consensus transfers mean? publish, pay, race, fork, parallelReduce?",
+          "isBook": false,
+          "rank": 70
+        },
+        "logging": {
+          "path": [
+            "guide",
+            "logging"
+          ],
+          "children": {},
+          "here": "guide/logging",
+          "title": "How do I add tracing logs to my Reach program?",
+          "isBook": false,
+          "rank": 50
+        },
+        "loop-invs": {
+          "path": [
+            "guide",
+            "loop-invs"
+          ],
+          "children": {},
+          "here": "guide/loop-invs",
+          "title": "Finding and using loop invariants",
+          "isBook": false,
+          "rank": 90
+        },
+        "assert": {
+          "path": [
+            "guide",
+            "assert"
+          ],
+          "children": {},
+          "here": "guide/assert",
+          "title": "How and what to verify",
+          "isBook": false,
+          "rank": 80
+        },
+        "determ": {
+          "path": [
+            "guide",
+            "determ"
+          ],
+          "children": {},
+          "here": "guide/determ",
+          "title": "Determinism, simultaneity, and choice in decentralized applications",
+          "isBook": false,
+          "rank": 110
+        },
+        "ganache": {
+          "path": [
+            "guide",
+            "ganache"
+          ],
+          "children": {},
+          "here": "guide/ganache",
+          "title": "How to use Ganache with Reach",
+          "isBook": false,
+          "rank": 140
+        },
+        "limits": {
+          "path": [
+            "guide",
+            "limits"
+          ],
+          "children": {},
+          "here": "guide/limits",
+          "title": "What are Reach's limitations?",
+          "isBook": false,
+          "rank": 180
+        },
+        "race": {
+          "path": [
+            "guide",
+            "race"
+          ],
+          "children": {},
+          "here": "guide/race",
+          "title": "Racing non-determinism in decentralized applications",
+          "isBook": false,
+          "rank": 120
+        },
+        "nntoks": {
+          "path": [
+            "guide",
+            "nntoks"
+          ],
+          "children": {},
+          "here": "guide/nntoks",
+          "title": "How do network and non-network tokens differ?",
+          "isBook": false,
+          "rank": 60
+        },
+        "reach": {
+          "path": [
+            "guide",
+            "reach"
+          ],
+          "children": {},
+          "here": "guide/reach",
+          "title": "How does Reach work?",
+          "isBook": false,
+          "rank": 170
+        },
+        "packages": {
+          "path": [
+            "guide",
+            "packages"
+          ],
+          "children": {},
+          "here": "guide/packages",
+          "title": "Sharing and discovering shared Reach packages",
+          "isBook": false,
+          "rank": 160
+        },
+        "roadmap": {
+          "path": [
+            "guide",
+            "roadmap"
+          ],
+          "children": {},
+          "here": "guide/roadmap",
+          "title": "Reach's Roadmap",
+          "isBook": false,
+          "rank": 190
+        },
+        "staking": {
+          "path": [
+            "guide",
+            "staking"
+          ],
+          "children": {},
+          "here": "guide/staking",
+          "title": "Example: Staking and Unstaking Tokens",
+          "isBook": false,
+          "rank": 135
+        },
+        "lifecycle": {
+          "path": [
+            "guide",
+            "lifecycle"
+          ],
+          "children": {},
+          "here": "guide/lifecycle",
+          "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps",
+          "isBook": false,
+          "rank": 35
+        },
+        "invariants": {
+          "path": [
+            "guide",
+            "invariants"
+          ],
+          "children": {},
+          "here": "guide/invariants",
+          "title": "Writing Invariants",
+          "isBook": false,
+          "rank": 95
+        },
+        "solidity": {
+          "path": [
+            "guide",
+            "solidity"
+          ],
+          "children": {},
+          "here": "guide/solidity",
+          "title": "How does Reach development compare to Solidity development?",
+          "isBook": false,
+          "rank": 30
+        },
+        "windows": {
+          "path": [
+            "guide",
+            "windows"
+          ],
+          "children": {},
+          "here": "guide/windows",
+          "title": "Using Reach on Windows",
+          "isBook": false,
+          "rank": 10
+        },
+        "timeout": {
+          "path": [
+            "guide",
+            "timeout"
+          ],
+          "children": {},
+          "here": "guide/timeout",
+          "title": "Non-participation: What it is and how to protect against it",
+          "isBook": false,
+          "rank": 100
+        },
+        "abstract": {
+          "path": [
+            "guide",
+            "abstract"
+          ],
+          "children": {},
+          "here": "guide/abstract",
+          "title": "Building decentralized abstractions",
+          "isBook": false,
+          "rank": 130
+        },
+        "versions": {
+          "path": [
+            "guide",
+            "versions"
+          ],
+          "children": {},
+          "here": "guide/versions",
+          "title": "How does Reach use version numbers?",
+          "isBook": false,
+          "rank": 20
+        },
+        "rpc": {
+          "path": [
+            "guide",
+            "rpc"
+          ],
+          "children": {},
+          "here": "guide/rpc",
+          "title": "Do I have to use JavaScript to write my frontend? What about Python, Go, or other languages?",
+          "isBook": false,
+          "rank": 40
+        },
+        "testing": {
+          "path": [
+            "guide",
+            "testing"
+          ],
+          "children": {},
+          "here": "guide/testing",
+          "title": "How should I test a DApp?",
+          "isBook": false,
+          "rank": 51
+        }
+      },
+      "here": "guide",
+      "title": "Guide",
+      "isBook": true,
+      "rank": 110
+    },
+    "rpc": {
+      "path": [
+        "rpc"
+      ],
+      "children": {
+        "go": {
+          "path": [
+            "rpc",
+            "go"
+          ],
+          "children": {},
+          "here": "rpc/go",
+          "title": "Go",
+          "isBook": false,
+          "rank": 20
+        },
+        "cs": {
+          "path": [
+            "rpc",
+            "cs"
+          ],
+          "children": {},
+          "here": "rpc/cs",
+          "title": "C#",
+          "isBook": false,
+          "rank": 10
+        },
+        "proto": {
+          "path": [
+            "rpc",
+            "proto"
+          ],
+          "children": {},
+          "here": "rpc/proto",
+          "title": "Specification",
+          "isBook": false,
+          "rank": 50
+        },
+        "py": {
+          "path": [
+            "rpc",
+            "py"
+          ],
+          "children": {},
+          "here": "rpc/py",
+          "title": "Python",
+          "isBook": false,
+          "rank": 40
+        },
+        "client": {
+          "path": [
+            "rpc",
+            "client"
+          ],
+          "children": {},
+          "here": "rpc/client",
+          "title": "Client Walkthrough",
+          "isBook": false,
+          "rank": 60
+        },
+        "js": {
+          "path": [
+            "rpc",
+            "js"
+          ],
+          "children": {},
+          "here": "rpc/js",
+          "title": "JavaScript",
+          "isBook": false,
+          "rank": 30
+        }
+      },
+      "here": "rpc",
+      "title": "RPC Server",
+      "isBook": true,
+      "rank": 90
+    },
+    "workshop": {
+      "path": [
+        "workshop"
+      ],
+      "children": {
+        "hash-lock": {
+          "path": [
+            "workshop",
+            "hash-lock"
+          ],
+          "children": {},
+          "here": "workshop/hash-lock",
+          "title": "Hash Lock",
+          "isBook": false,
+          "rank": 10
+        },
+        "relay": {
+          "path": [
+            "workshop",
+            "relay"
+          ],
+          "children": {},
+          "here": "workshop/relay",
+          "title": "Relay Account",
+          "isBook": false,
+          "rank": 20
+        },
+        "fomo": {
+          "path": [
+            "workshop",
+            "fomo"
+          ],
+          "children": {},
+          "here": "workshop/fomo",
+          "title": "Fear of Missing Out",
+          "isBook": false,
+          "rank": 40
+        },
+        "fomo-generalized": {
+          "path": [
+            "workshop",
+            "fomo-generalized"
+          ],
+          "children": {},
+          "here": "workshop/fomo-generalized",
+          "title": "Fear of Missing Out+",
+          "isBook": false,
+          "rank": 50
+        },
+        "trust-fund": {
+          "path": [
+            "workshop",
+            "trust-fund"
+          ],
+          "children": {},
+          "here": "workshop/trust-fund",
+          "title": "Trust Fund",
+          "isBook": false,
+          "rank": 30
+        }
+      },
+      "here": "workshop",
+      "title": "Workshops",
+      "isBook": true,
+      "rank": 100
+    }
+  },
+  "here": "",
+  "title": "Reach",
+  "isBook": true,
+  "rank": 0
+}
diff --git a/docs/gen/package-lock.json b/docs/gen/package-lock.json
index 30439f6f1b..704282a2ae 100644
--- a/docs/gen/package-lock.json
+++ b/docs/gen/package-lock.json
@@ -1,5 +1,5 @@
 {
-  "name": "dev",
+  "name": "gen",
   "version": "0.0.1",
   "lockfileVersion": 2,
   "requires": true,
diff --git a/docs/src/guide/index.md b/docs/src/guide/index.md
index 117af76977..3c1c868a00 100644
--- a/docs/src/guide/index.md
+++ b/docs/src/guide/index.md
@@ -16,6 +16,7 @@ The following guides are available:
 + @{seclink("guide-ctransfers")}
 + @{seclink("guide-assert")}
 + @{seclink("guide-loop-invs")}
++ @{seclink("guide-invariants")}
 + @{seclink("guide-timeout")}
 + @{seclink("guide-determ")}
 + @{seclink("guide-race")}
diff --git a/docs/src/guide/invariants/config.json b/docs/src/guide/invariants/config.json
new file mode 100644
index 0000000000..50b434d351
--- /dev/null
+++ b/docs/src/guide/invariants/config.json
@@ -0,0 +1 @@
+{ "bookRank": 95 }
\ No newline at end of file
diff --git a/docs/src/guide/invariants/index.md b/docs/src/guide/invariants/index.md
new file mode 100644
index 0000000000..562921d9fa
--- /dev/null
+++ b/docs/src/guide/invariants/index.md
@@ -0,0 +1,500 @@
+# {#guide-invariants} Writing Invariants
+
+Invariants are an essential feature when writing complex Reach DApps. 
+If you're reading this guide then you've probably encountered `{!rsh} invariant`s in other parts of the documentation. 
+Our guide @{seclink("guide-loop-invs")} provides a deep theoretical understanding of loop invariants, and the @{seclink("tut")} and @{seclink("tut-rsvp")} tutorials both feature invariants. 
+Interesting Reach DApps require an intimate understanding of invariants.
+This guide will strengthen your ability to identify what values need to be restricted inside a `{!rsh} while` loop and help you write your own invariants.
+
+To understand their importance, we'll break working invariants and review the resulting error messages. 
+By the end of the guide you'll have a sense of the most common error messages that occur due to missing invariants. 
+You'll also gain a respect for how important invariants are in Reach applications and how important it is to understand your application before writing the codebase. 
+
+## Basics
+
+Invariant refers to something that is constant without variation. 
+
+Invariants are required in Reach `{!rsh} while` loops and in `{!rsh} parallelReduce`.
+They are written immediately before the loop begins. 
+You are allowed to write as many `{!rsh} invariant` statements as needed. 
+Inside a `{!rsh} parallelReduce`, use dot notation to place each `{!rsh} invariant` on its own line to easily distinguish each `{!rsh} invariant` from the other.
+
+The `{!rsh} while` loop condition and the body of the loop must uphold the `{!rsh} invariant`. 
+There are moments within the loop that the invariant may be invalidated, but by the end of the loop, the invariant must be true. 
+
+The invariant establishes properties for the rest of the program after the loop ends.
+So the invariants establish truth just before the loop, uphold that truth inside the loop, and remains true after the loop ends.
+
+## Importance of Invariants
+
+Let's look at examples of invariants and break them to understand their importance. 
+
+``` rsh
+load: /examples/rps-7-loops/index.rsh
+md5: ee287e712cdfe8d91bbb038c383d25d3
+range: 59-61
+```
+
+This is from the @{seclink("tut")} tutorial. 
+The while loop features two invariants. 
+The first (line 60) asserts the balance never changes and is always two times the wager. 
+The second invariant, also on line 60, ensures that the outcome is one of the enumerated outcomes from the top of the program (shown below).
+
+``` rsh
+load: /examples/rps-7-loops/index.rsh
+md5: ee287e712cdfe8d91bbb038c383d25d3
+range: 4-4
+```
+
+In this example, if the engineer ever modified the program in a way that the balance wasn't guaranteed to be two times the wager amount then there would be an error. 
+Alternatively, if the outcome of the game is anything other than `A_WINS`, `B_WINS`, or a `DRAW`, then a different error will be thrown. 
+
+The invariant indicates the importance of asserting the balance and the condition(s) of the loop. 
+In almost all cases, you'll want to constrain these items inside a `{!rsh} while` loop. 
+
+### Balance Invariant
+
+Let's remove the balance invariant and observe the output when we execute a `{!cmd} $ reach compile`.
+
+Our snippet now looks like: 
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 59-61
+```
+
+The verification engine outputs:
+
+``` txt
+load: /examples/rps-7-loops/index-balinv.txt
+md5: fa159888f678f8f5057e5564e8f319c1
+```
+
+The error message on line 7 indicates that the balance is not sufficient for the `{!rsh} transfer` on line 94. 
+This line is far from our `{!rsh} while` loop and invariant, which originates on line 49. 
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 93-95
+```
+
+Line 94 is where we transfer the winnings to Alice or Bob based on who won the round.
+
+If you don't understand the flow of the balance within your application then this error may be confusing. 
+Even though the trouble begins at the loop invariant in line 60, the error is triggered at line 94 because this is the first time we try to move the balance out of the contract. 
+
+Reading the Violation Witness may be more helpful in this situation. 
+(If you'd like to gain a better understanding of Violation Witnesses and Theorem Formalizations then read our guide, @{seclink("how-to-read-verification-failures")}).
+The verification engine is showing two possible places where the insufficient balance could have first occurred. 
+
+The first place could be from the `wager` property binding in the Participant Interact Interface on line 30.
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 27-32
+```
+
+The second indicates that the insufficient balance could be originating in the while loop in line 61.
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 60-62
+```
+
+The next thing we see is the Theorem Formalization. 
+The verification engine is showing the representation of the theorem "balance sufficient for transfer" as a program.
+
+``` txt
+load: /examples/rps-7-loops/index-balinv.txt
+md5: fa159888f678f8f5057e5564e8f319c1
+range: 21-25
+```
+
+Essentially, this theorem representation shows that the balance would not be equal to two times the wager amount. For a deeper study on Theorem Formalization, read our guide, @{seclink("how-to-read-verification-failures")}.
+
+If you didn't already know that the balance was failing in the while loop then you'd want to investigate the lines that the Violation Witness points to. 
+
+``` txt
+load: /examples/rps-7-loops/index-balinv.txt
+md5: fa159888f678f8f5057e5564e8f319c1
+range: 27-48
+```
+
+We see a second verification failure that indicates that the balance is not zero when the application exits. 
+This verification fails at line 27, which is where the Participant Interact Interface begins. 
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 27-32
+```
+
+The Violation Witness points to the same lines as the prior error. 
+Again, this indicates that something may be wrong in our `wager` property on line 30 or in the `{!rsh} while` loop on line 61.
+
+``` rsh
+load: /examples/rps-7-loops/index-balinv.rsh
+md5: 7e59eeb6efb5e26e97c4c1d4df6669c6
+range: 59-62
+```
+
+If you can rule out an error in the Participant Interact Interface then consider what invariants may be required by the `{!rsh} while` loop.
+If you haven't created an invariant for the balance and the condition(s) of the loop then it is possible that your current invariants may be insufficient for the verification engine to formally verify your application.
+A pattern will emerge as we progress through this guide.
+We'll see that the `{!rsh} invariant` should `{!rsh} assert` the balance, loop condition, and `{!rsh} Map` size, if applicable. 
+`{!rsh} check`s within the `{!rsh} parallelReduce` relate to the invariants. 
+
+We'll continue to explore this pattern for writing invariants. 
+We've examined an `{!rsh} invariant` for asserting the `balance`. 
+Now we'll review an `{!rsh} invariant` that asserts the loop's condition.
+
+### Condition Invariant
+
+Let's replace the balance invariant and remove the condition's invariant. 
+
+Our code now looks like: 
+
+``` rsh
+load: /examples/rps-7-loops/index-condinv.rsh
+md5: 607c8bd0c7fb7a49570946eb309c69df
+range: 59-61
+```
+
+The output now reads:
+
+```
+load: /examples/rps-7-loops/index-condinv.txt
+md5: addb49b7bdacdfad0fe4e9661c90b554
+```
+
+In this instance, the theorem fails on an `{!rsh} assert` on line 93. 
+
+``` rsh
+load: /examples/rps-7-loops/index-condinv.rsh
+md5: 607c8bd0c7fb7a49570946eb309c69df
+range: 93-93
+```
+
+We also read that there is one Violation Witness that points to the `{!rsh} while` loop on line 61. 
+The Theorem Formalization shows a failing ternary involving `outcome`.
+
+```
+load: /examples/rps-7-loops/index-condinv.txt
+md5: addb49b7bdacdfad0fe4e9661c90b554
+range: 17-21
+```
+
+Failing to write an invariant that asserts the loop's condition leaves the program open to violating static `{!rsh} assert`ions, such as the one controlling the `outcome` on line 93. 
+
+``` rsh
+load: /examples/rps-7-loops/index-condinv.rsh
+md5: 607c8bd0c7fb7a49570946eb309c69df
+range: 93-93
+```
+
+Line 93 `{!rsh} assert`s that `outcome` must be `A_WINS` or `B_WINS`, but the compiler cannot verify this assertion without an invariant in the `{!rsh} while` loop. 
+
+The verification engine is only able to formally verify the things inside a while loop through invariants. 
+By establishing invariants for the condition and the balance the verification engine is able to formally verify the entire application. 
+Without proper invariants the application cannot be formally verified and will fail to compile. 
+
+## Invariants in parallelReduce
+
+Let's look at the RSVP application. 
+This DApp is more complicated than the @{seclink("tut")} DApp, but the same principles apply. 
+We'll write invariants for the conditions of the `{!rsh} while` loop and the balance. 
+The one difference in this application is that one of the conditions, `done`, will be verified with a `{!rsh} check`, which is a dynamic assertion, rather than an invariant. 
+
+``` rsh
+load: /examples/rsvp-6-vevt/index.rsh
+md5: ed7d96413f2f23224d5ea6081ae4cc78
+range: 44-54
+```
+
+In RSVP, the `{!rsh} parallelReduce` tracks two constants, `done` and `howMany`.
+The first invariant on line 49 asserts that the size of `{!rsh} Map` `Guests` is equal to `howMany`. 
+If we remove this invariant, the compiler will not be able to verify that the size of the Guestbook is the same as how many guests have reserved or checked in. 
+
+### Map Invariant
+
+Let's view the compiled output when this first invariant is removed:
+
+```
+load: /examples/rsvp-6-vevt/index-mapinv.txt
+md5: 86c5c2187f037fb785f347ab28ccefd6
+```
+
+The verification engine fails because the balance may be insufficient for a `{!rsh} transfer` (line 7).
+Similar to before, on line 8, the theorem failure points further into the program when the `{!rsh} transfer` is attempted on line 68 (shown below). 
+Line 9 in the error message points to the DApp's return function that deletes `Guests` and controls the `{!rsh} transfer` logic (line 65).
+
+``` rsh
+load: /examples/rsvp-6-vevt/index-mapinv.rsh
+md5: 94acafe2646ee59c45c89b6e1c7a6592
+range: 65-72
+```
+
+The Violation Witness (lines 15-20) states that the Admin's details property in the Participant Interact Interface could be modified to result in an error.
+It also shows that the start of the `{!rsh} while` loop could be erroneously modified by the programmer.
+
+The Theorem Formalization shows a false relation to the reservation details and the balance. 
+If we didn't know the origination of this error then we would need to consider any static assertions that we may have overlooked. 
+Writing your assumptions about the application before crafting the code makes it easier to complete a `{!rsh} parallelReduce`.
+
+### Balance Invariant
+
+Removing the second invariant outputs a similar balance transfer error, and an additional "balance zero at application exit" error. 
+
+``` txt
+load: /examples/rsvp-6-vevt/index-balinv.txt
+md5: ffa07ffcab3de8b2bb5ec92c161877e0
+```
+
+We saw the "balance zero at application exit" verification failure in our Rock, Paper, Scissors example when we removed the balance logic from the invariant. 
+
+Again, we can see that the Violation Witnesses (above in lines 15-20) point to the Participant Interact Interface and the `{!rsh} paralellReduce`  (`index-balinv.rsh` lines 13 and 45, respectively).
+
+```
+load: /examples/rsvp-6-vevt/index-balinv.rsh
+md5: 5551e68590bad318743accb1a03639a4
+range: 45-50
+```
+
+The Participant Interact Interface violation reference is similar to before so we won't look at that again. 
+However, it's worth pointing out that the second violation points to the beginning of the `{!rsh} parallelReduce`.
+This is because a `{!rsh} parallelReduce` creates a race in a loop.
+When an `{!rsh} API` is involved, as in the RSVP application, invariants must make `{!rsh} assert`ions over the conditions of the `{!rsh} parallelReduce`. 
+Learn more about races and `{!rsh} parallelReduce` in our @{seclink("guide-ctransfers")} guide.
+
+The Theorem Formalizations in lines 24-26 and 44-46 show a representation of the theorem "balance sufficient for transfer" and "balance zero at application exit" as programs, respectively.
+It demonstrates how the program would error when calculating the balance. 
+
+``` txt
+load: /examples/rsvp-6-vevt/index-balinv.txt
+md5: ffa07ffcab3de8b2bb5ec92c161877e0
+range: 24-26
+```
+
+``` txt
+load: /examples/rsvp-6-vevt/index-balinv.txt
+md5: ffa07ffcab3de8b2bb5ec92c161877e0
+range: 44-46
+```
+
+Balance errors indicate the need to recalculate the balance's formula or identify missing assumptions about the program. 
+In this case, the balance is equal to the product of `howMany` guests completed a reservation and the reservation fee. 
+However, Reach cannot guarantee the efficacy of the program because we failed to `{!rsh} assert` the balance's formula in the `{!rsh} invariant`.
+
+## Distribute Supply of Non-Network Tokens
+
+Sometimes you may want to write an `{!rsh} assert`ion regarding the supply of non-network tokens. 
+In _Ticket Sales_ an Administrator issues non-network tokens and Buyer `{!rsh} API`s have the ability to buy the tokens, which are referred to as 'tickets', in this DApp.
+
+The `{!rsh} invariant` in this DApp is interesting because it makes `{!rsh} assert`s over the network token balance (line 26) and the non-network token balance (line 27).
+
+```
+load: /examples/ticket-sales/index.rsh
+md5: c425745032273893d106fe3de005f15e
+range: 25-37
+```
+
+The `{!rsh} parallelReduce` updates the value of `ticketsSold` and the condition is `true` as long as `ticketsSold` is less than the available `supply` of tickets. 
+The `{!rsh} API` calls on the `buyTicket` function, which increments the number of `ticketsSold` and returns the new value. 
+
+This program doesn't break after removing the first balance invariant because the network tokens aren't transferred within the `{!rsh} parallelReduce`. 
+The `{!rsh} parallelReduce` is in a race to sell the non-network tokens. 
+Writing an invariant about the network token balance provides stronger defenses to the program, but is not required for the compiler to complete its formal verification.
+However, removing the second invariant will cause a violation witness.
+
+The critical `{!rsh} invariant` on line 27 `{!rsh} assert`s that the non-network token balance is equal to the difference of the supply and the number of tickets sold.
+
+Once removed, the compiler returns
+
+```
+load: /examples/ticket-sales/index-tokinv.txt
+md5: bcb528856342039ea775659891bc24d0
+range: 4-23
+```
+
+We see the "balance sufficient for transfer" error, once again. 
+However, instead of referring to a network token transfer, the message is referring to the transfer of a non-network token. 
+In this example, the message points to the `{!rsh} transfer` on line 31 and the `return` statement on line 30.
+
+The Violation Witness on line 15 shows how the `{!rsh} parallelReduce` could fail, followed by the Theorem Formalization.
+
+```
+load: /examples/ticket-sales/index-tokinv.txt
+md5: bcb528856342039ea775659891bc24d0
+range: 25-37
+```
+
+The second verification failure, "balance zero at application exit" indicates that tokens could remain in the contract when it exits on line 38.
+This Violation Witness also points to the `{!rsh} parallelReduce` with a similar example as before.
+
+This example shows that it is critical to understand a non-network token's balance, as well as, the network token's balance.
+Failing to understand how to `{!rsh} assert` the `{!rsh} invariant`(s) will make it difficult to successfully compile the Reach application.
+
+## All Together Now
+
+Let's look at one more example that asserts `{!rsh} invariant`s over network tokens, non-network tokens, and a `{!rsh} Map`.
+At this point, we will have already discussed the error messages so we'll move at a faster pace.
+
+``` rsh
+load: /examples/point-of-sale/index.rsh
+md5: 102ed2e3f3a0d59a4f1a5aa5084823cf
+range: 26-44
+```
+
+This is a point-of-sale Reach application that allows an `{!rsh} API` member to make a purchase or request a refund. 
+An interesting feature in the point-of-sale application is that it takes in varying cost amounts and stores the inputs in a `{!rsh} Map` which is available to be returned through the refund function.
+
+You should be able to identify that the `{!rsh} invariant`(s) assert network and, if applicable, non-network balances, the loop condition, and the `{!rsh} Map` size, if applicable. 
+We also can identify a relationship between the `{!rsh} Map` `{!rsh} invariant` and the `{!rsh} check`.
+`{!rsh} Map`s with transfers inside a `{!rsh} parallelReduce` require an `{!rsh} invariant` and a `{!rsh} check`. 
+
+The other two `{!rsh} check`s are defensive. 
+`check(tokensSold != supply)` on line 34 offers insurance against split-second API calls, and `check(purchasePrice > min)` on line 36 is like a `try catch` to ensure that purchase calls meet the minimum price.
+
+### Lost Without a Map
+
+Let's remove each of the invariants and observe the outputs.
+First, we remove the `{!rsh} Map` `{!rsh} invariant`:
+
+``` rsh
+load: /examples/point-of-sale/index-mapinv.rsh
+md5: 76b0af6be62a70fe1ad5cca2f5f85307
+range: 27-31
+```
+
+The verification fails because the compiler cannot confirm that the balance is sufficient for a transfer. 
+
+``` rsh
+load: /examples/point-of-sale/index-mapinv.txt
+md5: f28ba47027648e7e39b34e44b73cc763
+range: 7-9
+```
+
+Failures point to the `{!rsh} API` refund return object on line 46 and the `{!rsh} transfer` on line 48.
+
+``` rsh
+load: /examples/point-of-sale/index-mapinv.rsh
+md5: 76b0af6be62a70fe1ad5cca2f5f85307
+range: 46-48
+```
+
+Without the `{!rsh} invariant`, Reach is not able `{!rsh} assert` the size of the `{!rsh} Map`.
+When an `{!rsh} API` member attempts to call a refund, the verification engine cannot guarantee that the balance will be sufficient to payout the transfer amount. 
+It is critical to know the size of a `{!rsh} Map` if it will be used in a `{!rsh} transfer`. 
+
+### Out of Balance
+
+Removing the balance `{!rsh} invariant` has similar results:
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.rsh
+md5: b2c319bf236e4d7ddade29937e162e39
+range: 27-31
+```
+
+As we saw before, the verification engine is not able to ensure that the balance is sufficient for a transfer in the `{!rsh} API`'s refund functionality. 
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.txt
+md5: 90ef94492eaaae686c052e46a29a9373
+range: 7-9
+```
+
+Removing the balance `{!rsh} invariant` causes a second failure point at line 54 when the contract transfers the `total` to the Administrator. 
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.txt
+md5: 90ef94492eaaae686c052e46a29a9373
+range: 34-35
+```
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.rsh
+md5: b2c319bf236e4d7ddade29937e162e39
+range: 54
+```
+
+The third and final error states that the verification engine cannot confirm that the network token balance is zero when the application exits on line 56.
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.txt
+md5: 90ef94492eaaae686c052e46a29a9373
+range: 57-58
+```
+
+``` rsh
+load: /examples/point-of-sale/index-balinv.rsh
+md5: b2c319bf236e4d7ddade29937e162e39
+range: 56-56
+```
+
+`{!rsh} invariant`s are always required for balances that will be transferred inside a `{!rsh} parallelReduce`.
+Failing to make an `{!rsh} assert`ion over the balance with an `{!rsh} invariant` creates a host of verification errors that could be difficult to resolve without properly understanding the application. 
+
+### Tokens
+
+For our final example, we remove the non-network token balance `{!rsh} invariant`.
+
+``` rsh
+load: /examples/point-of-sale/index-tokinv.rsh
+md5: 2280bcf03c528e31b6c37104786dc927
+range: 27-31
+```
+
+We observe that the verification failure message is the same, "balance sufficient for transfer". 
+However, it fails inside the `{!rsh} API` purchase functionality.
+
+``` rsh
+load: /examples/point-of-sale/index-tokinv.txt
+md5: 557d91780cd2f51743d5b84eca1d7989
+range: 7-9
+```
+
+Non-network tokens are transferred on line 39 and the non-network token balance is updated in line 36. 
+
+``` rsh
+load: /examples/point-of-sale/index-tokinv.rsh
+md5: 2280bcf03c528e31b6c37104786dc927
+range: 36-40
+```
+
+Similar to network tokens, transferring non-network tokens within a `{!rsh} parallelReduce` requires an `{!rsh} invariant`.
+
+Failing to provide the non-network token `{!rsh} invariant` also creates a "balance zero at application exit" error on line 56, which is where the application `{!rsh} exit`s.
+
+``` rsh
+load: /examples/point-of-sale/index-tokinv.txt
+md5: 557d91780cd2f51743d5b84eca1d7989
+range: 28-29
+```
+
+All tokens must be accounted for when the application is ready to exit. 
+Reach is not able to confirm balances after exiting a `{!rsh} parallelReduce` without `{!rsh} invariant`s.
+If the compiler fails with "balance zero at application exit" then ensure you've created `{!rsh} invariant`s that `{!rsh} assert` the correct equations for network and non-network tokens.  
+
+## Invariably, We Have Learned
+
+At this point, we've examined four invariants and how their absence results in Violation Witness errors. 
+This demonstrates how important it is to understand your program before it is time to write `{!rsh} invariant`s.
+You should be prepared to create `{!rsh} invariant`s as soon as you need a `{!rsh} parallelReduce`.
+
+Learn to quickly identify where your application needs a `{!rsh} parallelReduce` and what `{!rsh} invariant`(s) will be required to correctly `{!rsh} assert` the balance(s) and condition(s).
+For more practice, continue to find examples, remove the invariants, and study the compile errors. 
+
+If you'd like to experiment with invariants in additional examples then I recommend starting with the [NFT-Auction-API](https://github.com/reach-sh/reach-lang/blob/master/examples/nft-auction-api/index.rsh) and the [Chicken-Parallel](https://github.com/reach-sh/reach-lang/blob/master/examples/chicken-parallel/index.rsh) examples. 
+
+This can be a good way of developing a sense of when and how to use `{!rsh} invariant`s. 
+Common error messages you may see are "balance zero at application exit" and "balance sufficient for transfer". 
+If you see these errors in your applications, take time to consider the formula of the balance in your application. 
+Seek to identify a mathematical relationship between loop conditions and the balance.
+
+You should now have a better understanding of how to write `{!rsh} invariant`s and their importance in developing secure Reach DApps.
+If you need additional advice for your DApp, reach out in our [Discord](@{DISCORD}).
\ No newline at end of file
diff --git a/docs/xrefs.json b/docs/xrefs.json
index 9b4e4ed0bd..1b3ae4db6e 100644
--- a/docs/xrefs.json
+++ b/docs/xrefs.json
@@ -775,6 +775,10 @@
     "title": "Install VSCode",
     "path": "/guide/editor-support/#guide-install-VSCode"
   },
+  "guide-invariants": {
+    "title": "Writing Invariants",
+    "path": "/guide/invariants/#guide-invariants"
+  },
   "guide-lifecycle": {
     "title": "Contract Development Lifecycle and Best Practices for Building Reach DApps",
     "path": "/guide/lifecycle/#guide-lifecycle"
diff --git a/examples/point-of-sale/index-balinv.rsh b/examples/point-of-sale/index-balinv.rsh
new file mode 100644
index 0000000000..56ab93e326
--- /dev/null
+++ b/examples/point-of-sale/index-balinv.rsh
@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+ 
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(pMap.sum() == total, "tracking total wrong")
+    .invariant(balance(tok) == supply - tokensSold, "non-network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+
diff --git a/examples/point-of-sale/index-balinv.txt b/examples/point-of-sale/index-balinv.txt
new file mode 100644
index 0000000000..43722694e0
--- /dev/null
+++ b/examples/point-of-sale/index-balinv.txt
@@ -0,0 +1,80 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:48:26:application
+  at /app/index-balinv.rsh:46:35:application call to [unknown function] (defined at: /app/index-balinv.rsh:46:35:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 33037;
+
+  const map0_1/981 = <fresh Map>;
+  //    ^ could = <map: (Some(8026 ))>[<abstract address 0> <- None(null )]
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 8025
+  //      from: ./index-balinv.rsh:27:45:while
+  const this/760 = <an honest join from "Buyer_refund">;
+  //    ^ could = <abstract address 1>
+  //      from: ./index-balinv.rsh:27:45:dot
+
+  // Theorem Formalization
+
+  const v945 = fromSome(map0_1/981[this/760], 0 ) <= netBalance/679;
+  //    ^ would be false
+  assert(v945);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:54:21:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const total/671 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v957 = total/671 <= netBalance/679;
+  //    ^ would be false
+  assert(v957);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-balinv.rsh:56:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const total/671 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:27:45:while
+  const netBalance/679 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v961 = 0 == (netBalance/679 - total/671);
+  //    ^ would be false
+  assert(v961);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 7 failures (and 4 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/examples/point-of-sale/index-mapinv.rsh b/examples/point-of-sale/index-mapinv.rsh
new file mode 100644
index 0000000000..44774e4b25
--- /dev/null
+++ b/examples/point-of-sale/index-mapinv.rsh
@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+ 
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(balance() == total, "network token balance wrong")
+    .invariant(balance(tok) == supply - tokensSold, "non-network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+
diff --git a/examples/point-of-sale/index-mapinv.txt b/examples/point-of-sale/index-mapinv.txt
new file mode 100644
index 0000000000..a4d000b470
--- /dev/null
+++ b/examples/point-of-sale/index-mapinv.txt
@@ -0,0 +1,34 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-mapinv.rsh:48:26:application
+  at /app/index-mapinv.rsh:46:35:application call to [unknown function] (defined at: /app/index-mapinv.rsh:46:35:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 33037;
+
+  const map0_1/961 = <fresh Map>;
+  //    ^ could = <map: (None(null ))>[<abstract address 1> <- Some(30613 )]
+  //      from: ./index-mapinv.rsh:27:45:while
+  const netBalance/665 = <loop variable>;
+  //    ^ could = 30612
+  //      from: ./index-mapinv.rsh:27:45:while
+  const this/740 = <an honest join from "Buyer_refund">;
+  //    ^ could = <abstract address 1>
+  //      from: ./index-mapinv.rsh:27:45:dot
+
+  // Theorem Formalization
+
+  const v925 = fromSome(map0_1/961[this/740], 0 ) <= netBalance/665;
+  //    ^ would be false
+  assert(v925);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 3 failures (and 2 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/examples/point-of-sale/index-tokinv.rsh b/examples/point-of-sale/index-tokinv.rsh
new file mode 100644
index 0000000000..a054d7c383
--- /dev/null
+++ b/examples/point-of-sale/index-tokinv.rsh
@@ -0,0 +1,58 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      min: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    purchase: Fun([UInt], UInt),
+    refund: Fun([], UInt),
+  });
+  init();
+ 
+  A.only(() => {
+   const {min, tok, supply} = declassify(interact.params);
+  });
+  A.publish(min, tok, supply);
+  commit();
+  A.pay([[supply, tok]])
+  A.interact.launched(getContract());
+
+  const pMap = new Map(UInt);
+  const [tokensSold, total] = parallelReduce([0, 0])
+    .paySpec([tok])
+    .invariant(pMap.sum() == total, "tracking total wrong")
+    .invariant(balance() == total, "network token balance wrong")
+    .while(tokensSold < supply)
+    .api_(B.purchase, (purchasePrice) => {
+      check(tokensSold != supply, "sorry, out of tickets");
+      check(isNone(pMap[this]), "sorry, you are already in this list");
+      check(purchasePrice >= min, "sorry, amount too low");
+      return[[purchasePrice, [0, tok]], (ret) => {
+        pMap[this] = purchasePrice;
+        const sold = tokensSold + 1;
+        transfer(1, tok).to(this);
+        ret(sold);
+        return [sold, total + purchasePrice];
+      }];
+    })
+    .api_(B.refund, () => {
+      check(isSome(pMap[this]), "sorry, you are not in the list");
+      return[[0, [1, tok]], (ret) => {
+        const paid = fromSome(pMap[this], 0);
+        transfer(paid).to(this);
+        ret(paid);
+        delete pMap[this];
+        return[tokensSold - 1, total - paid]
+      }];
+    });
+  transfer(total).to(A);
+  commit();
+  exit();
+});
+
diff --git a/examples/point-of-sale/index-tokinv.txt b/examples/point-of-sale/index-tokinv.txt
new file mode 100644
index 0000000000..4752ac96b5
--- /dev/null
+++ b/examples/point-of-sale/index-tokinv.txt
@@ -0,0 +1,48 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-tokinv.rsh:39:28:application
+  at /app/index-tokinv.rsh:36:47:application call to [unknown function] (defined at: /app/index-tokinv.rsh:36:47:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 73349;
+
+  const tokenInfos/676 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 8855, false ] )
+  //      from: ./index-tokinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v822 = 1 <= tokenInfos/676[0][0];
+  //    ^ would be false
+  assert(v822);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-tokinv.rsh:56:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const tokenInfos/676 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [1, 11797, false ] )
+  //      from: ./index-tokinv.rsh:27:45:while
+
+  // Theorem Formalization
+
+  const v960 = 0 == tokenInfos/676[0][0];
+  //    ^ would be false
+  assert(v960);
+
+  Verifying when NO participants are honest
+Checked 68 theorems; 5 failures (and 3 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/examples/rps-7-loops/index-balinv.rsh b/examples/rps-7-loops/index-balinv.rsh
new file mode 100644
index 0000000000..8d2654d424
--- /dev/null
+++ b/examples/rps-7-loops/index-balinv.rsh
@@ -0,0 +1,100 @@
+'reach 0.1';
+
+const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3);
+const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3);
+
+const winner = (handAlice, handBob) =>
+  ((handAlice + (4 - handBob)) % 3);
+
+assert(winner(ROCK, PAPER) == B_WINS);
+assert(winner(PAPER, ROCK) == A_WINS);
+assert(winner(ROCK, ROCK) == DRAW);
+
+forall(UInt, handAlice =>
+  forall(UInt, handBob =>
+    assert(isOutcome(winner(handAlice, handBob)))));
+
+forall(UInt, (hand) =>
+  assert(winner(hand, hand) == DRAW));
+
+const Player = {
+  ...hasRandom,
+  getHand: Fun([], UInt),
+  seeOutcome: Fun([UInt], Null),
+  informTimeout: Fun([], Null),
+};
+
+export const main = Reach.App(() => {
+  const Alice = Participant('Alice', {
+    ...Player,
+    wager: UInt, // atomic units of currency
+    deadline: UInt, // time delta (blocks/rounds)
+  });
+  const Bob   = Participant('Bob', {
+    ...Player,
+    acceptWager: Fun([UInt], Null),
+  });
+  init();
+
+  const informTimeout = () => {
+    each([Alice, Bob], () => {
+      interact.informTimeout();
+    });
+  };
+
+  Alice.only(() => {
+    const wager = declassify(interact.wager);
+    const deadline = declassify(interact.deadline);
+  });
+  Alice.publish(wager, deadline)
+    .pay(wager);
+  commit();
+
+  Bob.only(() => {
+    interact.acceptWager(wager);
+  });
+  Bob.pay(wager)
+    .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
+
+  var outcome = DRAW;
+  invariant( isOutcome(outcome) );
+  while ( outcome == DRAW ) {
+    commit();
+
+    Alice.only(() => {
+      const _handAlice = interact.getHand();
+      const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice);
+      const commitAlice = declassify(_commitAlice);
+    });
+    Alice.publish(commitAlice)
+      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
+    commit();
+
+    unknowable(Bob, Alice(_handAlice, _saltAlice));
+    Bob.only(() => {
+      const handBob = declassify(interact.getHand());
+    });
+    Bob.publish(handBob)
+      .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
+    commit();
+
+    Alice.only(() => {
+      const saltAlice = declassify(_saltAlice);
+      const handAlice = declassify(_handAlice);
+    });
+    Alice.publish(saltAlice, handAlice)
+      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
+    checkCommitment(commitAlice, saltAlice, handAlice);
+
+    outcome = winner(handAlice, handBob);
+    continue;
+  }
+
+  assert(outcome == A_WINS || outcome == B_WINS);
+  transfer(2 * wager).to(outcome == A_WINS ? Alice : Bob);
+  commit();
+
+  each([Alice, Bob], () => {
+    interact.seeOutcome(outcome);
+  });
+});
diff --git a/examples/rps-7-loops/index-balinv.txt b/examples/rps-7-loops/index-balinv.txt
new file mode 100644
index 0000000000..5b65e5d585
--- /dev/null
+++ b/examples/rps-7-loops/index-balinv.txt
@@ -0,0 +1,53 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:94:25:application
+
+  // Violation Witness
+
+  const UInt.max = 4;
+
+  const wager/297 = "Alice".interact.wager;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:30:10:property binding
+  const netBalance/330 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:61:3:while
+
+  // Theorem Formalization
+
+  const v452 = (2 * wager/297) <= netBalance/330;
+  //    ^ would be false
+  assert(v452);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-balinv.rsh:27:30:compileDApp
+
+  // Violation Witness
+
+  const UInt.max = 6;
+
+  const wager/297 = "Alice".interact.wager;
+  //    ^ could = 0
+  //      from: ./index-balinv.rsh:30:10:property binding
+  const netBalance/330 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:61:3:while
+
+  // Theorem Formalization
+
+  const v456 = 0 == (netBalance/330 - (2 * wager/297));
+  //    ^ would be false
+  assert(v456);
+
+  Verifying when NO participants are honest
+Checked 77 theorems; 4 failures (and 2 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/examples/rps-7-loops/index-condinv.rsh b/examples/rps-7-loops/index-condinv.rsh
new file mode 100644
index 0000000000..39e720c225
--- /dev/null
+++ b/examples/rps-7-loops/index-condinv.rsh
@@ -0,0 +1,100 @@
+'reach 0.1';
+
+const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3);
+const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3);
+
+const winner = (handAlice, handBob) =>
+  ((handAlice + (4 - handBob)) % 3);
+
+assert(winner(ROCK, PAPER) == B_WINS);
+assert(winner(PAPER, ROCK) == A_WINS);
+assert(winner(ROCK, ROCK) == DRAW);
+
+forall(UInt, handAlice =>
+  forall(UInt, handBob =>
+    assert(isOutcome(winner(handAlice, handBob)))));
+
+forall(UInt, (hand) =>
+  assert(winner(hand, hand) == DRAW));
+
+const Player = {
+  ...hasRandom,
+  getHand: Fun([], UInt),
+  seeOutcome: Fun([UInt], Null),
+  informTimeout: Fun([], Null),
+};
+
+export const main = Reach.App(() => {
+  const Alice = Participant('Alice', {
+    ...Player,
+    wager: UInt, // atomic units of currency
+    deadline: UInt, // time delta (blocks/rounds)
+  });
+  const Bob   = Participant('Bob', {
+    ...Player,
+    acceptWager: Fun([UInt], Null),
+  });
+  init();
+
+  const informTimeout = () => {
+    each([Alice, Bob], () => {
+      interact.informTimeout();
+    });
+  };
+
+  Alice.only(() => {
+    const wager = declassify(interact.wager);
+    const deadline = declassify(interact.deadline);
+  });
+  Alice.publish(wager, deadline)
+    .pay(wager);
+  commit();
+
+  Bob.only(() => {
+    interact.acceptWager(wager);
+  });
+  Bob.pay(wager)
+    .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
+
+  var outcome = DRAW;
+  invariant( balance() == 2 * wager );
+  while ( outcome == DRAW ) {
+    commit();
+
+    Alice.only(() => {
+      const _handAlice = interact.getHand();
+      const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice);
+      const commitAlice = declassify(_commitAlice);
+    });
+    Alice.publish(commitAlice)
+      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
+    commit();
+
+    unknowable(Bob, Alice(_handAlice, _saltAlice));
+    Bob.only(() => {
+      const handBob = declassify(interact.getHand());
+    });
+    Bob.publish(handBob)
+      .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
+    commit();
+
+    Alice.only(() => {
+      const saltAlice = declassify(_saltAlice);
+      const handAlice = declassify(_handAlice);
+    });
+    Alice.publish(saltAlice, handAlice)
+      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
+    checkCommitment(commitAlice, saltAlice, handAlice);
+
+    outcome = winner(handAlice, handBob);
+    continue;
+  }
+
+  assert(outcome == A_WINS || outcome == B_WINS);
+  transfer(2 * wager).to(outcome == A_WINS ? Alice : Bob);
+  commit();
+
+  each([Alice, Bob], () => {
+    interact.seeOutcome(outcome);
+  });
+});
diff --git a/examples/rps-7-loops/index-condinv.txt b/examples/rps-7-loops/index-condinv.txt
new file mode 100644
index 0000000000..5cf00f1d09
--- /dev/null
+++ b/examples/rps-7-loops/index-condinv.txt
@@ -0,0 +1,26 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  at ./index-condinv.rsh:93:9:application
+
+  // Violation Witness
+
+  const UInt.max = 6;
+
+  const outcome/321 = <loop variable>;
+  //    ^ could = 3
+  //      from: ./index-condinv.rsh:61:3:while
+
+  // Theorem Formalization
+
+  const v446 = ((outcome/321 == 2) ? true : (outcome/321 == 0));
+  //    ^ would be false
+  assert(v446);
+
+  Verifying when NO participants are honest
+Checked 77 theorems; 2 failures (and 1 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/examples/rps-7-rpc/server/index.txt b/examples/rps-7-rpc/server/index.txt
index 7a3562f458..17663cd197 100644
--- a/examples/rps-7-rpc/server/index.txt
+++ b/examples/rps-7-rpc/server/index.txt
@@ -1,4 +1,3 @@
-Compiling `main`...
 Verifying knowledge assertions
 Verifying for generic connector
   Verifying when ALL participants are honest
diff --git a/examples/rsvp-6-vevt/index-balinv.rsh b/examples/rsvp-6-vevt/index-balinv.rsh
new file mode 100644
index 0000000000..069e61fd05
--- /dev/null
+++ b/examples/rsvp-6-vevt/index-balinv.rsh
@@ -0,0 +1,77 @@
+'reach 0.1';
+'use strict';
+
+const Details = Object({
+  name: Bytes(128),
+  reservation: UInt,
+  deadline: UInt,
+  host: Address,
+});
+
+export const main = Reach.App(() => {
+  const Admin = Participant('Admin', {
+    details: Details,
+    launched: Fun([Contract], Null),
+  });
+  const Guest = API('Guest', {
+    register: Fun([], Null),
+  });
+  const Host = API('Host', {
+    checkin: Fun([Address, Bool], Null),
+  });
+  const Info = View('Info', {
+    details: Details,
+    howMany: UInt,
+    reserved: Fun([Address], Bool),
+  });
+  const Notify = Events({
+    register: [Address],
+    checkin: [Address, Bool],
+  });
+  init();
+
+  Admin.only(() => {
+    const details = declassify(interact.details);
+  });
+  Admin.publish(details);
+  const { reservation, deadline, host } = details;
+  enforce( thisConsensusTime() < deadline, "too late" );
+  Admin.interact.launched(getContract());
+  Info.details.set(details);
+
+  const Guests = new Map(Bool);
+  Info.reserved.set((who) => isSome(Guests[who]));
+  const [ done, howMany ] =
+    parallelReduce([ false, 0 ])
+    .define(() => {
+      Info.howMany.set(howMany);
+    })
+    .invariant( Guests.size() == howMany, "howMany accurate" )
+    .while( ! ( done && howMany == 0 ) )
+    .api_(Guest.register, () => {
+      check(! done, "event started");
+      check(isNone(Guests[this]), "already registered");
+      return [ reservation, (ret) => {
+        enforce( thisConsensusTime() < deadline, "too late" );
+        Guests[this] = true;
+        Notify.register(this);
+        ret(null);
+        return [ false, howMany + 1 ];
+      } ];
+    })
+    .api_(Host.checkin, (guest, showed) => {
+      check(this == host, "not the host");
+      check(isSome(Guests[guest]), "no reservation");
+      return [ 0, (ret) => {
+        enforce( thisConsensusTime() >= deadline, "too early" );
+        delete Guests[guest];
+        transfer(reservation).to(showed ? guest : host);
+        Notify.checkin(guest, showed);
+        ret(null);
+        return [ true, howMany - 1 ];
+      } ];
+    });
+  commit();
+
+  exit();
+});
diff --git a/examples/rsvp-6-vevt/index-balinv.txt b/examples/rsvp-6-vevt/index-balinv.txt
new file mode 100644
index 0000000000..8093013b7f
--- /dev/null
+++ b/examples/rsvp-6-vevt/index-balinv.txt
@@ -0,0 +1,59 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-balinv.rsh:68:33:application
+  at /app/index-balinv.rsh:65:25:application call to [unknown function] (defined at: /app/index-balinv.rsh:65:25:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 2;
+
+  const details/728 = "Admin".interact.details;
+  //    ^ could = {deadline: 1, host: <abstract address 1>, name: "Bytes!val!1", reservation: 2 }
+  //      from: ./index-balinv.rsh:13:12:property binding
+  const netBalance/759 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:45:19:while
+
+  // Theorem Formalization
+
+  const v948 = details/728.reservation <= netBalance/759;
+  //    ^ would be false
+  assert(v948);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-balinv.rsh:76:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const netBalance/759 = <loop variable>;
+  //    ^ could = 1
+  //      from: ./index-balinv.rsh:45:19:while
+
+  // Theorem Formalization
+
+  const v962 = 0 == netBalance/759;
+  //    ^ would be false
+  assert(v962);
+
+  Verifying when NO participants are honest
+Checked 38 theorems; 5 failures (and 3 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
+warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format.
+
+  ./index-balinv.rsh:22:20:application
+
+  22|   const Info = View('Info', {
+
+For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005
+
diff --git a/examples/rsvp-6-vevt/index-mapinv.rsh b/examples/rsvp-6-vevt/index-mapinv.rsh
new file mode 100644
index 0000000000..a5d9bc1183
--- /dev/null
+++ b/examples/rsvp-6-vevt/index-mapinv.rsh
@@ -0,0 +1,77 @@
+'reach 0.1';
+'use strict';
+
+const Details = Object({
+  name: Bytes(128),
+  reservation: UInt,
+  deadline: UInt,
+  host: Address,
+});
+
+export const main = Reach.App(() => {
+  const Admin = Participant('Admin', {
+    details: Details,
+    launched: Fun([Contract], Null),
+  });
+  const Guest = API('Guest', {
+    register: Fun([], Null),
+  });
+  const Host = API('Host', {
+    checkin: Fun([Address, Bool], Null),
+  });
+  const Info = View('Info', {
+    details: Details,
+    howMany: UInt,
+    reserved: Fun([Address], Bool),
+  });
+  const Notify = Events({
+    register: [Address],
+    checkin: [Address, Bool],
+  });
+  init();
+
+  Admin.only(() => {
+    const details = declassify(interact.details);
+  });
+  Admin.publish(details);
+  const { reservation, deadline, host } = details;
+  enforce( thisConsensusTime() < deadline, "too late" );
+  Admin.interact.launched(getContract());
+  Info.details.set(details);
+
+  const Guests = new Map(Bool);
+  Info.reserved.set((who) => isSome(Guests[who]));
+  const [ done, howMany ] =
+    parallelReduce([ false, 0 ])
+    .define(() => {
+      Info.howMany.set(howMany);
+    })
+    .invariant( balance() == howMany * reservation, "balance accurate" )
+    .while( ! ( done && howMany == 0 ) )
+    .api_(Guest.register, () => {
+      check(! done, "event started");
+      check(isNone(Guests[this]), "already registered");
+      return [ reservation, (ret) => {
+        enforce( thisConsensusTime() < deadline, "too late" );
+        Guests[this] = true;
+        Notify.register(this);
+        ret(null);
+        return [ false, howMany + 1 ];
+      } ];
+    })
+    .api_(Host.checkin, (guest, showed) => {
+      check(this == host, "not the host");
+      check(isSome(Guests[guest]), "no reservation");
+      return [ 0, (ret) => {
+        enforce( thisConsensusTime() >= deadline, "too early" );
+        delete Guests[guest];
+        transfer(reservation).to(showed ? guest : host);
+        Notify.checkin(guest, showed);
+        ret(null);
+        return [ true, howMany - 1 ];
+      } ];
+    });
+  commit();
+
+  exit();
+});
diff --git a/examples/rsvp-6-vevt/index-mapinv.txt b/examples/rsvp-6-vevt/index-mapinv.txt
new file mode 100644
index 0000000000..5286d1395d
--- /dev/null
+++ b/examples/rsvp-6-vevt/index-mapinv.txt
@@ -0,0 +1,39 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-mapinv.rsh:68:33:application
+  at /app/index-mapinv.rsh:65:25:application call to [unknown function] (defined at: /app/index-mapinv.rsh:65:25:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const details/713 = "Admin".interact.details;
+  //    ^ could = {deadline: 1, host: <abstract address 1>, name: "Bytes!val!1", reservation: 1 }
+  //      from: ./index-mapinv.rsh:13:12:property binding
+  const netBalance/744 = <loop variable>;
+  //    ^ could = 0
+  //      from: ./index-mapinv.rsh:45:19:while
+
+  // Theorem Formalization
+
+  const v928 = details/713.reservation <= netBalance/744;
+  //    ^ would be false
+  assert(v928);
+
+  Verifying when NO participants are honest
+Checked 38 theorems; 3 failures (and 2 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
+warning[RW0005]: The `Object` type's format is controlled by Reach; you may want to use `Struct` instead for external interfaces, so you can mandate and document the format.
+
+  ./index-mapinv.rsh:22:20:application
+
+  22|   const Info = View('Info', {
+
+For further explanation of this warning, see: https://docs.reach.sh/rsh/errors/#RW0005
+
diff --git a/examples/ticket-sales/index-tokinv.rsh b/examples/ticket-sales/index-tokinv.rsh
new file mode 100644
index 0000000000..05f5e77399
--- /dev/null
+++ b/examples/ticket-sales/index-tokinv.rsh
@@ -0,0 +1,40 @@
+'reach 0.1';
+
+export const main = Reach.App(() => {
+  const A = Participant('Admin', {
+    params: Object({
+      cost: UInt,
+      tok: Token,
+      supply: UInt,
+    }),
+    launched: Fun([Contract], Null),
+  });
+  const B = API('Buyer', {
+    buyTicket: Fun([], Null),
+  });
+  init();
+
+  A.only(() => {
+    const {cost, tok, supply} = declassify(interact.params);
+  });
+  A.publish(cost, tok, supply);
+  commit();
+  A.pay([[supply, tok]]);
+  A.interact.launched(getContract());
+
+  const [ticketsSold] = parallelReduce([0])
+    .invariant(balance() == cost * ticketsSold)
+    .while(ticketsSold < supply)
+    .api_(B.buyTicket, () => {
+      check(ticketsSold != supply, "sorry, out of tickets");
+      return[cost, (ret) => {
+        transfer(1, tok).to(this);
+        ret(null);
+        return [ticketsSold + 1];
+      }];
+    });
+  transfer(cost * ticketsSold).to(A);
+  commit();
+  exit();
+});
+
diff --git a/examples/ticket-sales/index-tokinv.txt b/examples/ticket-sales/index-tokinv.txt
new file mode 100644
index 0000000000..bc2f6f4248
--- /dev/null
+++ b/examples/ticket-sales/index-tokinv.txt
@@ -0,0 +1,48 @@
+Verifying knowledge assertions
+Verifying for generic connector
+  Verifying when ALL participants are honest
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance sufficient for transfer"
+  at ./index-tokinv.rsh:31:28:application
+  at /app/index-tokinv.rsh:30:26:application call to [unknown function] (defined at: /app/index-tokinv.rsh:30:26:function exp)
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const tokenInfos/267 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [0, 0, false ] )
+  //      from: ./index-tokinv.rsh:25:39:while
+
+  // Theorem Formalization
+
+  const v299 = 1 <= tokenInfos/267[0][0];
+  //    ^ would be false
+  assert(v299);
+
+Verification failed:
+  when ALL participants are honest
+  of theorem: assert
+  msg: "balance zero at application exit"
+  at ./index-tokinv.rsh:38:7:application
+
+  // Violation Witness
+
+  const UInt.max = 1;
+
+  const tokenInfos/267 = <loop variable>;
+  //    ^ could = Array.const(Tuple(UInt, UInt, Bool), [1, 0, false ] )
+  //      from: ./index-tokinv.rsh:25:39:while
+
+  // Theorem Formalization
+
+  const v323 = 0 == tokenInfos/267[0][0];
+  //    ^ would be false
+  assert(v323);
+
+  Verifying when NO participants are honest
+Checked 23 theorems; 4 failures (and 2 omitted repeats) :'(
+
+For a guide to understanding verification failures, see: https://docs.reach.sh/rsh/errors/#how-to-read-verification-failures
diff --git a/hs/test/Reach/Test_Compiler.hs b/hs/test/Reach/Test_Compiler.hs
index 0913bb3db2..1a5abf6e07 100644
--- a/hs/test/Reach/Test_Compiler.hs
+++ b/hs/test/Reach/Test_Compiler.hs
@@ -104,10 +104,18 @@ test_examples = goldenTests "../examples" f
         [ "./pkg/index.rsh"
         , "./pkg/local.rsh"
         , "./pkg/index-master.rsh"
+        , "./point-of-sale/index-balinv.rsh"
+        , "./point-of-sale/index-mapinv.rsh"
+        , "./point-of-sale/index-tokinv.rsh"
         , "./rps-4-attack/index-bad.rsh"
         , "./rps-4-attack/index-fails.rsh"
+        , "./rps-7-loops/index-balinv.rsh"
+        , "./rps-7-loops/index-condinv.rsh"
         , "./overview/index-error.rsh"
         , "./rsvp-5-cede/index-fail.rsh"
+        , "./rsvp-6-vevt/index-balinv.rsh"
+        , "./rsvp-6-vevt/index-mapinv.rsh"
+        , "./ticket-sales/index-tokinv.rsh"
         ]
     f fp =
       case S.member fp fails of