Add ERC-4337 EntryPoint proof case study

[Th0rgal]

Summary

• add a new research case study for the ERC-4337 EntryPoint execution invariant
• add a toggleable English/formal guarantee component matching the Safe article pattern
• add the article to the research index metadata

Notes

• the article is written under the assumption that the faithful Verity model and benchmark proof work in Improve executable ERC-4337 semantic stubs verity#1746 and Add ERC-4337 EntryPoint invariant benchmark case verity-benchmark#32 are fixed/perfect, as requested
• links point to the benchmark PR branch and Verity PR used by the case study

Verification

• npm run build

---

Note

Low Risk
Low risk: changes are limited to new static research content/components and a metadata entry, with no backend logic or security-sensitive flows affected.

Overview
Adds a new research case study page at /research/erc4337-entrypoint-execution describing a formally verified ERC-4337 EntryPoint validation-before-execution invariant, including links, proof-status table, and verification instructions.

Introduces EntryPointGuarantee, a small UI component that auto-switches from an English statement to a set of formal invariants after 5 seconds (and allows manual toggling).

Updates data/research.js to include the new case study in the research index metadata.

^{Reviewed by Cursor Bugbot for commit bbd305b. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
lfglabs-dev	Ready	Preview, Comment	Apr 24, 2026 4:43pm

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit b2f7e9b. Configure here.}