Pinned Loading

1. mcp-seal mcp-seal Public

   Verified MCP approval-gate sidecar: blocks agent tool-calls until a human one-shot approval exists. Four safety rules proven in Lean 4.

   Lean

2. 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

3. safemesh safemesh Public

   Formally verified coordination primitives for ad-hoc mesh networks (Lean 4 + no_std Rust). BUSL-1.1.

   Rust

4. temporal-logic-lean temporal-logic-lean Public

   Sorry-free Lean 4 formalisation of LTL over infinite traces, ending in an executable safety monitor that turns the Safety Seal's enforcement guarantee from an axiom into a theorem.

   Lean

5. flywheel-universe flywheel-universe Public

   budgeted hebbian kuramoto with fixed support and symmetric-frobenius projection — control/calibration algorithm for oscillator-based ising machines

   Jupyter Notebook

6. kuramoto-lean kuramoto-lean Public

   Lean 4 / Mathlib formalization of finite-N Kuramoto synchronization: ODE existence + uniqueness, order-parameter bounds, Lyapunov descent, and convergence to synchrony for all-to-all AND general sy…

   Lean