Proofline

• 

  1. A plausible answer is not evidence: the same six gates turn a plausible 2/6 result into a reproducible 6/6 verification.

• 

  2. Six questions, asked twice: each property is tested independently, so familiar examples cannot conceal deeper failures.

• 

  3. One unit disappears: independent rounding loses the available unit; the conservation gate produces a concrete counterexample.

• 

  4. Treat the claim as hypothesis: Proofline applies the scientific method: state, isolate, test, revise, and rerun the unchanged experiment.

Public code repository

Proofline’s complete source code, six conformance gates, and test receipts are available at https://github.com/rbnbric/proofline-gauntlet.

Inspiration

AI coding tools can produce convincing code very quickly, but convincing is not the same as correct. A function may pass the examples we happened to try while still losing data, mishandling boundaries, or making unstated choices inconsistently.

This is a common hurdle for early adopters and seasoned full-stack developers alike. The use of sub-agents and constant “babysitting” reveals the underlying problem: an LLM can produce competent pieces of a solution while still requiring the work to be broken down carefully and checked afterward for emergent bad behavior.

Proofline grew from a question: can disciplined human judgment and deterministic testing turn a plausible AI-generated implementation into something measurably more trustworthy?

Our larger internal workflow uses automated gates to catch both local errors and systemic problems that might otherwise be replicated across a project. Proofline is a small, inspection worthy demonstration of that principle.

What it does

Proofline demonstrates the process using a proportional integer-allocation task.

The first implementation looks reasonable and passes familiar examples. Proofline then runs it through six independent conformance gates:

1. Familiar examples
2. Input and output contract
3. Conservation of the available total
4. Deterministic tie behavior
5. Boundary conditions
6. Efficiency

The original implementation passes only 2 of the 6 gates. It can create or lose units through independent rounding, fails on several invalid inputs, and does not implement a stable policy for indivisible totals.

This is not intended as one rigid verification structure. Like the Python imagery behind Proofline, the method is flexible, replicable, and adaptable. The particular gates should follow the user’s actual goal and the properties that matter within that domain.

Although this demonstration uses Python, the method is language-agnostic. The same scientific cycle can be applied successfully to JavaScript, TypeScript, Rust, Go, Java, C#, C++, or any environment capable of running deterministic checks and producing results worthy of inspection. Implementation will vary in difficulty according to the eccentricities and nuances of each language. Every ecosystem can use its native testing tools while preserving the same structure: define falsifiable requirements, isolate independent properties, test iteratively, revise against the evidence, and retain a reproducible receipt. Proofline is therefore a model for verification rather than a Python-specific testing technique.

A corrected largest-remainder implementation runs through the exact same gauntlet and passes all 6 gates. The result is recorded as reproducible JSON evidence rather than accepted from a completion claim.

How we built it

Proofline is a dependency-free Python experiment built around the standard library.

The two implementations are intentionally small so the effect of the verification process remains visible. The demonstration avoids unnecessary complexity while showing that “vibe coding” is only the first layer of the problem. What ultimately matters is having a real goal, expressing its requirements clearly, and testing whether the result fulfills them.

Each gate lives in its own unittest module and examines a separate part of the contract. The runner executes every gate independently, captures its exit status, duration, and bounded output, and produces a machine-readable report.

The conservation gate systematically checks 244 combinations instead of relying on a few hand-selected examples. This illustrates one of our central insights: deterministic systems can redirect the messy, divergent, and token-intensive results of ordinary prompting into a productive path.

Proofline applies the scientific method to AI-assisted development: state the expected behavior as a falsifiable claim, test it under controlled and repeatable conditions, examine the evidence, revise the implementation, and rerun the same experiment. The gauntlet turns informal prompting into a cycle of hypothesis, measurement, correction, and replication.

A person can improvise tests turn by turn, but systemizing those checks reduces the influence of personality, vague demands, distraction, and fatigue. The determinism gate establishes an explicit tie policy. Contract and boundary gates cover negative totals, empty inputs, Boolean values, zero weights, and totals too small to divide evenly.

Both implementations receive the same tests. The gauntlet changes the evidence available to the developer and identifies the precise assumptions that require correction.

This reverses the usual babysitting relationship. The user and the LLM check each other: the human acts as project director, while the agent is required to behave as a more stringent programmer working against an executable contract.

Challenges we ran into

The main challenge was avoiding tests that merely repeated the implementation.

It was easy to write examples that both versions passed. That is a recurring hazard in software work: a test can reproduce the same assumptions as the code and create confidence without independent evidence.

The useful tests came from identifying properties that must remain true across many inputs. Conservation was especially important: every allocated unit must come from the available total, and every available unit must be accounted for. Anyone working extensively with LLM-generated code will eventually encounter this broader problem as drift.

Tie behavior also required an explicit decision. “Proportional” does not completely specify what should happen when several recipients have equal fractional remainders. Proofline makes that ambiguity visible and requires a stable ordering policy. The assumptions shared between agent and user must be explicit if the design goal is going to be fulfilled.

We also had to separate correctness from performance. The original implementation is fast, but efficiency cannot compensate for incorrect results. Independent gates preserve that distinction. Performance matters, but incorrect behavior remains the more fundamental weakness.

Accomplishments that we're proud of

The clearest result is the measurable transition from plausible to conformant:

• Ungated implementation: 2/6 gates passed
• Corrected implementation: 6/6 gates passed
• Conservation cases examined: 244
• Both results captured as reproducible JSON reports

The ungated implementation produced its first five conservation violations within 244 cases; the corrected implementation passed all 20,176 enumerated cases.

We are also proud that the demonstration is compact enough to inspect. Reviewers can read both implementations, run the gauntlet locally, and verify that the reports agree with the actual test results.

Proofline does not claim that one experiment proves every AI-assisted program correct. It demonstrates a reusable principle: executable contracts can expose assumptions that ordinary examples and confident completion statements leave hidden.

Software that works reliably and leaves fewer defects to clean up later is especially necessary at this stage of AI-assisted development.

What we learned

The largest lesson was that tests shape implementation choices.

A familiar example asks whether the code works in one situation. A conformance gate asks whether a declared property continues to hold across a defined class of situations. That difference changes both the available evidence and the resulting code. We aim for software that is robust and resilient.

We also learned that deterministic verification is most useful when failures are narrow and actionable. “The code is bad” does not help. It is a thought-terminating cliché, and ugly code can work just as reliably as pretty code.

“Independent rounding violated conservation for these inputs” gives the developer a concrete repair target. It may not be elegant language, but it is useful.

AI tools remain valuable for generating and revising code. Proofline adds a disciplined process for deciding whether the resulting behavior deserves to be trusted.

We hope this kind of process becomes part of the future of AI-assisted development, allowing us to correct problems before unreliable “vibe-coded” systems become expensive disasters that someone else must repair.

What's next for Proofline

The next version will let users supply functions inside a controlled sandbox and evaluate them with custom conformance packs. We also plan pull-request integration, retained evidence histories, and comparisons across models and development workflows.

Built With

• ai-assisted
• css
• deterministic-testing
• developer-tools
• development
• html
• javascript
• json
• property-testing
• python
• unittest