367 lines
147 KiB
HTML
367 lines
147 KiB
HTML
<!DOCTYPE html><html lang="en" data-astro-cid-37fxchfa=""><head><meta charset="utf-8"><meta name="viewport" content="width=device-width,initial-scale=1"><title>Finding bugs in Raft implementations | Antithesis</title><script>
|
||
// Pre-paint: set data-theme, data-theme-preference, and the
|
||
// `dark` class on <html> before any content renders so the
|
||
// first frame uses the correct palette. Must be the very
|
||
// first child of <head> to beat CSS parsing.
|
||
//
|
||
// Storage key is shared with astro-theme-toggle (used in
|
||
// astrobook): `theme-toggle`, values "light" | "dark", absent
|
||
// means "follow system". data-theme-preference is our extra
|
||
// attribute that distinguishes explicit-light/dark from system
|
||
// — it's recomputed from storage, never persisted directly.
|
||
//
|
||
// We also set classList.toggle('dark') so the page lands in the
|
||
// exact DOM shape astro-theme-toggle expects; when its IIFE
|
||
// runs later in astrobook, it sees the DOM already aligned and
|
||
// produces no flicker.
|
||
(function () {
|
||
const KEY = "theme-toggle";
|
||
let stored = null;
|
||
try {
|
||
const v = localStorage.getItem(KEY);
|
||
if (v === "light" || v === "dark") stored = v;
|
||
} catch {
|
||
/* localStorage blocked */
|
||
}
|
||
let prefers_dark = false;
|
||
try {
|
||
prefers_dark = window.matchMedia(
|
||
"(prefers-color-scheme: dark)",
|
||
).matches;
|
||
} catch {
|
||
/* matchMedia unavailable — assume light */
|
||
}
|
||
const preference = stored || "system";
|
||
const applied = stored || (prefers_dark ? "dark" : "light");
|
||
const root = document.documentElement;
|
||
root.dataset.theme = applied;
|
||
root.dataset.themePreference = preference;
|
||
root.classList.toggle("dark", applied === "dark");
|
||
})();
|
||
</script><script type="module">(function(e,n,r,t,m){e[t]=e[t]||[],e[t].push({"gtm.start":new Date().getTime(),event:"gtm.js"});var g=n.getElementsByTagName(r)[0],a=n.createElement(r),s="";a.async=!0,a.src="https://www.googletagmanager.com/gtm.js?id="+m+s,g.parentNode.insertBefore(a,g)})(window,document,"script","dataLayer","GTM-W9GNSJM");</script><script>
|
||
// Pre-paint: hide announcement banners the user has already dismissed.
|
||
// Reads localStorage and injects a <style> rule keyed on data-banner-key
|
||
// before the body paints, so dismissed banners never flash visible.
|
||
(function () {
|
||
try {
|
||
const prefix = "antithesis:banner:";
|
||
const dismissed = [];
|
||
for (let i = 0; i < localStorage.length; i++) {
|
||
const k = localStorage.key(i);
|
||
if (
|
||
k &&
|
||
k.indexOf(prefix) === 0 &&
|
||
localStorage.getItem(k) === "1"
|
||
) {
|
||
dismissed.push(k.slice(prefix.length));
|
||
}
|
||
}
|
||
if (dismissed.length) {
|
||
const css = dismissed
|
||
.map(function (key) {
|
||
return (
|
||
'[data-banner-key="' +
|
||
CSS.escape(key) +
|
||
'"]{display:none!important;}'
|
||
);
|
||
})
|
||
.join("");
|
||
const style = document.createElement("style");
|
||
style.textContent = css;
|
||
document.head.appendChild(style);
|
||
}
|
||
} catch {
|
||
/* private mode / disabled storage — fall through */
|
||
}
|
||
})();
|
||
</script><style>@font-face{font-family:Stringer-c6f30cf7e392bd91;src:url("/_astro/fonts/b4329cf3d24405e5.woff2") format("woff2");font-display:swap;font-weight:100;font-style:normal;}@font-face{font-family:Stringer-c6f30cf7e392bd91;src:url("/_astro/fonts/19c6ea19dae76a22.woff2") format("woff2");font-display:swap;font-weight:300;font-style:normal;}@font-face{font-family:Stringer-c6f30cf7e392bd91;src:url("/_astro/fonts/71fc045da6bf1b36.woff2") format("woff2");font-display:swap;font-weight:400;font-style:normal;}@font-face{font-family:"Stringer-c6f30cf7e392bd91 fallback: Times New Roman";src:local("Times New Roman");font-display:swap;font-weight:100;font-style:normal;size-adjust:120.6154%;ascent-override:77.9337%;descent-override:21.5561%;line-gap-override:0%;}@font-face{font-family:"Stringer-c6f30cf7e392bd91 fallback: Times New Roman";src:local("Times New Roman");font-display:swap;font-weight:300;font-style:normal;size-adjust:120.6154%;ascent-override:77.9337%;descent-override:21.5561%;line-gap-override:0%;}@font-face{font-family:"Stringer-c6f30cf7e392bd91 fallback: Times New Roman";src:local("Times New Roman");font-display:swap;font-weight:400;font-style:normal;size-adjust:120.6154%;ascent-override:77.9337%;descent-override:21.5561%;line-gap-override:0%;}:root{--font-heading:Stringer-c6f30cf7e392bd91,"Stringer-c6f30cf7e392bd91 fallback: Times New Roman",Georgia,serif;}</style><style>@font-face{font-family:Onsite-310d0c5e24848452;src:url("/_astro/fonts/da09e39c103c809d.woff2") format("woff2");font-display:swap;font-weight:100 900;font-style:normal;}@font-face{font-family:Onsite-310d0c5e24848452;src:url("/_astro/fonts/618f3c433d6f5aa7.woff2") format("woff2");font-display:swap;font-weight:100 900;font-style:italic;}@font-face{font-family:"Onsite-310d0c5e24848452 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:normal;size-adjust:101.6149%;ascent-override:94.4743%;descent-override:19.6822%;line-gap-override:0%;}@font-face{font-family:"Onsite-310d0c5e24848452 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:italic;size-adjust:101.6149%;ascent-override:94.4743%;descent-override:19.6822%;line-gap-override:0%;}:root{--font-body:Onsite-310d0c5e24848452,"Onsite-310d0c5e24848452 fallback: Arial",system-ui,sans-serif;}</style><style>@font-face{font-family:"AT Textual-0ceab804b3a68a51";src:url("/_astro/fonts/fef5e52a89fda1b5.ttf") format("truetype");font-display:swap;font-weight:100 900;font-style:normal;}@font-face{font-family:"AT Textual-0ceab804b3a68a51";src:url("/_astro/fonts/d64cd15e5fa4dae1.ttf") format("truetype");font-display:swap;font-weight:100 900;font-style:italic;}@font-face{font-family:"AT Textual-0ceab804b3a68a51 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:normal;size-adjust:117.0927%;ascent-override:81.1323%;descent-override:17.0805%;line-gap-override:0%;}@font-face{font-family:"AT Textual-0ceab804b3a68a51 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:italic;size-adjust:117.0927%;ascent-override:81.1323%;descent-override:17.0805%;line-gap-override:0%;}:root{--font-eyebrow:"AT Textual-0ceab804b3a68a51","AT Textual-0ceab804b3a68a51 fallback: Arial",system-ui,sans-serif;}</style><style>@font-face{font-family:"Onsite Condensed-9df942b5bf56fd58";src:url("/_astro/fonts/ad33d7142fc8bbbf.woff2") format("woff2");font-display:swap;font-weight:100 900;font-style:normal;}@font-face{font-family:"Onsite Condensed-9df942b5bf56fd58";src:url("/_astro/fonts/835397aee34f56fb.woff2") format("woff2");font-display:swap;font-weight:100 900;font-style:italic;}@font-face{font-family:"Onsite Condensed-9df942b5bf56fd58 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:normal;size-adjust:89.5019%;ascent-override:107.2603%;descent-override:22.3459%;line-gap-override:0%;}@font-face{font-family:"Onsite Condensed-9df942b5bf56fd58 fallback: Arial";src:local("Arial");font-display:swap;font-weight:100 900;font-style:italic;size-adjust:89.5019%;ascent-override:107.2603%;descent-override:22.3459%;line-gap-override:0%;}:root{--font-dense-body:"Onsite Condensed-9df942b5bf56fd58","Onsite Condensed-9df942b5bf56fd58 fallback: Arial",system-ui,sans-serif;}</style><style>.izoom{position:absolute;inset:0;display:flex;align-items:center;justify-content:center;overflow:auto;cursor:zoom-out}#izoom-modal{background:#0009;backdrop-filter:blur(2px);-webkit-backdrop-filter:blur(2px)}
|
||
</style><link rel="stylesheet" href="/_astro/Outline.Ccm59ebL.css"><style>.video[data-astro-cid-rboccptt]{width:100%;aspect-ratio:var(--aspect);border-radius:var(--radius);overflow:hidden;background-color:var(--color-anti-black)}.video[data-astro-cid-rboccptt] iframe[data-astro-cid-rboccptt]{display:block;width:100%;height:100%;border:0}._figure_55xv6_5{margin:0}._image_55xv6_13{display:block;max-width:100%;height:auto;border-radius:6px}._caption_55xv6_20{margin-top:.5rem;font-family:var(--font-body);font-size:14px;line-height:1.45;color:var(--color-fg-subtle)}.callout[data-astro-cid-5if7h5vk]{width:100%;background-color:var(--callout-color);color:var(--color-fg);border-radius:12px;padding:24px 24px 18px;margin-bottom:24px}.callout[data-astro-cid-5if7h5vk].no-label{padding:24px}.callout[data-astro-cid-5if7h5vk] h4[data-astro-cid-5if7h5vk]{margin-left:-15px;margin-top:-15px;color:var(--title-color);text-transform:uppercase}.callout[data-astro-cid-5if7h5vk]>:last-child{margin-bottom:0}._big_16jda_4{margin:1.5rem 0;font-family:var(--font-body);font-size:1.25rem;font-weight:500;line-height:1.45}._brand_16jda_12{color:var(--color-coral-1)}._warning_16jda_16{color:var(--color-method-put)}._danger_16jda_20{color:var(--color-error)}._success_16jda_24{color:var(--color-method-post)}._info_16jda_28{color:var(--color-method-get)}
|
||
.code-block[data-astro-cid-oo7gdjzv] .expressive-code{margin:0}
|
||
:where(.callout,.release-note) .markdown a{color:var(--color-link);text-decoration:underline;text-decoration-thickness:1px;text-underline-offset:.15em;transition:color .1s ease}:where(.callout,.release-note) .markdown a:hover{color:var(--color-link-hover)}:where(.callout,.release-note) .markdown :is(ul,ol){list-style:revert;padding-left:1.5rem}:where(.callout,.release-note) .markdown>*+*,:where(.callout,.release-note) .markdown li+li{margin-top:.5rem}
|
||
.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o]{display:flex;align-items:center;cursor:pointer;padding:.75rem 0}.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o] .accordion-title[data-astro-cid-qrdmeu7o]{margin:0;font:inherit;color:inherit;text-wrap:inherit}.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o]:focus-visible{outline:2px solid var(--color-accent);outline-offset:-2px;border-radius:.25rem}.accordion[data-astro-cid-qrdmeu7o] .panel[data-astro-cid-qrdmeu7o]{padding-block:.75rem}.accordion[data-astro-cid-qrdmeu7o]::details-content{block-size:0;overflow:hidden;transition:block-size .15s ease-out,content-visibility .15s ease-out allow-discrete;interpolate-size:allow-keywords}.accordion[data-astro-cid-qrdmeu7o][open]::details-content{block-size:auto}.accordion[data-astro-cid-qrdmeu7o] .chevron[data-astro-cid-qrdmeu7o]{margin-left:auto;color:var(--color-fg-muted);transition:transform .15s ease-out}.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o]::marker,.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o]::-webkit-details-marker{display:none}.accordion[data-astro-cid-qrdmeu7o][open]>summary[data-astro-cid-qrdmeu7o]>.chevron[data-astro-cid-qrdmeu7o]{transform:rotate(90deg)}.accordion-group>.accordion[data-astro-cid-qrdmeu7o] summary[data-astro-cid-qrdmeu7o],.accordion-group>.accordion[data-astro-cid-qrdmeu7o] .panel[data-astro-cid-qrdmeu7o]{padding-inline:1rem}.accordion-group>.accordion[data-astro-cid-qrdmeu7o]:not(:first-of-type){border-top:1px solid var(--color-border)}.accordion-group[data-astro-cid-vn4mcufw]{border:1px solid var(--color-border);border-radius:.5rem}
|
||
</style><link rel="stylesheet" href="/_astro/iris.DiAaS2wT.css"><style>.breadcrumb[data-astro-cid-rjnc4y5o]{display:flex;gap:.5rem;align-items:flex-start}.square[data-astro-cid-rjnc4y5o]{width:.5rem;height:.5rem;background-color:var(--color-accent);flex-shrink:0;margin-top:.3125rem}.trail[data-astro-cid-rjnc4y5o]{list-style:none;margin:0;padding:0;display:flex;flex-wrap:wrap;align-items:center;gap:.25rem}.crumb[data-astro-cid-rjnc4y5o]{display:inline-flex;align-items:center;gap:.25rem}.crumb-label[data-astro-cid-rjnc4y5o]{color:var(--color-link);text-align:center;font-family:var(--font-eyebrow);font-size:12px;font-weight:110;line-height:160%;letter-spacing:.6px;text-transform:uppercase;text-decoration:none;display:inline-block;max-width:30ch;overflow:hidden;text-overflow:ellipsis;white-space:nowrap;vertical-align:bottom}.link[data-astro-cid-rjnc4y5o]{transition:color .15s ease}.link[data-astro-cid-rjnc4y5o]:hover{color:var(--color-link-hover)}.link[data-astro-cid-rjnc4y5o]:focus-visible{outline:2px solid var(--color-accent);outline-offset:3px}.non-link[data-astro-cid-rjnc4y5o]{color:var(--color-anti-white)}.force-light .non-link[data-astro-cid-rjnc4y5o],:root[data-theme=light] .non-link[data-astro-cid-rjnc4y5o]{color:var(--color-plum-1)}.sep[data-astro-cid-rjnc4y5o]{color:hsl(from var(--color-accent) h s l / 60%)}
|
||
:where([data-astro-image]){height:auto}:where([data-astro-image=full-width]){width:100%}:where([data-astro-image=constrained]){max-width:100%}[data-astro-image-fit=fill]{object-fit:fill}[data-astro-image-fit=contain]{object-fit:contain}[data-astro-image-fit=cover]{object-fit:cover}[data-astro-image-fit=scale-down]{object-fit:scale-down}:where([data-astro-image]:not([data-astro-image-fit])){object-fit:cover}[data-astro-image-pos=top]{object-position:top}[data-astro-image-pos=bottom]{object-position:bottom}[data-astro-image-pos=left]{object-position:left}[data-astro-image-pos=right]{object-position:right}[data-astro-image-pos=center]{object-position:center}[data-astro-image-pos=top-bottom]{object-position:top bottom}[data-astro-image-pos=top-left]{object-position:top left}[data-astro-image-pos=top-right]{object-position:top right}[data-astro-image-pos=top-center]{object-position:top center}[data-astro-image-pos=bottom-top]{object-position:bottom top}[data-astro-image-pos=bottom-left]{object-position:bottom left}[data-astro-image-pos=bottom-right]{object-position:bottom right}[data-astro-image-pos=bottom-center]{object-position:bottom center}[data-astro-image-pos=left-top]{object-position:left top}[data-astro-image-pos=left-bottom]{object-position:left bottom}[data-astro-image-pos=left-right]{object-position:left right}[data-astro-image-pos=left-center]{object-position:left center}[data-astro-image-pos=right-top]{object-position:right top}[data-astro-image-pos=right-bottom]{object-position:right bottom}[data-astro-image-pos=right-left]{object-position:right left}[data-astro-image-pos=right-center]{object-position:right center}[data-astro-image-pos=center-top]{object-position:center top}[data-astro-image-pos=center-bottom]{object-position:center bottom}[data-astro-image-pos=center-left]{object-position:center left}[data-astro-image-pos=center-right]{object-position:center right}:where([data-astro-image]:not([data-astro-image-pos])){object-position:center}
|
||
._button_17h79_1{--btn-height: 2.5rem;--btn-padding: .625rem 1rem;--btn-gap: .5rem;--btn-radius: 10px;--btn-font-size: .875rem;--btn-line-height: 160%;--btn-letter-spacing: .0088rem;display:inline-flex;width:max-content;height:var(--btn-height);padding:var(--btn-padding);justify-content:center;align-items:center;gap:var(--btn-gap);border-radius:var(--btn-radius);border-style:solid;border-width:1px;cursor:pointer;font-family:var(--font-body);font-size:var(--btn-font-size);font-weight:450;text-wrap-mode:nowrap;text-decoration:none;background-color:var(--btn-bg-color);border-color:var(--btn-br-color);color:var(--btn-fg-color);text-box:trim-both cap alphabetic;line-height:var(--btn-line-height);letter-spacing:var(--btn-letter-spacing);transition:background-color .1s ease-out,border-color .1s ease-out;background-clip:padding-box}._small_17h79_40{--btn-padding: .25rem .75rem;--btn-radius: .375rem;font-family:var(--font-eyebrow);font-weight:110;height:26px}._large_17h79_50{--btn-height: 3.25rem;--btn-padding: .625rem 1.25rem;--btn-font-size: 1rem;--btn-letter-spacing: .01rem}._toneCoral_17h79_57{--btn-tone: var(--color-coral);--btn-tone-hovered: var(--color-coral-hovered);--btn-tone-contrast: var(--color-anti-black)}._tonePlum_17h79_63{--btn-tone: var(--color-plum-2);--btn-tone-hovered: var(--color-plum-4);--btn-tone-contrast: var(--color-anti-white)}._full_17h79_69{--btn-bg-color: var(--btn-tone);--btn-br-color: var(--btn-tone);--btn-fg-color: var(--btn-tone-contrast);background-clip:border-box}._full_17h79_69:hover{--btn-bg-color: var(--btn-tone-hovered);--btn-br-color: var(--btn-tone-hovered)}._outline_17h79_83{--btn-bg-color: transparent;--btn-br-color: var(--btn-tone);--btn-fg-color: var(--btn-tone)}._glass_17h79_89{--btn-bg-color: hsl(from var(--btn-tone) h s l / 10%);--btn-br-color: hsl(from var(--btn-tone) h s l / 10%);--btn-fg-color: var(--btn-tone)}._outlineGlass_17h79_95{--btn-bg-color: hsl(from var(--btn-tone) h s l / 10%);--btn-br-color: var(--btn-tone);--btn-fg-color: var(--btn-tone)}._outline_17h79_83:hover,._glass_17h79_89:hover,._outlineGlass_17h79_95:hover{--btn-bg-color: hsl(from var(--btn-tone) h s l / 20%)}._ghost_17h79_107{--btn-bg-color: transparent;--btn-br-color: transparent;--btn-fg-color: var(--btn-tone)}._ghost_17h79_107:hover{--btn-bg-color: hsl(from var(--btn-tone) h s l / 20%)}._minimal_17h79_117{--btn-bg-color: transparent;--btn-br-color: transparent;--btn-fg-color: var(--btn-tone)}._minimal_17h79_117:hover{--btn-fg-color: var(--color-anti-white)}._button_17h79_1:disabled,._button_17h79_1[aria-disabled=true]{filter:saturate(50%);pointer-events:none}._icon_17h79_136{--btn-padding: .625rem;aspect-ratio:1 / 1}._small_17h79_40._icon_17h79_136{--btn-padding: .25rem}@media(width<=768px){._wideBoy_17h79_147{width:100%}}
|
||
.eyebrow[data-astro-cid-aokxteyj]{display:flex;gap:8px;align-items:center}.eyebrow[data-astro-cid-aokxteyj] .text[data-astro-cid-aokxteyj]{font-size:12px;text-align:center;font-family:var(--font-eyebrow);font-style:normal;font-weight:var(--eyebrow-text-weight, 110);line-height:150%;letter-spacing:.0437rem;text-transform:uppercase;text-wrap-mode:nowrap;opacity:var(--eyebrow-text-opacity, .7);color:var(--eyebrow-text-color-override, var(--eyebrow-text-color))}.eyebrow[data-astro-cid-aokxteyj] .square[data-astro-cid-aokxteyj]{flex-shrink:0;width:6px;height:6px;background-color:var(--eyebrow-square-color, var(--color-accent))}.surface-dark[data-astro-cid-aokxteyj] .text[data-astro-cid-aokxteyj]{--eyebrow-text-color: var(--color-coral-2)}.surface-light[data-astro-cid-aokxteyj] .text[data-astro-cid-aokxteyj]{--eyebrow-text-color: var(--color-plum-2)}.surface-page[data-astro-cid-aokxteyj] .text[data-astro-cid-aokxteyj]{--eyebrow-text-color: var(--color-fg)}.large[data-astro-cid-aokxteyj] .square[data-astro-cid-aokxteyj]{width:8px;height:8px}.large[data-astro-cid-aokxteyj] .text[data-astro-cid-aokxteyj]{font-size:14px}
|
||
.text-toc[data-astro-cid-rg4ou2fw]{display:flex;flex-direction:column;gap:32px;font-family:var(--font-body)}.authors[data-astro-cid-rg4ou2fw]{display:flex;flex-direction:column;gap:16px}.author[data-astro-cid-rg4ou2fw]{display:flex;align-items:center;justify-content:flex-start;gap:16px}.author-link[data-astro-cid-rg4ou2fw]{text-decoration:none;border-radius:8px;transition:opacity .1s ease-out}.author-link[data-astro-cid-rg4ou2fw]:hover{opacity:.8}.author-link[data-astro-cid-rg4ou2fw]:focus-visible{outline:2px solid var(--color-accent);outline-offset:4px}.author[data-astro-cid-rg4ou2fw] picture{display:block;flex-shrink:0}.pfp[data-astro-cid-rg4ou2fw]{width:80px;height:80px;border-radius:50%;object-fit:cover;display:block}.author-meta[data-astro-cid-rg4ou2fw]{display:flex;flex-direction:column;gap:2px;min-width:0}.author-name[data-astro-cid-rg4ou2fw]{color:var(--color-coral);font-size:18px;font-weight:110;line-height:100%;letter-spacing:.9px;font-family:var(--font-eyebrow)}.author-title[data-astro-cid-rg4ou2fw]{font-family:var(--font-eyebrow);color:var(--color-coral-2);font-size:16px;font-weight:110;line-height:120%;letter-spacing:.8px}.author-link[data-astro-cid-rg4ou2fw]:hover .author-name[data-astro-cid-rg4ou2fw]{text-decoration:underline;text-underline-offset:2px}.news[data-astro-cid-rg4ou2fw]{display:flex;flex-direction:column;gap:12px}.news-blurb[data-astro-cid-rg4ou2fw]{font-size:13px;line-height:1.45;color:var(--color-coral-3);margin:0;text-wrap-style:balance}.narrow-eyebrow[data-astro-cid-rg4ou2fw]{display:none}@media(width<=1180px){.wide-eyebrow[data-astro-cid-rg4ou2fw]{display:none}.narrow-eyebrow[data-astro-cid-rg4ou2fw]{display:block}}@media(width<=768px){.text-toc[data-astro-cid-rg4ou2fw]{gap:0}.authors[data-astro-cid-rg4ou2fw],.news[data-astro-cid-rg4ou2fw]{display:none}}
|
||
.diamond-helper[data-astro-cid-lhauwh7h]{width:100%;height:100%;position:relative;isolation:isolate}.diamond-children[data-astro-cid-lhauwh7h]{z-index:0}.diamond-grid[data-astro-cid-lhauwh7h]{pointer-events:none;z-index:-1;position:absolute;inset:var(--offset-top) 0 var(--offset-bottom) 0;height:384px;background:linear-gradient(var(--gradient-direction),hsl(from var(--color-sky) h s l / 15%),hsl(from var(--color-coral) h s l / 0%) 75%);mask-image:url(/_astro/diamond-grid.ClcDGxpq.svg);mask-repeat:repeat-x;mask-position:var(--align-pos);mask-size:256px 256px;-webkit-mask-image:url(/_astro/diamond-grid.ClcDGxpq.svg);-webkit-mask-repeat:repeat-x;-webkit-mask-position:var(--align-pos);-webkit-mask-size:256px 256px}
|
||
section[data-astro-cid-ektegib2]#cta{width:100%;background:var(--color-anti-black)}.cta-outer[data-astro-cid-ektegib2]{width:100%;padding-inline:var(--page-gutter);padding-top:120px;display:grid;place-items:start}.cta-inner[data-astro-cid-ektegib2]{display:flex;flex-direction:column;align-items:center;gap:32px;text-align:center;margin-inline:auto;padding-bottom:140px}.cta-title[data-astro-cid-ektegib2]{display:flex;flex-direction:column;align-items:center;gap:20px}.cta-title[data-astro-cid-ektegib2] h1[data-astro-cid-ektegib2]{color:var(--color-anti-white);text-box:trim-both cap;font-family:var(--font-heading);font-size:48px;font-style:normal;font-weight:300;line-height:115%}.cta-body[data-astro-cid-ektegib2]{color:var(--color-anti-white);text-box:trim-both cap;font-family:var(--font-body);font-size:20px;font-style:normal;font-weight:400;line-height:145%;letter-spacing:.0163rem;max-width:640px}.cta-actions[data-astro-cid-ektegib2]{display:flex;gap:1.5rem}.divider[data-astro-cid-ektegib2]{border:none;height:1px;background:linear-gradient(to right,hsl(from var(--color-coral) h s l / 0%) 0%,var(--color-coral) 25%,var(--color-coral) 75%,hsl(from var(--color-coral) h s l / 0%) 100%);width:100%;margin:20px auto}@media(width<=768px){.cta-outer[data-astro-cid-ektegib2]{padding-block:60px 0}.cta-inner[data-astro-cid-ektegib2]{padding-bottom:60px}.cta-title[data-astro-cid-ektegib2]{align-items:start;gap:14px}.cta-title[data-astro-cid-ektegib2] h1[data-astro-cid-ektegib2]{font-size:26px;font-weight:300;line-height:140%;letter-spacing:-.78px;text-align:left}.cta-body[data-astro-cid-ektegib2]{text-align:left;font-size:16px;font-style:normal;font-weight:400;line-height:150%;letter-spacing:-.16px;opacity:.8}.cta-actions[data-astro-cid-ektegib2]{flex-direction:column;width:100%;gap:16px;& button[data-astro-cid-ektegib2]{width:100%}}}
|
||
</style><link rel="stylesheet" href="/_astro/BaseLayout.BUhsEDns.css"><link rel="stylesheet" href="/_astro/MktoForm.Dp8-P3eE.css"><style>.video-toc[data-astro-cid-n6yailqd]{font-family:var(--font-body)}.video-toc-inner[data-astro-cid-n6yailqd]{display:flex;flex-direction:column;gap:24px}.thumb[data-astro-cid-n6yailqd]{width:100%;aspect-ratio:1 / 1;border-radius:8px;object-fit:cover;display:block}.series-info[data-astro-cid-n6yailqd]{display:flex;flex-direction:column;gap:12px}.series-blurb[data-astro-cid-n6yailqd]{margin:0;font-size:14px;line-height:1.45;color:var(--color-coral-3)}.pager[data-astro-cid-n6yailqd]{display:flex;flex-direction:row;gap:8px}.pager-link[data-astro-cid-n6yailqd]{flex:1;display:inline-flex;align-items:center;justify-content:center;gap:6px;padding:10px 12px;border-radius:6px;border:1px solid var(--color-coral-1);background:transparent;color:var(--color-coral);font-family:var(--font-eyebrow);font-size:12px;font-weight:110;letter-spacing:.05em;text-transform:uppercase;text-decoration:none;transition:background-color .1s ease,color .1s ease,border-color .1s ease}a[data-astro-cid-n6yailqd].pager-link:hover{background-color:hsl(from var(--color-coral) h s l / 12%);color:var(--color-coral-hovered);border-color:var(--color-coral)}a[data-astro-cid-n6yailqd].pager-link:focus-visible{outline:2px solid var(--color-accent);outline-offset:2px}.pager-link[data-astro-cid-n6yailqd].disabled{border-color:hsl(from var(--color-coral-1) h s l / 25%);color:hsl(from var(--color-coral) h s l / 30%);pointer-events:none;cursor:default}.pager-icon[data-astro-cid-n6yailqd]{flex-shrink:0}.news[data-astro-cid-n6yailqd]{display:flex;flex-direction:column;gap:12px}.news-blurb[data-astro-cid-n6yailqd]{font-size:13px;line-height:1.45;color:var(--color-coral-3);margin:0}@media(width<=768px){.video-toc-inner[data-astro-cid-n6yailqd]{max-width:400px;margin-inline:auto}}
|
||
</style><style>._speaker_1qysz_6{margin:2.5rem 0 1rem}._head_1qysz_9{display:flex;align-items:center;gap:.75rem}._speaker_1qysz_6 ._head_1qysz_9 ._avatar_1qysz_6{width:48px;height:48px;margin:0;border-radius:50%;object-fit:cover;flex-shrink:0}._meta_1qysz_32{display:flex;flex-direction:column;line-height:1.2}._name_1qysz_38{font-family:var(--font-body);font-size:17px;font-weight:600;color:var(--color-anti-black)}._title_1qysz_45{font-family:var(--font-body);font-size:13px;color:hsl(from var(--color-anti-black) h s l / 60%)}._speaker_1qysz_6 ._question_1qysz_6._question_1qysz_6{margin:.75rem 0 0;font-family:var(--font-body);font-size:20px;font-weight:500;line-height:1.4;color:var(--color-anti-black);border-left:3px solid var(--color-coral);padding-left:1rem}
|
||
</style><link rel="preload" href="/_astro/fonts/b4329cf3d24405e5.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/19c6ea19dae76a22.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/71fc045da6bf1b36.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/da09e39c103c809d.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/618f3c433d6f5aa7.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/fef5e52a89fda1b5.ttf" as="font" type="font/ttf" crossorigin=""><link rel="preload" href="/_astro/fonts/d64cd15e5fa4dae1.ttf" as="font" type="font/ttf" crossorigin=""><link rel="preload" href="/_astro/fonts/ad33d7142fc8bbbf.woff2" as="font" type="font/woff2" crossorigin=""><link rel="preload" href="/_astro/fonts/835397aee34f56fb.woff2" as="font" type="font/woff2" crossorigin=""><link rel="sitemap" href="/sitemap-index.xml"><link rel="alternate" type="application/rss+xml" title="Antithesis blog" href="/blog/rss.xml"><meta name="generator" content="Astro v6.4.0"><link rel="canonical" href="https://antithesis.com/blog/2026/finding-bugs-in-raft-implementations/"><meta name="description" content="Why formal verification is not enough to maintain consensus in real systems"><meta property="og:type" content="website"><meta property="og:site_name" content="Antithesis"><meta property="og:url" content="https://antithesis.com/blog/2026/finding-bugs-in-raft-implementations/"><meta property="og:title" content="Finding bugs in Raft implementations | Antithesis"><meta property="og:description" content="Why formal verification is not enough to maintain consensus in real systems"><meta property="og:image" content="https://antithesis.com/_astro/cover.C2TWoGrq_Z1dNdEc.jpg"><meta property="og:image:width" content="1200"><meta property="og:image:height" content="675"><meta property="og:image:type" content="image/jpeg"><meta property="og:image:alt" content="Finding bugs in Raft implementations | Antithesis"><meta name="twitter:card" content="summary_large_image"><meta name="twitter:url" content="https://antithesis.com/blog/2026/finding-bugs-in-raft-implementations/"><meta name="twitter:title" content="Finding bugs in Raft implementations | Antithesis"><meta name="twitter:description" content="Why formal verification is not enough to maintain consensus in real systems"><meta name="twitter:image" content="https://antithesis.com/_astro/cover.C2TWoGrq_Z1dNdEc.jpg"><meta name="twitter:image:alt" content="Finding bugs in Raft implementations | Antithesis"><link rel="manifest" href="/manifest.webmanifest"><meta name="mobile-web-app-capable" content="yes"><meta name="theme-color" media="(prefers-color-scheme: light)" content="#16031b"><meta name="theme-color" media="(prefers-color-scheme: dark)" content="#16031b"><meta name="application-name" content="Antithesis"><link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon.png"><link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon-precomposed.png"><link rel="mask-icon" href="/safari-pinned-tab.svg" color="#16031b"><meta name="apple-mobile-web-app-capable" content="yes"><meta name="apple-mobile-web-app-status-bar-style" content="black-translucent"><meta name="apple-mobile-web-app-title" content="Antithesis"><link rel="icon" type="image/x-icon" href="/favicon.ico"><link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png"><link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png"><link rel="icon" type="image/png" sizes="48x48" href="/favicon-48x48.png"><link rel="icon" type="image/svg+xml" href="/favicon.svg"><meta name="msapplication-TileColor" content="#16031b"><meta name="msapplication-TileImage" content="/mstile-144x144.png"><meta name="msapplication-config" content="/browserconfig.xml"><link rel="yandex-tableau-widget" href="/yandex-browser-manifest.json"></head> <body data-astro-cid-37fxchfa=""> <!-- Google Tag Manager (noscript) --><noscript><iframe src="https://www.googletagmanager.com/ns.html?id=GTM-W9GNSJM" height="0" width="0" style="display:none;visibility:hidden"></iframe></noscript><!-- End Google Tag Manager (noscript) --> <div class="root" data-layout="base" id="izoom-body-id" data-astro-cid-37fxchfa=""> <style>astro-island,astro-slot,astro-static-slot{display:contents}</style><script>(()=>{var e=async t=>{await(await t())()};(self.Astro||(self.Astro={})).load=e;window.dispatchEvent(new Event("astro:load"));})();</script><script>(()=>{var g=Object.defineProperty;var w=(c,s,d)=>s in c?g(c,s,{enumerable:!0,configurable:!0,writable:!0,value:d}):c[s]=d;var l=(c,s,d)=>w(c,typeof s!="symbol"?s+"":s,d);var E=new Set(["__proto__","constructor","prototype"]);{let c={0:t=>y(t),1:t=>d(t),2:t=>new RegExp(t),3:t=>new Date(t),4:t=>new Map(d(t)),5:t=>new Set(d(t)),6:t=>BigInt(t),7:t=>new URL(t),8:t=>new Uint8Array(t),9:t=>new Uint16Array(t),10:t=>new Uint32Array(t),11:t=>Number.POSITIVE_INFINITY*t},s=t=>{let[p,e]=t;return p in c?c[p](e):void 0},d=t=>t.map(s),y=t=>typeof t!="object"||t===null?t:Object.fromEntries(Object.entries(t).map(([p,e])=>[p,s(e)]));class f extends HTMLElement{constructor(){super(...arguments);l(this,"Component");l(this,"hydrator");l(this,"hydrate",async()=>{var b;if(!this.hydrator||!this.isConnected)return;let e=(b=this.parentElement)==null?void 0:b.closest("astro-island[ssr]");if(e){e.addEventListener("astro:hydrate",this.hydrate,{once:!0});return}let n=this.querySelectorAll("astro-slot"),r={},i=this.querySelectorAll("template[data-astro-template]");for(let o of i){let a=o.closest(this.tagName);a!=null&&a.isSameNode(this)&&(r[o.getAttribute("data-astro-template")||"default"]=o.innerHTML,o.remove())}for(let o of n){let a=o.closest(this.tagName);a!=null&&a.isSameNode(this)&&(r[o.getAttribute("name")||"default"]=o.innerHTML)}let u;try{u=this.hasAttribute("props")?y(JSON.parse(this.getAttribute("props"))):{}}catch(o){let a=this.getAttribute("component-url")||"<unknown>",v=this.getAttribute("component-export");throw v&&(a+=` (export ${v})`),console.error(`[hydrate] Error parsing props for component ${a}`,this.getAttribute("props"),o),o}let h;await this.hydrator(this)(this.Component,u,r,{client:this.getAttribute("client")}),this.removeAttribute("ssr"),this.dispatchEvent(new CustomEvent("astro:hydrate"))});l(this,"unmount",()=>{this.isConnected||this.dispatchEvent(new CustomEvent("astro:unmount"))})}disconnectedCallback(){document.removeEventListener("astro:after-swap",this.unmount),document.addEventListener("astro:after-swap",this.unmount,{once:!0})}connectedCallback(){if(!this.hasAttribute("await-children")||document.readyState==="interactive"||document.readyState==="complete")this.childrenConnectedCallback();else{let e=()=>{document.removeEventListener("DOMContentLoaded",e),n.disconnect(),this.childrenConnectedCallback()},n=new MutationObserver(()=>{var r;((r=this.lastChild)==null?void 0:r.nodeType)===Node.COMMENT_NODE&&this.lastChild.nodeValue==="astro:end"&&(this.lastChild.remove(),e())});n.observe(this,{childList:!0}),document.addEventListener("DOMContentLoaded",e)}}async childrenConnectedCallback(){let e=this.getAttribute("before-hydration-url");e&&await import(e),this.start()}getRetryImportUrl(e){let n=new URL(e,document.baseURI),r=`astro-retry=${Date.now()}`,i=n.hash.replace(/^#/,"");return n.hash=i?`${i}&${r}`:r,n.toString()}async importWithRetry(e){try{return await import(e)}catch(n){return await new Promise(r=>setTimeout(r,1e3)),import(this.getRetryImportUrl(e))}}handleHydrationError(e){let n=this.getAttribute("component-url"),r=new CustomEvent("astro:hydration-error",{cancelable:!0,bubbles:!0,composed:!0,detail:{error:e,componentUrl:n}});this.dispatchEvent(r)&&console.error(`[astro-island] Error hydrating ${n}`,e)}async start(){let e=JSON.parse(this.getAttribute("opts")),n=this.getAttribute("client");if(Astro[n]===void 0){window.addEventListener(`astro:${n}`,()=>this.start(),{once:!0});return}try{await Astro[n](async()=>{let r=this.getAttribute("renderer-url");try{let[i,{default:u}]=await Promise.all([this.importWithRetry(this.getAttribute("component-url")),r?this.importWithRetry(r):Promise.resolve({default:()=>()=>{}})]),h=this.getAttribute("component-export")||"default";if(h.includes(".")){this.Component=i;for(let m of h.split(".")){if(E.has(m)||!this.Component||typeof this.Component!="object"&&typeof this.Component!="function"||!Object.hasOwn(this.Component,m))throw new Error(`Invalid component export path: ${h}`);this.Component=this.Component[m]}}else{if(E.has(h))throw new Error(`Invalid component export path: ${h}`);this.Component=i[h]}return this.hydrator=u,this.hydrate}catch(i){return this.handleHydrationError(i),()=>{}}},e,this)}catch(r){this.handleHydrationError(r)}}attributeChangedCallback(){this.hydrate()}}l(f,"observedAttributes",["props"]),customElements.get("astro-island")||customElements.define("astro-island",f)}})();</script><astro-island uid="23rx5T" prefix="r9" component-url="/_astro/index.BmDpZpWX.js" component-export="default" renderer-url="/_astro/client.BoS663YN.js" props="{"featured":[0,{"latestBlog":[0,{"title":[0,"Ways research teams fail"],"link":[0,"/blog/2026/ways-research-teams-fail/"],"imageURL":[0,"/_astro/8-bit-iceberg.CENNwCbe_ZFo3C3.webp"]}]}],"data-astro-cid-37fxchfa":[0,true]}" ssr="" client="load" opts="{"name":"Header","value":true}" await-children=""><div class="_headerWrapper_c2c8p_1" data-search-warm-scope="true"><div class="_wrapper_k6vvt_1" data-banner-key="bb-eur-2026-announcement"><div class="_banner_k6vvt_15"><div class="_inner_k6vvt_28" data-sid="d2eb.0"><span>Bug Bash is coming to Copenhagen this fall!</span><a href="/bugbash/europe/2026/" role="button" class="_button_17h79_1 _toneCoral_17h79_57 _full_17h79_69 _small_17h79_40 _cta_k6vvt_60">Learn more<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-right" aria-hidden="true"><path d="M5 12h14"></path><path d="m12 5 7 7-7 7"></path></svg></a></div><button type="button" aria-label="Dismiss announcement" class="_button_17h79_1 _toneCoral_17h79_57 _ghost_17h79_107 _small_17h79_40 _icon_17h79_136 _close_k6vvt_47"><svg xmlns="http://www.w3.org/2000/svg" width="20" height="20" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-x" aria-hidden="true"><path d="M18 6 6 18"></path><path d="m6 6 12 12"></path></svg></button></div></div><div class="_headerOuter_c2c8p_5"><div class="_headerInner_c2c8p_24"><a href="/" class="_logoLink_c2c8p_72" aria-label="Antithesis home"><img src="/_astro/antithesis.poHvWeoa.svg" alt="" class="_logo_c2c8p_72"><img src="/_astro/iris.C79y6VkI.svg" alt="" class="_logoIris_c2c8p_91"></a><nav class="_desktopNav_c2c8p_35"><ul class="_list_c2c8p_41"><div class="_listLeft_c2c8p_56"><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_menuDropdownTrigger_c2c8p_60">Product<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-down _menuChevron_c2c8p_194" aria-hidden="true"><path d="m6 9 6 6 6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_menuDropdownTrigger_c2c8p_60 _gradientTriggerStyle_c2c8p_149">Developers<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-down _menuChevron_c2c8p_194" aria-hidden="true"><path d="m6 9 6 6 6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_menuDropdownTrigger_c2c8p_60">Learn<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-down _menuChevron_c2c8p_194" aria-hidden="true"><path d="m6 9 6 6 6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_menuDropdownTrigger_c2c8p_60">Company<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-down _menuChevron_c2c8p_194" aria-hidden="true"><path d="m6 9 6 6 6-6"></path></svg></button></li></div><div class="_listRight_c2c8p_66"><div class="_root_13wyo_16 _asButton_13wyo_2 _headerSearch_c2c8p_105"><label class="_bar_13wyo_26" for="_r9R_pq_"><svg xmlns="http://www.w3.org/2000/svg" width="20" height="20" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-search _icon_13wyo_121" aria-hidden="true"><path d="m21 21-4.34-4.34"></path><circle cx="11" cy="11" r="8"></circle></svg><input data-list-empty="" autocomplete="off" spellcheck="false" autocorrect="off" autocapitalize="none" role="combobox" aria-expanded="false" aria-haspopup="listbox" aria-autocomplete="none" type="text" id="_r9R_pq_" aria-label="search" data-search-trigger="true" placeholder="Search" class="_input_13wyo_126" value=""></label></div><input id="base-ui-_r9R_4pq_-hidden-input" style="clip-path:inset(50%);overflow:hidden;white-space:nowrap;border:0;padding:0;width:1px;height:1px;margin:-1px;position:fixed;top:0;left:0" tabindex="-1" aria-hidden="true" value=""><div class="_divider_c2c8p_98"></div><a href="/login/" role="button" class="_button_17h79_1 _toneCoral_17h79_57 _minimal_17h79_117 _logInButton_c2c8p_510"><svg xmlns="http://www.w3.org/2000/svg" width="20" height="20" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-log-in" aria-hidden="true"><path d="m10 17 5-5-5-5"></path><path d="M15 12H3"></path><path d="M15 3h4a2 2 0 0 1 2 2v14a2 2 0 0 1-2 2h-4"></path></svg><span>Log in</span></a><a href="/company/contact/?topic=book-a-demo" role="button" class="_button_17h79_1 _toneCoral_17h79_57 _full_17h79_69"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-calendar" aria-hidden="true"><path d="M8 2v4"></path><path d="M16 2v4"></path><rect width="18" height="18" x="3" y="4" rx="2"></rect><path d="M3 10h18"></path></svg>Book a demo</a></div></ul></nav><button type="button" aria-expanded="false" aria-label="Open menu" class="_button_17h79_1 _toneCoral_17h79_57 _minimal_17h79_117 _icon_17h79_136 _mobileMenuButton_dsfq1_1"><svg xmlns="http://www.w3.org/2000/svg" width="32" height="32" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-menu _menuIcon_dsfq1_12" aria-hidden="true"><path d="M4 5h16"></path><path d="M4 12h16"></path><path d="M4 19h16"></path></svg><svg xmlns="http://www.w3.org/2000/svg" width="32" height="32" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-x _closeIcon_dsfq1_13 _iconHidden_dsfq1_25" aria-hidden="true"><path d="M18 6 6 18"></path><path d="m6 6 12 12"></path></svg></button></div></div><nav aria-hidden="true" inert="" class="_mobileNav_dsfq1_30"><div class="_contentArea_dsfq1_34"><ul class="_list_dsfq1_41"><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_mainItem_dsfq1_293">Product<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-right _mainItemChevron_dsfq1_322" aria-hidden="true"><path d="m9 18 6-6-6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_mainItem_dsfq1_293">Developers<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-right _mainItemChevron_dsfq1_322" aria-hidden="true"><path d="m9 18 6-6-6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_mainItem_dsfq1_293">Learn<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-right _mainItemChevron_dsfq1_322" aria-hidden="true"><path d="m9 18 6-6-6-6"></path></svg></button></li><li><button type="button" aria-disabled="false" tabindex="0" aria-expanded="false" data-base-ui-navigation-menu-trigger="" class="_mainItem_dsfq1_293">Company<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-right _mainItemChevron_dsfq1_322" aria-hidden="true"><path d="m9 18 6-6-6-6"></path></svg></button></li></ul><div id="_r9R_2f_" class="_viewport_dsfq1_66"><div></div></div></div><div class="_bottomSection_dsfq1_357"><button type="button" tabindex="0" data-base-ui-click-trigger="" id="base-ui-_r9R_tn_" class="_triggerBar_13wyo_351"><svg xmlns="http://www.w3.org/2000/svg" width="18" height="18" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-search _icon_13wyo_121" aria-hidden="true"><path d="m21 21-4.34-4.34"></path><circle cx="11" cy="11" r="8"></circle></svg><span class="_triggerLabel_13wyo_389">Search</span></button><input class="_keyboardPrimer_13wyo_152" type="text" tabindex="-1" aria-hidden="true" autocomplete="off"><div class="_bottomButtons_dsfq1_364"><a href="/company/contact/?topic=book-a-demo" role="button" class="_button_17h79_1 _toneCoral_17h79_57 _full_17h79_69 _tryBtn_dsfq1_370"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-calendar" aria-hidden="true"><path d="M8 2v4"></path><path d="M16 2v4"></path><rect width="18" height="18" x="3" y="4" rx="2"></rect><path d="M3 10h18"></path></svg>Book a demo</a><a href="/login/" role="button" class="_button_17h79_1 _toneCoral_17h79_57 _glass_17h79_89 _logInBtn_dsfq1_371"><svg xmlns="http://www.w3.org/2000/svg" width="20" height="20" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-log-in" aria-hidden="true"><path d="m10 17 5-5-5-5"></path><path d="M15 12H3"></path><path d="M15 3h4a2 2 0 0 1 2 2v14a2 2 0 0 1-2 2h-4"></path></svg>Log in</a></div></div></nav></div><!--astro:end--></astro-island> <main data-astro-cid-37fxchfa=""> <style>
|
||
:root {
|
||
--header-bg: rgb(22 3 27);
|
||
}
|
||
</style> <script>
|
||
document.documentElement.classList.add("fn-js");
|
||
(function () {
|
||
function wire() {
|
||
for (const marker of document.querySelectorAll(".footnote-marker")) {
|
||
const body = document.getElementById(
|
||
(marker.getAttribute("href") || "").slice(1),
|
||
);
|
||
if (!body) continue;
|
||
marker.setAttribute("role", "button");
|
||
marker.setAttribute("aria-controls", body.id);
|
||
marker.setAttribute("aria-expanded", "false");
|
||
marker.addEventListener("click", (e) => {
|
||
e.preventDefault();
|
||
const open = body.classList.toggle("footnote-open");
|
||
marker.setAttribute("aria-expanded", open ? "true" : "false");
|
||
});
|
||
// Anchors activate on Enter (fires a click) but not Space — forward it.
|
||
marker.addEventListener("keydown", (e) => {
|
||
if (e.key === " ") {
|
||
e.preventDefault();
|
||
marker.click();
|
||
}
|
||
});
|
||
}
|
||
}
|
||
if (document.readyState === "loading")
|
||
document.addEventListener("DOMContentLoaded", wire);
|
||
else wire();
|
||
})();
|
||
</script> <div class="article-page" data-variant="text" data-mobile-toc-mode="sticky" data-astro-cid-ee7emijr=""> <div class="hero-band" aria-hidden="true" data-astro-cid-ee7emijr=""> <picture class="no-zoom" data-astro-cid-ee7emijr="true"> <source srcset="/_astro/cover.C2TWoGrq_ZYezKu.webp 800w, /_astro/cover.C2TWoGrq_Zz1PLD.webp 1200w, /_astro/cover.C2TWoGrq_1BrT8w.webp 1672w" type="image/webp" sizes="(min-width: 1672px) 1672px, 100vw"> <img src="/_astro/cover.C2TWoGrq_Z219gO8.jpg" srcset="/_astro/cover.C2TWoGrq_Z26HvSq.jpg 800w, /_astro/cover.C2TWoGrq_dE7TV.jpg 1200w, /_astro/cover.C2TWoGrq_2p8RP6.jpg 1672w" alt="" sizes="(min-width: 1672px) 1672px, 100vw" style="--hero-bg-position-y: 10%" data-astro-cid-ee7emijr="true" loading="lazy" decoding="async" width="1920" height="1080" class="hero-bg"> </picture><div class="hero-overlay" aria-hidden="true" data-astro-cid-ee7emijr=""></div> </div> <div class="hero-crumbs" data-astro-cid-ee7emijr=""> <nav class="breadcrumb" aria-label="Breadcrumb" data-astro-cid-rjnc4y5o=""> <span class="square" aria-hidden="true" data-astro-cid-rjnc4y5o=""></span> <ol class="trail" data-astro-cid-rjnc4y5o=""> <li class="crumb" data-astro-cid-rjnc4y5o=""> <a class="crumb-label link" href="/" title="Home" data-astro-cid-rjnc4y5o=""> Home </a> <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" aria-hidden="true" data-astro-cid-rjnc4y5o="true" class="lucide lucide-chevron-right sep"> <path d="m9 18 6-6-6-6"></path> </svg> </li><li class="crumb" data-astro-cid-rjnc4y5o=""> <a class="crumb-label link" href="/learn/?category=Blog#resources" title="Blog" data-astro-cid-rjnc4y5o=""> Blog </a> <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" aria-hidden="true" data-astro-cid-rjnc4y5o="true" class="lucide lucide-chevron-right sep"> <path d="m9 18 6-6-6-6"></path> </svg> </li><li class="crumb" data-astro-cid-rjnc4y5o=""> <span class="crumb-label non-link current" aria-current="page" title="Finding bugs in Raft implementations" data-astro-cid-rjnc4y5o=""> Finding bugs in Raft implementations </span> </li> </ol> </nav> </div> <div class="hero-headline" data-astro-cid-ee7emijr=""> <p class="hero-date" data-astro-cid-ee7emijr="" data-sid="d2eb.1"> <span data-astro-cid-ee7emijr=""> July 27, 2026 </span> <span class="hero-byline" data-astro-cid-ee7emijr=""> | <span class="hero-byline-name" data-astro-cid-ee7emijr="">TW Lim</span> , Technical Writer | <span class="hero-byline-name" data-astro-cid-ee7emijr="">Rohan Padhye</span> , Research Fellow | <span class="hero-byline-name" data-astro-cid-ee7emijr="">Marco Primi</span> , Distributed Systems Engineer </span> </p> <h1 class="hero-title" data-astro-cid-ee7emijr="" data-sid="d2eb.2">Finding bugs in Raft implementations</h1> </div> <aside class="article-toc" data-astro-cid-ee7emijr=""> <aside class="text-toc" data-article-toc="" data-astro-cid-rg4ou2fw=""> <section class="authors" data-astro-cid-rg4ou2fw=""> <a class="author author-link" href="/author/tw-lim/" data-astro-cid-rg4ou2fw=""> <picture data-astro-cid-rg4ou2fw="true"> <source srcset="/_astro/069_tw.DHr19spq_21Uywr.webp 80w, /_astro/069_tw.DHr19spq_1E9qlX.webp 160w" type="image/webp"> <img src="/_astro/069_tw.DHr19spq_1h4adg.jpg" srcset="/_astro/069_tw.DHr19spq_1h4adg.jpg 80w, /_astro/069_tw.DHr19spq_1hUTqm.jpg 160w" alt="TW Lim" data-astro-cid-rg4ou2fw="true" loading="lazy" decoding="async" sizes="80px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="80" height="80" class="pfp"> </picture><div class="author-meta" data-astro-cid-rg4ou2fw=""> <span class="author-name" data-astro-cid-rg4ou2fw="">TW Lim</span> <span class="author-title" data-astro-cid-rg4ou2fw="">Technical Writer</span> </div> </a><a class="author author-link" href="/author/rohan-padhye/" data-astro-cid-rg4ou2fw=""> <picture data-astro-cid-rg4ou2fw="true"> <source srcset="/_astro/rohan-padhye.C9feRA4F_Z1Gs1ns.webp 80w, /_astro/rohan-padhye.C9feRA4F_Z1n5n5U.webp 160w" type="image/webp"> <img src="/_astro/rohan-padhye.C9feRA4F_SytTO.jpg" srcset="/_astro/rohan-padhye.C9feRA4F_SytTO.jpg 80w, /_astro/rohan-padhye.C9feRA4F_1to1yX.jpg 160w" alt="Rohan Padhye" data-astro-cid-rg4ou2fw="true" loading="lazy" decoding="async" sizes="80px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="80" height="80" class="pfp"> </picture><div class="author-meta" data-astro-cid-rg4ou2fw=""> <span class="author-name" data-astro-cid-rg4ou2fw="">Rohan Padhye</span> <span class="author-title" data-astro-cid-rg4ou2fw="">Research Fellow</span> </div> </a><a class="author author-link" href="/author/marco-primi/" data-astro-cid-rg4ou2fw=""> <picture data-astro-cid-rg4ou2fw="true"> <source srcset="/_astro/001_marco_primi.C8sTreDD_Z15NsA3.webp 80w, /_astro/001_marco_primi.C8sTreDD_Z29rb9a.webp 160w" type="image/webp"> <img src="/_astro/001_marco_primi.C8sTreDD_17JBgv.jpg" srcset="/_astro/001_marco_primi.C8sTreDD_17JBgv.jpg 80w, /_astro/001_marco_primi.C8sTreDD_Z2laiWY.jpg 160w" alt="Marco Primi" data-astro-cid-rg4ou2fw="true" loading="lazy" decoding="async" sizes="80px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="80" height="80" class="pfp"> </picture><div class="author-meta" data-astro-cid-rg4ou2fw=""> <span class="author-name" data-astro-cid-rg4ou2fw="">Marco Primi</span> <span class="author-title" data-astro-cid-rg4ou2fw="">Distributed Systems Engineer</span> </div> </a> </section> <details class="outline-details" open="" data-outline-details="" data-astro-cid-5dfgbyiq=""><summary class="outline-summary" data-astro-cid-5dfgbyiq=""><div class="eyebrow surface-dark" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj="" data-sid="d2eb.3"> In this post </div> </div><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-chevron-down outline-chevron" aria-hidden="true" data-astro-cid-5dfgbyiq="true"><path d="m6 9 6 6 6-6"></path></svg></summary><ul class="outline-list" data-astro-cid-5dfgbyiq=""><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.4"><a class="outline-link" href="#introduction" data-toc-target="introduction" data-astro-cid-5dfgbyiq="">Introduction</a></li><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.5"><a class="outline-link" href="#why-this-matters" data-toc-target="why-this-matters" data-astro-cid-5dfgbyiq="">Why this matters</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.6"><a class="outline-link" href="#bugs-are-not-a-fact-of-life" data-toc-target="bugs-are-not-a-fact-of-life" data-astro-cid-5dfgbyiq="">Bugs are not a fact of life</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.7"><a class="outline-link" href="#specifications-are-not-code" data-toc-target="specifications-are-not-code" data-astro-cid-5dfgbyiq="">Specifications are not code</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.8"><a class="outline-link" href="#testing-can-actually-be-simple" data-toc-target="testing-can-actually-be-simple" data-astro-cid-5dfgbyiq="">Testing can actually be simple</a></li><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.9"><a class="outline-link" href="#testing-raft" data-toc-target="testing-raft" data-astro-cid-5dfgbyiq="">Testing Raft</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.10"><a class="outline-link" href="#about-antithesis" data-toc-target="about-antithesis" data-astro-cid-5dfgbyiq="">About Antithesis</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.11"><a class="outline-link" href="#about-raft" data-toc-target="about-raft" data-astro-cid-5dfgbyiq="">About Raft</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.12"><a class="outline-link" href="#our-testing-approach" data-toc-target="our-testing-approach" data-astro-cid-5dfgbyiq="">Our testing approach</a></li><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.13"><a class="outline-link" href="#results" data-toc-target="results" data-astro-cid-5dfgbyiq="">Results</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.14"><a class="outline-link" href="#hashicorp-raft" data-toc-target="hashicorp-raft" data-astro-cid-5dfgbyiq="">HashiCorp Raft</a></li><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.15"><a class="outline-link" href="#reflections" data-toc-target="reflections" data-astro-cid-5dfgbyiq="">Reflections</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.16"><a class="outline-link" href="#assumption-1-each-node-is-a-synchronous-process" data-toc-target="assumption-1-each-node-is-a-synchronous-process" data-astro-cid-5dfgbyiq="">Assumption 1: Each node is a synchronous process</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.17"><a class="outline-link" href="#assumption-2-each-response-can-be-mapped-to-a-request" data-toc-target="assumption-2-each-response-can-be-mapped-to-a-request" data-astro-cid-5dfgbyiq="">Assumption 2: Each response can be mapped to a request</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.18"><a class="outline-link" href="#assumption-3-currentterm-and-votedfor-are-consistent" data-toc-target="assumption-3-currentterm-and-votedfor-are-consistent" data-astro-cid-5dfgbyiq="">Assumption 3: currentTerm and votedFor are consistent</a></li><li class="outline-item depth-3" data-astro-cid-5dfgbyiq="" data-sid="d2eb.19"><a class="outline-link" href="#assumption-4-the-entire-protocol-is-formally-verified" data-toc-target="assumption-4-the-entire-protocol-is-formally-verified" data-astro-cid-5dfgbyiq="">Assumption 4: The entire protocol is formally verified</a></li><li class="outline-item depth-2" data-astro-cid-5dfgbyiq="" data-sid="d2eb.20"><a class="outline-link" href="#conclusion" data-toc-target="conclusion" data-astro-cid-5dfgbyiq="">Conclusion</a></li></ul></details><script>
|
||
(function () {
|
||
if (!window.matchMedia("(max-width: 768px)").matches) return;
|
||
const nodes = document.querySelectorAll("[data-outline-details]");
|
||
for (let i = 0; i < nodes.length; i++) nodes[i].removeAttribute("open");
|
||
})();
|
||
</script><script type="module">const v=()=>{const d=document.querySelector("[data-article-toc]");if(!d)return;const u=d.querySelectorAll("[data-toc-target]");if(u.length===0)return;const i=new Map;for(const t of u){const e=t.dataset.tocTarget;e&&i.set(e,t)}const n=[];for(const t of i.keys()){const e=document.getElementById(t);e&&n.push(e)}if(n.length===0)return;const r=d.querySelector("[data-outline-details]"),f=window.matchMedia("(max-width: 768px)");r&&f.addEventListener("change",t=>{t.matches?r.removeAttribute("open"):r.setAttribute("open","")});const b=window.matchMedia("(prefers-reduced-motion: reduce)");for(const t of u)t.addEventListener("click",e=>{const c=t.dataset.tocTarget;if(!c)return;const l=document.getElementById(c);if(!l||e.defaultPrevented)return;const o=e;o.metaKey||o.ctrlKey||o.shiftKey||o.altKey||(e.preventDefault(),l.scrollIntoView({behavior:b.matches?"auto":"smooth",block:"start"}),history.pushState(null,"",`#${c}`),r&&f.matches&&r.removeAttribute("open"))});let s=null;const y=t=>{if(t!==s){if(s){const e=i.get(s);e&&e.removeAttribute("aria-current")}if(t){const e=i.get(t);e&&e.setAttribute("aria-current","location")}s=t}},_=()=>f.matches?300:120;let w=[];const g=()=>{w=n.map(t=>t.getBoundingClientRect().top+window.scrollY)},E=()=>{const t=document.documentElement;if(t.scrollHeight>window.innerHeight+4&&window.innerHeight+window.scrollY>=t.scrollHeight-4)return n[n.length-1].id;const l=window.scrollY+_();let o=n[0].id;for(let a=0;a<n.length&&w[a]<=l;a++)o=n[a].id;return o};let m=null;const h=()=>{m===null&&(m=requestAnimationFrame(()=>{m=null,y(E())}))},p=()=>{g(),h()};window.addEventListener("scroll",h,{passive:!0}),window.addEventListener("resize",p,{passive:!0}),window.addEventListener("load",p,{once:!0}),g(),h()};document.readyState==="loading"?document.addEventListener("DOMContentLoaded",v,{once:!0}):v();</script> <section class="news" data-astro-cid-rg4ou2fw=""> <div class="wide-eyebrow" data-astro-cid-rg4ou2fw=""> <div class="eyebrow surface-dark" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj="" data-sid="d2eb.21"> The latest from antithesis </div> </div> </div> <div class="narrow-eyebrow" data-astro-cid-rg4ou2fw=""> <div class="eyebrow surface-dark" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj="" data-sid="d2eb.22"> The latest </div> </div> </div> <p class="news-blurb" data-astro-cid-rg4ou2fw="" data-sid="d2eb.23">
|
||
Monthly reliability and distributed systems news, curated for teams
|
||
building critical software.
|
||
</p> <div data-mkto-form="" data-mkto-state="idle" data-mkto-variant="compact" data-mkto-surface="dark" data-mkto-base="//pages.antithesis.com" data-mkto-munchkin="337-FYY-625" data-mkto-form-id="1012" data-mkto-label-submitting="Subscribing…" data-mkto-label-success="Subscribed" data-astro-cid-rg4ou2fw="true"> <form id="mktoForm_1012" aria-label="Email signup"></form> <astro-island uid="Z11QO3E" prefix="r11" component-url="/_astro/MktoSelectEnhancer.MI1SZRP2.js" component-export="default" renderer-url="/_astro/client.BoS663YN.js" props="{}" ssr="" client="load" opts="{"name":"MktoSelectEnhancer","value":true}" await-children=""><span data-mkto-select-enhancer="true" hidden=""></span><!--astro:end--></astro-island> <noscript> <p data-mkto-noscript>
|
||
Please enable JavaScript in your browser to load and submit this form.
|
||
</p> </noscript> <div data-mkto-slot="success" role="status" aria-live="polite" hidden=""> <p data-astro-cid-rg4ou2fw="" data-sid="d2eb.24">Thanks — you're subscribed.</p> </div> <div data-mkto-slot="error" role="alert" aria-live="assertive" hidden=""> <p data-astro-cid-rg4ou2fw="" data-sid="d2eb.25">Something went wrong. Please try again.</p> </div> </div> <script type="module" src="/_astro/MktoForm.astro_astro_type_script_index_0_lang.DSJkHfDD.js"></script> </section> </aside> </aside> <div class="diamond-helper article-surface" data-astro-cid-lhauwh7h=""> <div class="diamond-grid" style="--gradient-direction: to bottom; --align-pos: top; --offset-top: 16px; --offset-bottom: auto" data-astro-cid-lhauwh7h=""></div> <div class="diamond-children" data-astro-cid-lhauwh7h=""> <div class="article-body force-light" data-astro-cid-ee7emijr=""> <h2 id="introduction" data-sid="d2eb.26"><a href="#introduction" class="anchor-link">Introduction</a></h2>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/069_tw.DHr19spq_2mCqTD.webp 96w, /_astro/069_tw.DHr19spq_Z1UQeub.webp 192w" type="image/webp"> <img src="/_astro/069_tw.DHr19spq_1BL2As.jpg" srcset="/_astro/069_tw.DHr19spq_1BL2As.jpg 96w, /_astro/069_tw.DHr19spq_Z2i4KpM.jpg 192w" alt="TW Lim headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.27"> <span class="_name_1qysz_38">TW Lim</span> <span class="_title_1qysz_45">Technical Writer</span> </div> </div> </div>
|
||
<p data-sid="d2eb.28">The Raft consensus protocol is one of the foundations of the internet. Raft offers a <a href="https://github.com/ongardie/raft.tla">formal specification in TLA+</a> and <a href="https://raft.github.io/raft.pdf">a concrete, detailed implementation guide</a>, and hundreds of groups have created open-source implementations of the algorithm by following the instructions in the guide. It is, by far, the most widely used consensus algorithm in production systems.</p>
|
||
<p data-sid="d2eb.29">Despite the paper’s famously accessible style, <strong>we’ve found bugs in <em>every</em> Raft implementation we’ve tested</strong>, including HashiCorp Raft, Aeron Cluster, OpenRaft, and MicroRaft — despite the investment in formal methods, careful code review, unit testing, and years of testing in production. The bugs we found manifest as violations of Raft’s main invariant (called <em>state machine safety</em> in the paper, commonly referred to elsewhere as <em>total order delivery</em>). If you’re using a Raft implementation, you might want to check it for bugs.</p>
|
||
<p data-sid="d2eb.30">We’ve sent bug reports upstream. This isn’t intended as a critique of Raft, its authors, its implementers, or any particular implementation. Raft implementations, even with a formal specification and a detailed implementation guide, are not easy to write.</p>
|
||
<p data-sid="d2eb.31">Rather, this is a story about correctness in distributed systems — the inevitability of bugs, the inadequacy of any single approach, and the high cost of learned helplessness.</p>
|
||
<p data-sid="d2eb.32">This is a long post. The first section is a position paper, but the rest is a detailed analysis of the issues we found, using one implementation as an example, a discussion of how we found them, and <em>why</em> we think they’re there.</p>
|
||
<h2 id="why-this-matters" data-sid="d2eb.33"><a href="#why-this-matters" class="anchor-link">Why this matters</a></h2>
|
||
<p data-sid="d2eb.34">If you’ve worked on distributed systems, you’ve been part of a war room at some point (if you haven’t, don’t worry, you will be), dealing with an outage like <a href="https://blog.cloudflare.com/a-byzantine-failure-in-the-real-world/">this one</a>, or <a href="https://www.cockroachlabs.com/docs/advisories/a162085">this one</a> — both of which were caused by consensus failures. When a consensus issue results in an incident, it’s inevitably far reaching and extremely painful to root cause, replicate, and fix. Many consensus issues remain “unsolved”, because they evade reproduction.</p>
|
||
<p data-sid="d2eb.35">It’s hard to know exactly what the real world consequences of these problems are, because consensus protocols sit so low in the stack. Are they corrupting the archive of someone’s personal D&D game? Security risks at a nuclear plant? Delaying trains in Germany? It all depends on where the protocol’s deployed.</p>
|
||
<p data-sid="d2eb.36">What’s certain is that these bugs are a colossal waste of developer time, and affect millions, if not hundreds of millions, of users.</p>
|
||
<p data-sid="d2eb.37">Yet we accept consensus issues and other deep distributed systems bugs as a fact of life — but once upon a time we accepted cholera, and waiting for your turn on the mainframe, as facts of life as well. Developers deserve something better. Everyone who depends on the software we write deserves something better.</p>
|
||
<h3 id="bugs-are-not-a-fact-of-life" data-sid="d2eb.38"><a href="#bugs-are-not-a-fact-of-life" class="anchor-link">Bugs are not a fact of life</a></h3>
|
||
<p data-sid="d2eb.39">We have long accepted consensus bugs as inevitable because consensus protocols are just really, really hard to test properly. To really, thoroughly test a Raft implementation — or any distributed system — you effectively need to imagine every possible thing that could go wrong in your entire stack, and write a test to see if it will break your consensus protocol. It’s virtually impossible to write enough tests to provide this kind of assurance in critical systems.</p>
|
||
<p data-sid="d2eb.40">We get around this in two ways. First, we inflict the testing on our users, in the form of outages, downstream bugs, war rooms, and so on. It’s impossible for a team of developers to write enough tests, but with enough deployments and enough users across enough system configurations, you’re eventually going to find all the problems.</p>
|
||
<p data-sid="d2eb.41">Second, we rely on formal verification, and this is how consensus algorithms are built today. We define a model that we can mathematically <em>prove</em> to be correct, and then we… translate this perfect, platonic thing into code. Most Raft implementations are built this way.<a href="#fn-body-1" class="footnote-marker" role="doc-noteref" aria-label="Footnote 1"></a></p><div id="fn-body-1" class="footnote-body" role="doc-footnote"><div class="footnote-body-inner">
|
||
<p data-sid="d2eb.42">There are degrees here. The Raft protocol is one of very few consensus protocols that meets the strictest standard of “formal verification,” with a manual proof, a model check, and a mechanized proof-of-correctness. Every public consensus protocol we’re aware of has a manual proof/written correctness argument, but only Raft, Paxos, and MultiPaxos have mechanized proofs.</p>
|
||
</div></div>
|
||
<h3 id="specifications-are-not-code" data-sid="d2eb.43"><a href="#specifications-are-not-code" class="anchor-link">Specifications are not code</a></h3>
|
||
<p data-sid="d2eb.44">Formal verification is a great starting point, in that it helps confirm that a core design is sound. Implementing a distributed consensus protocol without starting from a formal spec would result in many orders of magnitude more bugs than any Raft implementation has.<a href="#fn-body-2" class="footnote-marker" role="doc-noteref" aria-label="Footnote 2"></a></p><div id="fn-body-2" class="footnote-body" role="doc-footnote"><div class="footnote-body-inner">
|
||
<p data-sid="d2eb.45">Conversely, one might wonder what the FoundationDB team might have done if they’d started with a formal spec.</p>
|
||
</div></div>
|
||
<p data-sid="d2eb.46">But the issues here demonstrate the difficulties inherent in going from a formal specification to actual production code. As long as the implementations are being done by unreliable, imperfect programmers (whether humans or LLMs), the actual code, and the systems using it, will only be as solid as the implementors’ assumptions — not the formally verified model.</p>
|
||
<p data-sid="d2eb.47">Furthermore, formal specifications are rarely truly complete — in the case of Raft, the TLA spec covers the core protocol, but doesn’t speak to details like <code>installSnapshot</code>, or replica replacement, or handling network packet corruption.</p>
|
||
<h3 id="testing-can-actually-be-simple" data-sid="d2eb.48"><a href="#testing-can-actually-be-simple" class="anchor-link">Testing can actually be simple</a></h3>
|
||
<p data-sid="d2eb.49">Surfacing these bugs didn’t require particularly deep knowledge of consensus or distributed systems. We found these using a simple approach, which a junior engineer could implement in less than a day, literally the simplest state-machine replication workload we could come up with. The key is that this is happening while the system is running in Antithesis, subject to the kind of faults that happen in a real world environment.</p>
|
||
<p data-sid="d2eb.50">We want to emphasize this point because all too often, we encounter a learned helplessness around testing complex systems. Our profession thinks (with some justification) that writing tests for distributed systems requires more expertise, time, or tokens than we have. This results in a state of perpetual under-testing, which in turn results in extraordinary amounts of developer time being wasted on firefighting (to say nothing of the mental and emotional exhaustion).</p>
|
||
<p data-sid="d2eb.51">Developers deserve something better. Everyone who depends on the software we write deserves something better.</p>
|
||
<h2 id="testing-raft" data-sid="d2eb.52"><a href="#testing-raft" class="anchor-link">Testing Raft</a></h2>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/001_marco_primi.C8sTreDD_ZgooaE.webp 96w, /_astro/001_marco_primi.C8sTreDD_rcfhT.webp 192w" type="image/webp"> <img src="/_astro/001_marco_primi.C8sTreDD_1W9FFT.jpg" srcset="/_astro/001_marco_primi.C8sTreDD_1W9FFT.jpg 96w, /_astro/001_marco_primi.C8sTreDD_ft7t5.jpg 192w" alt="Marco Primi headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.53"> <span class="_name_1qysz_38">Marco Primi</span> <span class="_title_1qysz_45">Distributed Systems Engineer</span> </div> </div> </div>
|
||
|
||
<h3 id="about-antithesis" data-sid="d2eb.54"><a href="#about-antithesis" class="anchor-link">About Antithesis</a></h3>
|
||
<p data-sid="d2eb.55">Antithesis is an autonomous testing platform that runs distributed systems in a deterministic simulation environment, with randomly generated inputs, under aggressive fault injection. To use Antithesis, you deploy a full distributed system to the simulation environment along with a workload — a client that drives the system under test.</p>
|
||
<p data-sid="d2eb.56">Antithesis exposes the system under test to the kind of unpredictable turbulence it will experience in production, within the safety of a simulation environment. By randomizing the inputs and faults, and intelligently searching the state space of the system to see if system invariants are ever violated.</p>
|
||
<p data-sid="d2eb.57">We maintain an internal curriculum of systems and bugs we use to benchmark Antithesis’ bug-finding performance.<a href="#fn-body-3" class="footnote-marker" role="doc-noteref" aria-label="Footnote 3"></a> We’ve been adding consensus benchmarks to the curriculum, so we’ve been testing a lot of Raft implementations.</p><div id="fn-body-3" class="footnote-body" role="doc-footnote"><div class="footnote-body-inner">
|
||
<p data-sid="d2eb.58">Part of the difficulty of building something unique is that you also need to build a way to measure its performance.</p>
|
||
</div></div>
|
||
|
||
|
||
<h3 id="about-raft" data-sid="d2eb.59"><a href="#about-raft" class="anchor-link">About Raft</a></h3>
|
||
<p data-sid="d2eb.60">A common architectural pattern in distributed systems is state machine replication (SMR): all replicas in the system run copies of the same deterministic state machine, and the same sequence of commands is delivered to all of them to transform the data/state. This causes the replicas to progress in soft-lockstep — the state after applying N commands is <em>consistent</em> across all replicas, and all replicas <em>eventually</em> apply all commands.</p>
|
||
<p data-sid="d2eb.61">Distributed databases (FoundationDB, Aerospike, etc.), message queues (Kafka, NATS, etc.), key-value stores (etcd, Zookeeper), blockchains (Bitcoin, Ethereum), and many other systems are based on SMR.</p>
|
||
<p data-sid="d2eb.62">A fundamental requirement for implementing SMR is that all replicas <em>must</em> receive the same set of commands in the same order — total order delivery. Total order delivery is simple to describe, but hard to architect in the face of network turbulence, process crashes, and disk failures.</p>
|
||
<p data-sid="d2eb.63">Because total order delivery needs to be <em>guaranteed</em> for SMR to work, most systems rely on one of a handful of messaging abstractions, with atomic broadcast, also known as total order broadcast, being the most common. Raft is viewed as the friendliest atomic broadcast protocol, Paxos and viewstamped replication are also in wide use.</p>
|
||
|
||
<h3 id="our-testing-approach" data-sid="d2eb.64"><a href="#our-testing-approach" class="anchor-link">Our testing approach</a></h3>
|
||
<p data-sid="d2eb.65">To test a Raft implementation, we run a 3-node Raft cluster in Antithesis with a simple workload we call <a href="/docs/resources/chain-of-blocks/">Chain of Blocks</a>.</p>
|
||
<p data-sid="d2eb.66">Chain of Blocks tests Raft’s most important invariant: after N commands are applied, the state of all replicas matches. It consists of two trivially simple components:</p>
|
||
<ul>
|
||
<li data-sid="d2eb.67">A single-state state machine that just hashes the bytes of incoming commands. After each applied command, the state consists of <number of commands applied, current hash>. This is sufficient to allow us to observe state divergence between replicas.</li>
|
||
<li data-sid="d2eb.68">A stateless client whose only responsibility is submitting new commands that consist of random arrays of bytes.</li>
|
||
</ul>
|
||
<p data-sid="d2eb.69">You can read more about this workload, and see a sample implementation, <a href="https://github.com/antithesishq/hashicorp-raft-poc">here</a>.</p>
|
||
<p data-sid="d2eb.70">Components like Raft are developed and reviewed by experts and battle-hardened by years of exposure. So it’s striking to us that this single, simple testing strategy — that a junior engineer could write in an afternoon (or Claude could write for a handful of tokens) — still finds bugs when it’s run in Antithesis.</p>
|
||
<h2 id="results" data-sid="d2eb.71"><a href="#results" class="anchor-link">Results</a></h2>
|
||
<p data-sid="d2eb.72">In all cases, network partitions and turbulence were sufficient to surface examples of divergence (i.e. no node kill/restart required, or disk corruption, or other faults)</p>
|
||
<p data-sid="d2eb.73">Here’s an example snippet from logs that shows a state machine divergence:</p>
|
||
<div class="expressive-code"><link rel="stylesheet" href="/_astro/ec.p4j2x.css"><script type="module" src="/_astro/ec.0vx5m.js"></script><figure class="frame"><figcaption class="header"></figcaption><pre data-language="plaintext"><code><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">[node1]: Applied block 244 (2ad8d...) state: 01fd753a => faf6ba1e</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">[node2]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">[node3]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c</span></div></div></code></pre><div class="copy"><div aria-live="polite"></div><button title="Copy to clipboard" data-copied="Copied!" data-code="[node1]: Applied block 244 (2ad8d...) state: 01fd753a => faf6ba1e[node2]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c[node3]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c"><div></div></button></div></figure></div>
|
||
<p data-sid="d2eb.74">After applying 243 blocks, the hashes of all replicas matched (0x01fd753a). Node1 then applies a different 244th command from Node2 and Node3 (0x2ad8d… vs 0xc92fb…). This results in a different state hash after 244 commands applied (0xfaf6ba1e vs 0xdab0977c), violating the primary safety property of Raft (and the underlying atomic broadcast): that all replicas apply the same sequence of command in the same order.</p>
|
||
<p data-sid="d2eb.75">As an example, here’s a detailed look at the bugs we’ve found in one notable open-source Raft implementation during this process. We emphasize that we’ve found similar bugs in other implementations as well, but are going deep rather than broad here and only presenting one set of bugs to keep the length of this post somewhat manageable.</p>
|
||
<p data-sid="d2eb.76">We plan to update this post with details of bugs in the other Raft implementations we’ve worked with.</p>
|
||
<h3 id="hashicorp-raft" data-sid="d2eb.77"><a href="#hashicorp-raft" class="anchor-link">HashiCorp Raft</a></h3>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/rohan-padhye.C9feRA4F_Y0v79.webp 96w, /_astro/rohan-padhye.C9feRA4F_Z1JWarM.webp 192w" type="image/webp"> <img src="/_astro/rohan-padhye.C9feRA4F_Z1va7ov.jpg" srcset="/_astro/rohan-padhye.C9feRA4F_Z1va7ov.jpg 96w, /_astro/rohan-padhye.C9feRA4F_16wed6.jpg 192w" alt="Rohan Padhye headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.78"> <span class="_name_1qysz_38">Rohan Padhye</span> <span class="_title_1qysz_45">Research Fellow</span> </div> </div> </div>
|
||
<p data-sid="d2eb.79">HashiCorp Raft is a mature, popular open-source Raft implementation, and the foundational consensus engine underpinning widely-used production infrastructure tools like Consul, Nomad, and Vault.</p>
|
||
<p data-sid="d2eb.80"><em>We do not believe HashiCorp Raft is any less reliable than the other implementations we tested, or that the bugs in HashiCorp Raft are more serious than the bugs in other implementations</em> — they all violate the same core property of state machine safety.</p>
|
||
<p data-sid="d2eb.81">We found three distinct bugs in total: one causes numerous safety violations (i.e., data divergence as described above) and two cause liveness violations (where some nodes or the whole cluster cannot make progress unless an operator intervenes). The Chain of Blocks implementation we used is <a href="https://github.com/antithesishq/hashicorp-raft-poc">here</a>.</p>
|
||
<p data-sid="d2eb.82">When run with Antithesis for <em>just one hour</em> of testing, we see a report that looks like this:</p>
|
||
<figure class="_figure_55xv6_5"> <div class="media-frame media-frame-sized" style="--ar-num:4.551111111111111;--nat-w:2048px;"> <picture> <source srcset="/_astro/findings.CKPiWc3M_ZkMPNx.webp 640w, /_astro/findings.CKPiWc3M_ZHnCDa.webp 1024w, /_astro/findings.CKPiWc3M_1YxHJ0.webp 1536w, /_astro/findings.CKPiWc3M_8fLlj.webp 2048w" type="image/webp"> <img src="/_astro/findings.CKPiWc3M_ZcPAsG.png" srcset="/_astro/findings.CKPiWc3M_Z29xFT6.png 640w, /_astro/findings.CKPiWc3M_Z13u0sa.png 1024w, /_astro/findings.CKPiWc3M_1DrkU0.png 1536w, /_astro/findings.CKPiWc3M_ZcPAsG.png 2048w" alt="Antithesis report." sizes="(min-width: 2048px) 2048px, 100vw" loading="lazy" decoding="async" data-astro-image="constrained" data-astro-image-fit="cover" data-astro-image-pos="center" width="2048" height="450" class="_image_55xv6_13"> </picture> </div> </figure>
|
||
<h4 id="technical-primer-on-raft" data-sid="d2eb.83"><a href="#technical-primer-on-raft" class="anchor-link">Technical primer on Raft</a></h4>
|
||
<p data-sid="d2eb.84">To better understand the nature of these bugs, we should define some terms used frequently in the <a href="https://raft.github.io/raft.pdf">Raft paper</a>:</p>
|
||
<ul>
|
||
<li data-sid="d2eb.85">“Term”, “Leader”, “Follower”, “Election” + “RequestVote” RPC: Raft ensures consensus among a cluster of distributed nodes by dividing the protocol into strictly increasing <em>terms</em> starting with term=1. In each term, the nodes attempt to elect exactly one node as the <em>leader</em> by taking a majority vote; all other nodes are called <em>followers</em>. Leader election is conducted using a remote-procedure call (RPC) called <em>RequestVote</em>.</li>
|
||
<li data-sid="d2eb.86">“Log”, “Commit”, “Replication” + “AppendEntries” RPC: Each node maintains a replicated <em>log</em> of data entries (e.g., the commands issued by clients), some prefix of which is said to be <em>committed</em>; that is, the node’s state machine is updated when an entry <em>commits</em>. When a client sends some command to the cluster, only the current leader can service this request, and the leader <em>replicates</em> the associated data entry to all its followers via an RPC called <em>AppendEntries</em>. When a majority of nodes in the cluster have replicated the same data entry in their logs, the leader <em>commits</em> it to its own state machine and broadcasts this fact to its followers. If some follower nodes fall behind because of network faults, or if their entry logs have uncommitted data from previous terms, then the current leader can always catch them up via more AppendEntries RPCs. The AppendEntries RPC is also used as a regular heartbeat mechanism to broadcast that a leader is active.</li>
|
||
<li data-sid="d2eb.87">“Compaction”, “Snapshot” + “InstallSnapshot” RPC: When the entry log grows too large, a Raft node can choose to <em>compact</em> all the committed entries in the log and only store on disk a <em>snapshot</em> of the state machine until that point. If a leader node needs to replicate data entries to followers via AppendEntries but its log has already been compacted, it can instead issue an <em>InstallSnapshot</em> RPC to transit the entire state machine to the follower.</li>
|
||
</ul>
|
||
<h4 id="bug-1---broken-consensus-due-to-async-heartbeats" data-sid="d2eb.88"><a href="https://github.com/hashicorp/raft/issues/695"><strong>Bug 1 - Broken Consensus due to Async Heartbeats</strong></a></h4>
|
||
<p data-sid="d2eb.89">This is the most serious bug we have found. It can affect four of the five safety properties from the <a href="https://raft.github.io/raft.pdf#page=5">Raft paper (Image 3)</a>:</p>
|
||
<ul class="contains-task-list">
|
||
<li class="task-list-item" data-sid="d2eb.90"><input type="checkbox" checked="" disabled=""> <strong>Log Matching</strong> (violated through mechanism A - seen in the report above)</li>
|
||
<li class="task-list-item" data-sid="d2eb.91"><input type="checkbox" checked="" disabled=""> <strong>Leader Completeness</strong> (violated through mechanism A - seen in the report above)</li>
|
||
<li class="task-list-item" data-sid="d2eb.92"><input type="checkbox" checked="" disabled=""> <strong>State Machine Safety</strong> (violated through mechanism A - seen in the report above)</li>
|
||
<li class="task-list-item" data-sid="d2eb.93"><input type="checkbox" checked="" disabled=""> <strong>Election Safety</strong> (violated through mechanism B - not in the report shown above)</li>
|
||
<li class="task-list-item" data-sid="d2eb.94"><input type="checkbox" disabled=""> <strong>Leader Append-Only</strong> (not violated)</li>
|
||
</ul>
|
||
<h5 id="root-cause-and-trigger" data-sid="d2eb.95"><a href="#root-cause-and-trigger" class="anchor-link">Root Cause and Trigger</a></h5>
|
||
<ul>
|
||
<li data-sid="d2eb.96">The Raft paper assumes that all the operations (handling RPCs, client requests, elections, etc.) are atomic and don’t interleave with each other. Essentially, every node in the protocol is a finite-state machine.</li>
|
||
<li data-sid="d2eb.97">In HashiCorp raft, most state-changing operations are handled by a big switch-loop in the main thread, with several other floating goroutines doing async work that should not affect protocol state (e.g., peer-peer “replication” routines for dispatching append-entries, and per-connection “transport” goroutines that listen for incoming RPCs and hand them off to the main thread for processing).</li>
|
||
<li data-sid="d2eb.98">EXCEPT there is an <a href="https://github.com/hashicorp/raft/blob/4c8f61ac9255bb95fb3b8319dfcf0ae53ab325b6/docs/divergence.md#asynchronous-heartbeats">optimization that diverges from the protocol</a>: incoming heart-beat messages (i.e., AppendEntries without an entry) are handled on the I/O “transport” thread itself, instead of queuing it up for the main thread’s loop like with other RPCs. Presumably, this is to quickly reset the keep-alive timers and reduce spurious re-elections.</li>
|
||
<li data-sid="d2eb.99">CAVEAT is that an incoming heart-beat message (like any other AppendEntries RPC) can change the state if it carries a new term when someone else was elected leader, and this bumps up the global currentTerm which everything else in the main thread relies on, and also sets the current state to be FOLLOWER. It is definitely not sound to perform these state changes concurrently with the main thread, and it can lead to different types of race condition bugs.</li>
|
||
</ul>
|
||
<h5 id="mechanism-a-incoming-heartbeat-races-with-dispatchlogs-on-main-thread" data-sid="d2eb.100"><a href="#mechanism-a-incoming-heartbeat-races-with-dispatchlogs-on-main-thread" class="anchor-link">Mechanism A - Incoming heartbeat races with dispatchLogs() on main thread</a></h5>
|
||
<p data-sid="d2eb.101">Here’s how the bug causes divergence in a 3-node setup A/B/C:</p>
|
||
<ul>
|
||
<li data-sid="d2eb.102">Assume the network link between node A and node B is down.</li>
|
||
<li data-sid="d2eb.103">Node A becomes candidate for term T, requests votes (eventually gets it from Node C)</li>
|
||
<li data-sid="d2eb.104">Node B also runs for term T but no votes</li>
|
||
<li data-sid="d2eb.105">Node B becomes candidate for term T+1, requests votes (gets it from Node C)</li>
|
||
<li data-sid="d2eb.106">Node B wins election for term T+1</li>
|
||
<li data-sid="d2eb.107">Node A wins election for term T (just received the old vote from Node C)</li>
|
||
<li data-sid="d2eb.108">Node B sends out heart-beat AppendEntries with term=T+1, which Node A doesn’t immediately receive</li>
|
||
<li data-sid="d2eb.109">Node A gets a client request to apply a new data entry X, and it still thinks it is a leader for term T, so on the main thread it prepares to create a log entry (data=X, term=T) and send out AppendEntries to peers.
|
||
<ul>
|
||
<li data-sid="d2eb.110">HOWEVER: Just before it can create the log entry, the heart-beat from Node B sent in step 7 above reaches, setting currentTerm=T+1. Because this is done on the fast-path on the network-transport thread, it races with the main thread.</li>
|
||
<li data-sid="d2eb.111">The main thread ends up preparing a log entry (data=X, term=T+1) and also dispatching AppendEntries with these values before the next main-loop iteration where it realizes it is actually now a follower for term T+1.</li>
|
||
</ul>
|
||
</li>
|
||
<li data-sid="d2eb.112">Things get really bad from here. Some nodes apply this bogus data=X, term=T+1 to their logs, while others follow whatever Node B (the true leader for term T+1) says, e.g., they might apply data=Y at the same index with term=T+1. Logs diverge in data but get committed since all say term T+1 for the same index. State machines diverge.</li>
|
||
</ul>
|
||
<h5 id="mechanism-b-incoming-heartbeat-races-with-requestvote-on-main-thread" data-sid="d2eb.113"><a href="#mechanism-b-incoming-heartbeat-races-with-requestvote-on-main-thread" class="anchor-link">Mechanism B - Incoming heartbeat races with requestVote() on main thread</a></h5>
|
||
<p data-sid="d2eb.114">The same bug can cause another kind of safety violation when the async heartbeat handler races with a concurrent handler for the RequestVote RPC on the main thread. If both the incoming heartbeat and the RequestVote carry higher-numbered but different terms T1 and T2 respectively — this is possible when the receiver just recovers from a fault and is catching up to queued messages from peers — and if T1 is less than T2, then it is possible for the receiver to (i) realize the heartbeat’s term T1 is higher than its current term, then (2) on the main thread processing RequestVote realize that T2 is higher than its current term and so set its current term to T2 and then grant a vote; and then (3) back on the heartbeat handler’s thread set its current term to the lower value T1. Needless to say, it should never be possible for a node that has granted a vote for term T2 to regress its current term back down to a lower value T1! When this node at some later point increments its term to T2 again, it has no memory of the fact that it has already voted in this term.</p>
|
||
<p data-sid="d2eb.115">In summary, the race can eventually cause a node to grant two votes in the same term (T2 above), which in the worst case can lead to two different nodes being elected as leader in the same term! Here are some sample log messages from HashiCorp Raft when we have observed this race condition and its violation of election safety:</p>
|
||
<div class="expressive-code"><figure class="frame"><figcaption class="header"></figcaption><pre data-language="plaintext"><code><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">20:11:59.941133 [DEBUG] node-1: vote granted: from="node-2" tally=2 term=286</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">[...]</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">20:11:59.941133 [INFO] node-1: election won: tally=2 term=286</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">[...]</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">20:11:59.944273 [DEBUG] node-0: vote granted: from="node-2" tally=2 term=286</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">[...]</span></div></div><div class="ec-line"><div class="code"><span class="indent"><span style="--0:#a9b1d6;--1:#4c4f69"> </span></span><span style="--0:#a9b1d6;--1:#4c4f69">20:11:59.944274 [INFO] node-0: election won: tally=2 term=286</span></div></div></code></pre><div class="copy"><div aria-live="polite"></div><button title="Copy to clipboard" data-copied="Copied!" data-code=" 20:11:59.941133 [DEBUG] node-1: vote granted: from="node-2" tally=2 term=286 [...] 20:11:59.941133 [INFO] node-1: election won: tally=2 term=286 [...] 20:11:59.944273 [DEBUG] node-0: vote granted: from="node-2" tally=2 term=286 [...] 20:11:59.944274 [INFO] node-0: election won: tally=2 term=286"><div></div></button></div></figure></div>
|
||
<h4 id="bug-2---deadlock-after-leadership-transfer" data-sid="d2eb.116"><a href="https://github.com/hashicorp/raft/issues/696"><strong>Bug 2 - Deadlock after Leadership Transfer</strong></a></h4>
|
||
<p data-sid="d2eb.117">This bug causes a liveness issue — a leader node is unable to service client requests or commit new entries while the cluster is healthy. The root cause is a deadlock during a leadership transfer operation (<a href="https://developer.hashicorp.com/consul/commands/operator/raft#transfer-leader">a Raft protocol extension used by Consul</a> where you can ask a current leader to transfer leadership to someone else, say for upgrades) that does not immediately signal any warnings but bites you way into the future by getting the whole cluster stuck.</p>
|
||
<ul>
|
||
<li data-sid="d2eb.118">When you initiate a leadership transfer from A to B the current leader A first tries to get B’s logs up to date via an async replication thread.</li>
|
||
<li data-sid="d2eb.119">The leadership transfer logic is a separate goroutine that waits for this replication before telling B to take over.</li>
|
||
<li data-sid="d2eb.120">While all this is happening, A might have to step-down as leader for unrelated reasons (e.g., the lease timer runs out, or it cannot reach a quorum due to network) and say another node C becomes leader.</li>
|
||
<li data-sid="d2eb.121">When A steps-down as leader, it aborts all replication threads (including the A—>B catchup) but the leadership transfer goroutine is still blocked waiting for it to complete (an implementation bug).</li>
|
||
</ul>
|
||
<p data-sid="d2eb.122">There is no problem so far, because C is the new leader and it does its job for a while.</p>
|
||
<ul>
|
||
<li data-sid="d2eb.123">Unfortunately, the leadership transfer goroutine in A has set a global flag “<em>leadership transfer in progress</em>” and this flag cannot be unset until it is unblocked… but it never will be!!!</li>
|
||
<li data-sid="d2eb.124">Crucially, this flag does not prevent it from participating in elections and the flag does not get reset if it wins a future election.</li>
|
||
<li data-sid="d2eb.125">So in the future, A can legitimately get re-elected as leader but it will refuse to accept any client requests and stall on future commits with the reason “<em>leadership transfer in progress</em>”.</li>
|
||
<li data-sid="d2eb.126">When the network is healthy and A is a leader, there is no way to get out of this other than rebooting the node A to clear the flag.</li>
|
||
</ul>
|
||
<p data-sid="d2eb.127">We caught this using an Antithesis <a href="https://antithesis.com/docs/product/writing_tests/test_templates/test_composer_reference/#eventually-command">eventually test command</a> that checks for commit progress after fault injection is turned off.</p>
|
||
<h4 id="bug-3---livelock-in-snapshot-installation" data-sid="d2eb.128"><a href="https://github.com/hashicorp/raft/issues/697"><strong>Bug 3 - Livelock in Snapshot Installation</strong></a></h4>
|
||
<p data-sid="d2eb.129">This bug causes a liveness issue: a follower node becomes unable to replicate log entries and is effectively not able to participate in the consensus protocol. The bug can also cause resource exhaustion, where the node starts creating a potentially unbounded number of temporary snapshot files on disk.</p>
|
||
<p data-sid="d2eb.130">The root cause for this bug is painfully simple: in the version of HashiCorp Raft we tested, the implementation of the InstallSnapshot RPC simply does not follow Rule 7 from <a href="https://raft.github.io/raft.pdf#page=12">Image 13 in the Raft paper</a> which handles the case when an incoming snapshot represents a state that diverges from the receiver’s uncommitted log entries. In the paper, Rule 7 says:</p>
|
||
<p data-sid="d2eb.131">“<em>discard the entire log</em>”</p>
|
||
<p data-sid="d2eb.132">HashiCorp Raft does not discard the existing log, and so after installing the snapshot its state machine can, in some cases, disagree with the data in its own (stale) log entries.</p>
|
||
<p data-sid="d2eb.133">At first, this might sound benign because the state machine should be the final source of truth. However, when the node receives a subsequent <code>AppendEntries</code> RPC from the leader, it faithfully implements a part of the protocol (Rule 2) that says: “[reject <code>AppendEntries</code>] if log doesn’t contain an entry at <code>prevLogIndex</code> whose term matches <code>prevLogTerm</code>”. So, because of the stale logs, the follower rejects subsequent <code>AppendEntries</code>, causing the leader to respond with a new <code>InstallSnapshot</code>, and this cycle goes on forever.</p>
|
||
<p data-sid="d2eb.134">We caught this using an Antithesis <a href="https://antithesis.com/docs/product/writing_tests/test_templates/test_composer_reference/#eventually-command">eventually test command</a> that checks for state-machine convergence after fault injection is turned off. Sample logs from a test run look like this:</p>
|
||
<div class="expressive-code"><figure class="frame"><figcaption class="header"></figcaption><pre data-language="plaintext"><code><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:13.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:15.954Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:48504->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:23.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:26.038Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:35706->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:33.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:36.135Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30394]: read tcp 10.89.0.7:37032->10.89.0.4:8300: i/o timeout"`</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:43.072Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:46.249Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29575]: read tcp 10.89.0.7:54324->10.89.0.4:8300: i/o timeout"`</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:53.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:17:56.381Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30303]: read tcp 10.89.0.7:57842->10.89.0.4:8300: i/o timeout"`</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:03.072Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:06.626Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31122]: read tcp 10.89.0.7:46978->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:13.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:17.032Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30758]: read tcp 10.89.0.7:54192->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:23.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:27.745Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31850]: read tcp 10.89.0.7:36218->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:33.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:39.083Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 33943]: read tcp 10.89.0.7:53700->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:43.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:51.725Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 38402]: read tcp 10.89.0.7:52390->10.89.0.4:8300: i/o timeout"</span></div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:53.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"</span></div></div><div class="ec-line"><div class="code">
|
||
</div></div><div class="ec-line"><div class="code"><span style="--0:#a9b1d6;--1:#4c4f69">2026-07-07T17:18:55.497Z [ERROR] eventually-fsm-convergence: convergence-check give-up; cluster healthy but did not converge: attempts_taken=24 per_node="map[raft-node-0:8400:map[applied_index:534 last_index:535 reachable:true state:Follower term:74 value:23641] raft-node-1:8400:map[applied_index:569 last_index:569 reachable:true state:Leader term:74 value:25232] raft-node-2:8400:map[applied_index:569 last_index:569 reachable:true state:Follower term:74 value:25232]]"</span></div></div></code></pre><div class="copy"><div aria-live="polite"></div><button title="Copy to clipboard" data-copied="Copied!" data-code="2026-07-07T17:17:13.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:17:15.954Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:48504->10.89.0.4:8300: i/o timeout"2026-07-07T17:17:23.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:17:26.038Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:35706->10.89.0.4:8300: i/o timeout"2026-07-07T17:17:33.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:17:36.135Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30394]: read tcp 10.89.0.7:37032->10.89.0.4:8300: i/o timeout"`2026-07-07T17:17:43.072Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:17:46.249Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29575]: read tcp 10.89.0.7:54324->10.89.0.4:8300: i/o timeout"`2026-07-07T17:17:53.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:17:56.381Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30303]: read tcp 10.89.0.7:57842->10.89.0.4:8300: i/o timeout"`2026-07-07T17:18:03.072Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:06.626Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31122]: read tcp 10.89.0.7:46978->10.89.0.4:8300: i/o timeout"2026-07-07T17:18:13.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:17.032Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30758]: read tcp 10.89.0.7:54192->10.89.0.4:8300: i/o timeout"2026-07-07T17:18:23.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:27.745Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31850]: read tcp 10.89.0.7:36218->10.89.0.4:8300: i/o timeout"2026-07-07T17:18:33.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:39.083Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 33943]: read tcp 10.89.0.7:53700->10.89.0.4:8300: i/o timeout"2026-07-07T17:18:43.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:51.725Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 38402]: read tcp 10.89.0.7:52390->10.89.0.4:8300: i/o timeout"2026-07-07T17:18:53.073Z [INFO] node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"2026-07-07T17:18:55.497Z [ERROR] eventually-fsm-convergence: convergence-check give-up; cluster healthy but did not converge: attempts_taken=24 per_node="map[raft-node-0:8400:map[applied_index:534 last_index:535 reachable:true state:Follower term:74 value:23641] raft-node-1:8400:map[applied_index:569 last_index:569 reachable:true state:Leader term:74 value:25232] raft-node-2:8400:map[applied_index:569 last_index:569 reachable:true state:Follower term:74 value:25232]]""><div></div></button></div></figure></div>
|
||
<h2 id="reflections" data-sid="d2eb.135"><a href="#reflections" class="anchor-link">Reflections</a></h2>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/069_tw.DHr19spq_2mCqTD.webp 96w, /_astro/069_tw.DHr19spq_Z1UQeub.webp 192w" type="image/webp"> <img src="/_astro/069_tw.DHr19spq_1BL2As.jpg" srcset="/_astro/069_tw.DHr19spq_1BL2As.jpg 96w, /_astro/069_tw.DHr19spq_Z2i4KpM.jpg 192w" alt="TW Lim headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.136"> <span class="_name_1qysz_38">TW Lim</span> <span class="_title_1qysz_45">Technical Writer</span> </div> </div> </div>
|
||
<p data-sid="d2eb.137">If there is a single lesson to be learned here, it’s that formal methods alone cannot ensure that software works, because the formal specification still needs to be implemented, and even if you have mechanized verification, you’re verifying the model and not the implementation itself.</p>
|
||
<p data-sid="d2eb.138">We believe formal methods <em>are</em> useful and necessary — they can confirm the basic soundness of a design, and provide a map that saves engineers from many of the errors that can arise in the implementation of a complex system.</p>
|
||
<p data-sid="d2eb.139">But as these bugs show, errors continue to arise when translating the formal specification to production code. In the course of our work with various Raft implementations, we identified a number of assumptions in the Raft paper that remain implicit. An implementer who misses any of these details is likely to run into trouble.</p>
|
||
<h3 id="assumption-1-each-node-is-a-synchronous-process" data-sid="d2eb.140"><a href="#assumption-1-each-node-is-a-synchronous-process" class="anchor-link">Assumption 1: Each node is a synchronous process</a></h3>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/001_marco_primi.C8sTreDD_ZgooaE.webp 96w, /_astro/001_marco_primi.C8sTreDD_rcfhT.webp 192w" type="image/webp"> <img src="/_astro/001_marco_primi.C8sTreDD_1W9FFT.jpg" srcset="/_astro/001_marco_primi.C8sTreDD_1W9FFT.jpg 96w, /_astro/001_marco_primi.C8sTreDD_ft7t5.jpg 192w" alt="Marco Primi headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.141"> <span class="_name_1qysz_38">Marco Primi</span> <span class="_title_1qysz_45">Distributed Systems Engineer</span> </div> </div> </div>
|
||
<p data-sid="d2eb.142">The paper implicitly assumes that each node is a synchronous process, performing atomic state transitions when handling RPCs and updating its own internal state. The <a href="https://github.com/ongardie/raft.tla">TLA+ spec</a> is designed as such.</p>
|
||
<p data-sid="d2eb.143">At the same time, none of the implementations we’ve looked at have actually been a synchronous process, and there’s no explicit guidance in the implementation guide as to whether and how one can deviate from the synchronous design.</p>
|
||
<p data-sid="d2eb.144">Consider the following situation:
|
||
Can a leader with an outstanding RPC request respond to a vote, or does it need to wait for a <code>response||timeout</code>? Or should it respond, shut down the request and disregard a future response in order to stay correct?</p>
|
||
<p data-sid="d2eb.145">HashiCorp Raft is <em>mostly</em> synchronous in handling RPCs, with a single thread in a select loop, except when it isn’t — it does asynchronous heartbeat handling, bypassing its main loop, and this is what allows Bug #1 to creep in.</p>
|
||
<h3 id="assumption-2-each-response-can-be-mapped-to-a-request" data-sid="d2eb.146"><a href="#assumption-2-each-response-can-be-mapped-to-a-request" class="anchor-link">Assumption 2: Each response can be mapped to a request</a></h3>
|
||
<p data-sid="d2eb.147">In the Raft paper, every call is made using RPC, which means that every response can be mapped to a request.</p>
|
||
<p data-sid="d2eb.148">If one implements Raft on top of simple TCP or UDP, and doesn’t realize that request/response correlation is a crucial part of correctness, bad stuff can easily happen.</p>
|
||
<p data-sid="d2eb.149">If you’re not working in a language with a nice RPC library, it’s not obvious how to establish this correspondence. For example, the Raft authors have a simulation on their <a href="https://raft.github.io/">website</a>, which for obvious reasons is often considered a demo/canonical implementation even though they’ve never described it as such. But even their own implementation deviates from the protocol and <a href="https://github.com/ongardie/raftscope/blob/5b0c10ab51f873721895e7470b49e04c94bf826f/raft.js#L215C5-L215C15">includes an extra <code>matchIndex</code> field in the AppendEntries response</a> in order to avoid matching requests to responses.</p>
|
||
<h3 id="assumption-3-currentterm-and-votedfor-are-consistent" data-sid="d2eb.150"><a href="#assumption-3-currentterm-and-votedfor-are-consistent" class="anchor-link">Assumption 3: <code>currentTerm</code> and <code>votedFor</code> are consistent</a></h3>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/rohan-padhye.C9feRA4F_Y0v79.webp 96w, /_astro/rohan-padhye.C9feRA4F_Z1JWarM.webp 192w" type="image/webp"> <img src="/_astro/rohan-padhye.C9feRA4F_Z1va7ov.jpg" srcset="/_astro/rohan-padhye.C9feRA4F_Z1va7ov.jpg 96w, /_astro/rohan-padhye.C9feRA4F_16wed6.jpg 192w" alt="Rohan Padhye headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.151"> <span class="_name_1qysz_38">Rohan Padhye</span> <span class="_title_1qysz_45">Research Fellow</span> </div> </div> </div>
|
||
<p data-sid="d2eb.152">Image 2 of the Raft paper states:</p>
|
||
<figure class="_figure_55xv6_5"> <div class="media-frame media-frame-sized" style="--ar-num:2.051948051948052;--nat-w:632px;"> <picture> <source srcset="/_astro/raft_paper_state.CAYonghL_2pVtCF.webp 632w" type="image/webp"> <img src="/_astro/raft_paper_state.CAYonghL_Z1reAW3.png" srcset="/_astro/raft_paper_state.CAYonghL_Z1reAW3.png 632w" alt="Raft paper figure 2 snippet." sizes="(min-width: 632px) 632px, 100vw" loading="lazy" decoding="async" data-astro-image="constrained" data-astro-image-fit="cover" data-astro-image-pos="center" width="632" height="308" class="_image_55xv6_13"> </picture> </div> </figure> <script type="module" src="/_astro/index.astro_astro_type_script_index_0_lang.BjpKTqc4.js"></script>
|
||
<p data-sid="d2eb.153">One key assumption is that <code>currentTerm</code> and <code>votedFor</code> are consistent, because the latter records the vote in the current term. If these go out of sync bad things can happen, especially if <code>votedFor</code> is null.</p>
|
||
<p data-sid="d2eb.154">For safety, the writing of these values to persistent storage should be done atomically. But in the protocol, these values actually change at different places, so ensuring that both values are updated together is subtle.</p>
|
||
<p data-sid="d2eb.155">The online simulator in JavaScript does not actually distinguish persistent state from in-memory state, so there is no “reference implementation” of how to do this.</p>
|
||
<p data-sid="d2eb.156">HashiCorp Raft, for instance, deviates from the protocol and non-atomically stores three separate values for <code>currentTerm</code>, <code>lastVoteTerm</code> and <code>lastVoteCand</code>, with a worst-case risk to performance but not safety (i.e., it might persist an updated <code>lastVoteTerm</code> and then crash before updating <code>lastVoteCand</code>, but when it restarts it will just have a pre-determined vote for that term instead of choosing a candidate as normal).</p>
|
||
<h3 id="assumption-4-the-entire-protocol-is-formally-verified" data-sid="d2eb.157"><a href="#assumption-4-the-entire-protocol-is-formally-verified" class="anchor-link">Assumption 4: The <em>entire</em> protocol is formally verified</a></h3>
|
||
<p data-sid="d2eb.158">Figures 2 and 13 in the Raft paper state, respectively:</p>
|
||
<figure class="_figure_55xv6_5"> <div class="media-frame media-frame-sized" style="--ar-num:0.7934508816120907;--nat-w:630px;"> <picture> <source srcset="/_astro/raft_paper_append_entries.BaTxItye_1Hulmm.webp 630w" type="image/webp"> <img src="/_astro/raft_paper_append_entries.BaTxItye_Z1X9jN1.png" srcset="/_astro/raft_paper_append_entries.BaTxItye_Z1X9jN1.png 630w" alt="Raft paper figure 2 snippet." sizes="(min-width: 630px) 630px, 100vw" loading="lazy" decoding="async" data-astro-image="constrained" data-astro-image-fit="cover" data-astro-image-pos="center" width="630" height="794" class="_image_55xv6_13"> </picture> </div> </figure>
|
||
<figure class="_figure_55xv6_5"> <div class="media-frame media-frame-sized" style="--ar-num:0.7469586374695864;--nat-w:614px;"> <picture> <source srcset="/_astro/raft_paper_install_snapshot.Bv6wVgAZ_Z2kpjzw.webp 614w" type="image/webp"> <img src="/_astro/raft_paper_install_snapshot.Bv6wVgAZ_Z2aSijv.png" srcset="/_astro/raft_paper_install_snapshot.Bv6wVgAZ_Z2aSijv.png 614w" alt="Raft paper figure 13." sizes="(min-width: 614px) 614px, 100vw" loading="lazy" decoding="async" data-astro-image="constrained" data-astro-image-fit="cover" data-astro-image-pos="center" width="614" height="822" class="_image_55xv6_13"> </picture> </div> </figure>
|
||
<p data-sid="d2eb.159">Rule 2 for <code>AppendEntries</code> and Rule 6 for <code>InstallSnapshot</code> creates a potential pitfall. If you implement this naively when you have discarded your log because of a previous <code>InstallSnapshot</code>, you end up doing the wrong thing (most likely creating infinite loops of RPCs between leader and follower, as I have painfully discovered).</p>
|
||
<p data-sid="d2eb.160">The Raft TLA+ spec and the authors’ simulation don’t actually include <code>InstallSnapshot</code> (though <a href="https://web.stanford.edu/~ouster/cgi-bin/papers/OngaroPhD.pdf#page=66">Diego Ongaro’s PhD thesis</a> does discuss the nuances in more depth), so different implementations use different workarounds. HashiCorp Raft, for instance, just avoids discarding logs altogether — which led to Bug #3 above.</p>
|
||
<p data-sid="d2eb.161">Bug #2 above, the deadlock, is in a feature called “leadership transfer” which is an extension to the core protocol. Like <code>InstallSnapshot</code>, this feature was never formally verified in the TLA+ spec.</p>
|
||
<h2 id="conclusion" data-sid="d2eb.162"><a href="#conclusion" class="anchor-link">Conclusion</a></h2>
|
||
<div class="_speaker_1qysz_6"> <div class="_head_1qysz_9"> <picture> <source srcset="/_astro/069_tw.DHr19spq_2mCqTD.webp 96w, /_astro/069_tw.DHr19spq_Z1UQeub.webp 192w" type="image/webp"> <img src="/_astro/069_tw.DHr19spq_1BL2As.jpg" srcset="/_astro/069_tw.DHr19spq_1BL2As.jpg 96w, /_astro/069_tw.DHr19spq_Z2i4KpM.jpg 192w" alt="TW Lim headshot" loading="lazy" decoding="async" sizes="96px" data-astro-image="fixed" data-astro-image-fit="cover" data-astro-image-pos="center" width="96" height="96" class="_avatar_1qysz_6"> </picture> <div class="_meta_1qysz_32" data-sid="d2eb.163"> <span class="_name_1qysz_38">TW Lim</span> <span class="_title_1qysz_45">Technical Writer</span> </div> </div> </div>
|
||
<p data-sid="d2eb.164">We have long accepted bugs as inevitable. Distributed systems are almost impossible to test thoroughly because their state spaces are so large, and as our stacks get more complex, the problem only gets worse.</p>
|
||
<p data-sid="d2eb.165">But technological progress also moves the frontier of what’s possible. We ended cholera in the developed world by building water treatment plants and sewage systems. We no longer wait for mainframes because we’ve made computing power cheap and abundant.</p>
|
||
<p data-sid="d2eb.166">The abundance of compute is a recent phenomenon. It’s held true for maybe the last 15 years, less than a tenth of the history of computing. It’s spurred, among other things, the recent surge of interest in formal verification — the hope that mechanized proof and model checking can finally become easy enough, and cheap enough, that we’ll be able to apply these approaches wherever we need. But what our experience with Raft has shown is that implementations of even mechanically proven models can have flaws, because there’s no mechanical way to check the implementors’ assumptions.</p>
|
||
<p data-sid="d2eb.167">Fortunately, cheap and abundant compute has also made it possible to test software in ways we couldn’t before. And the other thing our testing of Raft has shown is that when you run systems under fault, even basic testing methods reveal issues that would once have taken months of manual testing to find.</p>
|
||
<p data-sid="d2eb.168">Developers deserve something better, and so does everyone who depends on our software.</p> </div> </div> </div> </div> <section id="cta" class="article-cta" data-astro-cid-ektegib2=""> <div class="diamond-helper" data-astro-cid-lhauwh7h=""> <div class="diamond-grid" style="--gradient-direction: to bottom; --align-pos: top; --offset-top: 16px; --offset-bottom: auto" data-astro-cid-lhauwh7h=""></div> <div class="diamond-children" data-astro-cid-lhauwh7h=""> <div class="cta-outer" data-astro-cid-ektegib2=""> <div class="cta-inner" data-astro-cid-ektegib2=""> <div class="cta-title" data-astro-cid-ektegib2=""> <div class="eyebrow surface-dark" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj="" data-sid="d2eb.169"> get started </div> </div> <h1 data-astro-cid-ektegib2="" data-sid="d2eb.170">Velocity and verification. Finally, both.</h1> </div> <div class="cta-body" data-astro-cid-ektegib2="" data-sid="d2eb.171">
|
||
Talk with one of our product experts to see how Antithesis can help
|
||
you ship confidently, no matter who’s writing your code.
|
||
</div> <div class="cta-actions" data-astro-cid-ektegib2=""> <a data-astro-cid-ektegib2="true" href="/company/contact/?topic=book-a-demo" role="button" class="_button_17h79_1 _wideBoy_17h79_147 _toneCoral_17h79_57 _full_17h79_69 _large_17h79_50"><svg xmlns="http://www.w3.org/2000/svg" width="20" height="20" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" aria-hidden="true" data-astro-cid-ektegib2="true" class="lucide lucide-calendar"> <path d="M8 2v4"></path><path d="M16 2v4"></path><rect width="18" height="18" x="3" y="4" rx="2"></rect><path d="M3 10h18"></path> </svg> Book a demo</a> <a target="_blank" data-astro-cid-ektegib2="true" href="https://discord.com/invite/antithesis" role="button" class="_button_17h79_1 _wideBoy_17h79_147 _toneCoral_17h79_57 _outline_17h79_83 _large_17h79_50"><i class="icon icon-discord" data-astro-cid-ektegib2=""></i> Chat with us</a> </div> </div> <hr class="divider" data-astro-cid-ektegib2=""> </div> </div> </div> </section> </main> <footer data-astro-cid-5dd27owy=""> <div class="footer-inner" data-astro-cid-5dd27owy=""> <div class="upper" data-astro-cid-5dd27owy=""> <div class="sitemap" data-astro-cid-5dd27owy=""> <div class="page-column" data-astro-cid-5dd27owy=""> <div class="eyebrow surface-dark footer-eyebrow" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj=""> product </div> </div> <div class="page-list" data-astro-cid-5dd27owy=""> <a href="/product/#why-antithesis" data-astro-cid-5dd27owy="">Why Antithesis</a> <a href="/product/#how-to-use" data-astro-cid-5dd27owy="">Using the platform</a> <a href="/product/#faqs" data-astro-cid-5dd27owy="">FAQs</a> </div> </div> <div class="page-column" data-astro-cid-5dd27owy=""> <div class="eyebrow surface-dark footer-eyebrow" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj=""> company </div> </div> <div class="page-list" data-astro-cid-5dd27owy=""> <a href="/company/about/" data-astro-cid-5dd27owy="">About</a> <a href="/company/careers/" data-astro-cid-5dd27owy="">Careers</a> <a href="/company/contact/" data-astro-cid-5dd27owy="">Contact us</a> <a href="/bugbash/conference2026/" data-astro-cid-5dd27owy="">Bug Bash</a> <a href="/security/manifesto/" data-astro-cid-5dd27owy="">Security approach</a> <a href="https://trust.antithesis.com/" target="_blank" data-astro-cid-5dd27owy="">Trust Center</a> </div> </div> <div class="page-column" data-astro-cid-5dd27owy=""> <div class="eyebrow surface-dark footer-eyebrow" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj=""> learn </div> </div> <div class="page-list" data-astro-cid-5dd27owy=""> <a href="/learn/?category=Blog#resources" data-astro-cid-5dd27owy=""> Blog </a><a href="/learn/?category=Bug%20Bash%20talks#resources" data-astro-cid-5dd27owy=""> Bug Bash talks </a><a href="/learn/?category=Customer%20stories#resources" data-astro-cid-5dd27owy=""> Customer stories </a><a href="/learn/?category=Newsletter#resources" data-astro-cid-5dd27owy=""> Newsletter </a><a href="/learn/?category=Other%20talks#resources" data-astro-cid-5dd27owy=""> Other talks </a><a href="/learn/?category=Podcast#resources" data-astro-cid-5dd27owy=""> Podcast </a><a href="/learn/?category=Reports#resources" data-astro-cid-5dd27owy=""> Reports </a><a href="/learn/?category=Resources#resources" data-astro-cid-5dd27owy=""> Resources </a> </div> </div> <div class="page-column" data-astro-cid-5dd27owy=""> <div class="eyebrow surface-dark footer-eyebrow" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj=""> developers </div> </div> <div class="page-list" data-astro-cid-5dd27owy=""> <a href="/docs/introduction/welcome/" data-astro-cid-5dd27owy="">Docs</a> <a href="https://github.com/antithesishq/hands-on-tutorial-1" data-astro-cid-5dd27owy="">Get started <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-up-right" aria-hidden="true" data-astro-cid-5dd27owy="true"><path d="M7 7h10v10"></path><path d="M7 17 17 7"></path></svg></a> <a href="https://github.com/antithesishq/antithesis-skills" data-astro-cid-5dd27owy="">Agent skills <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-up-right" aria-hidden="true" data-astro-cid-5dd27owy="true"><path d="M7 7h10v10"></path><path d="M7 17 17 7"></path></svg></a> <a href="https://hegel.dev/" data-astro-cid-5dd27owy="">Hegel <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-up-right" aria-hidden="true" data-astro-cid-5dd27owy="true"><path d="M7 7h10v10"></path><path d="M7 17 17 7"></path></svg></a> <a href="https://bombadil.bot/" data-astro-cid-5dd27owy="">Bombadil <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-up-right" aria-hidden="true" data-astro-cid-5dd27owy="true"><path d="M7 7h10v10"></path><path d="M7 17 17 7"></path></svg></a> <a href="https://github.com/antithesishq/" data-astro-cid-5dd27owy="">GitHub <svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="lucide lucide-arrow-up-right" aria-hidden="true" data-astro-cid-5dd27owy="true"><path d="M7 7h10v10"></path><path d="M7 17 17 7"></path></svg></a> </div> </div> <!-- <div class="page-column">
|
||
<Eyebrow surface="dark" class="footer-eyebrow">partners</Eyebrow>
|
||
<div class="page-list">
|
||
<a href="">AWS</a>
|
||
</div>
|
||
</div> --> </div> <div class="connect-section" data-astro-cid-5dd27owy=""> <div class="contact-form-wrapper" data-astro-cid-5dd27owy=""> <div class="eyebrow surface-dark footer-eyebrow" data-astro-cid-aokxteyj=""> <div class="square" data-astro-cid-aokxteyj=""></div> <div class="text" data-astro-cid-aokxteyj=""> Curated reliability news Monthly </div> </div> <div data-mkto-form="" data-mkto-state="idle" data-mkto-variant="compact" data-mkto-surface="dark" data-mkto-base="//pages.antithesis.com" data-mkto-munchkin="337-FYY-625" data-mkto-form-id="1012" data-mkto-label-submitting="Subscribing…" data-mkto-label-success="Subscribed" data-astro-cid-5dd27owy="true"> <form id="mktoForm_1012" aria-label="Email signup"></form> <astro-island uid="Z11QO3E" prefix="r12" component-url="/_astro/MktoSelectEnhancer.MI1SZRP2.js" component-export="default" renderer-url="/_astro/client.BoS663YN.js" props="{}" ssr="" client="load" opts="{"name":"MktoSelectEnhancer","value":true}" await-children=""><span data-mkto-select-enhancer="true" hidden=""></span><!--astro:end--></astro-island> <noscript> <p data-mkto-noscript>
|
||
Please enable JavaScript in your browser to load and submit this form.
|
||
</p> </noscript> <div data-mkto-slot="success" role="status" aria-live="polite" hidden=""> <p data-astro-cid-5dd27owy="">Thanks — you're subscribed.</p> </div> <div data-mkto-slot="error" role="alert" aria-live="assertive" hidden=""> <p data-astro-cid-5dd27owy="">Something went wrong. Please try again.</p> </div> </div> <p class="newsletter-checkout" data-astro-cid-5dd27owy="">
|
||
Check out our <a href="/learn/?category=Newsletter#resources" data-astro-cid-5dd27owy="">previous issues</a>.
|
||
</p> </div> <div class="social-links" data-astro-cid-5dd27owy=""> <a target="_blank" href="https://www.linkedin.com/company/antithesis-operations/" aria-label="Antithesis on LinkedIn" data-astro-cid-5dd27owy=""><i class="icon icon-linkedin" data-astro-cid-5dd27owy=""></i></a> <a target="_blank" href="https://github.com/antithesishq" aria-label="Antithesis on GitHub" data-astro-cid-5dd27owy=""><i class="icon icon-github" data-astro-cid-5dd27owy=""></i></a> <a target="_blank" href="https://discord.com/invite/antithesis" aria-label="Antithesis on Discord" data-astro-cid-5dd27owy=""><i class="icon icon-discord" data-astro-cid-5dd27owy=""></i></a> <a target="_blank" href="https://www.youtube.com/@antithesis-hq" aria-label="Antithesis on YouTube" data-astro-cid-5dd27owy=""><i class="icon icon-youtube" data-astro-cid-5dd27owy=""></i></a> <a target="_blank" href="https://x.com/antithesishq/" aria-label="Antithesis on X" data-astro-cid-5dd27owy=""><i class="icon icon-twitter" data-astro-cid-5dd27owy=""></i></a> </div> </div> </div> <div class="lower" data-astro-cid-5dd27owy=""> <div class="badges" data-astro-cid-5dd27owy=""> <a href="https://trust.antithesis.com/" target="_blank" data-astro-cid-5dd27owy=""> <svg width="72" height="72" viewBox="0 0 72 72" fill="none" aria-label="Antithesis' SOC 2 Type II certification badge" data-astro-cid-5dd27owy="true">
|
||
<g clip-path="url(#clip0_1222_4427)">
|
||
<path d="M36 72C55.8823 72 72 55.8823 72 36C72 16.1177 55.8823 0 36 0C16.1177 0 0 16.1177 0 36C0 55.8823 16.1177 72 36 72Z" fill="url(#paint0_linear_1222_4427)"></path>
|
||
<path d="M36 72C55.8823 72 72 55.8823 72 36C72 16.1177 55.8823 0 36 0C16.1177 0 0 16.1177 0 36C0 55.8823 16.1177 72 36 72Z" fill="url(#paint1_linear_1222_4427)"></path>
|
||
<path d="M36 64.8002C51.9058 64.8002 64.7999 51.906 64.7999 36.0002C64.7999 20.0944 51.9058 7.2002 36 7.2002C20.0942 7.2002 7.19995 20.0944 7.19995 36.0002C7.19995 51.906 20.0942 64.8002 36 64.8002Z" stroke="#240627" stroke-width="0.914286" stroke-miterlimit="10"></path>
|
||
<path d="M16.4552 32.0082L19.7651 22.7017H22.2769L25.6012 32.0082H23.4865L21.0406 24.9357H20.9747L18.5144 32.0082H16.4531H16.4552ZM18.6481 30.2925L19.3126 28.5378H22.7418L23.4063 30.2925H18.646H18.6481Z" fill="#240627"></path>
|
||
<path d="M26.4515 32.0082V22.7017H28.4984V32.0082H26.4515Z" fill="#240627"></path>
|
||
<path d="M34.3393 32.1418C33.4527 32.1418 32.6792 31.9546 32.0189 31.5761C31.3585 31.1996 30.8463 30.6524 30.4842 29.9345C30.1201 29.2166 29.9391 28.3567 29.9391 27.3548C29.9391 26.353 30.1201 25.4931 30.4842 24.7752C30.8483 24.0572 31.3585 23.51 32.0189 23.1336C32.6792 22.7571 33.4527 22.5679 34.3393 22.5679C35.4728 22.5679 36.3759 22.8456 37.0445 23.399C37.713 23.9523 38.1677 24.7032 38.4063 25.6515H36.2936C36.1167 25.2524 35.8739 24.9459 35.5695 24.7279C35.263 24.5098 34.8536 24.4028 34.3393 24.4028C33.8703 24.4028 33.4589 24.516 33.1091 24.7423C32.7594 24.9686 32.4858 25.3039 32.2925 25.7462C32.097 26.1884 32.0003 26.7254 32.0003 27.3548C32.0003 27.9843 32.097 28.5212 32.2925 28.9635C32.4879 29.4079 32.7594 29.7411 33.1091 29.9674C33.4589 30.1937 33.8682 30.3068 34.3393 30.3068C34.8536 30.3068 35.263 30.1978 35.5695 29.9818C35.876 29.7638 36.1167 29.4572 36.2936 29.0582H38.4063C38.1677 30.0065 37.713 30.7574 37.0445 31.3107C36.3759 31.8641 35.4728 32.1418 34.3393 32.1418Z" fill="#240627"></path>
|
||
<path d="M39.7195 32.0082V22.7017H43.6013C44.239 22.7017 44.8068 22.8395 45.3026 23.1131C45.7983 23.3887 46.1851 23.7693 46.4587 24.2569C46.7343 24.7444 46.8701 25.2937 46.8701 25.9046C46.8701 26.5156 46.7323 27.0793 46.4587 27.5668C46.183 28.0543 45.7983 28.4349 45.3026 28.7106C44.8068 28.9862 44.239 29.122 43.6013 29.122H41.7663V32.0061H39.7195V32.0082ZM43.3894 27.2891C43.7001 27.2891 43.9593 27.2335 44.167 27.1225C44.3748 27.0114 44.5373 26.8509 44.6525 26.637C44.7677 26.4251 44.8253 26.1803 44.8253 25.9067C44.8253 25.4809 44.6998 25.1476 44.4468 24.9028C44.1938 24.6601 43.842 24.5366 43.3894 24.5366H41.7684V27.2891H43.3894Z" fill="#240627"></path>
|
||
<path d="M46.3922 32.0082L49.7022 22.7017H52.216L55.5403 32.0082H53.4256L50.9796 24.9357H50.9138L48.4535 32.0082H46.3922ZM48.5851 30.2925L49.2496 28.5378H52.6788L53.3433 30.2925H48.5831H48.5851Z" fill="#240627"></path>
|
||
<path d="M20.7241 44.4908C20.0247 44.4908 19.3972 44.3797 18.8439 44.1596C18.2905 43.9375 17.8441 43.6063 17.5088 43.1619C17.1714 42.7196 16.9719 42.1786 16.9102 41.5409H18.957C19.0187 41.9132 19.2059 42.2012 19.5145 42.4049C19.8251 42.6085 20.2283 42.7114 20.7241 42.7114C21.1232 42.7114 21.4462 42.6661 21.6951 42.5777C21.944 42.4892 22.125 42.3637 22.2402 42.1992C22.3554 42.0346 22.413 41.8433 22.413 41.6211C22.413 41.3989 22.3307 41.2056 22.1662 41.0636C22.0016 40.9217 21.7979 40.8168 21.5552 40.7509C21.3104 40.6851 20.9627 40.5987 20.5122 40.4917C19.8395 40.3683 19.282 40.2264 18.8439 40.0659C18.4057 39.9055 18.0292 39.636 17.7145 39.2554C17.3998 38.8748 17.2434 38.342 17.2434 37.6591C17.2434 37.0831 17.3956 36.5873 17.7022 36.1697C18.0087 35.7541 18.4242 35.4415 18.9508 35.2316C19.4775 35.0239 20.0699 34.9189 20.7262 34.9189C21.4523 34.9189 22.0756 35.0362 22.594 35.2707C23.1124 35.5052 23.5136 35.8282 23.7975 36.2417C24.0814 36.6531 24.2583 37.1304 24.3282 37.6714H22.2814C22.2196 37.3608 22.0571 37.1221 21.7959 36.9535C21.5346 36.7848 21.1952 36.7004 20.7796 36.7004C20.469 36.7004 20.2057 36.7395 19.9876 36.8197C19.7696 36.9 19.6112 37.0152 19.5083 37.1653C19.4055 37.3155 19.3561 37.4801 19.3561 37.657C19.3561 37.9141 19.4404 38.1157 19.6091 38.2618C19.7778 38.4079 19.9897 38.5231 20.2468 38.6074C20.504 38.6917 20.8681 38.7823 21.3371 38.881C21.9934 39.0229 22.5364 39.1752 22.9664 39.3397C23.3963 39.5043 23.7625 39.7676 24.0628 40.1297C24.3632 40.4938 24.5154 40.9896 24.5154 41.6191C24.5154 42.1683 24.3694 42.66 24.0772 43.094C23.7851 43.5281 23.3531 43.8696 22.7812 44.1185C22.2094 44.3674 21.5243 44.4908 20.7282 44.4908H20.7241Z" fill="#240627"></path>
|
||
<path d="M29.8956 44.4909C29.009 44.4909 28.2355 44.3037 27.5751 43.9252C26.9148 43.5488 26.4026 43.0016 26.0405 42.2836C25.6764 41.5657 25.4954 40.7058 25.4954 39.704C25.4954 38.7021 25.6764 37.8422 26.0405 37.1243C26.4046 36.4064 26.9148 35.8592 27.5751 35.4827C28.2355 35.1062 29.009 34.917 29.8956 34.917C30.7822 34.917 31.5578 35.1062 32.2222 35.4827C32.8867 35.8592 33.3968 36.4064 33.7507 37.1243C34.1045 37.8422 34.2814 38.7021 34.2814 39.704C34.2814 40.7058 34.1045 41.5657 33.7507 42.2836C33.3968 43.0016 32.8867 43.5488 32.2222 43.9252C31.5578 44.3017 30.7822 44.4909 29.8956 44.4909ZM29.8956 42.658C30.3646 42.658 30.7781 42.5449 31.1319 42.3186C31.4858 42.0923 31.7614 41.759 31.9568 41.3147C32.1523 40.8724 32.249 40.3355 32.249 39.706C32.249 39.0765 32.1523 38.5417 31.9568 38.0973C31.7614 37.655 31.4878 37.3197 31.1319 37.0934C30.7781 36.8672 30.3646 36.754 29.8956 36.754C29.4266 36.754 29.0151 36.8672 28.6654 37.0934C28.3157 37.3197 28.0421 37.655 27.8487 38.0973C27.6533 38.5417 27.5566 39.0765 27.5566 39.706C27.5566 40.3355 27.6533 40.8724 27.8487 41.3147C28.0442 41.759 28.3157 42.0923 28.6654 42.3186C29.0151 42.5449 29.4245 42.658 29.8956 42.658Z" fill="#240627"></path>
|
||
<path d="M40.0015 44.4909C39.1149 44.4909 38.3414 44.3037 37.6811 43.9252C37.0207 43.5488 36.5085 43.0016 36.1444 42.2836C35.7803 41.5657 35.5992 40.7058 35.5992 39.704C35.5992 38.7021 35.7803 37.8422 36.1444 37.1243C36.5085 36.4064 37.0207 35.8592 37.6811 35.4827C38.3414 35.1062 39.1149 34.917 40.0015 34.917C41.135 34.917 42.0381 35.1947 42.7067 35.7481C43.3752 36.3014 43.8299 37.0523 44.0685 38.0006H41.9558C41.7789 37.6016 41.5362 37.293 41.2317 37.077C40.9252 36.8589 40.5158 36.752 40.0015 36.752C39.5325 36.752 39.1211 36.8651 38.7714 37.0914C38.4216 37.3177 38.148 37.653 37.9526 38.0953C37.7572 38.5396 37.6605 39.0745 37.6605 39.704C37.6605 40.3334 37.7592 40.8704 37.9526 41.3126C38.148 41.757 38.4196 42.0902 38.7714 42.3165C39.1211 42.5428 39.5304 42.656 40.0015 42.656C40.5158 42.656 40.9252 42.5469 41.2317 42.3309C41.5382 42.1129 41.7789 41.8064 41.9558 41.4073H44.0685C43.8299 42.3556 43.3752 43.1065 42.7067 43.6598C42.0381 44.2132 41.135 44.4909 40.0015 44.4909Z" fill="#240627"></path>
|
||
<path d="M48.1218 44.3586V42.5236L52.1765 38.9874C52.3883 38.8022 52.5509 38.6192 52.6619 38.4422C52.773 38.2653 52.8286 38.0699 52.8286 37.858C52.8286 37.5042 52.7237 37.2306 52.5159 37.0413C52.3081 36.85 51.981 36.7554 51.5387 36.7554C51.2898 36.7554 51.0738 36.8006 50.8866 36.8891C50.7015 36.9776 50.5451 37.1072 50.4217 37.2738C50.2983 37.4425 50.2181 37.642 50.1831 37.8724H48.1218C48.1918 37.2429 48.3749 36.7122 48.667 36.2761C48.9591 35.842 49.3499 35.5067 49.8375 35.2722C50.325 35.0377 50.8928 34.9204 51.5387 34.9204C52.2999 34.9204 52.9355 35.0418 53.4395 35.2866C53.9456 35.5314 54.3241 35.8585 54.5771 36.2699C54.8302 36.6813 54.9557 37.1627 54.9557 37.712C54.9557 38.0041 54.9063 38.288 54.8096 38.5636C54.7129 38.8393 54.5689 39.1046 54.3776 39.3618C54.1863 39.6189 53.9497 39.872 53.6658 40.1188L50.9134 42.5257H55.0873V44.3606H48.1218V44.3586Z" fill="#240627"></path>
|
||
<path d="M25.7457 52.5839V48.2433H24.1453V47.3999H28.2781V48.2433H26.6858V52.5839H25.7457Z" fill="#240627"></path>
|
||
<path d="M30.319 52.5839V50.7325L28.5046 47.3999H29.5126L30.7798 49.7924H30.8169L32.0902 47.3999H33.0756L31.2612 50.7325V52.5839H30.3211H30.319Z" fill="#240627"></path>
|
||
<path d="M33.7218 52.5839V47.3999H35.8098C36.1554 47.3999 36.4619 47.474 36.7273 47.6221C36.9927 47.7702 37.2004 47.9759 37.3485 48.2372C37.4967 48.4984 37.5707 48.7946 37.5707 49.1258C37.5707 49.457 37.4967 49.7533 37.3485 50.0186C37.2004 50.282 36.9927 50.4877 36.7273 50.6337C36.4619 50.7798 36.1554 50.8518 35.8098 50.8518H34.6701V52.5839H33.7218ZM35.7213 50.0084C35.9085 50.0084 36.0711 49.9734 36.2068 49.9014C36.3426 49.8294 36.4455 49.7265 36.5175 49.5949C36.5895 49.4612 36.6244 49.3069 36.6244 49.1279C36.6244 48.8605 36.5442 48.6486 36.3837 48.4881C36.2233 48.3277 36.0032 48.2474 35.7213 48.2474H34.6701V50.0104H35.7213V50.0084Z" fill="#240627"></path>
|
||
<path d="M38.5945 52.5839V47.3999H42.0237V48.2433H39.5428V51.7384H42.0978V52.5818H38.5945V52.5839ZM39.3721 50.3704V49.5784H41.8756V50.3704H39.3721Z" fill="#240627"></path>
|
||
<path d="M44.9929 52.5839V47.3999H45.9413V52.5839H44.9929Z" fill="#240627"></path>
|
||
<path d="M46.9054 52.5839V47.3999H47.8537V52.5839H46.9054Z" fill="#240627"></path>
|
||
</g>
|
||
<defs>
|
||
<linearGradient id="paint0_linear_1222_4427" x1="11.0769" y1="4.93414e-07" x2="24.1861" y2="65.6857" gradientUnits="userSpaceOnUse">
|
||
<stop stop-color="#DAD7FF"></stop>
|
||
<stop offset="1" stop-color="#FFDEDA"></stop>
|
||
</linearGradient>
|
||
<linearGradient id="paint1_linear_1222_4427" x1="11.0769" y1="4.93414e-07" x2="24.1861" y2="65.6857" gradientUnits="userSpaceOnUse">
|
||
<stop stop-color="#8A7FFE"></stop>
|
||
<stop offset="1" stop-color="#FF9F91"></stop>
|
||
</linearGradient>
|
||
<clipPath id="clip0_1222_4427">
|
||
<rect width="72" height="72" fill="white"></rect>
|
||
</clipPath>
|
||
</defs>
|
||
</svg> </a> <a href="https://aws.amazon.com/marketplace/seller-profile?id=seller-r72bkjfiyczum" target="_blank" data-astro-cid-5dd27owy=""> <svg width="72" height="44" viewBox="0 0 72 44" fill="none" aria-label="Antithesis' AWS partnership badge" data-astro-cid-5dd27owy="true">
|
||
<g clip-path="url(#clip0_1222_4449)">
|
||
<path d="M20.2956 15.7934C20.2956 16.6934 20.3856 17.4134 20.5656 17.9384C20.7606 18.4634 21.0006 19.0484 21.3306 19.6784C21.4506 19.8734 21.4956 20.0684 21.4956 20.2334C21.4956 20.4734 21.3456 20.7134 21.0456 20.9534L19.5306 21.9734C19.3206 22.1234 19.0956 22.1984 18.9156 22.1984C18.6756 22.1984 18.4356 22.0784 18.1956 21.8534C17.8656 21.4934 17.5806 21.1034 17.3406 20.7134C17.1006 20.3084 16.8606 19.8434 16.6056 19.2884C14.7456 21.5084 12.3906 22.6334 9.57062 22.6334C7.56062 22.6334 5.95563 22.0484 4.78563 20.8934C3.61563 19.7384 3.01562 18.1784 3.01562 16.2434C3.01562 14.1884 3.73563 12.5234 5.19063 11.2634C6.64563 10.0034 8.59562 9.3734 11.0556 9.3734C11.8656 9.3734 12.7056 9.4484 13.5906 9.5684C14.4756 9.6884 15.3906 9.8834 16.3506 10.0934V8.3234C16.3506 6.4784 15.9606 5.2034 15.2256 4.4534C14.4606 3.7034 13.1706 3.3434 11.3256 3.3434C10.4856 3.3434 9.63062 3.4334 8.74563 3.6584C7.86062 3.8834 7.00563 4.1384 6.16563 4.4834C5.77563 4.6484 5.49062 4.7534 5.32562 4.7984C5.16062 4.8434 5.04062 4.8734 4.93562 4.8734C4.60562 4.8734 4.42563 4.6334 4.42563 4.1234V2.9384C4.42563 2.5484 4.47062 2.2634 4.59062 2.0984C4.71062 1.9334 4.92062 1.7534 5.26562 1.5884C6.10562 1.1534 7.11063 0.793398 8.28062 0.493398C9.45062 0.178398 10.6956 0.0283984 12.0156 0.0283984C14.8656 0.0283984 16.9506 0.688398 18.2856 1.9934C19.6056 3.2984 20.2656 5.2784 20.2656 7.9484V15.7784H20.3106L20.2956 15.7934ZM10.5756 19.4684C11.3706 19.4684 12.1806 19.3184 13.0356 19.0334C13.8906 18.7484 14.6706 18.2084 15.3156 17.4884C15.7056 17.0234 15.9906 16.5134 16.1256 15.9434C16.2756 15.3584 16.3656 14.6684 16.3656 13.8434V12.8234C15.6756 12.6584 14.9256 12.5084 14.1606 12.4184C13.3956 12.3284 12.6456 12.2684 11.9106 12.2684C10.3056 12.2684 9.13562 12.5834 8.34062 13.2434C7.54562 13.9034 7.17063 14.8184 7.17063 16.0184C7.17063 17.1584 7.45563 17.9984 8.05562 18.5834C8.62562 19.1834 9.46562 19.4834 10.5756 19.4834V19.4684ZM29.8056 22.0784C29.3706 22.0784 29.0856 22.0034 28.8906 21.8384C28.6956 21.6884 28.5306 21.3584 28.3956 20.8934L22.7556 2.2034C22.6056 1.7234 22.5456 1.4084 22.5456 1.2434C22.5456 0.853398 22.7406 0.643398 23.1156 0.643398H25.4556C25.9056 0.643398 26.2206 0.718398 26.3856 0.883398C26.5806 1.0334 26.7156 1.3634 26.8656 1.8284L30.8856 17.8334L34.6206 1.8284C34.7406 1.3484 34.8906 1.0334 35.0706 0.883398C35.2656 0.733398 35.5956 0.643398 36.0306 0.643398H37.9506C38.4006 0.643398 38.7156 0.718398 38.9106 0.883398C39.1056 1.0334 39.2706 1.3634 39.3606 1.8284L43.1406 18.0284L47.2806 1.8284C47.4306 1.3484 47.5956 1.0334 47.7606 0.883398C47.9556 0.733398 48.2556 0.643398 48.6906 0.643398H50.9256C51.3156 0.643398 51.5256 0.838398 51.5256 1.2434C51.5256 1.3634 51.4956 1.4834 51.4806 1.6334C51.4656 1.7834 51.4056 1.9784 51.3156 2.2334L45.5406 20.9234C45.3906 21.4034 45.2256 21.7184 45.0456 21.8684C44.8656 22.0184 44.5506 22.1084 44.1306 22.1084H42.0756C41.6256 22.1084 41.3106 22.0334 41.1156 21.8684C40.9206 21.7034 40.7556 21.3884 40.6656 20.8934L36.9606 5.2934L33.2706 20.8634C33.1506 21.3434 33.0006 21.6584 32.8206 21.8384C32.6256 22.0034 32.2956 22.0784 31.8606 22.0784H29.8056ZM60.5706 22.7384C59.3256 22.7384 58.0806 22.5884 56.8806 22.3034C55.6806 22.0184 54.7506 21.7034 54.1206 21.3284C53.7306 21.1034 53.4756 20.8634 53.3856 20.6534C53.2956 20.4434 53.2356 20.1884 53.2356 19.9784V18.7484C53.2356 18.2384 53.4306 17.9984 53.7906 17.9984C53.9406 17.9984 54.0756 18.0284 54.2256 18.0734C54.3756 18.1184 54.5856 18.2234 54.8256 18.3134C55.6356 18.6734 56.5206 18.9584 57.4656 19.1534C58.4256 19.3484 59.3556 19.4384 60.3156 19.4384C61.8306 19.4384 63.0006 19.1684 63.8106 18.6434C64.6206 18.1184 65.0556 17.3384 65.0556 16.3484C65.0556 15.6734 64.8456 15.1184 64.4106 14.6534C63.9756 14.1884 63.1656 13.7834 61.9956 13.3934L58.5306 12.2984C56.7756 11.7434 55.4856 10.9184 54.7056 9.8234C53.9106 8.7584 53.5056 7.5734 53.5056 6.3134C53.5056 5.2934 53.7156 4.4084 54.1506 3.6284C54.5856 2.8484 55.1556 2.1734 55.8756 1.6484C56.5956 1.0934 57.4056 0.673398 58.3656 0.388398C59.3256 0.103398 60.3306 -0.0166016 61.3806 -0.0166016C61.9056 -0.0166016 62.4606 0.0133984 62.9856 0.0733984C63.5406 0.148398 64.0356 0.238398 64.5456 0.343398C65.0256 0.463398 65.4756 0.583398 65.9106 0.733398C66.3456 0.883398 66.6756 1.0184 66.9156 1.1684C67.2456 1.3634 67.4856 1.5584 67.6356 1.7684C67.7856 1.9634 67.8456 2.2334 67.8456 2.5634V3.7034C67.8456 4.2134 67.6506 4.4834 67.2906 4.4834C67.0956 4.4834 66.7956 4.3934 66.3756 4.1984C65.0106 3.5684 63.4806 3.2534 61.7856 3.2534C60.4206 3.2534 59.3406 3.4784 58.6056 3.9284C57.8706 4.3934 57.4806 5.0834 57.4806 6.0734C57.4806 6.7484 57.7206 7.3334 58.2006 7.7984C58.6806 8.2634 59.5656 8.7134 60.8406 9.1334L64.2456 10.2284C65.9706 10.7834 67.2156 11.5634 67.9506 12.5534C68.6856 13.5434 69.0456 14.6834 69.0456 15.9434C69.0456 16.9784 68.8356 17.9234 68.4156 18.7484C67.9806 19.5734 67.4106 20.2934 66.6606 20.8784C65.9256 21.4784 65.0256 21.9134 64.0056 22.2284C62.9256 22.5734 61.8006 22.7384 60.5856 22.7384H60.5706Z" fill="#FCFBF9"></path>
|
||
<path d="M65.1009 34.4845C57.2259 40.3645 45.7809 43.4845 35.9409 43.4845C22.1559 43.4845 9.72088 38.3395 0.330881 29.7745C-0.419119 29.0995 0.255881 28.1845 1.14088 28.7095C11.2959 34.6645 23.8209 38.2645 36.7659 38.2645C45.5109 38.2645 55.1109 36.4345 63.9459 32.6545C65.2659 32.0545 66.3909 33.5245 65.1009 34.4845ZM68.3709 30.7195C67.3659 29.4145 61.7109 30.0895 59.1459 30.4045C58.3809 30.4945 58.2609 29.8195 58.9509 29.3095C63.4509 26.1145 70.8459 27.0295 71.7159 28.0945C72.5859 29.1895 71.4759 36.6595 67.2609 40.2295C66.6159 40.7845 65.9859 40.4995 66.2859 39.7645C67.2459 37.3645 69.3759 31.9795 68.3709 30.6895V30.7195Z" fill="#FCFBF9"></path>
|
||
</g>
|
||
<defs>
|
||
<clipPath id="clip0_1222_4449">
|
||
<rect width="72" height="43.485" fill="white"></rect>
|
||
</clipPath>
|
||
</defs>
|
||
</svg> </a> </div> <div class="info-section" data-astro-cid-5dd27owy=""> <div class="logomark" data-astro-cid-5dd27owy=""> <a href="/" aria-label="Antithesis home" data-astro-cid-5dd27owy=""> <img src="/_astro/antithesis.poHvWeoa_Dv67C.svg" srcset="/_astro/antithesis.poHvWeoa_Dv67C.svg 154w" alt="Antithesis logomark" loading="lazy" decoding="async" sizes="(min-width: 154px) 154px, 100vw" data-astro-image="constrained" data-astro-image-fit="cover" data-astro-image-pos="center" width="154" height="24"> </a> </div> <div class="info-text" data-astro-cid-5dd27owy=""> <span class="copyright" data-astro-cid-5dd27owy="">© 2026 Antithesis Operations LLC</span> <div class="legal-links" data-astro-cid-5dd27owy=""> <a href="/legal/privacy_policy/" data-astro-cid-5dd27owy="">Privacy policy</a> <a href="/legal/security/" data-astro-cid-5dd27owy="">Security</a> <a href="/legal/terms_of_use/" data-astro-cid-5dd27owy="">Terms of use</a> </div> </div> </div> </div> </div> </footer> </div> <script type="module">const p="sterm",T="marks",f=e=>{if(!e)return;const t=e.closest("details");t&&(t.classList.add("no-animate"),t.open=!0,t.addEventListener("transitionend",()=>{t.classList.remove("no-animate")},{once:!0}),f(t.parentElement))},h=e=>e.replace(/[.*+?^${}()|[\]\\]/g,"\\$&"),w=(e,t)=>{if(!t)return;const n=new RegExp(h(t),"gi"),s=document.createTreeWalker(e,NodeFilter.SHOW_TEXT,{acceptNode(r){if(!r.nodeValue||!r.nodeValue.trim())return NodeFilter.FILTER_REJECT;const o=r.parentElement;return!o||o.closest("mark,script,style,noscript")?NodeFilter.FILTER_REJECT:NodeFilter.FILTER_ACCEPT}}),c=[];for(;s.nextNode();)c.push(s.currentNode);for(const r of c){const o=r.nodeValue??"";if(n.lastIndex=0,!n.test(o))continue;n.lastIndex=0;const l=document.createDocumentFragment();let i=0,a;for(;(a=n.exec(o))!==null;){a.index>i&&l.appendChild(document.createTextNode(o.slice(i,a.index)));const u=document.createElement("mark");u.textContent=a[0],l.appendChild(u),i=a.index+a[0].length}i<o.length&&l.appendChild(document.createTextNode(o.slice(i))),r.parentNode?.replaceChild(l,r)}},g=e=>e?e.split(",").map(t=>t.trim()).filter(Boolean):[];let E=!1,d=!1;const C=()=>{d=!0};for(const e of["wheel","touchmove","keydown"])window.addEventListener(e,C,{passive:!0,once:!0});const m=()=>{const e=new URLSearchParams(window.location.search),t=e.get("sid");if(!t)return;const n=document.querySelector(`[data-sid="${CSS.escape(t)}"]`);if(n instanceof HTMLElement){if(!E){if(f(n),!n.querySelector("mark")){const s=[],c=e.get(p);c&&s.push(c);for(const r of g(e.get(T)))s.push(r);for(const r of[...new Set(s)])w(n,r)}E=!0}d||(n.scrollIntoView({block:"center",inline:"nearest"}),window.requestAnimationFrame(()=>{d||n.scrollIntoView({block:"center",inline:"nearest"})}))}};document.readyState==="loading"?document.addEventListener("DOMContentLoaded",m,{once:!0}):m();window.addEventListener("load",m,{once:!0});</script> <script type="module" src="/_astro/BaseLayout.astro_astro_type_script_index_0_lang.BQ2j0KKI.js"></script> </body></html> |