diff --git a/.cargo/config.toml b/.cargo/config.toml
new file mode 100644
index 000000000000..7b4add9ae883
--- /dev/null
+++ b/.cargo/config.toml
@@ -0,0 +1,37 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[target.'cfg(all())']
+rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
+
+    # Purposefully disabled lints
+    "-Aclippy::expect_fun_call",
+    "-Aclippy::or_fun_call",
+
+    # todo address the following lints.
+    "-Aclippy::cargo_common_metadata",
+    "-Aclippy::derive_partial_eq_without_eq",
+    "-Aclippy::explicit_auto_deref",
+    "-Aclippy::if_same_then_else",
+    "-Aclippy::iter_nth_zero",
+    "-Aclippy::let_and_return",
+    "-Aclippy::manual_map",
+    "-Aclippy::manual_range_contains",
+    "-Aclippy::manual_strip",
+    "-Aclippy::map_entry",
+    "-Aclippy::match_like_matches_macro",
+    "-Aclippy::missing_safety_doc",
+    "-Aclippy::module_inception",
+    "-Aclippy::needless_arbitrary_self_type",
+    "-Aclippy::needless_bool",
+    "-Aclippy::needless_return",
+    "-Aclippy::new_ret_no_self",
+    "-Aclippy::new_without_default",
+    "-Aclippy::redundant_clone",
+    "-Aclippy::too_many_arguments",
+    "-Aclippy::type_complexity",
+    "-Aclippy::unnecessary_lazy_evaluations",
+    "-Aclippy::useless_conversion",
+    "-Aclippy::needless_borrow",
+    "-Aclippy::unnecessary_filter_map",
+]
diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml
index 29f1ed612089..e3f0d9ff5515 100644
--- a/.github/workflows/format-check.yml
+++ b/.github/workflows/format-check.yml
@@ -20,3 +20,29 @@ jobs:
         run: |
             pip3 install --upgrade autopep8
             ./scripts/run-autopep8.sh
+
+  clippy-check:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v2
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+            os: ubuntu-20.04
+
+      - name: "Install jq for parsing."
+        run: |
+          sudo apt-get install -y jq
+
+      - name: "Run Clippy"
+        run: |
+          cargo clippy --all -- -D warnings
+
+      - name: "Print Clippy Statistics"
+        run: |
+          rm .cargo/config.toml
+          (cargo clippy --all --message-format=json 2>/dev/null  | \
+          jq 'select(.message!=null) | .message.code.code' | grep -v '^null$' | \
+          sort | uniq -c) || true
diff --git a/.gitignore b/.gitignore
index 714cb05350d7..f53d5beacf76 100644
--- a/.gitignore
+++ b/.gitignore
@@ -24,9 +24,6 @@ Session.vim
 
 ## Tool
 .valgrindrc
-.cargo
-# Included because it is part of the test case
-!/test/run-make/thumb-none-qemu/example/.cargo
 
 ## Configuration
 /config.toml
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index 38bcf93ec6dc..c4df9573d7e9 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -6,6 +6,7 @@ name = "cprover_bindings"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 test = true
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index b94b11a04c36..38414408a792 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -6,6 +6,7 @@ name = "kani-compiler"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 ar = { version = "0.9.0", optional = true }
diff --git a/kani-compiler/kani_queries/Cargo.toml b/kani-compiler/kani_queries/Cargo.toml
index 7910ae6548ef..e4fe9fa7c90d 100644
--- a/kani-compiler/kani_queries/Cargo.toml
+++ b/kani-compiler/kani_queries/Cargo.toml
@@ -6,6 +6,7 @@ name = "kani_queries"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 tracing = {version = "0.1"}
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index d60ecb2d132f..58391cd5d31a 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -9,6 +9,7 @@ description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
 homepage = "https://github.com/model-checking/kani"
 repository = "https://github.com/model-checking/kani"
+publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index dd79fe89571c..e121939ccb7c 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -6,6 +6,7 @@ name = "kani_metadata"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index d679873278e6..8fd8d8175129 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -6,6 +6,7 @@ name = "kani"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani_macros = { path = "../kani_macros" }
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
index dbbcc87d474a..222ba5a60e29 100644
--- a/library/kani/src/invariant.rs
+++ b/library/kani/src/invariant.rs
@@ -67,7 +67,7 @@ unsafe impl Invariant for char {
     fn is_valid(&self) -> bool {
         // Kani translates char into i32.
         let val = *self as i32;
-        val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF)
+        val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)
     }
 }
 
diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
index a1b50b838ff8..618bb0ad9688 100644
--- a/library/kani/src/slice.rs
+++ b/library/kani/src/slice.rs
@@ -149,6 +149,10 @@ where
     AnySlice::<T, MAX_SLICE_LENGTH>::new()
 }
 
+/// # Safety
+///
+/// TODO: Safety of any_raw_slice is a complex matter. See
+/// https://github.com/model-checking/kani/issues/1394
 pub unsafe fn any_raw_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH> {
     AnySlice::<T, MAX_SLICE_LENGTH>::new_raw()
 }
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index 9f4f7bd9065d..68cf3fbdfafe 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -6,6 +6,7 @@ name = "kani_macros"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 proc-macro = true
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 43c709832a62..97888cdbfdf2 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -39,7 +39,7 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
 pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
-    assert!(attr.to_string().len() == 0, "#[kani::proof] does not take any arguments");
+    assert!(attr.to_string().is_empty(), "#[kani::proof] does not take any arguments");
     result.extend("#[kanitool::proof]".parse::<TokenStream>().unwrap());
     // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
     result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
@@ -67,7 +67,7 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
     // Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)]
-    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.clone().to_string() + ")]";
+    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.to_string() + ")]";
     result.extend(insert_string.parse::<TokenStream>().unwrap());
 
     result.extend(item);
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index 349b50000f3c..bf8edeaf6ffb 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -8,6 +8,7 @@ name = "std"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani = {path="../kani"}
diff --git a/tools/bookrunner/Cargo.toml b/tools/bookrunner/Cargo.toml
index bafbbea1ce65..f98b4ec72a83 100644
--- a/tools/bookrunner/Cargo.toml
+++ b/tools/bookrunner/Cargo.toml
@@ -6,6 +6,7 @@ name = "bookrunner"
 version = "0.1.0"
 edition = "2018"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 Inflector = "0.11.4"
diff --git a/tools/bookrunner/librustdoc/Cargo.toml b/tools/bookrunner/librustdoc/Cargo.toml
index cc65a1e44727..f83c6e25803c 100644
--- a/tools/bookrunner/librustdoc/Cargo.toml
+++ b/tools/bookrunner/librustdoc/Cargo.toml
@@ -7,6 +7,8 @@ name = "rustdoc"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
+
 # From upstream librustdoc:
 # https://github.com/rust-lang/rust/tree/master/src/librustdoc
 # Upstream crate does not list license but Rust statues:
diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml
index 83427b1e8e96..c525d2ec2db0 100644
--- a/tools/compiletest/Cargo.toml
+++ b/tools/compiletest/Cargo.toml
@@ -8,6 +8,7 @@ name = "compiletest"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 # From upstream compiletest:
 # https://github.com/rust-lang/rust/tree/master/src/tools/compiletest
 # Upstream crate does not list license but Rust statues:
diff --git a/tools/make-kani-release/Cargo.toml b/tools/make-kani-release/Cargo.toml
index b72d1fa654eb..7f3fb7ce8f24 100644
--- a/tools/make-kani-release/Cargo.toml
+++ b/tools/make-kani-release/Cargo.toml
@@ -7,6 +7,7 @@ version = "0.1.0"
 edition = "2021"
 description = "Contructs a Kani release bundle"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 anyhow = "1"