diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index 6d1e6ff5943e4..76a774c9d1fc2 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -9,49 +9,24 @@ import rmc
 import rmc_flags
 import os
 import pathlib
+import toml
 
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
 RMC_C_LIB = MY_PATH / "library" / "rmc" / "rmc_lib.c"
 EXIT_CODE_SUCCESS = 0
 CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
-
 def main():
-    # Remove "rmc" from arg if invoked `cargo rmc ...`
-    if len(sys.argv) >= 2 and sys.argv[1] == "rmc":
-        del sys.argv[1]
-
-    parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate. For more information, see https://github.com/model-checking/rmc.")
-
-    crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
-    crate_group.add_argument("crate", help="crate to verify", nargs="?")
-    crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
-
-    exclude_flags = []
-    rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
-    args = parser.parse_args()
-
-    if args.crate:
-        rmc.ensure(args.crate_flag is None, "Please provide a single crate to verify.")
-    else:
-        rmc.ensure(args.crate_flag is not None, "Please provide a crate to verify.")
-        args.crate = args.crate_flag
-
-    if args.quiet:
-        args.verbose = False
+    args = parse_args()
 
     rmc.ensure_dependencies_in_path()
 
-    # Add some CBMC flags by default unless `--no-default-checks` is being used
-    if not args.no_default_checks:
-        rmc.add_selected_default_cbmc_flags(args)
-
     rmc.cargo_build(args.crate, args.target_dir,
                     args.verbose, args.debug, args.mangler, args.dry_run, [])
 
     pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
-    rmc.ensure(len(jsons) == 1, "Unexpected number of json outputs.")
+    rmc.ensure(len(jsons) == 1, f"Unexpected number of json outputs: {len(jsons)}")
 
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
@@ -89,6 +64,162 @@ def main():
 
     return retcode
 
+def parse_args():
+    # Create parser
+    def create_parser():
+        parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate. For more information, see https://github.com/model-checking/rmc.")
+
+        crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
+        crate_group.add_argument("crate", help="crate to verify", nargs="?")
+        crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
+
+        config_group = parser.add_argument_group("Config", "You can configure cargo rmc with your Cargo.toml file.")
+        config_group.add_argument("--config-toml", help="Where to read configuration from; defaults to crate's Cargo.toml")
+        config_group.add_argument("--no-config-toml", action="store_true", help="Do not use any configuration toml")
+
+        exclude_flags = []
+        rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
+        
+        return parser
+
+    # Determine what crate to analyze from flags
+    def get_crate_from_args(args):
+        validate(args)
+        return args.crate or args.crate_flag or "."
+
+    # Combine the command line parameter to get a config file; 
+    # return None if no_config_toml is set
+    def get_config_toml(no_config_toml, config_toml, args):
+        crate = get_crate_from_args(args)
+        if no_config_toml:
+            return None
+        elif config_toml is not None:
+            # If config_toml is explicitly given, ensure it exists
+            rmc.ensure(pathlib.Path(config_toml).is_file(), f"Invalid path to config file: {config_toml}")
+            return config_toml
+        else:
+            # If no config flags are set, look for config toml in default location (<crate>/Cargo.toml)
+            cargo_toml = pathlib.Path(crate).joinpath("Cargo.toml")
+            rmc.ensure(cargo_toml.is_file(), f"Cannot find configuration toml at expected location: {cargo_toml}")
+            return cargo_toml
+
+    # Combine args set by config toml and provided on command line
+    def get_combined_args(parser, config_toml):
+        # Extract flags from config_toml
+        toml_flags = extract_flags_from_toml(config_toml)
+
+        # Load args from toml flags
+        combined_args = argparse.Namespace()
+        parser.parse_args(toml_flags, namespace=combined_args)
+
+        # Set relative paths to be rooted at config toml's directory rather than cwd
+        def fix_paths(value):
+            if type(value) == list:
+                return list(map(fix_paths, value))
+            elif isinstance(value, pathlib.PurePath):
+                return pathlib.Path(config_toml).parent.joinpath(value)
+            else:
+                return value
+
+        ca_dict = combined_args.__dict__
+        for key in ca_dict:
+            ca_dict[key] = fix_paths(ca_dict[key])
+
+        # Load args from command line using toml args as default
+        parser.parse_args(sys.argv[1:], namespace=combined_args)
+
+        return combined_args
+
+    # Check for conflicting flags
+    def validate(args):
+        rmc.ensure(not (args.crate and args.crate_flag), "Please provide a single crate to verify.")   
+        rmc.ensure(not (args.no_config_toml and args.config_toml), "Incompatible flags: --config-toml, --no-config-toml")
+
+    # Fix up args before returning
+    def post_process(args):
+        # Combine positional and flag argument for input
+        args.crate = get_crate_from_args(args)
+
+        # --quiet overrides --verbose
+        if args.quiet:
+            args.verbose = False
+
+        # Add some CBMC flags by default unless `--no-default-checks` is being used
+        if args.default_checks:
+            rmc.add_selected_default_cbmc_flags(args)
+
+    # Remove "rmc" from arg if invoked `cargo rmc ...`
+    if len(sys.argv) >= 2 and sys.argv[1] == "rmc":
+        del sys.argv[1]
+
+    # Parse command line args to find crate and check for config flags
+    parser = create_parser()
+    cl_args = parser.parse_args()
+    validate(cl_args)
+
+    # Try to find the config_toml based on command line arguments
+    config_toml = get_config_toml(cl_args.no_config_toml, cl_args.config_toml, cl_args)
+
+    if config_toml is not None:
+        # If config_toml is found, combine configuration with command line arguments
+        combined_args = get_combined_args(parser, config_toml)
+        validate(combined_args)
+        post_process(combined_args)
+        return combined_args
+    else:
+        # If config_toml is missing, just use the parsed command line arguments
+        post_process(cl_args)
+        return cl_args
+
+# Extract a list of args based on given config toml
+def extract_flags_from_toml(path):
+    # Load the flag data from toml
+    data = toml.load(path)
+
+    # Extract the rmc flags from the toml, if any present
+    if ("rmc" not in data) or ("flags" not in data["rmc"]):
+        # If no flags are present, just return none
+        return []
+    rmc_data = data["rmc"]
+    flag_data = rmc_data["flags"]
+
+    # Extract nested flags
+    flags = dict()
+    def find_flags(map):
+        for key in map:
+            if type(map[key]) == dict:
+                find_flags(map[key])
+            else:
+                flags[key] = map[key]
+    find_flags(flag_data)
+
+    # Add config toml flags to flag list
+    success = True
+    flag_list = []
+    def add_flag(flag, value):
+        if type(value) == bool:
+            if value:
+                flag_list.append(f"--{flag}")
+            else:
+                if flag.startswith("no-"):
+                    flag_list.append(f"--{flag[3:]}")
+                else:
+                    flag_list.append(f"--no-{flag}")
+        elif type(value) == list:
+            flag_list.append(f"--{flag}")
+            assert all(map(lambda arg: type(arg) == str, value)), f"ERROR: Invalid config: {flag} = {value}"
+            flag_list.extend(value)
+        elif type(value) == str:
+            flag_list.append(f"--{flag}")
+            flag_list.append(value)
+        else:
+            print(f"ERROR: Invalid config: {flag} = {value}")
+            success = False
+    for flag in flags:
+        add_flag(flag, flags[flag])
+    
+    rmc.ensure(success)
+    return flag_list
 
 if __name__ == "__main__":
     sys.exit(main())
diff --git a/scripts/rmc b/scripts/rmc
index 19e2fcb22e163..c2fae101f7f4f 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -14,38 +14,10 @@ RMC_C_LIB = MY_PATH / "library" / "rmc" / "rmc_lib.c"
 EXIT_CODE_SUCCESS = 0
 CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
-
 def main():
-    parser = argparse.ArgumentParser(description="Verify a single Rust file. For more information, see https://github.com/model-checking/rmc.")
-
-    input_group = parser.add_argument_group("Input", "You can pass in the rust file positionally or with the --input flag.")
-    input_group.add_argument("input", help="Rust file to verify", nargs="?")
-    input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
-
-    exclude_flags = [
-        # In the future we hope to make this configurable in the command line.
-        # For now, however, changing this from "main" breaks rmc.
-        # Issue: https://github.com/model-checking/rmc/issues/169
-        "--function"
-    ]
-    rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=exclude_flags)
-    args = parser.parse_args()
-    args.function = "main"
-
-    if args.input:
-        rmc.ensure(args.input_flag is None, "Please provide a single file to verify.")
-    else:
-        rmc.ensure(args.input_flag is not None, "Please provide a file to verify.")
-        args.input = args.input_flag
-    
-    if args.quiet:
-        args.verbose = False
+    args = parse_args()
 
     rmc.ensure_dependencies_in_path()
-    
-    # Add some CBMC flags by default unless `--no-default-checks` is being used
-    if not args.no_default_checks:
-        rmc.add_selected_default_cbmc_flags(args)
 
     base, ext = os.path.splitext(args.input)
     rmc.ensure(ext == ".rs", "Expecting .rs input file.")
@@ -91,6 +63,54 @@ def main():
 
     return retcode
 
+def parse_args():
+    # Create parser
+    def create_parser():
+        parser = argparse.ArgumentParser(description="Verify a single Rust file. For more information, see https://github.com/model-checking/rmc.")
+
+        input_group = parser.add_argument_group("Input", "You can pass in the rust file positionally or with the --input flag.")
+        input_group.add_argument("input", help="Rust file to verify", nargs="?")
+        input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
+
+        exclude_flags = [
+            # In the future we hope to make this configurable in the command line.
+            # For now, however, changing this from "main" breaks rmc.
+            # Issue: https://github.com/model-checking/rmc/issues/169
+            "--function"
+        ]
+        rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=exclude_flags)
+        
+        return parser
+
+    # Check for conflicting flags
+    def validate(args):
+        rmc.ensure(not (args.input and args.input_flag), "Please provide a single file to verify.")
+        rmc.ensure(args.input or args.input_flag, "Please provide a file to verify.")
+
+    # Fix up args before returning
+    def post_process(args):
+        # Combine positional and flag argument for input
+        args.input = args.input or args.input_flag
+
+        # --quiet overrides --verbose
+        if args.quiet:
+            args.verbose = False
+
+        # In the future we hope to make this configurable in the command line.
+        # For now, however, changing this from "main" breaks rmc.
+        # Issue: https://github.com/model-checking/rmc/issues/169
+        args.function = "main"
+
+        # Add some CBMC flags by default unless `--no-default-checks` is being used
+        if args.default_checks:
+            rmc.add_selected_default_cbmc_flags(args)
+
+    parser = create_parser()
+    args = parser.parse_args()
+    validate(args)
+    post_process(args)
+
+    return args
 
 if __name__ == "__main__":
     sys.exit(main())
diff --git a/scripts/rmc.py b/scripts/rmc.py
index dc71a4ac2f8dc..2047032fadfcc 100644
--- a/scripts/rmc.py
+++ b/scripts/rmc.py
@@ -51,9 +51,10 @@ def ensure_dependencies_in_path():
         ensure(is_exe(program), f"Could not find {program} in PATH")
 
 # Assert a condition holds, or produce a user error message.
-def ensure(condition, message, retcode=1):
+def ensure(condition, message=None, retcode=1):
     if not condition:
-        print(f"ERROR: {message}")
+        if message:
+            print(f"ERROR: {message}")
         sys.exit(retcode)
 
 # Deletes a file; used by atexit.register to remove temporary files on exit
@@ -76,11 +77,11 @@ def add_set_cbmc_flags(args, flags):
 
 # Add sets of selected default CBMC flags
 def add_selected_default_cbmc_flags(args):
-    if not args.no_memory_safety_checks:
+    if args.memory_safety_checks:
         add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS)
-    if not args.no_overflow_checks:
+    if args.overflow_checks:
         add_set_cbmc_flags(args, OVERFLOW_CHECKS)
-    if not args.no_unwinding_checks:
+    if args.unwinding_checks:
         add_set_cbmc_flags(args, UNWINDING_CHECKS)
 
 # Updates environment to use gotoc backend debugging
@@ -153,6 +154,8 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb
 
 # Generates a symbol table (and some other artifacts) from a rust crate
 def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0", dry_run=False, symbol_table_passes=[]):
+    ensure(os.path.isdir(crate), f"Invalid path to crate: {crate}")
+
     rustflags = [
         "-Z", "codegen-backend=gotoc", 
         "-Z", f"symbol-mangling-version={mangler}", 
diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py
index 2a3ef783c23ed..2e40f34dfeb52 100644
--- a/scripts/rmc_flags.py
+++ b/scripts/rmc_flags.py
@@ -3,23 +3,66 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 import argparse
+import pathlib as pl
+
+# Taken from https://github.com/python/cpython/blob/3.9/Lib/argparse.py#L858
+# Cannot use `BooleanOptionalAction` with Python 3.8
+class BooleanOptionalAction(argparse.Action):
+    def __init__(self,
+                 option_strings,
+                 dest,
+                 default=None,
+                 type=None,
+                 choices=None,
+                 required=False,
+                 help=None,
+                 metavar=None):
+
+        _option_strings = []
+        for option_string in option_strings:
+            _option_strings.append(option_string)
+
+            if option_string.startswith('--'):
+                option_string = '--no-' + option_string[2:]
+                _option_strings.append(option_string)
+
+        if help is not None and default is not None:
+            help += f" (default: {default})"
+
+        super().__init__(
+            option_strings=_option_strings,
+            dest=dest,
+            nargs=0,
+            default=default,
+            type=type,
+            choices=choices,
+            required=required,
+            help=help,
+            metavar=metavar)
+
+    def __call__(self, parser, namespace, values, option_string=None):
+        if option_string in self.option_strings:
+            setattr(namespace, self.dest, not option_string.startswith('--no-'))
+
+    def format_usage(self):
+        return ' | '.join(self.option_strings)
 
 # Add flags related to debugging output.
 def add_loudness_flags(make_group, add_flag, config):
     group = make_group(
         "Loudness flags", "Determine how much textual output to produce.")
-    add_flag(group, "--debug", action="store_true",
+    add_flag(group, "--debug", default=False, action=BooleanOptionalAction,
              help="Produce full debug information")
-    add_flag(group, "--quiet", "-q", action="store_true",
+    add_flag(group, "--quiet", "-q", default=False, action=BooleanOptionalAction,
              help="Produces no output, just an exit code and requested artifacts; overrides --verbose")
-    add_flag(group, "--verbose", "-v", action="store_true",
+    add_flag(group, "--verbose", "-v", default=False, action=BooleanOptionalAction,
              help="Output processing stages and commands, along with minor debug information")
 
 # Add flags which specify configurations for the proof.
 def add_linking_flags(make_group, add_flag, config):
     group = make_group("Linking flags",
                        "Provide information about how to link the prover for RMC.")
-    add_flag(group, "--c-lib", nargs="*", default=[], action="extend",
+    add_flag(group, "--c-lib", type=pl.Path, nargs="*", default=[], action="extend",
              help="Link external C files referenced by Rust code")
     add_flag(group, "--function", default="main",
              help="Entry point for verification")
@@ -33,36 +76,36 @@ def add_artifact_flags(make_group, add_flag, config):
 
     group = make_group(
         "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
-    add_flag(group, "--gen-c", action="store_true",
+    add_flag(group, "--gen-c", default=False, action=BooleanOptionalAction,
              help="Generate C file equivalent to inputted program")
-    add_flag(group, "--gen-symbols", action="store_true",
+    add_flag(group, "--gen-symbols", default=False, action=BooleanOptionalAction,
              help="Generate a goto symbol table")
-    add_flag(group, "--keep-temps", action="store_true",
+    add_flag(group, "--keep-temps", default=False, action=BooleanOptionalAction,
              help="Keep temporary files generated throughout RMC process")
-    add_flag(group, "--target-dir", default=default_target, metavar="DIR",
+    add_flag(group, "--target-dir", type=pl.Path, default=default_target, metavar="DIR",
              help=f"Directory for all generated artifacts; defaults to \"{default_target}\"")
 
 # Add flags to turn off default checks.
 def add_check_flags(make_group, add_flag, config):
     group = make_group("Check flags", "Disable some or all default checks.")
-    add_flag(group, "--no-default-checks", action="store_true",
-             help="Disable all default checks")
-    add_flag(group, "--no-memory-safety-checks", action="store_true",
-             help="Disable default memory safety checks")
-    add_flag(group, "--no-overflow-checks", action="store_true",
-             help="Disable default overflow checks")
-    add_flag(group, "--no-unwinding-checks", action="store_true",
-             help="Disable default unwinding checks")
+    add_flag(group, "--default-checks", default=True, action=BooleanOptionalAction,
+             help="Turn on all default checks")
+    add_flag(group, "--memory-safety-checks", default=True, action=BooleanOptionalAction,
+             help="Turn on default memory safety checks")
+    add_flag(group, "--overflow-checks", default=True, action=BooleanOptionalAction,
+             help="Turn on default overflow checks")
+    add_flag(group, "--unwinding-checks", default=True, action=BooleanOptionalAction,
+             help="Turn on default unwinding checks")
 
 # Add flags needed only for visualizer.
 def add_visualizer_flags(make_group, add_flag, config):
     group = make_group(
         "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
-    add_flag(group, "--srcdir", default=".",
+    add_flag(group, "--srcdir", type=pl.Path, default=".",
              help="The source directory: the root of the source tree")
-    add_flag(group, "--visualize", action="store_true",
+    add_flag(group, "--visualize", default=False, action=BooleanOptionalAction,
              help="Generate visualizer report to <target-dir>/report/html/index.html")
-    add_flag(group, "--wkdir", default=".",
+    add_flag(group, "--wkdir", type=pl.Path, default=".",
              help="""
                   The working directory: used to determine source locations in output;
                   this is generally the location from which rmc is currently being invoked
@@ -71,9 +114,9 @@ def add_visualizer_flags(make_group, add_flag, config):
 # Add flags for ad-hoc features.
 def add_other_flags(make_group, add_flag, config):
     group = make_group("Other flags")
-    add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
+    add_flag(group, "--allow-cbmc-verification-failure", default=False, action=BooleanOptionalAction,
              help="Do not produce error return code on CBMC verification failure")
-    add_flag(group, "--dry-run", action="store_true",
+    add_flag(group, "--dry-run", default=False, action=BooleanOptionalAction,
              help="Print commands instead of running them")
 
 # Add flags we don't expect end-users to use.
@@ -110,7 +153,6 @@ def add_flag(group, flag, *args, **kwargs):
         if flag in exclude_flags:
             excluded_flags.add(flag)
             return
-
         group.add_argument(flag, *args, **kwargs)
 
     add_groups = [
diff --git a/scripts/setup/macos-10.15/install_deps.sh b/scripts/setup/macos-10.15/install_deps.sh
index 5b98255e5c19d..34fe7d4bea592 100755
--- a/scripts/setup/macos-10.15/install_deps.sh
+++ b/scripts/setup/macos-10.15/install_deps.sh
@@ -7,3 +7,10 @@ set -eux
 # Update tools in macOS 10.15 via `brew`
 brew update
 brew install ctags
+
+# Add Python package dependencies
+PYTHON_DEPS=(
+  toml # Used for parsing `cargo-rmc` config toml
+)
+
+python3 -m pip install "${PYTHON_DEPS[@]}"
diff --git a/scripts/setup/ubuntu-20.04/install_deps.sh b/scripts/setup/ubuntu-20.04/install_deps.sh
index f3f65ae9dd5e0..a5b566350259d 100755
--- a/scripts/setup/ubuntu-20.04/install_deps.sh
+++ b/scripts/setup/ubuntu-20.04/install_deps.sh
@@ -32,3 +32,10 @@ set -x
 
 sudo apt-get --yes update
 sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"
+
+# Add Python package dependencies
+PYTHON_DEPS=(
+  toml # Used for parsing `cargo-rmc` config toml
+)
+
+python3 -m pip install "${PYTHON_DEPS[@]}"
diff --git a/src/test/cargo-rmc/simple-config-toml/Cargo.toml b/src/test/cargo-rmc/simple-config-toml/Cargo.toml
new file mode 100644
index 0000000000000..ed5c8942be82d
--- /dev/null
+++ b/src/test/cargo-rmc/simple-config-toml/Cargo.toml
@@ -0,0 +1,21 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "simple-config-toml"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]
+
+[rmc.flags.loudness]
+quiet = false
+
+[rmc.flags.artifacts.extra.suffixes]
+gen-c = true
+
+[rmc.flag]
+visualize = false
+mangler = "v0"
+cbmc-args = []
diff --git a/src/test/cargo-rmc/simple-config-toml/src/lib.rs b/src/test/cargo-rmc/simple-config-toml/src/lib.rs
new file mode 100644
index 0000000000000..9fda13682d350
--- /dev/null
+++ b/src/test/cargo-rmc/simple-config-toml/src/lib.rs
@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub mod pair;
+pub use pair::Pair;
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn it_works() {
+        assert_eq!(2 + 2, 4);
+    }
+}
+
+#[cfg(rmc)]
+mod rmc_tests {
+    use super::*;
+
+    fn __nondet<T>() -> T {
+        unimplemented!()
+    }
+    #[allow(dead_code)]
+    #[no_mangle]
+    fn test_sum() {
+        let a: u64 = __nondet();
+        let b: u64 = __nondet();
+        let p = Pair::new(a, b);
+        assert!(p.sum() == a.wrapping_add(b));
+    }
+}
diff --git a/src/test/cargo-rmc/simple-config-toml/src/pair.rs b/src/test/cargo-rmc/simple-config-toml/src/pair.rs
new file mode 100644
index 0000000000000..5a3413d9dabce
--- /dev/null
+++ b/src/test/cargo-rmc/simple-config-toml/src/pair.rs
@@ -0,0 +1,33 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub struct Pair(pub u64, pub u64);
+
+impl Pair {
+    pub fn new(a: u64, b: u64) -> Self {
+        Pair(a, b)
+    }
+    pub fn sum(&self) -> u64 {
+        self.0.wrapping_add(self.1)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    #[test]
+    fn one_plus_two() {
+        let p = Pair::new(1, 2);
+        assert_eq!(p.sum(), 3);
+    }
+}
+
+#[cfg(rmc)]
+mod rmc_tests {
+    use super::*;
+    #[allow(dead_code)]
+    #[no_mangle]
+    fn test_one_plus_two() {
+        let p = Pair::new(1, 2);
+        assert!(p.sum() == 3);
+    }
+}
diff --git a/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected b/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected
new file mode 100644
index 0000000000000..fc1b748eefd56
--- /dev/null
+++ b/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected
@@ -0,0 +1 @@
+[test_one_plus_two.assertion.1] line 31 assertion failed: p.sum() == 3: SUCCESS
diff --git a/src/test/cargo-rmc/simple-config-toml/test_sum.expected b/src/test/cargo-rmc/simple-config-toml/test_sum.expected
new file mode 100644
index 0000000000000..029fbf83bc1cc
--- /dev/null
+++ b/src/test/cargo-rmc/simple-config-toml/test_sum.expected
@@ -0,0 +1 @@
+[test_sum.assertion.1] line 27 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS
diff --git a/src/test/cargo-rmc/simple-extern/Cargo.toml b/src/test/cargo-rmc/simple-extern/Cargo.toml
index 30f31a9082475..77289d86be60a 100644
--- a/src/test/cargo-rmc/simple-extern/Cargo.toml
+++ b/src/test/cargo-rmc/simple-extern/Cargo.toml
@@ -8,3 +8,6 @@ edition = "2018"
 [dependencies]
 
 [workspace]
+
+[rmc.flags.linking]
+c-lib = ["src/helper.c"]
diff --git a/src/test/cargo-rmc/simple-extern/test_sum.expected b/src/test/cargo-rmc/simple-extern/test_sum.expected
new file mode 100644
index 0000000000000..dcd14c5e587b1
--- /dev/null
+++ b/src/test/cargo-rmc/simple-extern/test_sum.expected
@@ -0,0 +1 @@
+[external_c_assertion.assertion.1] line 13 assertion rust_add1(x) == x + 1: SUCCESS
diff --git a/src/test/cargo-rmc/simple-extern/test_sum.ignore b/src/test/cargo-rmc/simple-extern/test_sum.ignore
deleted file mode 100644
index 51e68d596b6af..0000000000000
--- a/src/test/cargo-rmc/simple-extern/test_sum.ignore
+++ /dev/null
@@ -1 +0,0 @@
-[call_into_rust.assertion.1] line 13 assertion takes_int(x) == x + 1: SUCCESS
diff --git a/src/test/cargo-rmc/simple-lib/Cargo.toml b/src/test/cargo-rmc/simple-lib/Cargo.toml
index bd7364c287259..30f31a9082475 100644
--- a/src/test/cargo-rmc/simple-lib/Cargo.toml
+++ b/src/test/cargo-rmc/simple-lib/Cargo.toml
@@ -1,3 +1,5 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
 [package]
 name = "simple-lib"
 version = "0.1.0"
diff --git a/src/test/cargo-rmc/simple-main/Cargo.toml b/src/test/cargo-rmc/simple-main/Cargo.toml
index 5818412ee5e64..295edc0cb8583 100644
--- a/src/test/cargo-rmc/simple-main/Cargo.toml
+++ b/src/test/cargo-rmc/simple-main/Cargo.toml
@@ -1,3 +1,5 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
 [package]
 name = "empty-main"
 version = "0.1.0"