Did not change
The coding model, the human-agreed target, and the scope.
Case study · Ada/SPARK
Same agent. Better solution. Independent verification changes the loop.
One bounded GNATprove defect moved from a rejected implementation theory to source-bound FalseGreen ACCEPT without moving the definition of done.
The model was not retrained. The coding agent had to revise its solution because external evidence kept falsifying approaches that did not satisfy the agreed cross-unit behavior.
The upstream PR remains under maintainer review. FalseGreen ACCEPT refers only to the frozen verification criteria for this bounded change.
The bounded Job
- target
- Generated Global handling for generic formal inputs across compilation units
- verified source
- cd927c837d90…
- result
- FalseGreen ACCEPT · 3/3 criteria · 6/6 checks
The definition of done
Humans fixed the target. Evidence judged the work.
SPARK issue #62 ↗ documented a specific GNATprove failure involving generated Global contracts for a generic formal parameter of modein.
AdaCore’s review then made the missing boundary explicit: the first patch could not support callers in another compilation unit. The eventual repair had to preserve both the caller-facing proper dependency and the instance-facing refined dependency.
Frozen verification perimeter
- Build a new gnat2why from the submitted source instead of trusting a pre-existing executable.
- Preserve the proper dependency for callers and the refined dependency inside the generic instance.
- Propagate the cross-unit Clock_Time dependency and reject the invalid Global => null case.
- Pass the three maintainer regression cases plus the nearby generic-flow perimeter.
- Retain the exact allowed SARIF warnings and reject unknown warnings or tool failures.
The verification loop
Wrong theories became evidence, not excuses.
The acceptance boundary stayed fixed while the implementation changed. Each failed observation removed an incorrect theory from the solution space.
14:19 UTC
The first theory was rejected.
AdaCore’s review showed that late flow-analysis remapping worked only inside one compilation unit. The required cross-unit dependency had to be computed during generated-global construction.
20:55 UTC
The target was frozen.
The four review threads, three upstream regressions, source-bound build, and exact warning policy became the fixed verification perimeter. The coding agent could change the implementation, not the meaning of done.
21:07–22:18 UTC
Evidence narrowed the solution.
Unconditional normalization broke the instance’s local view. Recomputing phase 2 reintroduced the wrong formal. A broader explicit-contract change broke a nearby case. The repair narrowed to a source-generation-only rule that preserved the proper/refined pair and left ordinary explicit contracts alone.
22:57 UTC
The first verification attempt ended Incomplete.
The source-bound build passed, but the behavioral criterion was not established. FalseGreen preserved that attempt as Not Accepted instead of calling the Job done.
23:39 UTC
The repaired, rebased source reached FalseGreen ACCEPT.
A later verification run against the same frozen definition of done passed all three criteria and all six controller-owned behavioral checks. The stopping condition came from evidence against the fixed target—not from the coding agent declaring itself finished or from upstream project governance.
What changed
The agent stayed the same. The solution got more rigorous.
The final rule was narrower than the overbroad attempts: map in the source-generation context, preserve the proper/refined distinction, and leave ordinary explicit contracts on their existing path.
The code did not become correct because the agent grew more intelligent. It improved because the agent could not redefine the cross-unit tests, source binding, or warning policy after seeing the result.
Independent verification gave the coding loop a real stopping condition.
Did change
The implementation theory, source structure, and evidence supporting completion.
Result and timing
Rigorous did not mean bureaucratic.
The retained record shows about 2 hours 44 minutes from the frozen target to FalseGreen ACCEPT on August 19, 2026. That window includes falsified theories, repairs, and the Incomplete verifier-harness run.
2h 44m
Frozen target to independently verified FalseGreen ACCEPT
<30m
Estimated human attention
6m 37s
Final independent verification run
Within that process, the final independent run was active at 23:32:47 UTC and returned FalseGreen ACCEPT at 23:39:24 UTC.
The human did not spend 2 hours 44 minutes continuously supervising the coding agent. Active human attention was retrospectively estimated at less than 30 minutes: define and approve the target, then provide limited judgment while the agent iterated against FalseGreen’s independent evidence. Define done. Let the agent work. Come back to evidence.
The 2h 44m elapsed time and 6m 37s final run come from retained records. Human attention is a retrospective estimate. These observations are from one bounded Job, not guarantees for future Jobs.
2,685 ms
Committed layout and source binding
227,475 ms
Clean source-bound gnat2why build
10,885 ms
Maintainer regressions and SARIF policy
These are the exact retained command runtimes from the FalseGreen ACCEPT report. They total 241,045 ms and do not include all planning, repair, artifact preparation, or orchestration time.
Evidence record
Bound to public source and a retained FalseGreen result.
The public issue, review, commits, and PR establish the source history. The upstream PR remains under maintainer review. The retained FalseGreen result binds FalseGreen ACCEPT—not upstream acceptance—to the final commit and frozen verification plan.
Original defectAdaCore/spark2014 issue #62 ↗Falsifying review evidenceThe multi-unit failure in PR #67 ↗
FalseGreen record
- task
- task_1b29c5e656fb47a2b2eebf56f2db29d5
- run
- run_db7d907a0b5549b8b430518360ee98c5
- plan
- f8cdcb510cb5d360d8b6161371e0b5f4805813e92572f228cae2184c93af60ae
- source
- c0070f07000e8de24177b684b672517d6d58153e44fe7b38e62ecbf391277e1c
- result
- verified / ACCEPT
One bounded Job
One frozen definition of done. One independent result.
FalseGreen did not verify all of SPARK. It established that one exact source-bound change satisfied the agreed criteria.