+ )
+}
diff --git a/data/research.js b/data/research.js
index 468b89d..4f5c7e2 100644
--- a/data/research.js
+++ b/data/research.js
@@ -1,4 +1,14 @@
export const research = [
+ {
+ slug: 'kleros-sortition-tree',
+ title: 'Kleros Sortition Tree Conservation & Draw Invariants',
+ subtitle:
+ 'Formally verified stake conservation and fair juror selection for the Kleros dispute resolution protocol.',
+ description:
+ 'How we proved total stake conservation and draw fairness across the Kleros sortition tree using Verity and Lean 4.',
+ date: '2026-04-16',
+ tag: 'Case study'
+ },
{
slug: 'stream-recovery-claim',
title: 'StreamRecoveryClaim Accounting Invariants',
diff --git a/pages/research/index.jsx b/pages/research/index.jsx
index 87159e4..245ee58 100644
--- a/pages/research/index.jsx
+++ b/pages/research/index.jsx
@@ -15,7 +15,8 @@ const caseStudyOrder = [
'safe-owner-reachability',
'lido-vault-solvency',
'nexus-mutual-book-value',
- 'stream-recovery-claim'
+ 'stream-recovery-claim',
+ 'kleros-sortition-tree'
]
export default function ResearchPage() {
diff --git a/pages/research/kleros-sortition-tree.jsx b/pages/research/kleros-sortition-tree.jsx
new file mode 100644
index 0000000..fe6e8bf
--- /dev/null
+++ b/pages/research/kleros-sortition-tree.jsx
@@ -0,0 +1,505 @@
+import Head from 'next/head'
+import Link from 'next/link'
+import PageLayout from '../../components/PageLayout'
+import ResearchCard from '../../components/ResearchCard'
+import KlerosGuarantee from '../../components/research/KlerosGuarantee'
+import Disclosure from '../../components/research/Disclosure'
+import CodeBlock from '../../components/research/CodeBlock'
+import ExternalLink from '../../components/research/ExternalLink'
+import Hypothesis from '../../components/research/Hypothesis'
+import SortitionTreeDiagram from '../../components/research/SortitionTreeDiagram'
+import SortitionDrawExample from '../../components/research/SortitionDrawExample'
+import { getSortedResearch } from '../../lib/getSortedResearch'
+
+const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark
+cd verity-benchmark
+lake build Benchmark.Cases.Kleros.SortitionTrees.Compile`
+
+const UPSTREAM_CONTRACT =
+ 'https://github.com/kleros/kleros-v2/blob/75125dfa/contracts/src/libraries/SortitionTrees.sol'
+
+const VERITY_CONTRACT =
+ 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Contract.lean'
+
+const SPECS_URL =
+ 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Specs.lean'
+
+const PROOFS_URL =
+ 'https://github.com/lfglabs-dev/verity-benchmark/blob/main/Benchmark/Cases/Kleros/SortitionTrees/Proofs.lean'
+
+export default function KlerosSortitionTreePage() {
+ const otherResearch = getSortedResearch().filter(
+ (r) => r.slug !== 'kleros-sortition-tree'
+ )
+
+ return (
+ <>
+
+
+ Kleros Sortition Tree Conservation & Draw Invariants | Research | LFG
+ Labs
+
+
+
+
+
+
+
+
+
+ Kleros Sortition Tree Conservation & Draw Invariants
+
+
+
+ {/* The Guarantee */}
+
+
+
+ Kleros is a
+ decentralized dispute resolution protocol, an on-chain
+ court system. When two parties disagree (over an escrow payment, a
+ content moderation decision, an insurance claim), they submit the
+ dispute to Kleros. The protocol randomly selects a panel of jurors
+ from a pool of PNK token stakers, the jurors vote, and the
+ majority ruling is enforced on-chain.
+
+
+ For this to be fair, juror selection must be both random and
+ stake-weighted: a juror who staked twice as much PNK should be
+ twice as likely to be drawn. The{' '}
+
+ sortition tree
+ {' '}
+ is the data structure that makes this possible. It is a
+ sum-tree where each leaf holds one juror's staked weight, and
+ each internal node holds the sum of its children. The root always
+ equals the total staked amount.
+
+
+
+ To select a juror, the protocol picks a random number
+ (the “ticket”) between 0 and the root. Think of it
+ as a number line of length 800, split into segments, one per
+ juror, sized by their stake. The tree turns this lookup into a
+ three-step walk from root to leaf.
+
+
+ Example with{' '}
+ ticket = 200:
+
+
+
+ Root (800): left subtree = 350.
+ 200 < 350, so go left.
+
+
+ Node1 (350): left child = 150.
+ 200 ≥ 150, so subtract 150 and go right.
+ Remaining ticket = 50.
+
+
+ Node4 (200): left child (L2) = 100.
+ 50 < 100, so go left. The draw lands
+ on L2.
+
+
+
+
+ Any ticket from 150 to 249 follows the same path and lands on
+ L2. The ticket is drawn uniformly at random from 0 to 799,
+ so L2 owns 100 out of 800 possible values: its selection
+ probability is exactly 100/800. The same applies to every leaf.
+
+
+
+
+
+ {/* Why this matters */}
+
+
+ Why this matters
+
+
+ Kleros handles real arbitration with real money at stake. If a
+ propagation bug means the root does not reflect actual total
+ stake, draw intervals shift and some jurors are systematically
+ over- or under-selected. Every dispute resolved by a biased
+ jury is compromised.
+
+
+
+ In scope (12 proven theorems):
+
+
+
+ level2_parent_equals_sum_of_children: Each
+ grandparent-of-leaves node equals the sum of its two leaf
+ children (4 nodes verified)
+
+
+ level1_parent_equals_sum_of_children: Each
+ subtree-root node equals the sum of its two level-2 children (2
+ nodes verified)
+
+
+ root_equals_sum_of_leaves: Root = sum of all 8
+ leaf weights (total stake conservation)
+
+
+ root_minus_left_equals_right_subtree: Root
+ partitions cleanly into left and right subtrees
+
+
+ draw_selects_valid_leaf: Every draw lands on a
+ valid leaf index (7..14)
+
+
+ draw_interval_matches_weights: Draw intervals
+ match leaf weights across all 3 traversal levels (8-way
+ coverage)
+
+
+ node_id_bijection: Forward and reverse ID
+ mappings are consistent
+
+
+ sequential_setLeaf_root_conservation:
+ Conservation holds inductively after multiple operations
+
+
+
+
+ overflow_safety_of_no_wrap /{' '}
+ level1_overflow_safety_of_no_wrap: node sums
+ never exceed 2256 - 1 and wrap around
+ to zero, proven under explicit no-wrap assumptions
+
+
+ remove_leaf_zeroed /{' '}
+ remove_leaf_clears_associated_id: removing a
+ juror sets their leaf weight to zero and clears all associated
+ mappings
+
+
+
+ No ghost draws (not proven as a separate
+ theorem): we originally wanted to prove that a draw can never
+ select a juror whose stake is zero. When we tried to formalize
+ this as its own statement, a counterexample showed the naive
+ formulation was wrong. However, the guarantee still holds: it
+ follows directly from two theorems that are already proven. If
+ the root equals the sum of all leaves (
+
+ root_equals_sum_of_leaves
+
+ ) and each leaf's draw interval equals its weight (
+
+ draw_interval_matches_weights
+
+ ), then a leaf with weight 0 has an interval of size 0, so no
+ ticket can ever land on it.
+
+
+ Simplifications (the benchmark works on a
+ simplified version of the production contract):
+
+
+
+ The production tree supports a variable number of children per
+ node (K-ary). The benchmark fixes K=2 (binary tree) to isolate
+ the core logic.
+
+ Ticket generation uses keccak256 in production. The benchmark
+ treats the ticket as an opaque number, proving fairness for any
+ ticket value, not just hash-derived ones.
+
+
+
+ The benchmark specializes the production sortition tree to a
+ balanced binary tree with eight leaves (three levels). This
+ preserves the core algorithmic logic (parent-sum propagation and
+ weighted-interval draw traversal) while abstracting encoding and
+ randomness details that Verity does not yet support.
+
+
+
+
+ {/* How this was proven */}
+
+
+ How this was proven
+
+
+ We translated the Solidity{' '}
+
+ SortitionTrees.sol
+ {' '}
+ into{' '}
+ Verity, our
+ Lean 4 framework for writing smart contract logic as
+ mathematical definitions. Once the contract is expressed in Lean,
+ we can state properties about it and prove them.
+
+
+ Two kinds of properties were proven:
+
+
+
+ Conservation: after any{' '}
+ setLeaf call,
+ every parent still equals the sum of its children, all the way
+ up to the root. We proved this level by level (leaves →
+ mid-nodes → root), then composed those results to show
+ that the root always equals the sum of all 8 leaves.
+
+
+ Draw fairness: for any valid ticket, the draw
+ function lands on a real leaf, and each leaf's draw
+ interval matches its weight exactly. The proof considers each
+ of the 8 leaf positions separately, but within each position
+ it covers every possible combination of weights and ticket
+ values, not just specific examples. Eight universal proofs,
+ not eight test cases.
+
+
+
+ All proofs are checked by Lean 4's type-checking kernel.
+ This is not testing or simulation: if any proof step were wrong,
+ the code would not compile.
+
+
+ {VERIFY_COMMAND}
+
+ If the build succeeds, the proofs are correct.{' '}
+
+ Source repository
+
+
+
+
+
+ {/* Proof status */}
+
+
+ Proof status
+
+
+ All 12 theorems are proven.{' '}
+ Proofs.lean{' '}
+ contains no unfinished proofs.
+
+
+ The table below shows which properties have been proven for each
+ function. “Conservation” means the tree sums stay
+ correct. “Draw correctness” means the draw always
+ picks a valid leaf with the right probability.
+ “Composition” means the property still holds after
+ multiple operations in sequence.
+
+
+
+
+
+
+ Function
+
+
+ Conservation
+
+
+ Draw correctness
+
+
+ ID mapping
+
+
+ Composition
+
+
+
+
+
+
setLeaf
+
+ proven
+
+
+ –
+
+
+ proven
+
+
+ proven
+
+
+
+
draw
+
+ –
+
+
+ proven
+
+
+ –
+
+
+ –
+
+
+
+
removeLeaf
+
+ –
+
+
+ –
+
+
+ proven
+
+
+ –
+
+
+
+
+
+
+
+ {/* Assumptions */}
+
+
+ Assumptions
+
+
+ The proofs use zero axioms. Most hypotheses correspond directly
+ to Solidity{' '}
+ require statements
+ that revert the transaction if violated. The overflow and removal
+ proofs carry additional assumptions noted below.
+
+
+
+ The caller passes a valid leaf index. Enforced by{' '}
+ require guards in
+ the contract. Matches the Solidity implementation's bounds
+ check for the 8-leaf tree.
+
+
+ The tree is non-empty. Enforced by{' '}
+
+ require(root != 0)
+ {' '}
+ in the draw function. A draw on an empty tree would be
+ meaningless.
+
+
+ The ticket is within the valid range. Enforced by{' '}
+
+ require(ticket {'<'} root)
+ {' '}
+ in the draw function. Ensures the ticket falls within the total
+ stake interval.
+
+
+ The mathematical sum of leaf weights does not exceed
+ 2256 - 1. This assumption is only used by
+ the overflow safety theorems. The core conservation and draw
+ proofs do not depend on it.
+
+
+ The caller knows which juror ID was associated with the leaf
+ being removed. Used only by the removal cleanup proofs.
+
+