diff --git a/constants.properties b/constants.properties
index 869bc9cc21..3d170ec880 100644
--- a/constants.properties
+++ b/constants.properties
@@ -2,6 +2,8 @@
 # because some versions here need to be matched by app authors in
 # their own projects. So don't get fancy with syntax!
 
+# It is also parsed by the scripts in djvm/shell/.
+
 cordaVersion=5.0-SNAPSHOT
 gradlePluginsVersion=4.0.42
 kotlinVersion=1.2.71
diff --git a/djvm/shell/djvm b/djvm/shell/djvm
index ec3c19e5a7..645a50b0ba 100755
--- a/djvm/shell/djvm
+++ b/djvm/shell/djvm
@@ -3,7 +3,7 @@
 file="${BASH_SOURCE[0]}"
 linked_file="$(test -L "$file" && readlink "$file" || echo "$file")"
 base_dir="$(cd "$(dirname "$linked_file")/../" && pwd)"
-version="$(cat $base_dir/../build.gradle | sed -n 's/^[ ]*ext\.corda_release_version[ =]*"\([^"]*\)".*$/\1/p')"
+version="$(cat $base_dir/../constants.properties | sed -n 's/^[ ]*cordaVersion[ =]*\(.*\).*$/\1/p')"
 jar_file="$base_dir/cli/build/libs/corda-djvm-$version-cli.jar"
 
 CLASSPATH="${CLASSPATH:-}"
diff --git a/djvm/shell/install b/djvm/shell/install
index 7e458e0bb4..5dba7ecd02 100755
--- a/djvm/shell/install
+++ b/djvm/shell/install
@@ -2,7 +2,7 @@
 
 file="${BASH_SOURCE[0]}"
 base_dir="$(cd "$(dirname "$file")/" && pwd)"
-version="$(cat $base_dir/../../build.gradle | sed -n 's/^[ ]*ext\.corda_release_version[ =]*"\([^"]*\)".*$/\1/p')"
+version="$(cat $base_dir/../../constants.properties | sed -n 's/^[ ]*cordaVersion[ =]*\(.*\).*$/\1/p')"
 
 # Build DJVM module and CLI
 cd "$base_dir/.."
diff --git a/docs/source/key-concepts-djvm.rst b/docs/source/key-concepts-djvm.rst
index a3c5755f1f..4566c27b9c 100644
--- a/docs/source/key-concepts-djvm.rst
+++ b/docs/source/key-concepts-djvm.rst
@@ -93,7 +93,9 @@ type's members. This is what controls things like ensuring that all methods impl
 and normalisation of synchronised methods.
 
 Lastly, there is a set of emitters. These are used to instrument the byte code for cost accounting purposes, and also
-to inject code for checks that we want to perform at runtime or modifications to out-of-the-box behaviour.
+to inject code for checks that we want to perform at runtime or modifications to out-of-the-box behaviour. Many of
+these emitters will rewrite non-deterministic operations to throw ``RuleViolationError`` exceptions instead, which
+means that the ultimate proof that a function is *truly* deterministic is that it executes successfully inside the DJVM.
 
 
 Static Byte Code Analysis
@@ -342,7 +344,9 @@ The output should be pretty self-explanatory, but just to summarise:
 
 Other commands to be aware of are:
 
- * ``djvm check`` which allows you to perform the up-front static analysis without running the code.
+ * ``djvm check`` which allows you to perform some up-front static analysis without running the code. However, be aware
+   that the DJVM also transforms some non-deterministic operations into ``RuleViolationError`` exceptions. A successful
+   ``check`` therefore does *not* guarantee that the code will behave correctly at runtime.
 
  * ``djvm inspect`` which allows you to inspect what byte code modifications will be applied to a class.