Verified Software Generation: The First Protozoa Experiments

01Why this matters

The gap in practice is rarely “can a model produce code for this task.” It is the distance between a confident‑looking draft and software you would actually ship: software that builds, that passes tests, that behaves correctly at the edges, and that stays correct when it is changed later. Most of the effort — and most of the risk — lives in that gap.

Protozoa's stance is that verification is not a step that happens after generation; it is part of generation. A generated system is not considered done because it looks complete. It is considered done when it satisfies its checks, and a change is not accepted because it looks reasonable but because it keeps every prior check passing while satisfying a new one. This is an old idea from disciplined software engineering — specify, test, and only then trust — applied to autonomous generation.

The practical consequence is that the output of Protozoa is meant to be evidence‑backed. For each system we can say not only “here is the code” but “here is the specification it was built to, here are the checks it passes, and here is the record of how it got there.” The two experiments below are the first tests of whether that method produces real, working software across genuinely different kinds of program.

02What Protozoa does

At a capability level, and independent of how it is implemented, Protozoa can:

• Generate from a specification. Given a description of the software to build, it produces a complete, runnable project — source, tests, and the files needed to build and run it — rather than isolated snippets.
• Verify against automated checks. It runs the project against an automated test suite and treats passing those checks as the definition of done.
• Harden and repair under explicit gates. When a check fails, or when a new requirement is introduced, it revises the software under explicit acceptance conditions and re‑verifies. A defect is addressed by first stating the condition that should have caught it, confirming that condition fails on the current software, and then changing the software until that condition passes without breaking any existing check.
• Execute independent work concurrently. Parts of a build that do not depend on one another can proceed in parallel.
• Preserve development evidence. It retains a record of how each system was produced — the specification, the checks, and the outcomes — so that results can be audited and reproduced rather than taken on faith.

The rest of this note reports what happened when this capability set was applied to two concrete systems.

03Experimental setup

We selected two target systems that stress different parts of the method:

• AI Thread Vault — a Python command‑line tool and library that imports exported AI chat histories (ChatGPT, Claude, Gemini, and generic JSON/Markdown), stores them in a local SQLite database with full‑text search, and queries them offline. This exercises data handling, multiple input formats, persistence, and a searchable index — and it must work end to end from the command line with no network access.
• Pong Arcade — a browser game written in TypeScript with a deterministic game core rendered to an HTML canvas. This exercises real‑time behavior, collision and scoring rules, an opponent with tunable difficulty, and the need to actually run and be playable in a browser.

For each experiment we report verified outcomes: whether the software builds and its tests pass; for the game, whether it runs and is playable in a browser; the specific defect‑to‑repair episode where one occurred; and, where the build record was retained, the number of attempts and verification failures. We deliberately do not report token, cost, cache, or timing figures for these runs — see the note on measurement at the end of this report.

Both reported experiments used GPT‑5.4; model‑tier routing was not evaluated here.

04Experiment 1 — AI Thread Vault

What it is. A local, offline search vault for AI conversation history. It reads the export files that chat tools produce, normalizes them into a common thread‑and‑message model, stores them in SQLite with a full‑text index, and lets the user search, read, export, and count conversations from the command line. Nothing leaves the machine; the tool never calls an AI service.

What was produced. Protozoa generated the full project — roughly 555 lines of Python across 12 files, including the importers, the storage layer, the search query, and the command‑line interface — together with an acceptance suite of five end‑to‑end tests.

Verification. The five acceptance tests each drive the real command‑line interface with small fixtures under a blocked network, exercising the genuine import‑to‑search round trip rather than mocking it: JSONL import and search, Markdown import and search, statistics after import, role fidelity (the assistant role must not collapse onto the user role), and Gemini import and search. The generated system passes all five. The per‑attempt trace for this run was not retained, so we do not report an attempts‑to‑pass count for it.

Iteration. Two capabilities were added after the initial generation, each introduced by first writing a failing acceptance test and then producing the code that makes it pass: a Gemini importer (mapping Gemini's export roles into the common model) and a fidelity fix for a case where an earlier version collapsed the assistant role onto the user role. Both are covered by the committed test suite.

AI Thread Vault is the more sequential of the two systems and served as a first proof that the method produces a coherent, testable, multi‑format tool end to end.

05Experiment 2 — Pong Arcade, and the side‑wall episode

What it is. A colorful browser Pong with a deterministic game core. The player faces a fallible computer opponent by default, with a local two‑player mode available. The rules — serving, paddle movement, ball physics, collisions, scoring, win conditions, and three opponent difficulty levels — live in a core that is deterministic for a given seed and is unit‑tested in isolation, separate from the rendering and input layers.

What was produced. Protozoa generated the full game — roughly 744 lines of TypeScript across five modules — plus a regression test suite of 21 tests encoding the game's rules. The initial build passed cleanly: 11 components, 11 attempts, zero verification failures — every part passed its checks on the first attempt. The production build succeeds, the test suite passes, and the game runs and is playable in Google Chrome.

Pong was not produced in a single shot. Like real software, it took three distinct passes: the initial generation, a hardening phase, and — days later — a separate pass to fix a specific defect. That third pass is the heart of this note.

Hardening. The hardening phase made three concrete, test-encoded changes: paddle returns impart spin from paddle motion, with the impact offset on the paddle controlling the return angle and a small speed-up per return; the opponent became fallible and difficulty-ordered, its reaction lag, aim error, and paddle speed scaling deterministically with the selected level; and serves vary in angle and starting height in a seed-reproducible way. Across the hardening iterations, 4 verification failures were repaired — all in ball physics, the same behavioral surface where the human-reported side-wall defect later appeared.

The defect. While playing the generated game, a human noticed that on steep returns the ball would collapse toward the side wall and rattle rather than bouncing cleanly back into play. This is exactly the kind of behavioral bug that looks fine in the code and only appears in motion.

The regression condition. Rather than eyeball a fix, the feedback was turned into an explicit, measurable condition: after every paddle return, the ball's horizontal speed must stay at least half of its total speed — meaning the return can never deflect so steeply that the ball crawls down the wall. This condition was written as a test that sweeps returns across the whole face of the paddle.

Failure on the flawed version. Run against the pre‑fix version, the condition fails: the worst‑case horizontal‑speed ratio measured 0.481, below the 0.5 floor. The regression condition genuinely reproduces the reported defect.

Bounded repair. Protozoa then repaired the collision behavior under that condition — capping the return angle so the ball always makes real horizontal progress — while every one of the game's existing checks had to keep passing.

Verified result. On the repaired version, the same condition passes: the worst‑case ratio measures 0.500, exactly at the floor, and the full existing test suite remains green. The defect metric moved from 0.481 to 0.500, the game still builds, and it still plays in the browser.

A defect a person felt while playing became a precise condition, that condition was shown to fail on the broken software, a bounded change was made under it, and the software was then shown to satisfy both the new condition and everything it already guaranteed. The verification carried the correctness, not a hopeful edit.

06Results and analysis

What the numbers show

Both systems verify. The generated software builds and passes its automated checks in both experiments, and the game additionally runs and is playable in a browser. Verification is not decorative here; the side‑wall episode shows it failing on a real defect and then passing on the repair.

Where the iteration actually happened. In‑run automatic repair was light: Pong's initial build passed with zero verification failures, and the hardening phase repaired four. Most iteration was human‑in‑the‑loop — re‑running hardening passes and reporting the side‑wall defect — followed by bounded, verified repair. We report this plainly rather than implying a dense autonomous repair loop the traces do not show; on these two builds, the verification machinery's value was catching and encoding human‑observed defects, not rescuing failing generations.

Scaling. Protozoa can execute independent work concurrently, although these two experiments were substantially dependency‑bound — the work formed mostly sequential chains, so the available concurrency was largely untapped. Where future builds parallelize, wall‑clock time can be reduced by adding compute.

Cross‑domain. The method produced coherent, verified software in two quite different settings — a data‑and‑search command‑line tool and a real‑time graphical game — which is more informative than two variations on one kind of program.

07What these early experiments suggest

Taken together, and stated as capabilities the platform exhibits rather than as general guarantees, the experiments suggest that Protozoa can:

• generate complete, runnable software from a specification in more than one language and domain;
• treat an automated test suite as the definition of done, and act on it — the game's defect was resolved by making a failing condition pass, not by an unverified edit;
• perform verification‑guided repair under explicit gates, keeping prior guarantees intact while satisfying a new one.

We describe the repair behavior as verification‑guided repair under explicit gates, not as fully autonomous self‑repair: the defect was reported by a person, and the repair succeeded because it was constrained by an explicit condition and the existing suite.

08Limitations

These are early results and should be read as such.

• Two experiments. Two systems, however different, do not establish general capability or superiority. They establish that the method works on these tasks and give a baseline to improve from.
• Bounded domains. A Python CLI and a browser game are far from the full range of software — large systems, unfamiliar frameworks, ambiguous or shifting requirements, and integration with external services remain untested here.
• Human in the loop. People wrote the specifications, reviewed results, and, in the Pong case, reported the defect. The repair was autonomous within an explicit condition; the surrounding judgment was not.
• Not yet fully instrumented. The early runs did not instrument per‑run model usage reliably, which is why no token, cost, or timing figures appear in this note. Model‑tier routing — sending simpler work to more moderate or cheaper models — was also not evaluated; both runs used a single frontier model throughout.
• No competitive comparison. We report Protozoa's own verified outcomes. We do not compare them here against other coding‑agent systems.

09Where this is going

Several directions follow naturally, and we state them as intent and planned evaluation rather than as claims about these two runs:

• Controlled comparisons. Controlled comparisons with other coding‑agent systems are planned, measuring correctness, cost, and iteration on the same tasks under the same conditions. Only such a study can support any claim about relative cost or quality.
• Model‑tier routing. Routing simpler work to more moderate or cheaper models, reserving stronger models for the hardest parts, is a design direction intended to reduce cost further; it has not yet been evaluated.
• Measured economics. Protozoa will generate many more systems than these first two, and complete, auditable per‑run instrumentation — tokens, cache reuse, cost, and time — is being built into the platform. The next set of experiments will report those cost metrics alongside the verified outcomes, so the economics of verified software generation can be judged on evidence rather than estimates.
• Broader domains and scale. Extending beyond these two systems to larger, less forgiving software, and exercising the concurrency that these dependency‑bound experiments left mostly untapped.
• Development evidence as an asset. Because Protozoa preserves the record of how each system was produced — the specification, the checks, the failures, and the repairs — that evidence can, over time, support evaluation corpora and, as a longer‑term direction, the training of specialist models for particular languages or domains. This is a direction, not a present capability.

10Reproducibility and notes

The two generated systems are public:

• Pong Arcade — github.com/smartinfer/pong
• AI Thread Vault — github.com/smartinfer/ai-thread-vault

Each repository contains the committed code and test suites behind the figures cited above. The verification claims — that the tests pass, that the game builds and runs in Chrome, and the before‑and‑after measurement of the side‑wall regression (0.481 → 0.500) — are reproducible from those repositories.

A note on measurement. Token, cost, cache, and timing figures are deliberately omitted from this note. The early runs did not instrument per‑run model usage reliably, and we do not report numbers we cannot verify from the committed repositories and retained build records. Where a build record was not retained — the Vault run's per‑attempt trace — we say so rather than estimating. Complete, auditable per‑run evidence capture is ongoing work.