tech
-
Essay
Verified Inference Between Adversaries Revised from 29 August 2026
An operator can fabricate execution logs and hold approved weights while running something else. VerInf investigates proofs of language-model inference that mutually distrustful parties can verify on their own hardware. This living document explains what the proof certifies, the system I started from, and my work on profiling, prover optimization, and scale-out during the MARS V fellowship.
Upstream merge status and the limits of archived Maverick proofs: constraint repairs and incomplete model binding.
-
Essay
Proof Broker accepts nothing it cannot check. For R6, I put a live language model behind that boundary and asked it for arithmetic proof certificates on a census of fifteen obligations from a real Lean development, the eleven its interface could pose, eight times each, with the analysis frozen before the cohort’s first call. Every certificate it was asked for that could exist came back and verified: 80 of 80. Proof coverage stayed at six of fifteen obligations from the first draw to the eighth, because posing goals and turning certificates into proofs, not finding certificates, was the constraint. This essay reports that result, what an outside reader can verify about it, the two amendments made after collection, and what “consumed” turned out to mean.
-
Essay
Proof Broker: Separating Proof Search from Trust Revised from 5 September 2026
Proof search is improving faster than the case for trusting it. Proof Broker puts a boundary between the two: Lean and Rocq send a goal out to external provers, take back a certificate with a graded trust tier, verify it at the boundary, and still require a proof term the home kernel checks. Nothing behind the boundary is trusted, so the search behind it can be as aggressive, heterogeneous, or unreliable as finding proofs requires. This essay sets out the architecture, what it makes possible, the first downstream demonstration — 19 of 19 arithmetic obligations closed in a real verification project — and the research program that evidence opens.
R6: the live-model claim updated; companion essay
-
Essay
From Path Tubes to a Near-Critical Domination Bound Revised from 22 July 2026
A first-person, code-heavy companion tracing the near-critical bound that led to The Annealed Critical Window for Growing-Radius Domination in Random Regular Graphs. Rather than reproducing its theorem-and-proof form, this page traces where the problem came from — a cops-and-robbers hypergraph question that collapsed into a domination bound — why the answer carries an unnecessary coupon-collector logarithm, and how a chain of computational detours (a failed concavity conjecture, a catastrophic cancellation, an independent audit that caught a stale constant) repeatedly redirected the proof before it reached its final shape.
Clarified the scope of the tube interpretation, linked the corrected current preprint, and recorded the resolved bounded critical window.
-
Essay
Software engineering does so little epistemic work that it hardly earns the name “engineering.” The field has never learned to distinguish provenance — where an artifact came from — from warrant — why anyone is entitled to rely on it. Authorship, a passing test suite, and a completed review are routinely mistaken for the second when they are only ever the first; libraries are the rare exception, where warrant is actually constructed and amortized across users who never read the source. LLM-generated code inherits neither comforting story, and the discomfort that provokes is not a new problem but the oldest one in the profession, finally felt without the anaesthetic that provenance usually supplies.
-
Essay
As we approach AGI, the increase in the ability of Artificial Intelligence models to infer a robust specification from a sparse prompt will lead to a devastating trend of homogeneity. We argue that this is the primary concern regarding the interaction of AI and human intelligence, rather than blanket claims that “AI reduces human cognitive ability.”
-
Essay
TCP/IP, RIP, UDP, and DNS implementations in Go, supporting file transmission of up to 1 GB across networks of up to 8 virtual machines. Extended with a fully RFC-compliant SSH implementation (2,000+ additional lines) supporting sustained sessions of arbitrary length.
-
Essay
Full Unix-like kernel in ~7,000 lines of C, written for Brown CS 169 (Operating Systems with Lab): virtual memory, VFS, system calls, threading, device drivers and interrupt handlers, and file systems. Custom linker support for running userspace x86-64 ELF binaries.
-
Essay
AI labs are likely deliberately reluctant to scale because they are aware that any imminient shift to locally run models as the norm would render their compute redundant. We take Anthropic as a principal case study to validate this hypothesis.
-
Essay
We systematically decompose the sources of SIMD speedup for ML-KEM (Kyber) on Intel x86-64 AVX2. By benchmarking four compilation variants, we demonstrate that GCC’s auto-vectorizer provides negligible benefit, and that hand-written AVX2 assembly delivers a – performance increase for core arithmetic operations. This drives an end-to-end KEM speedup of –.