Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
name: CI

on:
pull_request:
paths-ignore:
- 'README.md'
- 'CLAUDE.md'
- 'agent.md'
push:
branches:
- main
paths-ignore:
- 'README.md'
- 'CLAUDE.md'
- 'agent.md'

env:
FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true
NEXT_TELEMETRY_DISABLED: 1

concurrency:
group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true

jobs:
build:
runs-on: ubuntu-latest
timeout-minutes: 10

steps:
- name: Checkout
uses: actions/checkout@v6

- name: Setup Bun
uses: oven-sh/setup-bun@v2
with:
bun-version: 1.3.9

- name: Restore Next.js cache
uses: actions/cache@v5
with:
path: .next/cache
key: ${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}-${{ hashFiles('pages/**/*', 'components/**/*', 'lib/**/*', 'data/**/*', 'styles/**/*', 'content/**/*', 'public/**/*', 'next.config.js', 'postcss.config.js', 'tailwind.config.js') }}
restore-keys: |
${{ runner.os }}-nextjs-${{ hashFiles('bun.lock', 'package.json') }}-

- name: Install dependencies
run: bun install --frozen-lockfile

- name: Build site
run: bun run build
39 changes: 39 additions & 0 deletions components/research/Hypothesis.jsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
export default function Hypothesis({
name,
constraint,
source,
children,
border = true
}) {
return (
<li
className={`list-none ${border ? 'border-b border-gray-200/50' : ''}`}
>
<details className="group/hyp">
<summary className="px-5 py-3 cursor-pointer select-none list-none flex items-center gap-3 [&::-webkit-details-marker]:hidden">
<svg
viewBox="0 0 24 24"
className="w-3.5 h-3.5 text-muted/50 transition-transform group-open/hyp:rotate-90 flex-shrink-0"
fill="none"
stroke="currentColor"
strokeWidth="1.5"
strokeLinecap="round"
strokeLinejoin="round"
>
<polyline points="9 6 15 12 9 18" />
</svg>
<code className="font-mono text-[12px] font-medium">{name}</code>
<span className="text-muted text-[13px]">{constraint}</span>
</summary>
<div className="px-5 pb-3 pl-12 text-[13px] text-muted leading-relaxed">
<p className="mb-1">
<span className="text-[11px] font-mono uppercase tracking-wider text-muted/60">
{source}
</span>
</p>
<p>{children}</p>
</div>
</details>
</li>
)
}
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

New shared Hypothesis duplicates existing inline component

Low Severity

The newly extracted components/research/Hypothesis.jsx is an exact duplicate of the inline Hypothesis function still present in pages/research/nexus-mutual-book-value.jsx (lines 11–43). The Lido page was refactored to use the shared component, but the Nexus Mutual page was missed, leaving two identical implementations. Any future fix to one copy risks not being applied to the other.

Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.

84 changes: 84 additions & 0 deletions components/research/SafeGuarantee.jsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
import { useState, useEffect, useRef } from 'react'

const FORMAL_INVARIANTS = [
'\u2200 key, next(key) \u2260 0 \u2192 reachable(SENTINEL, key)',
'\u2200 key \u2260 0, next(key) \u2260 0 \u2194 reachable(SENTINEL, key)',
'\u2200 a b, reachable(a, b) \u2227 reachable(b, a) \u2192 a = b'
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Formal invariant displays property page says is false

Medium Severity

The third entry in FORMAL_INVARIANTS∀ a b, reachable(a, b) ∧ reachable(b, a) → a = b — is antisymmetry of reachability, which the page's own text explicitly calls out as false on Safe's circular list ("antisymmetry is false on Safe's circular list (SENTINEL → o → SENTINEL makes both directions reachable)"). This formula is meant to represent the acyclic invariant but instead shows a property the page says doesn't hold, creating a direct contradiction on a research page about mathematical proofs.

Additional Locations (1)
Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.

]

export default function SafeGuarantee() {
const [showEnglish, setShowEnglish] = useState(true)
const timerRef = useRef(null)

useEffect(() => {
timerRef.current = setTimeout(() => setShowEnglish(false), 5000)
return () => clearTimeout(timerRef.current)
}, [])

const handleToggle = () => {
if (timerRef.current) {
clearTimeout(timerRef.current)
timerRef.current = null
}
setShowEnglish((prev) => !prev)
}

return (
<div className="py-6">
<button
onClick={handleToggle}
className="inline-flex items-center gap-1.5 text-[12px] font-semibold text-muted hover:text-heading transition-colors cursor-pointer mb-4"
>
<svg
viewBox="0 0 24 24"
className="w-[13px] h-[13px]"
fill="none"
stroke="currentColor"
strokeWidth="1.5"
strokeLinecap="round"
strokeLinejoin="round"
>
<path d="m5 8 6 6" />
<path d="m4 14 6-6 2-3" />
<path d="M2 5h12" />
<path d="M7 2h1" />
<path d="m22 22-5-10-5 10" />
<path d="M14 18h6" />
</svg>
{showEnglish ? 'Switch to formal' : 'Switch to English'}
</button>

<div className="grid text-center [&>*]:col-start-1 [&>*]:row-start-1">
<div
className="flex flex-col items-center justify-center gap-4 md:gap-5 transition-opacity duration-200 text-[0.945rem] md:text-[1.18125rem] font-mono text-primary leading-snug"
style={{
opacity: showEnglish ? 0 : 1,
pointerEvents: showEnglish ? 'none' : 'auto'
}}
aria-hidden={showEnglish}
>
{FORMAL_INVARIANTS.map((formal, i) => (
<code
key={i}
className="block w-full max-w-full overflow-x-auto px-1"
>
{formal}
</code>
))}
</div>
<div
className="flex items-center justify-center transition-opacity duration-200"
style={{
opacity: showEnglish ? 1 : 0,
pointerEvents: showEnglish ? 'auto' : 'none'
}}
aria-hidden={!showEnglish}
>
<p className="text-xl md:text-2xl leading-snug font-serif max-w-prose mx-auto px-1">
The owners mapping forms a proper loop-free circular linked list.
</p>
</div>
</div>
</div>
)
}
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

SafeGuarantee duplicates Guarantee toggle logic and structure

Low Severity

SafeGuarantee is a near-complete copy of Guarantee — the state management (useState, useRef, useEffect with 5-second timer), handleToggle handler, toggle button with identical SVG icon, and the grid-based opacity-swap layout are all line-for-line identical. Only the inner content and one label string ("Switch to formal" vs "Switch to math") differ. A shared wrapper component accepting the formal/English content, toggle label, and Lean link as props would eliminate ~60 lines of duplication and make future case study pages trivial to add.

Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit 934c77e. Configure here.

50 changes: 50 additions & 0 deletions components/research/TikZDiagram.jsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
import { useEffect, useRef } from 'react'

export default function TikZDiagram({ tikz, className = '' }) {
const ref = useRef(null)

useEffect(() => {
const container = ref.current
if (!container) return

// Add TikZJax fonts CSS if not already present
if (!document.querySelector('link[href*="tikzjax.com"]')) {
const link = document.createElement('link')
link.rel = 'stylesheet'
link.type = 'text/css'
link.href = 'https://tikzjax.com/v1/fonts.css'
document.head.appendChild(link)
}

// Create the <script type="text/tikz"> element
const tikzEl = document.createElement('script')
tikzEl.type = 'text/tikz'
tikzEl.textContent = tikz
container.appendChild(tikzEl)

const existingScript = document.querySelector('script[src*="tikzjax.com"]')
if (!existingScript) {
// First load: add tikzjax.js — it sets window.onload to its processing
// function, but in a SPA that event already fired, so we call it manually.
const script = document.createElement('script')
script.src = 'https://tikzjax.com/v1/tikzjax.js'
script.onload = () => {
if (typeof window.onload === 'function') {
window.onload()
}
}
document.head.appendChild(script)
} else {
// Already loaded: call the handler again to process new elements
if (typeof window.onload === 'function') {
window.onload()
}
}

return () => {
container.innerHTML = ''
}
}, [tikz])

return <div ref={ref} className={className} />
}
28 changes: 19 additions & 9 deletions data/research.js
Original file line number Diff line number Diff line change
@@ -1,4 +1,14 @@
export const research = [
{
slug: 'safe-owner-reachability',
title: 'Safe Owner List Invariants',
subtitle:
'Formally verified linked list invariants of the Safe smart account.',
description:
'How we proved reachability and acyclicity across all four ownership-mutating functions in the Safe OwnerManager using Verity and Lean 4.',
date: '2026-04-09',
tag: 'Case study'
},
{
slug: 'nexus-mutual-book-value',
title: 'Nexus Mutual Book Value Invariant',
Expand Down Expand Up @@ -38,15 +48,6 @@ export const research = [
date: '2025-07-01',
tag: 'Publication'
},
{
slug: 'what-is-a-formal-proof',
title: 'What is a formal proof?',
subtitle: 'A short explanation for non-specialists.',
description:
'An introduction to formal verification for smart contracts — what it means to prove a contract correct.',
date: '2025-06-01',
tag: 'Explainer'
},
{
slug: 'lido-vault-solvency',
title: 'Lido V3 Vault Solvency Guarantee',
Expand All @@ -56,5 +57,14 @@ export const research = [
'How we proved the solvency invariant of Lido V3 StakingVaults using Verity and Lean 4.',
date: '2025-06-15',
tag: 'Case study'
},
{
slug: 'what-is-a-formal-proof',
title: 'What is a formal proof?',
subtitle: 'A short explanation for non-specialists.',
description:
'An introduction to formal verification for smart contracts — what it means to prove a contract correct.',
date: '2025-06-01',
tag: 'Explainer'
}
]
5 changes: 5 additions & 0 deletions lib/getSortedResearch.js
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
import { research } from '../data/research'

export function getSortedResearch() {
return [...research].sort((a, b) => b.date.localeCompare(a.date))
}
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nexus Mutual page missed getSortedResearch migration

Low Severity

Every research page was migrated from import { research } to getSortedResearch() except nexus-mutual-book-value.jsx, which still imports the raw research array directly. This means the "More research" section on that page uses raw array order instead of the date-sorted order all other pages guarantee, creating an inconsistency that could produce different orderings if the data file is reordered in the future.

Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit e1fbac6. Configure here.

4 changes: 2 additions & 2 deletions pages/research/formalizing-transaction-interpretation.jsx
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import CodeBlock from '../../components/research/CodeBlock'
import Disclosure from '../../components/research/Disclosure'
import ExternalLink from '../../components/research/ExternalLink'
import HighlightedDSL from '../../components/research/HighlightedDSL'
import { research } from '../../data/research'
import { getSortedResearch } from '../../lib/getSortedResearch'

export default function WhyClearSigningShouldNotRequireTrustPage() {
const canonicalUrl =
Expand Down Expand Up @@ -36,7 +36,7 @@ export default function WhyClearSigningShouldNotRequireTrustPage() {
},
mainEntityOfPage: canonicalUrl
}
const otherResearch = research.filter(
const otherResearch = getSortedResearch().filter(
(r) => r.slug !== 'formalizing-transaction-interpretation'
)

Expand Down
4 changes: 3 additions & 1 deletion pages/research/index.jsx
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,11 @@ import Head from 'next/head'
import PageLayout from '../../components/PageLayout'
import ResearchCard from '../../components/ResearchCard'
import SectionHeader from '../../components/ui/SectionHeader'
import { research } from '../../data/research'
import { getSortedResearch } from '../../lib/getSortedResearch'

export default function ResearchPage() {
const research = getSortedResearch()

return (
<>
<Head>
Expand Down
39 changes: 3 additions & 36 deletions pages/research/lido-vault-solvency.jsx
Original file line number Diff line number Diff line change
Expand Up @@ -6,48 +6,15 @@ import Guarantee from '../../components/research/Guarantee'
import Disclosure from '../../components/research/Disclosure'
import CodeBlock from '../../components/research/CodeBlock'
import ExternalLink from '../../components/research/ExternalLink'
import { research } from '../../data/research'

function Hypothesis({ name, constraint, source, children, border = true }) {
return (
<li
className={`list-none ${border ? 'border-b border-gray-200/50' : ''}`}
>
<details className="group/hyp">
<summary className="px-5 py-3 cursor-pointer select-none list-none flex items-center gap-3 [&::-webkit-details-marker]:hidden">
<svg
viewBox="0 0 24 24"
className="w-3.5 h-3.5 text-muted/50 transition-transform group-open/hyp:rotate-90 flex-shrink-0"
fill="none"
stroke="currentColor"
strokeWidth="1.5"
strokeLinecap="round"
strokeLinejoin="round"
>
<polyline points="9 6 15 12 9 18" />
</svg>
<code className="font-mono text-[12px] font-medium">{name}</code>
<span className="text-muted text-[13px]">{constraint}</span>
</summary>
<div className="px-5 pb-3 pl-12 text-[13px] text-muted leading-relaxed">
<p className="mb-1">
<span className="text-[11px] font-mono uppercase tracking-wider text-muted/60">
{source}
</span>
</p>
<p>{children}</p>
</div>
</details>
</li>
)
}
import Hypothesis from '../../components/research/Hypothesis'
import { getSortedResearch } from '../../lib/getSortedResearch'

const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
./scripts/run_default_agent.sh lido/vaulthub_locked/locked_funds_solvency`

export default function LidoVaultSolvencyPage() {
const otherResearch = research.filter(
const otherResearch = getSortedResearch().filter(
(r) => r.slug !== 'lido-vault-solvency'
)

Expand Down
Loading