diff --git a/apps/simplex-badge-service/src/BadgeService/Ledger.hs b/apps/simplex-badge-service/src/BadgeService/Ledger.hs
new file mode 100644
index 0000000000..3838a6bccd
--- /dev/null
+++ b/apps/simplex-badge-service/src/BadgeService/Ledger.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE NamedFieldPuns #-}
+
+-- | Pure, database-free transitions over the badge ledger state (UX \"Transitions\"). Kept free
+-- of 'BadgeService.Store' so every boundary case can be exercised exhaustively by
+-- @Bots.BadgeLedgerTests@ without a database.
+--
+-- Calling convention: 'advance' is run before every 'credit', 'debitAll' and 'issue' call, by the
+-- caller, against the same timestamp; a 'Just' result is one @debit(lapse)@ row the caller writes
+-- before writing the row for the credit/debit/issue that follows.
+module BadgeService.Ledger
+  ( LedgerState (..),
+    advance,
+    credit,
+    debitAll,
+    issue,
+    initialLedgerState,
+  )
+where
+
+import Data.Time.Clock (UTCTime)
+import Simplex.Chat.Badges (BadgeType)
+import Simplex.Chat.Badges.Months (addMonths, fullMonthsBetween)
+import Simplex.Chat.Badges.Service (StatementCreditType, StatementDebitType)
+
+data LedgerState = LedgerState
+  { balanceMonths :: Int,
+    balanceStartTs :: UTCTime,
+    balanceBadgeType :: BadgeType
+  }
+  deriving (Eq, Show)
+
+-- | One @debit(lapse)@ transition for the fully elapsed, unissued months since 'balanceStartTs'.
+-- @k = min balanceMonths (fullMonthsBetween balanceStartTs t)@: capped at the balance so a long
+-- absence on a small or zero balance can never lapse more months than are actually owed. Returns
+-- 'Nothing' (state unchanged) when @k@ would be 0 — never 'Just (0, _)'.
+advance :: UTCTime -> LedgerState -> Maybe (Int, LedgerState)
+advance t st@LedgerState {balanceMonths, balanceStartTs}
+  | k <= 0 = Nothing
+  | otherwise = Just (k, st {balanceMonths = balanceMonths - k, balanceStartTs = addMonths k balanceStartTs})
+  where
+    k = min balanceMonths (fullMonthsBetween balanceStartTs t)
+
+-- | @grant(src) +n@: a zero balance restarts the coverage window at @max balanceStartTs t@ (the
+-- settlement time, or the old start if that's already later); a positive balance just grows,
+-- since the months are fungible and already counted from the existing start.
+credit :: UTCTime -> Int -> StatementCreditType -> LedgerState -> LedgerState
+credit t n _creditType st@LedgerState {balanceMonths, balanceStartTs}
+  | balanceMonths == 0 = st {balanceMonths = n, balanceStartTs = max balanceStartTs t}
+  | otherwise = st {balanceMonths = balanceMonths + n}
+
+-- | @debit(reason)@: zeroes the balance without moving 'balanceStartTs' (refund, upgrade
+-- conversion, transfer-out, correction — the caller identifies which via 'StatementDebitType').
+debitAll :: StatementDebitType -> LedgerState -> LedgerState
+debitAll _reason st = st {balanceMonths = 0}
+
+-- | @consume@: issues a credential for @[balanceStartTs, addMonths 1 balanceStartTs)@, debiting
+-- one month. 'Nothing' when @balanceMonths == 0@ (nothing to issue) or when the current month is
+-- already issued (@balanceStartTs > t@ — 'balanceStartTs' only reaches the next period's start
+-- once this one has been consumed); the caller tells the two apart by the balance.
+issue :: UTCTime -> LedgerState -> Maybe (LedgerState, UTCTime, UTCTime)
+issue t st@LedgerState {balanceMonths, balanceStartTs}
+  | balanceMonths == 0 = Nothing
+  | balanceStartTs > t = Nothing
+  | otherwise = Just (st {balanceMonths = balanceMonths - 1, balanceStartTs = periodEnd}, periodStart, periodEnd)
+  where
+    periodStart = balanceStartTs
+    periodEnd = addMonths 1 periodStart
+
+-- | The state of a purchase with no ledger entry yet: zero balance, 'balanceStartTs' the given
+-- time. A purchase created in the same transaction has no prior row to read, so this is where its
+-- first 'credit' starts from.
+initialLedgerState :: UTCTime -> BadgeType -> LedgerState
+initialLedgerState t badgeType = LedgerState {balanceMonths = 0, balanceStartTs = t, balanceBadgeType = badgeType}
diff --git a/plans/2026-08-21-badges-web-checkout.md b/plans/2026-08-21-badges-web-checkout.md
index ee245fb32c..5dd249bac0 100644
--- a/plans/2026-08-21-badges-web-checkout.md
+++ b/plans/2026-08-21-badges-web-checkout.md
@@ -134,7 +134,7 @@ The two `-m` filters are needed because the badge tests live under two hspec pat
 | A5 | Cabal dependencies for the service | — | ☑ |
 | A6 | `badge_service.ini`: configuration file | A3, A4, A5 | ☑ |
 | B1 | Store layer: purchases, ledger, issuances, codes, catalog | A2, A3, A4, A5 | ☑ |
-| B2 | `Ledger.hs`: pure transitions and property tests | A5 | ☐ |
+| B2 | `Ledger.hs`: pure transitions and property tests | A5 | ☑ |
 | B3 | `Codes.hs`: derive, encode, hash, classify | A5, A6, B1 | ☐ |
 | B4 | Issuer key loading and credential signing | A5, A6, B2 | ☐ |
 | B5 | RPC dispatcher: envelope, version, signer, throttle | A2, A6, B1 | ☐ |
diff --git a/simplex-chat.cabal b/simplex-chat.cabal
index 8a01eef3a2..9181c6dd1c 100644
--- a/simplex-chat.cabal
+++ b/simplex-chat.cabal
@@ -40,6 +40,7 @@ library
       Simplex.Chat.AppSettings
       Simplex.Chat.Badges
       Simplex.Chat.Badges.CLI
+      Simplex.Chat.Badges.Months
       Simplex.Chat.Badges.Service
       Simplex.Chat.Badges.Types
       Simplex.Chat.Names
@@ -418,6 +419,7 @@ executable simplex-badge-service
   other-modules:
       BadgeService.Catalog
       BadgeService.Config
+      BadgeService.Ledger
       BadgeService.Options
       BadgeService.Service
       BadgeService.Store
@@ -698,10 +700,12 @@ test-suite simplex-chat-test
       API.TypeInfo
       BadgeService.Catalog
       BadgeService.Config
+      BadgeService.Ledger
       BadgeService.Options
       BadgeService.Service
       BadgeService.Store
       BadgeService.Store.Migrate
+      Bots.BadgeLedgerTests
       Bots.BadgeServiceTests
       Broadcast.Bot
       Broadcast.Options
diff --git a/src/Simplex/Chat/Badges/Months.hs b/src/Simplex/Chat/Badges/Months.hs
new file mode 100644
index 0000000000..bae1ce7a2b
--- /dev/null
+++ b/src/Simplex/Chat/Badges/Months.hs
@@ -0,0 +1,43 @@
+-- | Calendar-month arithmetic shared by the badge ledger (BadgeService.Ledger) and the client,
+-- which needs 'addMonths' to render a badge's paid-through date. The clamping rule lives here
+-- once so the two sides can't drift into different roundings of "31 January plus one month".
+module Simplex.Chat.Badges.Months
+  ( addMonths,
+    fullMonthsBetween,
+    sundayAfter,
+  )
+where
+
+import Data.Time.Calendar (addDays, addGregorianMonthsClip, toGregorian)
+import Data.Time.Calendar.WeekDate (toWeekDate)
+import Data.Time.Clock (UTCTime (..), secondsToDiffTime)
+
+-- | Add @n@ months to a time, clamping the day to the last valid day of the target month (31
+-- January plus one month is 28 or 29 February) and preserving the time of day.
+addMonths :: Int -> UTCTime -> UTCTime
+addMonths n (UTCTime day tod) = UTCTime (addGregorianMonthsClip (fromIntegral n) day) tod
+
+-- | The largest @m >= 0@ with @addMonths m start <= t@. Returns 0 when @t < start@.
+--
+-- 'addMonths' is monotonic and moves to a new calendar month on every step, so the plain
+-- year/month difference between @start@ and @t@ is never more than one month away from the
+-- answer; at most one correction step is needed either way.
+fullMonthsBetween :: UTCTime -> UTCTime -> Int
+fullMonthsBetween start t
+  | t < start = 0
+  | addMonths (approx + 1) start <= t = approx + 1
+  | addMonths approx start > t = approx - 1
+  | otherwise = approx
+  where
+    (sy, sm, _) = toGregorian (utctDay start)
+    (ty, tm, _) = toGregorian (utctDay t)
+    approx = fromInteger (ty - sy) * 12 + (tm - sm)
+
+-- | 23:59:59 UTC of the next Sunday strictly after @t@. A @t@ that already falls on a Sunday
+-- yields the following Sunday (7 days later), never the same day.
+sundayAfter :: UTCTime -> UTCTime
+sundayAfter (UTCTime day _) = UTCTime (addDays daysToSunday day) endOfDay
+  where
+    (_, _, dow) = toWeekDate day -- 1 = Monday .. 7 = Sunday
+    daysToSunday = if dow == 7 then 7 else toInteger (7 - dow)
+    endOfDay = secondsToDiffTime (23 * 3600 + 59 * 60 + 59)
diff --git a/tests/Bots/BadgeLedgerTests.hs b/tests/Bots/BadgeLedgerTests.hs
new file mode 100644
index 0000000000..a8c84400bf
--- /dev/null
+++ b/tests/Bots/BadgeLedgerTests.hs
@@ -0,0 +1,265 @@
+{-# LANGUAGE LambdaCase #-}
+
+-- | Property tests for the pure, database-free badge ledger transitions (BadgeService.Ledger).
+-- Registered under the "Supporter badges" hspec path (not "SimpleX Badge service bot"): these
+-- tests need no database and must run in CI.
+module Bots.BadgeLedgerTests (badgeLedgerTests) where
+
+import BadgeService.Ledger
+import Data.List (foldl')
+import Data.Time.Calendar (addDays, fromGregorian)
+import Data.Time.Calendar.WeekDate (toWeekDate)
+import Data.Time.Clock (DiffTime, UTCTime (..), addUTCTime, nominalDay, secondsToDiffTime)
+import Simplex.Chat.Badges (BadgeType (..))
+import Simplex.Chat.Badges.Months (addMonths, fullMonthsBetween, sundayAfter)
+import Simplex.Chat.Badges.Service (StatementCreditType (..), StatementDebitType (..))
+import Test.Hspec
+import Test.Hspec.QuickCheck (modifyMaxSuccess, prop)
+import Test.QuickCheck (Gen, Property, chooseInt, discard, elements, forAll, oneof, property, vectorOf)
+
+badgeLedgerTests :: Spec
+badgeLedgerTests = modifyMaxSuccess (const 500) $ do
+  describe "addMonths clamping" $ do
+    it "clamps 31 January to 28 February in a non-leap year, preserving time of day" $
+      addMonths 1 (UTCTime (fromGregorian 2025 1 31) noon) `shouldBe` UTCTime (fromGregorian 2025 2 28) noon
+    it "clamps 31 January to 29 February in a leap year, preserving time of day" $
+      addMonths 1 (UTCTime (fromGregorian 2028 1 31) noon) `shouldBe` UTCTime (fromGregorian 2028 2 29) noon
+  prop "sundayAfter a time already on a Sunday returns the following Sunday at 23:59:59 UTC (property 7)" prop_sundayAfterSunday
+  prop "every recorded row matches the transition applied to its predecessor (property 1)" prop_rowsMatchTransitions
+  prop "balance stays non-negative, changeMonths sums to it, start is non-decreasing (property 2)" prop_invariants
+  prop "issue always debits exactly one month for exactly one period (property 3)" prop_issueDebitsOneMonth
+  prop "re-running issue inside an already-issued period appends nothing (property 4)" prop_issueIdempotentWithinPeriod
+  prop "advance lapses only fully elapsed, unissued months (property 5)" prop_advanceOnlyFullyElapsed
+  it "reproduces the worked example: buy 3 months, app off a month, reissue (property 6)" testWorkedExample
+
+noon :: DiffTime
+noon = secondsToDiffTime (12 * 3600)
+
+endOfDay :: DiffTime
+endOfDay = secondsToDiffTime (23 * 3600 + 59 * 60 + 59)
+
+-- Generators
+
+genBadgeType :: Gen BadgeType
+genBadgeType = elements [BTSupporter, BTLegend, BTInvestor]
+
+genCreditType :: Gen StatementCreditType
+genCreditType = elements [SCSupport, SCOpening]
+
+genDebitType :: Gen StatementDebitType
+genDebitType = elements [SDRefund, SDBadge, SDLapse, SDSupport]
+
+genTime :: Gen UTCTime
+genTime = do
+  dayOffset <- chooseInt (0, 3000)
+  secOfDay <- chooseInt (0, 86399)
+  pure $ UTCTime (addDays (toInteger dayOffset) (fromGregorian 2020 1 1)) (secondsToDiffTime (toInteger secOfDay))
+
+genLedgerState :: Gen LedgerState
+genLedgerState = do
+  months <- chooseInt (0, 36)
+  start <- genTime
+  badgeType <- genBadgeType
+  pure LedgerState {balanceMonths = months, balanceStartTs = start, balanceBadgeType = badgeType}
+
+-- | A state paired with a time offset from that state's own start (positive or negative), so a
+-- decent fraction of generated pairs land in every interesting region: before the start, inside
+-- the current period, and many months past it.
+genStateAndTime :: Gen (LedgerState, UTCTime)
+genStateAndTime = do
+  st <- genLedgerState
+  offsetDays <- chooseInt (-60, 400)
+  let t = addUTCTime (fromIntegral offsetDays * nominalDay) (balanceStartTs st)
+  pure (st, t)
+
+data Cmd = CmdCredit Int StatementCreditType | CmdDebit StatementDebitType | CmdIssue
+  deriving (Show)
+
+genCmd :: Gen Cmd
+genCmd =
+  oneof
+    [ CmdCredit <$> chooseInt (1, 24) <*> genCreditType,
+      CmdDebit <$> genDebitType,
+      pure CmdIssue
+    ]
+
+-- | A genesis time, badge type and a bounded, time-ordered sequence of commands with random
+-- non-negative day gaps between them (0 days apart is allowed, so consecutive same-instant calls
+-- are exercised too).
+genRun :: Gen (UTCTime, BadgeType, [(UTCTime, Cmd)])
+genRun = do
+  t0 <- genTime
+  badgeType <- genBadgeType
+  n <- chooseInt (0, 15)
+  deltasAndCmds <- vectorOf n ((,) <$> chooseInt (0, 400) <*> genCmd)
+  let times = drop 1 $ scanl (\t d -> addUTCTime (fromIntegral d * nominalDay) t) t0 (map fst deltasAndCmds)
+  pure (t0, badgeType, zip times (map snd deltasAndCmds))
+
+-- History replay
+
+data EntryKind = EKLapse Int | EKCredit Int | EKDebit Int | EKConsume
+
+-- | kind, time of the call, state before, state after.
+data Row = Row EntryKind UTCTime LedgerState LedgerState
+
+rowKind :: Row -> EntryKind
+rowKind (Row k _ _ _) = k
+
+rowNext :: Row -> LedgerState
+rowNext (Row _ _ _ next) = next
+
+-- | advance-then-command, exactly the calling convention documented for the ledger: advance runs
+-- before every credit, debit and issue.
+applyStep :: UTCTime -> Cmd -> LedgerState -> (LedgerState, [Row])
+applyStep t cmd st0 =
+  let (st1, lapseRows) = case advance t st0 of
+        Nothing -> (st0, [])
+        Just (k, st1') -> (st1', [Row (EKLapse k) t st0 st1'])
+   in case cmd of
+        CmdCredit n ct ->
+          let st2 = credit t n ct st1 in (st2, lapseRows <> [Row (EKCredit n) t st1 st2])
+        CmdDebit reason ->
+          let n = balanceMonths st1
+              st2 = debitAll reason st1
+           in (st2, lapseRows <> [Row (EKDebit n) t st1 st2])
+        CmdIssue -> case issue t st1 of
+          Nothing -> (st1, lapseRows)
+          Just (st2, _periodStart, _periodEnd) -> (st2, lapseRows <> [Row EKConsume t st1 st2])
+
+runFromGenesis :: UTCTime -> BadgeType -> [(UTCTime, Cmd)] -> (LedgerState, [Row])
+runFromGenesis t0 badgeType = foldl' go (initialLedgerState t0 badgeType, [])
+  where
+    go (st, rows) (t, cmd) = let (st', rs) = applyStep t cmd st in (st', rows <> rs)
+
+-- | Re-derives each row's next state from its predecessor using the UX "Transitions" formulas
+-- directly (not by re-invoking advance/credit/debitAll/issue), so a bug in those functions'
+-- arithmetic shows up as a mismatch here.
+verifyRow :: Row -> Bool
+verifyRow (Row kind t prev next) = case kind of
+  EKLapse k ->
+    balanceMonths next == balanceMonths prev - k
+      && balanceStartTs next == addMonths k (balanceStartTs prev)
+      && balanceBadgeType next == balanceBadgeType prev
+  EKCredit n ->
+    balanceMonths next == balanceMonths prev + n
+      && balanceBadgeType next == balanceBadgeType prev
+      && balanceStartTs next == (if balanceMonths prev == 0 then max (balanceStartTs prev) t else balanceStartTs prev)
+  EKDebit n ->
+    balanceMonths prev == n
+      && balanceMonths next == 0
+      && balanceStartTs next == balanceStartTs prev
+      && balanceBadgeType next == balanceBadgeType prev
+  EKConsume ->
+    balanceMonths next == balanceMonths prev - 1
+      && balanceStartTs next == addMonths 1 (balanceStartTs prev)
+      && balanceBadgeType next == balanceBadgeType prev
+
+changeMonthsOf :: EntryKind -> Int
+changeMonthsOf = \case
+  EKLapse k -> negate k
+  EKCredit n -> n
+  EKDebit n -> negate n
+  EKConsume -> -1
+
+isNonDecreasing :: Ord a => [a] -> Bool
+isNonDecreasing xs = and (zipWith (<=) xs (drop 1 xs))
+
+-- Properties
+
+prop_rowsMatchTransitions :: Property
+prop_rowsMatchTransitions = forAll genRun $ \(t0, badgeType, steps) ->
+  let (_, rows) = runFromGenesis t0 badgeType steps in property (all verifyRow rows)
+
+prop_invariants :: Property
+prop_invariants = forAll genRun $ \(t0, badgeType, steps) ->
+  let (finalSt, rows) = runFromGenesis t0 badgeType steps
+      allStates = initialLedgerState t0 badgeType : map rowNext rows
+      totalChange = sum (map (changeMonthsOf . rowKind) rows)
+   in property $
+        all ((>= 0) . balanceMonths) allStates
+          && totalChange == balanceMonths finalSt
+          && isNonDecreasing (map balanceStartTs allStates)
+
+prop_issueDebitsOneMonth :: Property
+prop_issueDebitsOneMonth = forAll genStateAndTime $ \(st, t) -> case issue t st of
+  Nothing -> discard
+  Just (st', periodStart, periodEnd) ->
+    property $
+      balanceMonths st' == balanceMonths st - 1
+        && periodStart == balanceStartTs st
+        && periodEnd == addMonths 1 periodStart
+        && balanceStartTs st' == periodEnd
+        && balanceBadgeType st' == balanceBadgeType st
+
+prop_issueIdempotentWithinPeriod :: Property
+prop_issueIdempotentWithinPeriod = forAll genStateAndTime $ \(st, t) ->
+  let st1 = maybe st snd (advance t st)
+   in case issue t st1 of
+        Nothing -> discard
+        Just (st2, _, _) ->
+          let st3 = maybe st2 snd (advance t st2)
+           in property (issue t st3 == Nothing)
+
+prop_advanceOnlyFullyElapsed :: Property
+prop_advanceOnlyFullyElapsed = forAll genStateAndTime $ \(st, t) -> case advance t st of
+  Nothing -> property (fullMonthsBetween (balanceStartTs st) t == 0 || balanceMonths st == 0)
+  Just (k, st') ->
+    property $
+      k > 0
+        && k <= balanceMonths st
+        && addMonths k (balanceStartTs st) <= t
+        && (k == balanceMonths st || addMonths (k + 1) (balanceStartTs st) > t)
+        && balanceStartTs st' == addMonths k (balanceStartTs st)
+        && balanceMonths st' == balanceMonths st - k
+
+genSunday :: Gen UTCTime
+genSunday = do
+  anyTime <- genTime
+  secOfDay <- chooseInt (0, 86399)
+  let day = utctDay anyTime
+      (_, _, dow) = toWeekDate day
+      toSunday = if dow == 7 then 0 else toInteger (7 - dow)
+  pure $ UTCTime (addDays toSunday day) (secondsToDiffTime (toInteger secOfDay))
+
+prop_sundayAfterSunday :: Property
+prop_sundayAfterSunday = forAll genSunday $ \sunday ->
+  let next = sundayAfter sunday
+   in property (utctDay next == addDays 7 (utctDay sunday) && utctDayTime next == endOfDay)
+
+-- Property 6 (worked example, UX §3): buy 3 months Tue Mar 10, 2026; issue right away; app off
+-- Apr 5 - May 20; advance and reissue May 20. Reproduces the doc's four rows verbatim.
+testWorkedExample :: IO ()
+testWorkedExample = do
+  let marTen = UTCTime (fromGregorian 2026 3 10) noon
+      aprTen = addMonths 1 marTen
+      mayTen = addMonths 2 marTen
+      junTen = addMonths 3 marTen
+      mayTwenty = UTCTime (fromGregorian 2026 5 20) noon
+      st0 = initialLedgerState marTen BTSupporter
+  -- row 1: grant(payment) +3, months=3, start=Mar10; paidThrough = Jun10
+  let st1 = credit marTen 3 SCSupport st0
+  balanceMonths st1 `shouldBe` 3
+  balanceStartTs st1 `shouldBe` marTen
+  addMonths (balanceMonths st1) (balanceStartTs st1) `shouldBe` junTen
+  -- no lapse yet: the first month hasn't elapsed
+  advance marTen st1 `shouldBe` Nothing
+  -- row 2: consume -1, 2, Apr10; issuance Mar10-Apr10, expiry Sun Apr 12
+  Just (st2, periodStart2, periodEnd2) <- pure (issue marTen st1)
+  balanceMonths st2 `shouldBe` 2
+  balanceStartTs st2 `shouldBe` aprTen
+  periodStart2 `shouldBe` marTen
+  periodEnd2 `shouldBe` aprTen
+  sundayAfter periodEnd2 `shouldBe` UTCTime (fromGregorian 2026 4 12) endOfDay
+  -- app off Apr5-May20: on the next contact (May20), advance lapses the one fully elapsed,
+  -- unissued month (Apr10-May10)
+  Just (lapsedMonths, st3) <- pure (advance mayTwenty st2)
+  lapsedMonths `shouldBe` 1
+  balanceMonths st3 `shouldBe` 1
+  balanceStartTs st3 `shouldBe` mayTen
+  -- row 4: consume -1, 0, Jun10; issuance May10-Jun10, expiry Sun Jun 14
+  Just (st4, periodStart4, periodEnd4) <- pure (issue mayTwenty st3)
+  balanceMonths st4 `shouldBe` 0
+  balanceStartTs st4 `shouldBe` junTen
+  periodStart4 `shouldBe` mayTen
+  periodEnd4 `shouldBe` junTen
+  sundayAfter periodEnd4 `shouldBe` UTCTime (fromGregorian 2026 6 14) endOfDay
diff --git a/tests/Test.hs b/tests/Test.hs
index 6d0e299273..1251d76ee4 100644
--- a/tests/Test.hs
+++ b/tests/Test.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE TupleSections #-}
 
+import Bots.BadgeLedgerTests
 import Bots.BadgeServiceTests
 import Bots.BroadcastTests
 import Bots.DirectoryTests
@@ -64,6 +65,7 @@ main = do
       around tmpBracket $ describe "WebRTC encryption" webRTCTests
 #endif
       describe "Supporter badges" badgeTests
+      describe "Supporter badges" badgeLedgerTests
       describe "SimpleX chat markdown" markdownTests
       describe "JSON Tests" jsonTests
       describe "Member relations" memberRelationsTests