Like many others, I’ve watched AI code pile up at work, and get increasingly lighter reviews due to its size and maddening uniformity. On my side projects at night, I see the full speed and fragility of vibe coding. Neither practice seems sustainable, so I’ve been playing around for the last few months looking for a balanced, middle ground.
The key idea here is similar to chip design: if AI written software functionally does what you intended it to (by virtue of increasingly sophisticated testing against a codification of your intent), then it’s perhaps less important to manually review every line of generated code.
Overplane is a labor of love that brings that idea to life as an open-source experiment, combining some old personal loves: containerization, content addressed build systems, and formal verification.
The example I’d start with is rustdis, a partial, wire-compatible Redis clone in Rust with an empty [dependencies] section. Created with seven short specs and about $45 of Claude Opus, in about three hours: https://www.overplane.dev/examples
What sold me on the approach is that the one IR generated by Overplane from the specs paid for itself downstream: Z3 checks at build time, 48 generated proptest properties, and Kani proofs on the parser and arithmetic core.
It also holds up against redis-benchmark better than I expected, within about 90% of real Redis on my box unpipelined and a bit ahead on some pipelined workloads, which I mostly attribute to rustdis doing less than Redis does.
It’s v0.0.8 and rough. If you’ve tried spec-first workflows or lightweight formal methods in anger, I’d love to hear where they broke down for you.