Satchel Hamilton
About

Making the unverifiable verifiable

Satchel Hamilton

Independent — building open verification tooling for AI systems. Open to senior roles in verification, dev-tooling, and AI reliability.

I'm Satchel Hamilton — a software engineer shaped by EDA, the one corner of software where correctness-under-combinatorial-complexity is the whole job: formal verification, exhaustive test strategy, automation that has to be right at production scale. For two years at Synopsys I built design-automation tooling in exactly that culture — and what I took from it isn't a toolchain, it's a posture: if a system matters, you should be able to prove things about it.

Now I aim that posture at AI, where trust and reliability are the central unsolved problem. The result is a family of tools that each make one unverifiable thing verifiable: Congruent proves an AI-rewritten function equivalent or produces the input that breaks it; Toroid has an LLM propose formal properties for hardware designs and lets a model checker judge them; Kinescope records every nondeterministic moment of an agent run so it can be replayed exactly; Crucible turns test-time compute into measured accuracy via verifier-guided search; Gatecheck gates CI on eval regressions. The same instinct points beyond AI — Verderer keeps a tamper-evident, offline-verifiable ledger of how public environmental data changes.

Currently

  • Independent — building the verification-for-AI toolkit above, in the open.
  • Open to senior roles in verification, developer tooling, and AI reliability.
  • On the side: real-time graphics, simulation, and game systems.

Background

  • Synopsys — Design Automation Group (2024–2026). Agentic tooling that generated tested compliance checks from plain-English specs (cut authoring time ~80%; 12 engineers shipped 90+ checks across 6 products), a repo-local AI code-review framework across Python/Perl/Tcl with a RAG assistant grounded on a 500+-file engineering corpus, and a config-driven release-staging engine that took per-release staging from ~8 hours to under 30 minutes.
  • Before that: a multi-service REST API for ADS-B air-traffic data (Sagetech Avionics, WSU capstone) and a 7,000+-line VHDL test bench verifying 50+ modules of an industrial motion controller (Delta Motion).
  • B.S. Computer Science — Washington State University Vancouver.
  • Started in hardware: A.A. with an electronics-technology focus, Kaua'i CC.

Research

Civilodynamics is a founding research program that treats civilizational dynamics as a measurement problem — pre-registered, falsifiable, and honest that no index has been computed yet (DOI 10.5281/zenodo.20917966). And LSAP-1 points the same instrument-building instinct at prose: a pilot protocol that scores a passage of fiction on thirty anchored axes — and publishes its own reliability numbers, unflattering ones included. Research identity: ORCID 0009-0001-9871-5607.

The part that doesn't fit on a resume

I write fiction seriously — short stories and worldbuilding maintained with the same discipline as the code, down to custom tooling that checks new chapters against established canon. Rigor, it turns out, is portable: the same instinct that gates a silicon release also catches a continuity error in chapter twelve.

Find me