diff --git a/docs/theorem_prover.md b/docs/theorem_prover.md
new file mode 100644
index 0000000..48f9518
--- /dev/null
+++ b/docs/theorem_prover.md
@@ -0,0 +1,70 @@
+# Verified core of the Raft consensus logic
+
+The safety-critical consensus decisions now live in
+[`raft/core.py`](../raft/core.py) — the module the state machines
+(`raft/states/voter.py`, `candidate.py`, `follower.py`, `leader.py`) actually
+call.  That module is written in the **static-python subset** and is *both*
+executed (its `CHECKER.*` blocks are dead constants at runtime) *and*
+transpiled to Lean with `py2many --lean`, where `lake build` proves every
+pre/post condition, class invariant and lemma.  Because the implementation
+calls the very same functions that are verified, the two cannot silently
+diverge.
+
+## Layout
+
+* `raft/core.py` — the verified, total decision predicates
+  (`may_grant_vote`, `promote_to_leader`, `clamp_commit`, `log_matching_ok`,
+  `can_commit`, the `ConsensusState` invariant).  Each mirrors the live
+  implementation *exactly* (not an idealized paper version).
+* `raft/live.py` — the fallible runtime face: `Result[T, E]` (`Ok`/`Error`)
+  instead of exceptions for out-of-bounds log access, per the static-python
+  rule.  Not Lean-transpiled yet (Lean emission of `Ok`/`Error` is a pending
+  py2many change).
+* `py2many/` — a tiny *vendored* shim of `py2many.spec` / `py2many.theorem` /
+  `py2many.result` so the raft package imports standalone when the real py2many
+  is not installed.  It is excluded from the wheel (see `pyproject.toml`).
+
+## Why the predicates match the implementation, not the paper
+
+The original static-python spec was a paper-faithful idealization, but the
+live code differs in a few places.  To make the verified core the single
+source of truth *without changing consensus behavior*, the predicates were
+corrected to mirror the implementation:
+
+| Predicate | Live behavior it encodes |
+|---|---|
+| `may_grant_vote` | `cand_term > last_vote_term AND cand_index >= lastLogIndex` (stricter than the paper: an equal term never gets the vote) |
+| `promote_to_leader` | `num_votes > 1 AND num_votes > total/2` |
+| `clamp_commit` | `min(leader_commit, max(0, len(log)-1))` |
+| `log_matching_ok` | reject when `prev_log_index >= len(log)` or term mismatch; apply only when `prev < len AND term matches` |
+| `can_commit` | `entry_term == current_term AND new_commit_index > commitIndex` |
+
+## Verify
+
+From the `../py2many` checkout:
+
+```bash
+uv run python -m py2many --lean --outdir /tmp/core_lean raft/core.py
+../py2many/scripts/lean-runner.sh build /tmp/core_lean/core.lean   # exit 0 == proved
+```
+
+Run as Python (needs the raft deps; the vendored `py2many/` shim resolves the
+markers):
+
+```bash
+PYTHONPATH=. python -m raft.core
+pytest tests/ -q
+```
+
+### Notes / gotchas
+
+* `int` transpiles to `Nat`, so all quantified values are non-negative (the
+  only regime Raft terms/indexes live in).
+* `CHECKER.post` bodies that reference `result` become Lean subtypes
+  `{ r : T // post }` discharged by `by rfl`, so postconditions are written as
+  **definitional equalities**.  Boolean expressions are factored into
+  `may_grant_vote` / `promote_rule` / `log_matching_ok` / `commit_advance_rule`
+  so a post can reference a plain-Bool function call (a bare `x == y and ...`
+  would emit a Prop instead of a Bool and break the subtype).
+* The Lean backend cannot transpile a module-level docstring, so `raft/core.py`
+  intentionally has none (the explanation lives in this README).
diff --git a/py2many/__init__.py b/py2many/__init__.py
new file mode 100644
index 0000000..87c7564
--- /dev/null
+++ b/py2many/__init__.py
@@ -0,0 +1,15 @@
+"""Runtime marker shim for py2many's design-by-contract API.
+
+The static-python source files (``raft/core.py``) import the verification
+markers from ``py2many.spec`` / ``py2many.theorem`` / ``py2many.result``.
+py2many recognises these imports (and the ``CHECKER.pre`` / ``CHECKER.post`` /
+``CHECKER.invariant`` access) purely by name and drops the imports when it
+transpiles to Lean, so the *verified* Lean output never contains them.
+
+At Python runtime the markers must still resolve, because the ``if
+CHECKER.pre:`` blocks are dead-but-present code.  When the full py2many
+distribution is installed it provides these modules; this tiny vendored shim
+makes the raft package importable standalone with identical semantics (the
+markers evaluate to ``False`` / no-op decorators).  It shadows nothing that
+matters: it is a faithful subset of the real API.
+"""
diff --git a/py2many/result.py b/py2many/result.py
new file mode 100644
index 0000000..a94dab1
--- /dev/null
+++ b/py2many/result.py
@@ -0,0 +1,28 @@
+"""Runtime-only micro-shim of py2many.result (see the package docstring).
+
+Provides the ``Result[T, E]`` (Ok/Error) types used by ``raft/live.py`` for
+fallible operations instead of exceptions.
+"""
+
+from dataclasses import dataclass
+from enum import IntEnum
+from typing import Generic, TypeVar, Union
+
+T = TypeVar("T")
+E = TypeVar("E", Exception, IntEnum)
+
+
+@dataclass
+class Ok(Generic[T]):
+    value: T
+
+
+@dataclass
+class Error(Generic[E]):
+    error: E
+
+
+# std::result version
+StdResult = Union[Ok[T], Error[E]]
+# anyhow version
+Result = Ok[T]
diff --git a/py2many/spec.py b/py2many/spec.py
new file mode 100644
index 0000000..f9da739
--- /dev/null
+++ b/py2many/spec.py
@@ -0,0 +1,40 @@
+"""Runtime-only micro-shim of py2many.spec (see the package docstring).
+
+Pure Python mirror of the markers used by raft/core.py.  Kept in sync with
+py2many.spec: the sentinel attributes are always False, so the ``if
+CHECKER.*:`` blocks are dead at runtime.
+"""
+
+
+class _Checker:
+    pre = False
+    post = False
+    invariant = False
+
+
+CHECKER = _Checker()
+
+
+class _Result:
+    def __getattr__(self, name: str):
+        return None
+
+
+result = _Result()
+
+# Legacy flat exports (backward compatibility with py2many.smt).
+pre = CHECKER.pre
+post = CHECKER.post
+invariant = CHECKER.invariant
+
+
+def check(claim: bool):
+    assert claim
+
+
+def prove(fn):
+    import inspect
+    from itertools import product
+
+    n = len(inspect.signature(fn).parameters)
+    assert all(fn(*combo) for combo in product((True, False), repeat=n))
diff --git a/py2many/theorem.py b/py2many/theorem.py
new file mode 100644
index 0000000..5fd8949
--- /dev/null
+++ b/py2many/theorem.py
@@ -0,0 +1,19 @@
+"""Runtime-only micro-shim of py2many.theorem (see the package docstring).
+
+No-op decorator markers that py2many turns into ``theorem`` in Lean.
+"""
+
+
+def theorem(fn):
+    return fn
+
+
+def lemma(fn):
+    return fn
+
+
+def by(tactic: str):
+    def decorator(fn):
+        return fn
+
+    return decorator
diff --git a/pyproject.toml b/pyproject.toml
index 2a64ee3..58f0d9d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -28,6 +28,11 @@ dev = [
 [tool.isort]
 profile = "black"
 
+[tool.setuptools.packages.find]
+# The vendored py2many/ marker shim must not be installed as a top-level
+# package: it would shadow a real py2many installation.  Keep it source-only.
+exclude = ["py2many*", "static*", "static-python-skill*", "tests*", "docs*"]
+
 [build-system]
 requires = ["setuptools>=61.0", "wheel"]
 build-backend = "setuptools.build_meta"
diff --git a/raft/core.py b/raft/core.py
new file mode 100644
index 0000000..79b25ab
--- /dev/null
+++ b/raft/core.py
@@ -0,0 +1,302 @@
+from dataclasses import dataclass
+from typing import List
+
+from py2many.spec import CHECKER, result
+from py2many.theorem import by, lemma
+
+# ---------------------------------------------------------------------------
+# Durable replicated state with a class invariant (re-proved by omega at every
+# construction / mutation).
+# ---------------------------------------------------------------------------
+
+
+@dataclass
+class ConsensusState:
+    """The per-node consensus state that safety rests on.
+
+    Invariants (hold at every construction or mutation):
+      * the term, commit index and last log index are never negative;
+      * the commit index never exceeds the last log index -- a node can never
+        commit an entry it does not hold.
+    """
+
+    current_term: int
+    commit_index: int
+    last_log_index: int
+
+    if CHECKER.invariant:
+
+        def invariant(self):
+            return (
+                self.current_term >= 0
+                and self.commit_index >= 0
+                and self.last_log_index >= 0
+                and self.commit_index <= self.last_log_index
+            )
+
+    # Raft's forward-only commit rule: commitIndex is only ever moved forward
+    # and never past the log (Leader.set_server / on_response_received).
+    def advance_commit(self, new_commit: int) -> "ConsensusState":
+        if CHECKER.pre:
+            new_commit >= self.commit_index
+            new_commit <= self.last_log_index
+        self.commit_index = new_commit
+        if CHECKER.post:
+            result.commit_index == new_commit
+        return self
+
+    def inc_term(self) -> "ConsensusState":
+        """``Candidate._start_election``: ``currentTerm = 1 + currentTerm``."""
+        if CHECKER.pre:
+            self.current_term >= 0
+        self.current_term = self.current_term + 1
+        if CHECKER.post:
+            result.current_term == self.current_term + 1
+        return self
+
+
+# ---------------------------------------------------------------------------
+# Election restriction -- Voter.on_vote_request.
+# ---------------------------------------------------------------------------
+
+
+def may_grant_vote(
+    last_vote_term: int, last_log_index: int, cand_term: int, cand_index: int
+) -> bool:
+    """The live voter's check: the candidate's term is newer than the term we
+    last voted in AND its log is at least as long as ours.
+
+    (More restrictive than the paper's up-to-date rule: an equal term never
+    gets the vote, even with a longer log.)
+    """
+    if CHECKER.pre:
+        last_vote_term >= 0
+        last_log_index >= 0
+        cand_term >= 0
+        cand_index >= 0
+    return cand_term > last_vote_term and cand_index >= last_log_index
+
+
+def grant_vote(
+    last_vote_term: int, last_log_index: int, cand_term: int, cand_index: int
+) -> bool:
+    """The voter's decision in ``Voter.on_vote_request``."""
+    if CHECKER.pre:
+        last_vote_term >= 0
+        last_log_index >= 0
+        cand_term >= 0
+        cand_index >= 0
+    if CHECKER.post:
+        result == may_grant_vote(last_vote_term, last_log_index, cand_term, cand_index)
+    return may_grant_vote(last_vote_term, last_log_index, cand_term, cand_index)
+
+
+# ---------------------------------------------------------------------------
+# Strict majority / leader promotion -- Candidate.on_vote_received.
+# ---------------------------------------------------------------------------
+
+
+def is_strict_majority(num: int, total: int) -> bool:
+    """``num > total / 2`` expressed exactly over the integers."""
+    if CHECKER.pre:
+        num >= 0
+        total >= 0
+    return 2 * num > total
+
+
+def promote_rule(num_votes: int, total_nodes: int) -> bool:
+    if CHECKER.pre:
+        num_votes >= 0
+        total_nodes >= 0
+    return num_votes > 1 and is_strict_majority(num_votes, total_nodes)
+
+
+def promote_to_leader(num_votes: int, total_nodes: int) -> bool:
+    """``Candidate.on_vote_received``: promote to leader only on more than one
+    vote AND a strict majority of the cluster."""
+    if CHECKER.pre:
+        num_votes >= 0
+        total_nodes >= 0
+    if CHECKER.post:
+        result == promote_rule(num_votes, total_nodes)
+    return promote_rule(num_votes, total_nodes)
+
+
+# ---------------------------------------------------------------------------
+# Commit safety -- Follower._update_commit_index clamps the leader's commit
+# cursor to the follower's last log index.
+# ---------------------------------------------------------------------------
+
+
+def clamp_commit(leader_commit: int, log_len: int) -> int:
+    """The new commit index is the leader's commit index clamped to the last
+    index the follower actually holds."""
+    if CHECKER.pre:
+        leader_commit >= 0
+        log_len >= 0
+    if CHECKER.post:
+        result == min(leader_commit, max(0, log_len - 1))
+    return min(leader_commit, max(0, log_len - 1))
+
+
+# ---------------------------------------------------------------------------
+# Log Matching -- Follower.on_append_entries guard (the "induction proof" in
+# the code comments): entries are applied only where the follower already
+# agrees with the leader.
+# ---------------------------------------------------------------------------
+
+
+def log_matching_ok(
+    follower_log: List[int], prev_log_index: int, prev_log_term: int
+) -> bool:
+    """The follower may apply the leader's entries only when ``prev_log_index``
+    is inside its log AND its term at that index equals ``prev_log_term``.
+    Otherwise it is behind the leader or a term conflict exists."""
+    if CHECKER.pre:
+        prev_log_index >= 0
+    return prev_log_index < len(follower_log) and (
+        follower_log[prev_log_index] == prev_log_term
+    )
+
+
+def logs_match(
+    follower_log: List[int], prev_log_index: int, prev_log_term: int
+) -> bool:
+    if CHECKER.pre:
+        prev_log_index >= 0
+    if CHECKER.post:
+        result == log_matching_ok(follower_log, prev_log_index, prev_log_term)
+    return log_matching_ok(follower_log, prev_log_index, prev_log_term)
+
+
+# ---------------------------------------------------------------------------
+# Commit-advance rule -- Leader.on_response_received.
+# ---------------------------------------------------------------------------
+
+
+def commit_advance_rule(
+    new_commit_index: int, current_term: int, commit_term: int, commit_index: int
+) -> bool:
+    """Advance commitIndex only when the entry at ``new_commit_index`` carries
+    the leader's *current* term and the cursor moves strictly forward."""
+    if CHECKER.pre:
+        new_commit_index >= 0
+        current_term >= 0
+        commit_term >= 0
+        commit_index >= 0
+    return commit_term == current_term and new_commit_index > commit_index
+
+
+def can_commit(
+    new_commit_index: int, current_term: int, commit_term: int, commit_index: int
+) -> bool:
+    if CHECKER.pre:
+        new_commit_index >= 0
+        current_term >= 0
+        commit_term >= 0
+        commit_index >= 0
+    if CHECKER.post:
+        result == commit_advance_rule(
+            new_commit_index, current_term, commit_term, commit_index
+        )
+    return commit_advance_rule(
+        new_commit_index, current_term, commit_term, commit_index
+    )
+
+
+# ---------------------------------------------------------------------------
+# Lemmas -- the proof obligations discharged by omega / native_decide.
+# ---------------------------------------------------------------------------
+
+
+@lemma
+@by("omega")
+def quorums_overlap(a: int, b: int, total: int) -> bool:
+    """Any two strict majorities of a cluster must overlap, so Raft cannot
+    elect two leaders in the same term: if ``|Q1| > n/2`` and ``|Q2| > n/2``
+    then ``|Q1| + |Q2| > n``, forcing ``Q1 ∩ Q2 ≠ ∅``."""
+    if CHECKER.pre:
+        total >= 0
+        2 * a > total
+        2 * b > total
+    return a + b > total
+
+
+@lemma
+@by("native_decide")
+def reject_lower_term_candidate() -> bool:
+    """A candidate with a lower term is never granted a vote."""
+    return not grant_vote(3, 7, 2, 10)
+
+
+@lemma
+@by("native_decide")
+def grant_newer_term_with_log() -> bool:
+    """A candidate with a strictly newer term and a sufficient log is granted."""
+    return grant_vote(3, 7, 4, 9)
+
+
+@lemma
+@by("native_decide")
+def reject_equal_term_even_with_longer_log() -> bool:
+    """An equal term never gets the vote, even with a longer log (live rule)."""
+    return not grant_vote(3, 7, 3, 9)
+
+
+@lemma
+@by("native_decide")
+def majority_promotes() -> bool:
+    return promote_to_leader(3, 5)
+
+
+@lemma
+@by("native_decide")
+def single_vote_never_promotes() -> bool:
+    return not promote_to_leader(1, 5)
+
+
+@lemma
+@by("native_decide")
+def minority_never_promotes() -> bool:
+    return not promote_to_leader(2, 5)
+
+
+@lemma
+@by("native_decide")
+def matching_prev_accepted() -> bool:
+    """A matching prev index/term is accepted (prefix preserved)."""
+    return logs_match([1, 1, 2], 2, 2)
+
+
+@lemma
+@by("native_decide")
+def conflicting_term_rejected() -> bool:
+    """A term conflict at prev_log_index is rejected (the follower trims back)."""
+    return not logs_match([1, 1, 2], 2, 1)
+
+
+@lemma
+@by("native_decide")
+def beyond_log_rejected() -> bool:
+    """A prev_log_index past the follower's log is rejected (follower behind)."""
+    return not logs_match([1, 1, 2], 3, 2)
+
+
+@lemma
+@by("native_decide")
+def commit_requires_current_term() -> bool:
+    """A leader never commits an entry from a previous term."""
+    return not can_commit(3, 5, 4, 1)
+
+
+@lemma
+@by("native_decide")
+def commit_advances_only_forward() -> bool:
+    """Committing happens only when the cursor moves strictly forward."""
+    return can_commit(3, 5, 5, 1)
+
+
+if __name__ == "__main__":
+    initial = ConsensusState(1, 0, 3)
+    print("term:", initial.current_term)
+    print("grant newer term:", grant_vote(3, 7, 4, 9))
diff --git a/raft/live.py b/raft/live.py
new file mode 100644
index 0000000..7811d3d
--- /dev/null
+++ b/raft/live.py
@@ -0,0 +1,41 @@
+"""Runtime face of the verified core: ``Result[T, E]`` instead of exceptions.
+
+The pure decision predicates live in ``raft/core.py`` (transpiled to Lean and
+verified).  This module wraps the *fallible* operations -- most notably
+out-of-bounds log access, which the live code otherwise indexes directly and
+would raise ``IndexError`` on -- in ``Result[T, E]`` (``Ok`` / ``Error``) per
+the static-python rule.
+
+Lean emission for ``Ok`` / ``Error`` is a pending py2many change, so this file
+is intentionally evaluated only at runtime, never transpiled.  It is a thin
+wrapper over types from ``py2many.result`` (vendored shim or the real py2many).
+"""
+
+from typing import List
+
+from py2many.result import Error, Ok, StdResult
+
+
+class Err:
+    """Error codes for fallible raft-core operations (kept small & enum-like)."""
+
+    OUT_OF_BOUNDS = 0
+
+
+def log_get(log: List, i: int) -> StdResult[int, int]:
+    """Return ``log[i].term`` wrapped in ``Result``.
+
+    Falls over to ``Error(Err.OUT_OF_BOUNDS)`` when ``i`` is outside the log
+    instead of raising ``IndexError``, mirroring the defensive bounds check the
+    consensus code performs before indexing.
+    """
+    if i < 0 or i >= len(log):
+        return Error(Err.OUT_OF_BOUNDS)
+    return Ok(log[i].term)
+
+
+def ok_value(res: StdResult[int, int]):
+    """Unwrap an ``Ok`` to its value, ``None`` when it is an ``Error``."""
+    if isinstance(res, Ok):
+        return res.value
+    return None
diff --git a/raft/states/candidate.py b/raft/states/candidate.py
index 5254b3c..f93ac4a 100644
--- a/raft/states/candidate.py
+++ b/raft/states/candidate.py
@@ -1,6 +1,7 @@
 import asyncio
 import logging
 
+from ..core import promote_to_leader
 from ..messages.base import Term
 from ..messages.request_vote import RequestVoteMessage, RequestVoteResponseMessage
 from ..servers.server import Server
@@ -40,8 +41,9 @@ async def on_vote_received(self, message: RequestVoteResponseMessage):
             logger.debug(f"{num_votes} {total_nodes}\n{message}")
             # Guard for the case we're network partitioned from other nodes.
             # We shouldn't promote ourselves to a leader if the network comes
-            # back
-            if num_votes > 1 and num_votes > (total_nodes / 2):
+            # back.  Verified decision (raft.core.promote_to_leader): a strict
+            # majority AND more than one vote.
+            if promote_to_leader(num_votes, total_nodes):
                 self.timer.cancel()
                 leader = Leader()
                 leader.set_server(self._server)
diff --git a/raft/states/follower.py b/raft/states/follower.py
index 9fdb6d2..1c9c4ba 100644
--- a/raft/states/follower.py
+++ b/raft/states/follower.py
@@ -1,5 +1,6 @@
 import logging
 
+from ..core import clamp_commit, log_matching_ok
 from ..messages.append_entries import AppendEntriesMessage, Command
 from ..messages.base import Term
 from .config import FOLLOWER_TIMEOUT
@@ -15,10 +16,11 @@ def __init__(self, timeout=FOLLOWER_TIMEOUT):
 
     def _update_commit_index(self, message: AppendEntriesMessage) -> None:
         if message.leader_commit > self._server._commitIndex:
-            # If the leader is too far ahead then we
-            #   use the length of the log - 1
-            log = self._server._log
-            self._server._commitIndex = min(message.leader_commit, max(0, len(log) - 1))
+            # If the leader is too far ahead then we use the length of the
+            # log - 1.  Verified clamp (raft.core.clamp_commit).
+            self._server._commitIndex = clamp_commit(
+                message.leader_commit, len(self._server._log)
+            )
 
     async def on_append_entries(self, message: AppendEntriesMessage):
         await super().on_append_entries(message)
@@ -38,8 +40,13 @@ async def on_append_entries(self, message: AppendEntriesMessage):
 
         # We need to hold the induction proof of the algorithm here.
         #   So, we make sure that the prevLogIndex term is always
-        #   equal to the server.
-        if len(log) > 0 and log[message.prev_log_index].term != message.prev_log_term:
+        #   equal to the server.  The follower has already been checked to be
+        #   within the log (above), so the verified Log-Matching guard
+        #   (raft.core.log_matching_ok) reduces to: reject on a term conflict.
+        log_terms = [e.term for e in log]
+        if not log_matching_ok(
+            log_terms, message.prev_log_index, message.prev_log_term
+        ):
             # There is a conflict we need to resync so delete everything
             #   from this prevLogIndex and forward and send a failure
             #   to the server.
diff --git a/raft/states/leader.py b/raft/states/leader.py
index aa449ef..b3d3b5a 100644
--- a/raft/states/leader.py
+++ b/raft/states/leader.py
@@ -4,6 +4,8 @@
 from collections import defaultdict
 from typing import Optional
 
+from .. import live
+from ..core import can_commit
 from ..messages.append_entries import AppendEntriesMessage, Command
 from ..messages.base import Peer, Term
 from ..messages.response import ResponseMessage
@@ -130,10 +132,16 @@ async def on_response_received(
                     )
                     logger.debug(f"Learner: Advanced {message.sender} by {num_entries}")
                 new_commit_index = statistics.median_low(self._matchIndex.values())
-                if (
-                    self._server._log[new_commit_index].term
-                    == self._server._currentTerm
-                    and new_commit_index > self._server._commitIndex
+                commit_term = live.ok_value(
+                    live.log_get(self._server._log, new_commit_index)
+                )
+                # Verified decision (raft.core.can_commit): commit only entries
+                # from the leader's current term, moving strictly forward.
+                if commit_term is not None and can_commit(
+                    new_commit_index,
+                    int(self._server._currentTerm),
+                    commit_term,
+                    self._server._commitIndex,
                 ):
                     self._server._commitIndex = new_commit_index
                     async with self._server._condition:
diff --git a/raft/states/voter.py b/raft/states/voter.py
index 3474dbe..800d5d6 100644
--- a/raft/states/voter.py
+++ b/raft/states/voter.py
@@ -2,6 +2,7 @@
 import logging
 from typing import Tuple
 
+from ..core import may_grant_vote
 from ..messages.append_entries import AppendEntriesMessage
 from ..messages.base import Peer
 from ..messages.request_vote import RequestVoteMessage, RequestVoteResponseMessage
@@ -42,8 +43,13 @@ async def on_vote_request(self, message: RequestVoteMessage):
             await self._send_vote_response_message(message, yes=False)
 
         last_vote_term, voted_for = self.last_vote
-        eligible_to_vote = message.term > last_vote_term
-        if eligible_to_vote and message.last_log_index >= self._server._lastLogIndex:
+        # Verified decision (raft.core.may_grant_vote): match Voter.on_vote_request.
+        if may_grant_vote(
+            last_vote_term,
+            self._server._lastLogIndex,
+            message.term,
+            message.last_log_index,
+        ):
             self.last_vote = (message.term, message.sender)
             await self._send_vote_response_message(message)
         else: