Proof Website

Project Overview: Proof is my main focus today, and the most ambitious thing I’ve built so far. AI now writes a huge share of our code, which raises a question the industry has quietly skipped: AI writes your code — who verifies the intent? Tests check behavior on specific inputs, but they can’t tell you whether the code matches what you actually meant. That gap multiplies as AI generates code faster than any team can review it.

Proof closes that gap with formal methods. Instead of hoping your tests cover the right cases, you write requirements as precise, machine-checkable specifications, and Proof mathematically proves they hold. Tests check inputs. Proof checks intent.

The workflow is a four-stage chain:

1. Write — author requirements with AI assistance and real-time validation, stored as plain YAML in your Git repo.
2. Verify — formal verification using Kind2 realizability checking and Z3 SMT solvers proves your requirements are consistent, physically realizable, and free of vacuous conditions and gaps — before a line of code is written.
3. Trace — bidirectional traceability links requirements to code, tests, and documentation, so you see the blast radius of every change and catch drift instantly.
4. Document — compliance reports for standards like NPR 7150, DO-178C, and ISO 26262 are generated automatically from the trace data.

Proof also brings MC/DC (Modified Condition/Decision Coverage) — a capability that historically lived in $50K+/year aerospace toolchains — to modern languages: Go in production, JavaScript/TypeScript in beta, with C/C++ and Rust on the way.

The design principles come from a decade of building developer tools: AI-native, CLI-first, Git-native, zero vendor lock-in. Everything lives as YAML files in your repository, it layers on top of existing codebases without rewrites, integrates with Claude Code and Copilot, and runs in CI with fast feedback. The formal methods foundation draws on research from NASA FRET, CERN, and the aerospace industry — applied to everyday software teams who suddenly find themselves reviewing more code than they write.

Outcome

Proof is currently in private beta, working with teams that use AI coding tools and teams in regulated, safety-critical industries. It represents what I believe is the next necessary layer of the software stack: as AI takes over writing code, humans need mathematical confidence that the code does what was intended. Try it at reqproof.com.