mayank

Spent nights over the last six months combining AI coding agents with containers, spec-driven development, and formal verification, so that I (eventually) don't have to manually review 10k+ lines of AI code a day, or worry about the latest model wiping out my home directory:

https://www.overplane.dev/ (Apache-2.0)

TL;DR: Overplane is an AI build system that pairs popular AI coding agents with containers, spec driven development, and automatic lightweight formal verification for a safer, replayable AI codegen workflow.

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.

Such a great comment, and I agree with all of them.

For me in a similar vein:

- mar ‘24: thinking about how to survey the field and implement a hard research task in Natural Language Processing, and then just approximating it well enough with a prompt and a completions api

- mid ‘25: Llama 3 being able to analyze a good sized codebase I was onboarding onto, and synthesize it into diagrams that matched the quality of ones I’d generated by hand with deterministic tools.

- dec ‘25: opus 4.5 basically generating multi-class modules and tests perfectly (syntactically). Finding that errors were my own under-specification of the prompt. Stopped writing code by hand, mainly because it was good enough and came with tests, docs, build scripts, and other goodies for free.

Indeed! It’s a form of a branch table: https://en.m.wikipedia.org/wiki/Branch_table

Got a source for this? Because it’s brilliant.

Agreed and flagged, this almost seems LLM written, not a bit of data.

This seems odd. If your scribe can lie in complex and sometimes hard to detect ways, how do you not see some form of risk? What happens when (not if) your scribe misses something and real world damages ensue as a result? Are you expecting your users to cross check every report? And if so, what’s the benefit of your product?

They need to reword this. Whoever wrote it is a liability

Sounds like it’s been written specifically to avoid liability.

Very interesting! I wonder to what extent this assumption is true in tying completions to traditional code autocomplete.

One of the biggest constraints on the retrieval implementation is latency

If I’m getting a multi line block of code written automagically for me based on comments and the like, I’d personally value quality over latency and be more than happy to wait on a spinner. And I’d also be happy to map separate shortcuts for when I’m prepared to do so (avoiding the need to detect my intent).

aws s3 bucket needs to match the domain for website hosting.

This is outdated information, and not required anymore when using CloudFront.

And even in the past, you could use the S3 API to implement a reverse proxy without matching bucket and domain names.

the minimal runtime is typically the best estimator

Depends what you’re estimating. The minimum is usually not representative of “real world” performance, which is why we use measures of central tendency over many runs for performance benchmarks.

This is a pretty standard measure called the Trimmed Mean: https://statisticsbyjim.com/basics/trimmed-mean/

Very debatable, if both are done right.

It is in industry, but you may be shocked if you read “research code”

You don't actually write code with e2b. You write technical specs and then collaborate with an AI agent.

If I want to change 1 character of a generated source file, can I just go do that or will I have to figure out how to prompt the change in natural language?

Because there are many services (each with their own readiness criteria), a cold boot takes a long time until all services stabilize (worst case I've seen was over 30 minutes). With hibernation they can resume where they started off within a couple of minutes.

This is exactly what we use hibernation for in conjunction with EC2 Warm Pools -- fast autoscaling of services that have long boot times. There's an argument to be made that fixing slow boots should be the "correct" solution, but in large enough organizations, hibernated instances are a convenient workaround to buy you some time to navigate the organizational dynamics (and technical debt) that lead to the slow boot times in the first place.

This is a wonderful article, architecture, and project. Can anyone from Clickhouse comment on any non-technical factors that allowed such a rapid pace of development, e.g. team size, structure, etc.?

All modern languages heavily borrow from each other’s latest iterations. In the case of Java though, playing catch up is by design since it’s intended to be a conservative/stable language.

Wow....confirmed!

`{"errors":[{"message":"Your current API plan does not include access to this endpoint, please see https://developer.twitter.com/en/docs/twitter-api for more information","code":467}]}`

Can you comment on a reply below that claims there was promotional pricing in 2019 at launch?

https://news.ycombinator.com/item?id=33929132

Exactly! Hashcash was proposed in 1997: https://en.m.wikipedia.org/wiki/Hashcash similar mechanics for a different use case

- /organizations/:id

- /blogs/:id

The pragmatic, large-company-only counterpoint is the narrow edge case where:

- :id must be human-readable for "SEO reasons"

- there are many competing organizations and blogs to the point where there may be a name collision.

Although in that case, I'd still suggest:

/:organization-name/:blog-name

There's a hierarchical modeling paradigm/tools called C4 that (while being boxes and lines) helps with the zoom-in/zoom-out nature of understanding systems: https://c4model.com/

I still can't get over the banana-pants insanity of the first count... arguing that Twitter lied about its numbers for years specifically so that someone would buy it at an inflated price?

Not a lawyer, so could you explain why this is banana-pants insanity? There's malicious fraud (unlikely) and then there's the more likely case of under-investing in bot-detection and expunging efforts, e.g. "in favor of other priorities", to keep DAUs and subsequently valuations high for a potential sale.

I agree! But —

- BigQuery is available on GCP

- Bazel is an open source Blaze

- google source formatting (for java at least) is open source

There are probably more…

The big difference now is the convergence of code written for both server and client, and compilers which help strip down and optimize what happens in the client.

I understand the spirit of your comment, but this was/is also true of Google Web Toolkit (GWT).

I can detect a cyclic reference before I even finish writing the code, what's the point of letting the compiler figure it out?

The compiler generally has better attention to detail and the ability to deal with larger object graphs than the typical human.

Yes, but modern DI (like Dagger for Java) can detect cyclic dependencies at compile time and break the build.

Aurora on spot

How would that work for a database? And have you considered or tried Aurora Serverless?

I don't think this is cynical, it's a restatement of the "nobody gets fired for buying IBM" adage. Choosing PlanetScale at this stage in its market penetration is almost certainly going to be seen as the riskier business choice over RDS Aurora (even though it's not quite apples:apples) or GCP Spanner (which is). You can choose to spend your innovation token there, but you better be prepared for the downside when PlanetScale goes down and everything else is up.