diff --git a/build.xml b/build.xml
index b86c5cd..9bc7f82 100644
--- a/build.xml
+++ b/build.xml
@@ -134,6 +134,7 @@
 			<!-- Report execution statistics as azure-pipelien -->
 			<sysproperty key="tlc2.TLC.ide" value="azure-pipeline"/>
 			<sysproperty key="util.ExecutionStatisticsCollector.id" value="01ed03e40ba44f278a934849dd2b1038"/>
+			<sysproperty key="tlc2.overrides.IOUtils.enableExec" value="true"/>
 			
 			<arg value="-fp"/>
 			<arg value="1"/>
diff --git a/modules/IOUtils.tla b/modules/IOUtils.tla
index c8f914c..3de8ad9 100644
--- a/modules/IOUtils.tla
+++ b/modules/IOUtils.tla
@@ -14,6 +14,10 @@
 (* perform side effects when executed by TLC with the Java overrides.      *)
 (***************************************************************************)
 
+\* The external-process operators IOExec, IOEnvExec, IOExecTemplate and
+\* IOEnvExecTemplate are disabled by default. Set the system property
+\* -Dtlc2.overrides.IOUtils.enableExec=true to allow TLC to run OS commands.
+
 LOCAL INSTANCE TLC
 LOCAL INSTANCE Integers
 LOCAL INSTANCE Sequences
diff --git a/modules/tlc2/overrides/IOUtils.java b/modules/tlc2/overrides/IOUtils.java
index 7439b04..b44c598 100644
--- a/modules/tlc2/overrides/IOUtils.java
+++ b/modules/tlc2/overrides/IOUtils.java
@@ -370,6 +370,9 @@ private static Value runProcess(final Map<String, String> env, final String[] co
 	
 	private static Value runProcess(final ProcessBuilder processBuilder)
 			throws IOException, InterruptedException {
+		if (!Boolean.getBoolean("tlc2.overrides.IOUtils.enableExec")) {
+			throw new EvalException(EC.GENERAL, "IOUtils exec is disabled by default. Evaluating an IOUtils exec operator such as IOExec runs an OS command. Set -Dtlc2.overrides.IOUtils.enableExec=true to allow it.");
+		}
 		// 3. Run command-line and receive its output.
 		final Process process = processBuilder/* .inheritIO() */.start();
 
diff --git a/tests/IOUtilsUnixTests.tla b/tests/IOUtilsUnixTests.tla
index d55fb4a..761a901 100644
--- a/tests/IOUtilsUnixTests.tla
+++ b/tests/IOUtilsUnixTests.tla
@@ -100,7 +100,7 @@ ASSUME PrintT("IOUtilsUnixTests!C!d")
 \* Run TLC with some spec depending on CommunityModules and CM on the classpath.
 \* Pass an environment variable to the nested spec.
 ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
-                            <<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
+                            <<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "-Dtlc2.overrides.IOUtils.enableExec=true", "tlc2.TLC",
                                           "-config", "Counter.cfg", "tests/nested/CounterCM">>)
                                                                  IN /\ PrintT(ret)
                                                                     /\ ret.exitValue = 0