diff --git a/README.md b/README.md
index 3eca5386..3de7b00a 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,10 @@
 # VMC: a Library for Verified Monte Carlo Algorithms
 
-The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages.
+The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java and Python. For the future, we plan to extend both the functionality and the range of supported languages.
 
-## Java API Example
+## Java
+
+### Java API
 
 ```java
 import DafnyVMC.Random;
@@ -26,31 +28,71 @@ class Test {
 }
 ```
 
-## Dafny Examples
+### Java Examples
 
-To run the examples in the `docs/dafny` directory, use the following commands:
+To run the examples in the `docs/java` directory, use the following commands:
+
+```bash
+$ export TARGET_LANG=java
+$ bash scripts/build.sh
+$ bash build/java/run_samplers.sh
+$ bash build/java/run_shuffling.sh
+```
+
+To run the tests in the `docs/dafny` directory, use the following commands:
 
 ```bash
 $ dafny build docs/dafny/ExamplesRandom.dfy --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java dfyconfig.toml --no-verify
 $ java -jar docs/dafny/ExamplesRandom.jar
 ```
 
-## Java Examples
+To run the statistical tests in the `tests` directory, use the following commands:
+
+```bash
+$ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+```
+
+## Python
+
+### Python API
+
+```py
+import DafnyVMC
+
+def main():
+  r = DafnyVMC.Random()
+
+  print("Example of Fisher-Yates shuffling")
+  arr = ['a', 'b', 'c']
+  arr = r.Shuffle(arr)
+  print(arr)
+  
+  print("Example of Bernoulli sampling")
+  print(r.BernoulliSample(3, 5))
+```
+
+### Python Examples
 
 To run the examples in the `docs/java` directory, use the following commands:
 
 ```bash
-$ export TARGET_LANG=java
+$ export TARGET_LANG=py
 $ bash scripts/build.sh
-$ bash build/java/run.sh 
+$ bash build/py/run_samplers.sh
+$ bash build/py/run_shuffling.sh
 ```
 
-## Dafny Testing
+To run the tests in the `docs/dafny` directory, use the following commands:
+
+```bash
+$ dafny build docs/dafny/ExamplesRandom.dfy --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py dfyconfig.toml --no-verify
+$ python3 docs/dafny/ExamplesRandom-py/__main__.py
+```
 
 To run the statistical tests in the `tests` directory, use the following commands:
 
 ```bash
-$ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ dafny test --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
 
diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy
index 041f1ad0..be8658e3 100644
--- a/docs/dafny/ExamplesRandom.dfy
+++ b/docs/dafny/ExamplesRandom.dfy
@@ -73,7 +73,7 @@ module Examples {
       }
     }
 
-    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
+    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0)\n";
 
     t := 0;
     for i := 0 to n {