diff --git a/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java b/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java
index f2623c27c943495f8ebb3270579baf1e0f3a28a5..0b3f159aeec63554503d6d6c0aafe3b4709fa6b3 100644
--- a/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java
+++ b/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java
@@ -650,6 +650,19 @@ public class ProverJob extends Job {
 
         command.add(tlapmPath.toOSString());
 
+		// Use Windows Subsystem for Linux instead of Cygwin. This is experimental and
+		// a hack.  A user has to enter wsl.exe or C:\Windows\system32\wsl.exe on the
+        // Toolbox's preference page.  The next if block the appends 'tlapm'. 
+        final boolean useWSL = tlapmPath.toOSString().contains("wsl.exe");
+        if (useWSL) {
+			// Assume tlapm is on PATH in the Linux subsystem. With this, prefixing the
+			// command with 'wsl' tells Windows to invoke the binary (tlapm) via WSL. I
+			// expect this to only work with a single WSL distro installed (otherwise, we
+			// probably have to choose a distro). More information and how to install WSL is
+			// at https://docs.microsoft.com/en-us/windows/wsl/wsl2-install.
+    		command.add("tlapm");
+        }
+
         if (toolboxMode)
         {
             command.add("--toolbox");
@@ -721,12 +734,26 @@ public class ProverJob extends Job {
         if (pathList != null) {
             for (int i=0; i < pathList.length; i++) {
                 command.add("-I") ;
-                command.add(pathList[pathList.length - i - 1]) ;
+                if (useWSL) {
+					// 'wslpath' is executed inside the Linux subsystem. It converts an UNC (?) path
+					// such as "C:\\Users\\markus\\Library\\dir\\" to something that can be resolved
+					// in the Linux subsystem. Unfortunately, pathList[n] =
+					// "C:\Users\markus\Library\dir" which is why we replace \\ with \\\\
+					// backslashes.
+    				command.add(String.format("$(wslpath %s)", pathList[pathList.length - i - 1].replace("\\", "\\\\")));
+                } else {
+                    command.add(pathList[pathList.length - i - 1]) ;
+                }
             }
         }
         
-        // why just the last segment?
-        command.add(module.getLocation().toOSString());
+        if (useWSL) {
+        	// See pathList above about wslpath.  This path here is the actual spec to be verified.
+    		command.add(String.format("$(wslpath %s)", module.getLocation().toOSString().replace("\\", "\\\\")));
+        } else {
+            // why just the last segment?
+            command.add(module.getLocation().toOSString());
+        }
      
         // for debugging
         // for (int i=0; i<command.size(); i++) {