Ethics
I.I-XI of Spinoza's Ethics, formalized in Coq
Possibly Available
About
Formal methods for Ethereum in Lean 4 — building Jaune and Blanc.
Evidence-backed skills
Repositories
tesc
TESC proof format for first-order ATPs
blanc
Minimal EVM Language for Interactive Verification
jaune
An executable formal specification of the EVM, in Lean 4
execution-specs
Specification for the Execution Layer. Tracking network upgrades.
ethereum_formal_verification_overview
Overview of the formal verification projects in the Ethereum ecosystem.
MiniGoedel
Smullyan's miniature Gödelian language in Coq