diff --git a/examples/Random/.gitignore b/examples/Random/.gitignore
new file mode 100644
index 00000000..8777251e
--- /dev/null
+++ b/examples/Random/.gitignore
@@ -0,0 +1,8 @@
+random.cs
+random.dll
+random.jar
+random.js
+random.runtimeconfig.json
+node_modules
+package-lock.json
+package.json
diff --git a/examples/Random/random.dfy b/examples/Random/random.dfy
new file mode 100644
index 00000000..72d488a2
--- /dev/null
+++ b/examples/Random/random.dfy
@@ -0,0 +1,37 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+// RUN: %verify "%s"
+
+// #RUN: %run --no-verify --target:cs "%s" --input "%S/../../src/Random/Random.cs"
+// #RUN: %run --no-verify --target:java "%s" --input "%S/../../src/Random/Random.java"
+// #RUN: %run --no-verify --target:js "%s" --input "%S/../../src/Random/Random.js"
+
+include "../../src/Random/Random.dfy"
+
+module RandomExample {
+  import Dafny.Random
+
+  method Main(args: seq<string>) {
+    var verbose := false;
+    if |args| > 1 { verbose := args[1] == "--verbose"; }
+
+    var bvalue := Random.nextBool();
+    if verbose { print "Random boolean: ", bvalue, "\n"; }
+
+    var bound := 10;
+    var ivalue := Random.nextInt(bound);
+    if verbose { print "Random integer from [0,", bound, "): ", ivalue, "\n"; }
+    expect 0 <= ivalue < bound, "Random integer not within bounds [0,bound)";
+
+    var lvalue := Random.nextInt();
+    if verbose { print "Random integer from [0,MAXINT): ", lvalue, "\n"; }
+    expect 0 <= ivalue, "Random unbounded integer not within bounds [0,MAXINT)";
+
+    var rvalue: real := Random.nextReal();
+    if verbose { print "Random real from [0,1): ", rvalue, "\n"; }
+    expect 0.0 <= rvalue < 1.0, "Random real not within [0,1)";
+  }
+}
diff --git a/src/Random/README.md b/src/Random/README.md
new file mode 100644
index 00000000..793eacba
--- /dev/null
+++ b/src/Random/README.md
@@ -0,0 +1,62 @@
+# Dafny.Random
+
+## Overview
+
+The `Dafny.Random` module provides a uniform interface to random values across target languages.
+
+```
+    // Return an arbitrary boolean value
+    predicate nextBool()
+
+    // Return an arbitrary integer value in the range [0, bound)
+    function nextInt(bound: int := 0): (value: int)
+        ensures 0 <= value
+        ensures bound > 0 ==> value < bound
+
+    // Return an arbitrary real value in the range [0,1)
+     function nextReal(): (value: real)
+        ensures 0.0 <= value < 1.0
+```
+To see the need for a uniform interface to probability,
+C# provides random integer values and Java and JavaScript provide random real values,
+and Dafny actually models real numbers as rationals with integral numerators and denominators
+of arbitrary size.
+This module gives one interface to these various sources of randomness.
+This is a simple interface to probability.
+For a more sophisticated treatment of probability, see
+the [Verified Monte Carlo (VMC)](https://github.com/dafny-lang/Dafny-VMC) library.
+
+The `Dafny.Random` module also provides a uniform interface to nondeterminism and probability.
+For example, `nextInt(10)` returns an arbitrary integer from [0,10), but
+
+* in a proof context, the integer is chosen nondeterministcally, and
+* in a compiled code context, the integer is chose probabilistically according to the uniform probability distribution.
+
+Compare this with the Dafny construct `var value: int := *;` where value is arbitrary in a proof context and
+constant (typically 0) in compiled code.
+
+## Usage
+
+The `Random` module, like `FileIO` will not compile or run correctly without a language-specific
+implementation file.  Implementations are currently provided for C#, Java, and JavaScript.
+To use `Random` in your code, you must:
+* `include` and `import` the `Random` module as you would any other library module
+* incorporate the corresponding language-specific implementation file (e.g. `Random.cs`) when building or running your program
+
+The example [random.dfy](../../examples/Random/random.dfy) in the `examples` directory
+shows how to use the module.
+From the [examples](../../examples/Random) directory, compile and run the file `random.dfy` with
+
+```bash
+# C#
+$ dafny run random.dfy --target cs --input ../../src/Random/Random.cs -- --verbose
+
+# Java
+$ dafny run random.dfy --target java --input ../../src/Random/Random.java -- --verbose
+
+# JavaScript
+$ dafny run random.dfy --target js --input ../../src/Random/Random.js -- --verbose
+```
+
+If you aren't using `dafny run` to run your program, you will have to integrate the
+appropriate language-specific implementation file into your build system.
diff --git a/src/Random/Random.cs b/src/Random/Random.cs
new file mode 100644
index 00000000..f5d38253
--- /dev/null
+++ b/src/Random/Random.cs
@@ -0,0 +1,31 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+namespace DafnyLibraries
+{
+    using Dafny;
+    using System;
+    using System.Numerics;
+    public class Random
+    {
+        private static System.Random rnd = new System.Random();
+        public static bool nextBool()
+        {
+            return rnd.Next(2) == 0;
+        }
+        public static BigInteger nextInt(BigInteger Bound)
+        {
+            Int64 bound = (Int64) Bound;
+            Int64 bnd = bound > 0 ? bound : Int64.MaxValue;
+            return new BigInteger(rnd.NextInt64(bound));
+        }
+        public static BigRational nextReal()
+        {
+            Int64 num = rnd.NextInt64();
+            Int64 den = Int64.MaxValue;
+            return new BigRational(new BigInteger(num), new BigInteger(den));
+        }
+    }
+}
diff --git a/src/Random/Random.dfy b/src/Random/Random.dfy
new file mode 100644
index 00000000..c378e223
--- /dev/null
+++ b/src/Random/Random.dfy
@@ -0,0 +1,22 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+module Dafny.Random {
+
+    // Return an arbitrary boolean value.
+    predicate {:extern "DafnyLibraries.Random", "nextBool"} nextBool()
+
+    // Return an arbitrary integer value in the range [0, bound).  If the optional
+    // bound is omitted, return an arbitrary nonnegative integer (generally limited
+    // to a 64-bit integer value when compiled).
+    function {:extern "DafnyLibraries.Random", "nextInt"} nextInt(bound: int := 0): (value: int)
+        ensures 0 <= value
+        ensures bound > 0 ==> value < bound
+
+    // Return an arbitrary real value in the range [0,1).
+     function {:extern "DafnyLibraries.Random", "nextReal"} nextReal(): (value: real)
+        ensures 0.0 <= value < 1.0
+
+}
diff --git a/src/Random/Random.java b/src/Random/Random.java
new file mode 100644
index 00000000..d2c01d0b
--- /dev/null
+++ b/src/Random/Random.java
@@ -0,0 +1,28 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+package DafnyLibraries;
+
+import dafny.*;
+import java.math.*;
+
+public class Random {
+    public static boolean nextBool()
+    {
+        return Math.random() < 0.5;
+    }
+    public static BigInteger nextInt(BigInteger Bound)
+    {
+        long bound = Bound.longValue();
+        long bnd = bound > 0 ? bound : Long.MAX_VALUE;
+        return BigInteger.valueOf((long) Math.floor(Math.random() * bnd));
+    }
+    public static BigRational nextReal()
+    {
+        long num = (long) Math.floor(Math.random() * Long.MAX_VALUE);
+        long den = Long.MAX_VALUE;
+        return new BigRational(BigInteger.valueOf(num), BigInteger.valueOf(den));
+    }
+}
diff --git a/src/Random/Random.js b/src/Random/Random.js
new file mode 100644
index 00000000..5c97994d
--- /dev/null
+++ b/src/Random/Random.js
@@ -0,0 +1,30 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+var DafnyLibraries = DafnyLibraries || {};
+DafnyLibraries.Random = (function () {
+    let $module = {};
+
+    $module.nextBool = function () {
+        try {
+        return Math.random() < 0.5;
+        } catch (e) {
+            throw "nextBool failed";
+        }
+    }
+
+    $module.nextInt = function (bound) {
+        bound = bound > 0 ? bound : Number.MAX_SAFE_INTEGER;
+        return new BigNumber(Math.floor(Math.random() * bound));
+    }
+
+    $module.nextReal = function () {
+        num = Math.floor(Math.random() * Number.MAX_SAFE_INTEGER);
+        den = Number.MAX_SAFE_INTEGER;
+        return new _dafny.BigRational(new BigNumber(num), new BigNumber(den));
+    }
+
+    return $module;
+})();