diff --git a/spec/consensus/light-client.md b/spec/consensus/light-client.md
index ee9f792c4..76ad8c823 100644
--- a/spec/consensus/light-client.md
+++ b/spec/consensus/light-client.md
@@ -203,6 +203,7 @@ captured by the ```hasExpired``` function that depends on trusted period (`tp`)
     if h.Header.bfttime + tp - Delta < now { // Observation 1
       return true
     }
+    return false
   }
 
   // return true if header is correctly signed by 2/3+ voting power in the corresponding validator set; 
@@ -286,7 +287,7 @@ func CanTrust(h1,h2,trustlevel) (bool, error) {
        // try to move trusted header forward with stored headers
        ih := th
        // try to move trusted header forward
-       for h in stored headers s.t ih.Header.Height < h.Header.height < h2.Header.height do {  
+       for h in stored headers s.t ih.Header.Height < h.Header.height < h2.Header.height do {
             // we assume here that iteration is done in the order of header heights
             ok, err = CheckSupport(th,h,trustlevel)
             if err != nil { return (ok, err) }
@@ -295,7 +296,7 @@ func CanTrust(h1,h2,trustlevel) (bool, error) {
             }
         }
 
-        // at this point we have potentially updated th based on stored headers so we try to verify h2 
+        // at this point we have potentially updated th based on stored headers so we try to verify h2
         // based on new trusted header
         ok, err = CheckSupport(th,h2,trustlevel)
         if (ok or err != nil) return (ok, err)
@@ -320,7 +321,7 @@ func CanTrust(h1,h2,trustlevel) (bool, error) {
         }
   }
 }
-```  
+```
 
 ```go
 func CanTrustBisection(h1,h2,trustlevel) bool{
@@ -393,3 +394,97 @@ func Backwards(h1,h2) bool {
   return (hash(h2) == old.Header.hash)
  }
 ```
+
+```go
+// return true if header has expired, i.e., it is outside its trusted period; otherwise it returns false
+func hasExpired(h) bool {
+    if now - h.Header.bfttime > tp - Delta
+        return true  // Observation 1
+    return false
+}
+
+// return true if header is correctly signed by 2/3+ voting power in the corresponding validator set;
+// otherwise false. Additional checks should be done in the implementation
+// to ensure header is well formed.
+func verify(h) bool {
+    vp_all := totalVotingPower(h.Header.V) // total sum of voting power of validators in h
+    return votingpower_in(signers(h.Commit),h.Header.V) > 2/3 * vp_all
+}
+
+// Captures skipping condition. h1 and h2 has already passed basic validation (function `verify`).
+// returns (true, nil) in case h2 can be trusted based on h1, (false, nil) in case it cannot be trusted but no errors
+// are observed during check and (false, error) in case an error is detected (for example adjacent
+// headers are not consistent).
+func CheckSupport(h1,h2,trustlevel) (bool, error) {
+    assume h1.Header.Height < h2.header.Height
+
+    // check for adjacent headers
+    if h2.Header.height == h1.Header.height + 1 {
+        if h1.Header.NextV == h2.Header.V return nil
+        return false, ErrInvalidAdjacentHeaders
+    }
+
+    // total sum of voting power of validators in h1.NextV
+    vp_all := totalVotingPower(h1.Header.NextV)
+    // check for non-adjacent headers
+    return votingpower_in(signers(h2.Commit),h1.Header.NextV) > max(1/3,trustlevel) * vp_all, nil
+}
+
+// return nil in case we can trust header h2 based on header h1, error otherwise
+func Bisection(h1,h2,trustlevel) error {
+    assume h1.Header.Height < h2.header.Height
+
+    th := h1
+    pivot = h2.Header.height
+    untrustedHeaders = []
+
+    while h2 not in Store.Headers() { // could be replaced with while true and check if h2 is stored in the loop
+        // check support for pivot, bisect if no support until a higher trusted header is found
+        while pivot < h1.Header.height {
+            hp := Commit(pivot)
+            if !verify(hp) return ErrInvalidHeader(hp)
+            done, err = CheckSupport(th,hp,trustlevel)
+            if err != nil return err
+            if done {
+                th = hp
+                Store.Add(hp)
+                break
+            }
+            untrustedHeaders.add(hp)
+            pivot := (th.Header.height + endHeight) / 2
+        }
+
+        // try to move trusted header forward
+        for h in untrustedHeaders {
+            // we assume here that iteration is done in the order of header heights
+            done, err = CheckSupport(th,h,trustlevel)
+            if err != nil return err
+            if done {
+                th = h
+                Store.Add(h)
+            }
+        }
+    }
+    return nil
+}
+
+func VerifyHeader(h2, trustlevel) error {
+    if h2 in Store.Headers()
+        return nil
+
+    Store.DisableExpiration()
+    // get the highest trusted headers lower than h2
+    h1 = Store.HighestTrusted(h2.Header.height)
+    if h1 == nil
+        return ErrNoTrustedHeader
+
+    err = Bisection(h1, h2, trustlevel)
+    if err != nil return err
+
+    // remove all expired headers and start the expiration timer
+    Store.EnableExpiration()
+    if h2 in Store.Headers() return nil
+    return ErrHeaderExpired
+}
+
+```
\ No newline at end of file