diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index d82c7760360f..dee9c8f182a4 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -588,7 +588,7 @@ macro_rules! comma_tok {
     };
 }
 
-/// Parse the a token stream inside an attribute (like `kanitool::modifies`) as a comma separated
+/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated
 /// sequence of function parameter names on `local_def_id` (must refer to a function). Then
 /// translates the names into [`Local`]s.
 fn parse_modify_values<'a>(
diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
index 07e1b4cfaa19..4f963038cab9 100644
--- a/library/kani/src/contracts.rs
+++ b/library/kani/src/contracts.rs
@@ -118,7 +118,7 @@
 //!
 //! ## Specification Attributes Overview
 //!
-//! The basic two two specification attributes available for describing
+//! The basic two specification attributes available for describing
 //! function behavior are [`requires`][macro@requires] for preconditions and
 //! [`ensures`][macro@ensures] for postconditions. Both admit arbitrary Rust
 //! expressions as their bodies which may also reference the function arguments