Inspiration

Writing the code is the easy part. The dangerous work is everything after: a migration that runs clean but corrupts data or locks a table while every request queues behind it, a dependency with a fresh CVE, a dead app nobody maintains. That is "life after code," and it is where real systems go down.

The tools we had stop short. Linters read the SQL and guess ("may fail on NULLs"). The agents people build make small, safe edits, because they cannot prove the risky ones are safe. We wanted an agent that makes the change teams actually fear, proves it can't break production on the real data, and ships it with no one in the loop.

What it does

Molt is one agent for everything that happens after the code is written. You open a GitLab issue in plain English; a war room of agents makes the change, the engine proves it on a throwaway copy of the real system, and it ships to Google Cloud with no human in the loop. When a change isn't safe, molt refuses and shows the exact rows that break it.

  • "Store each user's last login." Molt writes a zero-downtime migration, proves the old and new app both keep working on 500,000 real rows under live load, opens the merge request with the proof, merges it, and rolls it out: 0 failed requests. Nobody clicked anything.
  • "Make emails unique." Refused: 7 people signed up twice, and which account survives is a human decision.
  • "Cut the assistant's vector storage to save money." Refused: it proved search quality would drop from 97% to 83%.
  • A dead app, revived as an AI app. helpy, a helpdesk abandoned since 2020, brought back on today's Postgres, turned into an AI app, and its years of security holes patched, each one proven to actually close the hole, not just bump a version.
  • Nine real third-party systems. Langfuse's own production outage caught before it ships, Mattermost's 57-second write lock measured, a mobile app that crashes on a renamed field, an AI agent whose tools change underneath it, a drone's safety flag that flips meaning between firmware releases.

The principle: the agents explore; the engine decides. Agents propose and repair within strict limits; a deterministic proof, not a model, returns SAFE or UNSAFE, so it can't be talked into a wrong "safe."

How we built it

Three GitLab Duo flows (migrate, keeper, incident) run as CI jobs and call molt's own MCP server. The proof engine runs on throwaway clones of the real database: it runs the migration's up over every row; runs both app builds mid-migration and checks their reads and writes still agree; tries adversarial edge values; checks the rollback restores every table byte-for-byte; and load-tests the change against the naive ALTER. For the AI app it also proves retrieval quality, agent memory, and tenant isolation. Zero-downtime rollout uses pgroll (expand/contract); a watcher checks seven production signals from inside the VPC and rolls back on any regression, opening an incident that a second flow diagnoses and fixes. The app is a store plus a multi-tenant AI support assistant, on Cloud Run with Postgres 16 + pgvector on a VM, deployed by the pipeline with keyless OIDC (no Google key stored anywhere). The engine is also proven against a live AWS RDS instance as a non-superuser.

Challenges we ran into

  • LangGraph's default wiring puts its checkpoint tables in pgroll's version schema, so the next ordinary migration silently deletes every agent conversation. We caught it and now refuse it.
  • Stock pgroll had real bugs under live load (writes failing while a NOT NULL column changes; index creation failing; a lock timeout that reached only one pooled connection; indexes copied without their operator class, breaking every vector index). We found and fixed five; they are offered upstream.
  • A heuristic that emits "safe" from the absence of evidence is worse than no check. We made every layer fail closed: it defers to a grounded source or refuses, and never guesses safe.
  • We kept the proof empirical (run on real rows under real load) rather than formal, because the failures that take systems down live in the data and the runtime, not in the SQL's abstract semantics.

Accomplishments that we're proud of

  • On the benchmark: 27 of 27 dangerous changes stopped with the real cause named every time, and 12 of 12 safe changes let through. Squawk, a popular linter, names 5 of 27 causes and passes none of the 12 safe.
  • Proven on nine real third-party systems, each re-run from a fresh clone in CI.
  • Revived a dead app and turned it into an AI app, every step proven.
  • Live and fully hands-off on Google Cloud, with a keyless deploy.

What we learned

Diversity belongs in exploration; determinism belongs in judgment. An LLM judge can be reward-hacked by a single crafted token, so the verdict has to be code; agents sit in judging only to raise concerns, never to clear a failure. And running against real data finds the bugs a formal proof would declare equivalent and ship.

What's next for molt

  • Make the captured real query workload (from the live database) the default source, so apps that build queries dynamically are covered.
  • A formal SQL-equivalence prover as an optional ceiling, behind the same interface as the empirical proof.
  • The keeper adopting more abandoned apps on a schedule, patching and reviving them with no one watching.

Built With

Share this project:

Updates

Submission history