I build tools for AI-agent approvals and distributed state, then make their evidence easier to inspect. Architect working across data platforms, APIs, formal methods and AI research.
Apps · Demos · Research · About
|
Approve the exact tool call. Keep the receipt. A local MCP approval gate for Claude Code. Inspect the proposed call, approve it at most once, and get a signed decision receipt. Seal refuses calls that drift from what you approved. It is a gate, not a sandbox. Check a receipt in your browser · Review the evidence with the CLI |
Make local edits. Bring replicas back together. A Rust CRDT core with language bindings for merging distributed state. Explore counters and set membership, save and restart replicas, then exchange their state. You bring the transport and application schema. Open the Lab → · Docs · Source Start with Rust or TypeScript. Source builds; |
The Seal family: seal gates calls; seal-check checks supported receipts locally in your browser; seal-assurance-kit makes the kernel's evidence runnable from a CLI. Separate tools let you inspect the product's claims from outside it, with shared kernel and format dependencies still in scope. Checking a receipt does not establish that the recorded tool effect happened.
Also in the toolbox: collision-check finds counterexamples to observational claims within a declared finite or sampled space. Roundtable coordinates AI CLI assistants through a local MCP server.
| Open a demo | What to explore |
|---|---|
| SafeMesh Lab → | Make independent edits, exchange state and watch replicas merge. Runs the Rust core through WASM. |
| Seal receipt checker → | Paste a supported receipt and inspect the result locally. Start with the example receipts. |
| Coordination Kernel → | Explore a numerical illustration of Kuramoto synchronisation, with theorem conditions and counterfactuals. The simulator itself is not verified. |
| Hebbian–Kuramoto playground → | Change topology, coupling and perturbations in an interactive research demo. |
Prefer a terminal? Follow Seal's approval walkthrough or SafeMesh's partition-and-heal example.
Alongside the apps I keep a machine-checked Lean 4 proof corpus on optimisation, learning, dynamics and distributed systems. It has its own index, with the repositories, theorem statements and current status: Lean index →. More about me and the research is on my website.
Witness Lab tests whether local witness information helps neural models on synthetic tasks. Most of the broad hypotheses did not survive. The remaining positive result is narrowly scoped; the retrospective explains what held up and what did not.
Claims need receipts. Lean proofs concern their stated models. Tests, finite conformance checks, numerical demos and deployed software each have a different scope. I keep those distinctions visible, including what remains assumed or unfinished.
For the apps, start with Seal's guarantees and non-guarantees and SafeMesh's proof boundary.
I'm Ben Cassie, velvetmonkey. My background is in ESG data platforms and API architecture; my current work brings practical tools, AI research and formal methods together.