The LTL paper got its August revision: the consistency-verifier divergence we reported in July now has a root cause, a one-line fix, and a zero. Here is the story in plain words.
We proved eleven theorems in two days and nobody ever disputed one. Making the words 'formally verified' survive a hostile stranger took months. Ideas we are developing toward a second paper.
Each of our four verified ed25519 libraries went from 16 proven statements to 44. But the real story of the past month is uglier and more useful — what it took to make the script that PRINTS "all green" as trustworthy as the proofs behind it.
Ed25519 signatures are deterministic — same key, same message, same signature, forever. We used that to audit ourselves, re-signing an already-published record and comparing byte for byte. The bytes matched. The exercise still caught a real bug.
We machine-checked the correctness of a quantum-resistant signature verifier, entered that fact into our public, append-only log — and from now on, every new page of that log is stamped twice, once with today's cryptography and once with cryptography built to survive tomorrow's computers.
The Lean Transparency Log looks a lot like an optimistic rollup for verification claims — cheap to assert, expensive to get away with. The resemblance is real and worth having, but the precise version is better than the slogan. Three layers of guarantee, two very different kinds of fault, three honest disanalogies, and one loop that needs no metaphor at all.
The Lean Transparency Log has always notarized proofs about other people's software. As of today it notarizes the proofs about its own machinery — entry 13 is a kernel-checked mechanization of the log's own accumulator, appended into the log itself, verifiable end to end from the live service by anyone with a stock toolchain.
A verification proof is a claim about a specific commit. Claims rot — the repo moves, the axioms drift, "it verified once" becomes folklore. The Lean Transparency Log is an append-only, Merkle-anchored ledger of signed attestations that named proofs re-check with exactly their documented assumptions, plus the agent tooling that asks the only question a downstream consumer cares about.
The Go re-implementation of Swiss Post's e-voting protocol grew up — it now runs as mutually distrusting parties over Rust-signed transport, its return codes are genuinely cast-as-intended, and, the headline, every cryptographic operation renders itself as typeset mathematics with live values, the instant it executes.
The four ed25519 verification pyramids each ended their first post with an honest asterisk — the signature apex was proven at the byte level, and lifting it to the point level was deferred. That deferral is now closed, on all four forks: decompress is extracted and proven, the modular square root is proven, compress is canonical, and the acceptance criterion now reads as a real curve-point equation.
A 106-page LaTeX/TikZ book plus compiling exercise files - a curriculum that takes an undergraduate with zero formal-methods background to the point of reading, and extending, the real Lean 4 proofs in the ed25519/Pallas verification family.
The proof pyramid rebuilt against Solana's solana-ed25519 crate — its own Charon/Aeneas extraction, its own compiled certificates. Forks drift; theorems about the upstream prove nothing about the fork.
The fourth ed25519 target - the curve25519-dalek fork used by Betrusted/Precursor, the security-first open hardware device whose entire boot chain and update trust reduce to this code accepting the right signatures.
Machine-checked correctness for the ed25519 implementation everyone actually ships — field, group law, scalar arithmetic, and the EdDSA acceptance criterion itself — proven in Lean 4 about the Aeneas-transpiled Rust, not about a flattering re-model.
Verification of the Pallas field layer in zcash/pasta_curves — Montgomery-form 4×64-limb arithmetic, with the 255-bit modulus's primality machine-checked via a Lucas/Pratt certificate. A do-over of an earlier attempt that axiomatized exactly the statements that needed proving.
The third target of the ed25519 verification family - RISC Zero's curve25519-dalek fork (v4.1.3), the one that runs inside zkVM guests. A ZK proof attests that code ran; it does not attest that the code is correct. These certificates cover the half the SNARK can't.
A walking, breathing PoC of Mirco Richter's Crisis protocol — a DAG-based BFT consensus that achieves total order in fully open peer-to-peer networks by *deducing* votes from causal structure instead of sending them. Plus a SwiftUI visualizer that walks the protocol end-to-end in extreme slow motion, and an agent-coordination layer that lifts the same machinery from machines reaching agreement to AI agents reaching agreement.
Tooling to study a "buy hashpower on Braiins, mine through OCEAN" strategy in monitor-only mode — recommendations, never orders. The whole point is the discipline of separating *deciding what the right trade is* from *placing it*.
Apple Silicon doesn't expose junction temperatures to userspace. So model them. A tmux-based wall display that takes `powermetrics` output, runs a thermal model with tunable thetas and a clamshell factor, and shows estimated CPU/GPU temperatures alongside the raw power numbers.
A cross-project Jupyter coordinator. `jupyter-hub status`, `ports`, `stop-all`, `orphans`, `which 8889`. The problem it solves is small. The reason it solves it well is that it treats your project layout as authoritative instead of asking you to remember which terminal owns which port.
A local-first, notebook-first course on the Number Theoretic Transform, sized for the version of NTT that actually matters — the negacyclic, modulus-q, base-multiplication NTT inside Kyber. Lecture → Lab → Problems → Studio, six bundles, no IBM dependency.
A local-first Qiskit learning platform that alternates between ideal mode (statevectors, clean circuits, conceptual clarity) and reality mode (transpilation, routing overhead, noisy simulation). The backward-designed target isn't "Qiskit literacy" — it's an independent hardware-aware quantum circuit designer.
A Karpathy-style autoresearch ratchet that proposes, evaluates, and learns from magic-state preparation circuits on the [[4,2,2]] error-detecting code — wrapped in a teaching layer of twelve Jupyter notebooks that explain the same physics through four different pedagogical lenses.
Pull every currently-valid leaf cert with matching SAN substrings out of the public CT logs; verify they're real leaves; assess intended usage via EKU/KeyUsage; scan their DNS names for effective CAA policy; emit a primary readable output as Markdown, LaTeX, and PDF. Made for the case where you want to *publish* the result.
A macOS app for ingesting your corpus — papers, notebooks, archives, the stuff you've read once and need to find again — and exposing it through semantic search and a 3D concept visualization. Local-first. Nothing leaves the device. The model isn't "search engine"; it's "refinery."
GGM-tree puncturable keys in Go. A macOS app/server manages derivation, provider issuance, asset encryption. A native iOS app exists for one purpose — remotely puncturing a provider when something has gone wrong. The asymmetry between primary and emergency surfaces is the point.
A ground-up reimplementation of Switzerland's official internet voting cryptographic protocol as a single Go binary. The reference production system is 14 Java repositories, 500K+ lines of code, and requires 50 GB of RAM. This distills the cryptographic core into 52 files and 2 dependencies.
Polymarket as a substrate for letting LLM-driven agents propose, defend, and rebalance positions on the future itself — a quiet sandbox for studying how machine reasoning behaves when it has skin in the game.
A fully functional proof-of-concept for a perpetual futures DEX whose state transitions are verified by a zero-knowledge proof from the RISC Zero zkVM. The state machine — matching, funding rates, liquidations — runs off-chain. The proof reduces "I have to trust this exchange" to "I can verify a single SNARK."
A small Jupyter-notebook scratchpad for working through where the bottlenecks actually live in Kyber and Dilithium implementations — not the published asymptotics, the real-world cycle counts on the hardware that's available now.
A reinforcement-learning replication of the R1-Zero training recipe on a small countdown task — using the TinyZero pipeline as the substrate. The point isn't the result; it's the discipline of reproducing a published recipe from scratch on consumer hardware.
The 2021 prototype that turned out to be the first draft of everything I've been doing with self-hosted infrastructure ever since — Terraform for the cloud, Kubernetes for the runtime, Ansible for the configuration, PKI for the trust, ACME for the cert lifecycle. Five letters, one pipe.
A 5 KB Solidity exercise from B9Lab's Ethereum developer course. Not a notable artifact on its own. Worth a note because it's the first time I sat with a smart-contract language and felt the specific category of caution it demands.
An archive of notebooks from NVIDIA's 2017 AI Summer School. Predates the current LLM-shaped attention economy by a decade. Worth keeping for what it shows about what people thought "AI" meant when transformers were a year old and 'attention' was the new mechanism nobody was sure about yet.
The default GitHub Pages profile site I set up in 2017. Modest, unmaintained, and exactly the kind of artifact that proves how long this account has been doing this kind of work. Not interesting on its own. Interesting as a date stamp.