diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index 6676e3aa7f61b537b74b782b037cfbf276eacbaf..b7ab26ebddd6e89f46b07d6e65307513afb5d401 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -589,6 +589,7 @@ name = "radium"
 version = "0.1.0"
 dependencies = [
  "log",
+ "rrconfig",
 ]
 
 [[package]]
diff --git a/rr_frontend/radium/Cargo.toml b/rr_frontend/radium/Cargo.toml
index 98d62751beaf9139a8b14d04d3afa2604fc7e345..910c3c3605760807bef75d6d1e612a81852b226f 100644
--- a/rr_frontend/radium/Cargo.toml
+++ b/rr_frontend/radium/Cargo.toml
@@ -7,3 +7,5 @@ edition = "2021"
 
 [dependencies]
 log = "0.4"
+rrconfig = { path = "../rrconfig" }
+
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index c76eb566143507d0128fc6f51d5b476bd1fc6356..33439e933ef6037c7009fca04198e7f3f4fb10b0 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -1123,7 +1123,12 @@ impl<'def> Function<'def> {
 
         out.push_str(format!("{}Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal \"{}\".\n", indent, self.name()).as_str());
 
-        out.push_str("Qed.\n");
+        if rrconfig::admit_proofs() {
+            out.push_str("Admitted. (* admitted due to admit_proofs config flag *)\n");
+        }
+        else {
+            out.push_str("Qed.\n");
+        }
         out
     }
 }
diff --git a/rr_frontend/radium/src/lib.rs b/rr_frontend/radium/src/lib.rs
index cf72485b394fcb84b9e9602063e9fe097ce90ae9..f296572e97dddcfe6b1c49b6a587423bcd83aeff 100644
--- a/rr_frontend/radium/src/lib.rs
+++ b/rr_frontend/radium/src/lib.rs
@@ -1,5 +1,6 @@
 #![feature(box_patterns)]
 
+use rrconfig;
 
 pub mod code;
 pub mod specs;
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index bf2d4a9cfb222f9e76efea009072256c5c3afba1..3dfd6469fa7f6c4e706e2173c944d841129eca69 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/rr_frontend/rrconfig/src/lib.rs
@@ -33,7 +33,8 @@ lazy_static! {
                 .set_default("verify_deps", false)?
                 .set_default("no_verify", false)?
                 .set_default("cargo_path", "cargo")?
-                .set_default("cargo_command", "check")?;
+                .set_default("cargo_command", "check")?
+                .set_default("admit_proofs", false)?;
 
             // 2. Override with the optional TOML file "RefinedRust.toml" (if there is any)
             builder = builder.add_source(
@@ -126,6 +127,11 @@ pub fn output_dir() -> Option<String> {
     read_optional_setting("output_dir")
 }
 
+/// Whether to admit proofs of functions instead of running Qed. 
+pub fn admit_proofs() -> bool {
+    read_setting("admit_proofs")
+}
+
 /// Which file to read shims from?
 pub fn shim_file() -> Option<String> {
     read_optional_setting("shims")