Wonderful data point!
It's been interesting investing into different classic verification & testing methods for gfql (CPU/GPU graph queries on dataframes) and Louie (agentic investigation harness) over the last couple of years with different model & harness generations. The ones below are fewer but more longitudinal efforts compared to the shallower ones Dan worked through, and seem largely consistent:
Overall, my takeaway on standard software has been LLMs favor smart, guided fuzzing, natural language specifications deployed as iterative parallel adverserial AI review (e.g., context-reset subagents) after the functional prototyping. For formal methods / static analysis, cheaper/faster/lighter ones, though for the next level of quality, I can see this changing. The concolic testing world's heuristic results carried through a lot for me vs most others, which is unsurprising as they went deep on engineering ROI curves for fuzzing large code bases and specializing for different bug classes.
Highlights:
- alloy for gfql fell on its face relative to fuzzing, even with guidance. This was disappointing as it was intended as a cheap experiment to justify doing more expensive formal methods.
- prompts & skills need tuning: auto-memory doesn't transfer across harnesses by default, and one-shot auto-authored skills evals badly. More about iterating. Manual version of iterating would be editing skills when we hit new/repeat classes of bugs, though not guaranteed faithfulness: this is what we do the most. Positive experiments automating here, but not enough to invest deeper when we have to do manual anyways.
- natural language specifications are now a thing. Our significant new features now come with a security.md, policy.md, concurrency.md, etc., and important for them to be close to the code and taught to the review skill. Coding and review agents then can triangulate between tests, specs, code, and their own skills & general knowledge. However, we find we prefer not to do localized invariants in method comments as that gets verbose and drifts, and instead, do those as tests. This gets a bit into the global cost question of better code gen iterations and/or better review phases.
- staging coding vs reviewing. Overtesting early kills progress, so we stage heavier quality engineering at the end, and architectural research at the beginning.
- Lessons from the concolic execution era: staging static LLM analysis early with dynamic LLM testing later. Test amplify findings by area, kind, etc to convergence.
- We love community suites. GFQL builds against known Cypher language standards correctness conformance and benchmark suites, and Louie tools often start with community agent evals/benchmarks before we add our own specializations.
I don't know how big and deep the experiment Dan ran was. Something like formal methods is generally a big & invasive investment, and the target of each kind is often a much higher quality rating for a narrow set of properties. This complicates benchmarking setup. Imagine building entire compilers, and experimenting with different combos of methods & having those methods come in at different times & places.
I expect the AI security vulnerability analysis world to have similar findings. We end up baking that into our review harness as well without changing our overall methods above.