Independent researcher · formal methods and systems
I build small, machine-checked developments in Lean 4 and the engineering that connects them to running code: conformance tests, signed evidence, and plainly stated limits.
Seal is a permission gate for AI agents. Its current production adapter mediates MCP
tools/call: protected actions are blocked by default, and a blocked action runs
only after a person approves that exact action, once. When the gate can write its receipt directory, every decision is recorded as a receipt.
It enforces authorization at the effect boundary; it does not claim to read intent.
Seal supports Linux x86-64 only. macOS, Windows, Linux ARM, and other
platforms are not supported by this download. Download
seal-v0.2.0-rc.2-linux-x64,
then install it with
./seal-v0.2.0-rc.2-linux-x64 --sha256 c652f47f82778bda978725837ec77f182229872f13c12fd5a1f8619149666347 --bytes 6146418 --prefix ~/.local.
A Lean 4 / Mathlib formalisation of hard and soft attention expressivity over Boolean cubes.
The main theorem shows that for every odd n ≥ 5, strict majority needs at least
(n+3)/2 attention heads — one more than its certificate bound — and the five-bit case is
exact: k(maj₅) = 4. Structural proofs are kernel-checked with no
sorry and no native_decide; enumerated cases are isolated and
pinned separately.
An embeddable library for state that must converge after network partitions. The verified claim is narrow and stated in-repo: five CRDTs (G-Set, G-Counter, PN-Counter, OR-Set, RGA/Text) carry Lean convergence proofs, tied to the Rust implementation by differential tests against a Lean-generated oracle. The event log, wire encoding, and language bindings are tested engineering, not proofs.
safemesh · crdt-lean · temporal-logic-lean
A family of small Lean 4 developments, each pinning one claim — gradient descent,
Kuramoto synchronisation, CRDT convergence, temporal-logic enforcement, PAC bounds — with
axiom footprints and non-claims listed per repository, indexed in one place. The
kuramoto-lean count is 39:
on its master branch, count only lines beginning theorem in tracked
*.lean files, excluding paths in test/tests and example/examples directories;
lemmas and private declarations do not count. From a fresh clone, run
git ls-files '*.lean' | awk '!/(^|\/)[Tt]ests?\// && !/(^|\/)[Ee]xamples?\//' | xargs -r grep -h -E '^theorem ' | wc -l.
For the reader who wants the proof story behind Seal, the family target is
one sentence: the agent authorization gate whose decision rule is machine-checked, whose
effect commitment is tested for sufficiency, and whose deployed decisions can be
independently re-derived against pinned kernel bytes. Each clause is a family claim with
today’s scope. The decision rule is a Lean 4 development whose theorems cover the
mediation kernel — non-bypass and a verifiable record — not the whole deployed system. The
effect commitment is tested to carry enough to identify the exact effect it
authorizes, not assumed to: the pre-v2 field set failed that check on a concrete collision,
and that is why args_hash exists. Independent re-derivation against pinned
kernel bytes holds for the family’s kernel receipts, which replay in seal-check
against wasm whose bytes are pinned and re-hashed: for those receipts, every decision emits
a tamper-evident receipt anyone can re-derive in a browser or CLI, with no toolchain to
install. Those claims remain scoped to the family’s kernel receipts. The
family’s Rust and wasm artifacts (seal-host and the assurance kit) are connected to
the proofs by byte-exact conformance tests over a corpus, not by a theorem about every
compiled instruction. What is proven, tested, assumed, and not
claimed is kept in one table: the
claims
matrix.