Skip to content

Navigation Menu

Sign in
Sign up
@velvetmonkey
velvetmonkey
Follow

Ben Cassie velvetmonkey

Claims need receipts. - Built in the open. When a repo says zero sorry, it means zero sorry.

Highlights

  • Pro

Block or report velvetmonkey

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
velvetmonkey /README.md

Ben Cassie — velvetmonkey

Claims need receipts.

Formal verification, AI research, and a healthy allergy to overclaiming.

Senior Software Architect (ESG data platforms, API architecture) working at the seam of formal verification and AI research. I build verified tools for AI agents and a machine-checked Lean 4 proof corpus. If it is claimed here, it is proved, tested, or it says plainly what is trusted.

Verified tools for AI agents

Repo What it is
seal A local MCP approval gate for Claude Code: exact-call prompts, at-most-once approval, drift refusal, and signed decision receipts. Seal is a gate, not a sandbox.
safemesh · Documentation Lean 4 proofs behind five CRDTs (G-Set, G-Counter, PN-Counter, OR-Set, RGA/Text) in no_std Rust, with C ABI, WASM/TypeScript and Python surfaces. You bring the transport.
canary LangGraph pipeline for ESG regulatory-change monitoring: fetch, detect, extract, verify, report.

The Lean 4 proof corpus

A cited, importable library of machine-checked mathematics spanning the spine of modern AI: optimisation, dynamical systems, learning theory. Most repos are zero-sorry; each states its axioms and any documented gaps.

Live landing page: https://velvetmonkey.github.io/lean/ This page is the index. Start here rather than hunting the individual repos.

Convex optimisation and gradient methods

Repo Result
gradient-descent-lean GD convergence for smooth convex optimisation. 17 theorems, zero sorry.
nesterov-lean Nesterov accelerated gradient descent.
heavy-ball-lean Polyak heavy-ball convergence.
proximal-gd-lean Proximal gradient descent for composite objectives.
projected-gd-lean Projected gradient descent convergence.
subgradient-lean Subgradient method for nonsmooth convex objectives.
mirror-descent-lean Mirror descent with Bregman divergence.
frank-wolfe-lean Frank-Wolfe (conditional gradient).
coordinate-descent-lean Cyclic coordinate descent convergence.
admm-lean ADMM convergence, primal/dual residuals.
newton-lean Newton's method quadratic convergence.
sgd-lean Stochastic gradient descent convergence.

Learning theory and online learning

Repo Result
pac-learning-lean PAC learning bounds, Hoeffding inequality.
online-learning-lean FTRL regret bounds for online convex optimisation.
replicator-lean Replicator dynamics on the standard simplex.

Dynamical systems and stability

Repo Result
kuramoto-lean Finite-N Kuramoto synchronisation.
lyapunov-odes-lean Lyapunov stability for autonomous ODEs.
lasalle-lean LaSalle's invariance principle.
barbalat-lean Barbalat's lemma and the Lyapunov-Barbalat route.
contraction-lean Contraction theory, Banach fixed point.
lotka-volterra-lean Lotka-Volterra predator-prey dynamics.
langevin-lean Bounded-noise Langevin dynamics.

Distributed systems and consensus

Repo Result
crdt-lean State-based CRDT convergence (AP): Strong Eventual Consistency, conditional liveness under fairness, concrete instances.
consensus-lean Quorum-based consensus safety (CP): quorum intersection implies agreement, at most one value ever chosen.

Neural and associative memory

Repo Result
hopfield-lean Hopfield network energy descent.
modern-hopfield-lean Modern Hopfield network energy descent.
attention-lean Hard-attention expressivity (Mathlib).

Linear algebra and logic

Repo Result
schur-complement-lean Schur complement nonsingular-inverse API and block matrices.
trace-logic-lean Hoffman trace logic formalisation.

Physics

Repo Result
hamiltonian-lean Hamiltonian mechanics and Liouville's theorem.
observer-patch-holography OPH: finite observer-patch reconstruction (active research).

Built in the open. When a repo says zero sorry, it means zero sorry.

📫 linktr.ee/thevelvetmonke · @thevelvetmonke

Pinned Loading

  1. seal seal Public

    A local MCP approval gate for Claude Code: exact-call prompts, at-most-once approval, drift refusal, and signed decision receipts. Seal is a gate, not a sandbox.

    Lean

  2. safemesh safemesh Public

    Lean 4 proofs behind five CRDTs (G-Set, G-Counter, PN-Counter, OR-Set, RGA/Text) in no_std Rust, with C ABI, WASM/TypeScript and Python surfaces. You bring the transport. Open source under Apache-2.0.

    Rust

  3. attention-lean attention-lean Public

    Lean 4 / Mathlib formalisation of hard and soft attention expressivity over finite Boolean cubes: exact head-count bounds proved to the kernel, carried from argmax to softmax at the Boolean-output ...

    Lean

AltStyle によって変換されたページ (->オリジナル) /