diff --git a/light-client/Cargo.toml b/light-client/Cargo.toml
index cb62e665b..98ab6689f 100644
--- a/light-client/Cargo.toml
+++ b/light-client/Cargo.toml
@@ -38,7 +38,7 @@ tendermint = { version = "0.24.0-pre.1", path = "../tendermint", default-feature
 tendermint-rpc = { version = "0.24.0-pre.1", path = "../rpc", default-features = false }
 tendermint-light-client-verifier = { version = "0.24.0-pre.1", path = "../light-client-verifier", default-features = false }
 
-contracts = { version = "0.4.0", default-features = false }
+contracts = { version = "0.6.2", default-features = false }
 crossbeam-channel = { version = "0.4.2", default-features = false }
 derive_more = { version = "0.99.5", default-features = false, features = ["display"] }
 futures = { version = "0.3.4", default-features = false }
diff --git a/light-client/src/components/scheduler.rs b/light-client/src/components/scheduler.rs
index 1014a6890..f0caf4dfa 100644
--- a/light-client/src/components/scheduler.rs
+++ b/light-client/src/components/scheduler.rs
@@ -20,8 +20,8 @@ pub trait Scheduler: Send + Sync {
     ///
     /// ## Postcondition
     /// - The resulting height must be valid according to `valid_schedule`. [LCV-SCHEDULE-POST.1]
-    #[pre(light_store.highest_trusted_or_verified().is_some())]
-    #[post(valid_schedule(ret, target_height, current_height, light_store))]
+    #[requires(light_store.highest_trusted_or_verified().is_some())]
+    #[ensures(valid_schedule(ret, target_height, current_height, light_store))]
     fn schedule(
         &self,
         light_store: &dyn LightStore,
@@ -53,8 +53,8 @@ where
 ///
 /// ## Postcondition
 /// - The resulting height must be valid according to `valid_schedule`. [LCV-SCHEDULE-POST.1]
-#[pre(light_store.highest_trusted_or_verified().is_some())]
-#[post(valid_schedule(ret, target_height, current_height, light_store))]
+#[requires(light_store.highest_trusted_or_verified().is_some())]
+#[ensures(valid_schedule(ret, target_height, current_height, light_store))]
 pub fn basic_bisecting_schedule(
     light_store: &dyn LightStore,
     current_height: Height,
@@ -120,8 +120,8 @@ pub fn valid_schedule(
     }
 }
 
-#[pre(low <= high)]
-#[post(low <= ret && ret <= high)]
+#[requires(low <= high)]
+#[ensures(low <= ret && ret <= high)]
 fn midpoint(low: Height, high: Height) -> Height {
     (low.value() + (high.value() + 1 - low.value()) / 2)
         .try_into()
diff --git a/light-client/src/evidence.rs b/light-client/src/evidence.rs
index 1821bfcbd..70da97310 100644
--- a/light-client/src/evidence.rs
+++ b/light-client/src/evidence.rs
@@ -24,7 +24,7 @@ mod prod {
     use super::*;
     use crate::utils::block_on;
 
-    use contracts::pre;
+    use contracts::requires;
     use std::{collections::HashMap, time::Duration};
 
     use tendermint_rpc as rpc;
@@ -40,7 +40,7 @@ mod prod {
 
     #[contract_trait]
     impl EvidenceReporter for ProdEvidenceReporter {
-        #[pre(self.peer_map.contains_key(&peer))]
+        #[requires(self.peer_map.contains_key(&peer))]
         fn report(&self, e: Evidence, peer: PeerId) -> Result<Hash, IoError> {
             let client = self.rpc_client_for(peer)?;
 
@@ -65,7 +65,7 @@ mod prod {
             Self { peer_map, timeout }
         }
 
-        #[pre(self.peer_map.contains_key(&peer))]
+        #[requires(self.peer_map.contains_key(&peer))]
         fn rpc_client_for(&self, peer: PeerId) -> Result<rpc::HttpClient, IoError> {
             let peer_addr = self.peer_map.get(&peer).unwrap().to_owned();
             rpc::HttpClient::new(peer_addr).map_err(IoError::rpc)
diff --git a/light-client/src/light_client.rs b/light-client/src/light_client.rs
index e90168c55..57485ec5a 100644
--- a/light-client/src/light_client.rs
+++ b/light-client/src/light_client.rs
@@ -140,8 +140,9 @@ impl LightClient {
     /// - If the core verification loop invariant is violated [LCV-INV-TP.1]
     /// - If verification of a light block fails
     /// - If the fetching a light block from the primary node fails
-    #[post(
-        ret.is_ok() ==> trusted_store_contains_block_at_target_height(
+    #[allow(clippy::nonminimal_bool)]
+    #[ensures(
+        ret.is_ok() -> trusted_store_contains_block_at_target_height(
             state.light_store.as_ref(),
             target_height,
         )
@@ -365,7 +366,7 @@ impl LightClient {
     ///
     /// ## Postcondition
     /// - The provider of block that is returned matches the given peer.
-    #[post(ret.as_ref().map(|(lb, _)| lb.provider == self.peer).unwrap_or(true))]
+    #[ensures(ret.as_ref().map(|(lb, _)| lb.provider == self.peer).unwrap_or(true))]
     pub fn get_or_fetch_block(
         &self,
         height: Height,
diff --git a/light-client/src/peer_list.rs b/light-client/src/peer_list.rs
index d1f3d58f4..3937656c1 100644
--- a/light-client/src/peer_list.rs
+++ b/light-client/src/peer_list.rs
@@ -1,6 +1,6 @@
 //! Provides a peer list for use within the `Supervisor`
 
-use contracts::{post, pre};
+use contracts::*;
 use std::collections::{BTreeSet, HashMap};
 
 use crate::errors::Error;
@@ -111,8 +111,8 @@ impl<T> PeerList<T> {
     /// ## Precondition
     /// - The given peer id must not be the primary peer id.
     /// - The given peer must be in the witness list
-    #[pre(faulty_witness != self.primary && self.witnesses.contains(&faulty_witness))]
-    #[post(Self::invariant(self))]
+    #[requires(faulty_witness != self.primary && self.witnesses.contains(&faulty_witness))]
+    #[ensures(Self::invariant(self))]
     pub fn replace_faulty_witness(&mut self, faulty_witness: PeerId) -> Option<PeerId> {
         let mut result = None;
 
@@ -134,7 +134,8 @@ impl<T> PeerList<T> {
     ///
     /// ## Errors
     /// - If there are no witness left, returns `ErrorKind::NoWitnessLeft`.
-    #[post(ret.is_ok() ==> Self::invariant(self))]
+    #[allow(clippy::nonminimal_bool)]
+    #[ensures(ret.is_ok() -> Self::invariant(self))]
     pub fn replace_faulty_primary(
         &mut self,
         primary_error: Option<Error>,
@@ -196,21 +197,21 @@ impl<T> PeerListBuilder<T> {
     }
 
     /// Register the given peer id and value as a witness.
-    #[pre(self.primary != Some(peer_id))]
+    #[requires(self.primary != Some(peer_id))]
     pub fn witness(&mut self, peer_id: PeerId, value: T) {
         self.values.insert(peer_id, value);
         self.witnesses.insert(peer_id);
     }
 
     /// Register the given peer id and value as a full node.
-    #[pre(self.primary != Some(peer_id))]
+    #[requires(self.primary != Some(peer_id))]
     pub fn full_node(&mut self, peer_id: PeerId, value: T) {
         self.values.insert(peer_id, value);
         self.full_nodes.insert(peer_id);
     }
 
     /// Register the given peer id and value as a faulty node.
-    #[pre(self.primary != Some(peer_id))]
+    #[requires(self.primary != Some(peer_id))]
     pub fn faulty_node(&mut self, peer_id: PeerId, value: T) {
         self.values.insert(peer_id, value);
         self.faulty_nodes.insert(peer_id);
@@ -220,8 +221,8 @@ impl<T> PeerListBuilder<T> {
     ///
     /// ## Precondition
     /// - A primary has been set with a call to `PeerListBuilder::primary`.
-    #[pre(self.primary.is_some())]
-    #[post(PeerList::invariant(&ret))]
+    #[requires(self.primary.is_some())]
+    #[ensures(PeerList::invariant(&ret))]
     pub fn build(self) -> PeerList<T> {
         PeerList {
             values: self.values,
diff --git a/light-client/src/state.rs b/light-client/src/state.rs
index c4ee0a56d..7f01b2349 100644
--- a/light-client/src/state.rs
+++ b/light-client/src/state.rs
@@ -32,7 +32,7 @@ impl State {
     ///
     /// ## Preconditions
     /// - `height` <= `target_height`
-    #[pre(height <= target_height)]
+    #[requires(height <= target_height)]
     pub fn trace_block(&mut self, target_height: Height, height: Height) {
         self.verification_trace
             .entry(target_height)