About

I’m an engineering leader with over 25 years building complex distributed systems, and I know from experience how much the quality of a system’s specification determines whether the project succeeds.

Large language models are remarkably good at producing code, specs, and reasoning — but they’re unreliable in exactly the ways that matter most for complex distributed systems. Formal verification tools like TLA+, Z3, and Alloy are precise and trustworthy in exactly those ways — but they’re expensive to use, hard to learn, and surprisingly easy to get subtly wrong even when you think you’ve got it right.

The gap is between neural systems that generalize and communicate fluently but are prone to error, and symbolic systems that are precise but don’t generalize easily and speak in structured grammars that are hard for humans to use. This site is my attempt to close that gap.

The approach I’m exploring is neuro-symbolic AI — combining neural systems (like LLMs) with symbolic reasoning (like formal logic and model checking). The specific technique I keep coming back to is CEGIS: Counterexample-Guided Inductive Synthesis. You use an LLM to generate candidate solutions and a formal verifier to check them, feeding counterexamples back until something passes. Neither side alone is enough; together they cover each other’s weaknesses.

I’m working through this in public, which means some of what I publish here will be wrong. I’ll say so when I find out. The goal isn’t to be authoritative — it’s to build something useful for the people who come next, whether that’s a resource for learning or a set of working patterns that hold up under scrutiny.

Reach out at [email protected] .