| name | fm-loop-engineering |
| description | Use when running or extending the fmhub formal-verification benchmarks — driving LLMs (codex / DeepSeek V4 Flash & Pro / GLM) to add ACSL/Dafny/Verus specs that a verifier proves, and lifting weaker/cheaper models toward codex quality via loop engineering. Covers the harness toolkit, the proven workflow levers, the Flash+Pro cascade, model/endpoint gotchas, and how to add a solver. Trigger on tasks about FMBench, spec generation, multi-turn verifier loops, hybrid model cascades, or improving a weak model's pass rate on these benchmarks. |
FM Loop Engineering Playbook
Thesis: codex's strength is half MODEL, half WORKFLOW. The workflow is a
transferable lever — borrow codex's loop patterns to lift cheap models
(DeepSeek Flash/Pro) toward codex quality at a fraction of the cost. See
LOOP_ENGINEERING_THESIS.md and BENCHMARK_METHODOLOGY.md.
The harness toolkit (benchmarks/)
| harness | when to use | key file |
|---|
| linear multi-turn | default; low-cheat models (DeepSeek) | run_fmbench_multi.py |
| hybrid Flash→Pro cascade | cost-optimal; the main deliverable | run_fmbench_hybrid.py |
| insertion-only (cheat-proof) | egregious cheaters (GLM 85%) | run_fmbench_insert.py |
| source-locked (reject cheats) | cheat detection studies | run_fmbench_locked.py |
| GDR scaffold / agent | width/agency experiments | run_fmbench_gdr.py / run_fmbench_agent.py |
The proven levers (apply in this order)
- Multi-turn verifier feedback — biggest lever (DeepSeek 31%→57%). Feed WP's
proved/total + failing goals back each round.
- parse_error mitigation (
acsl_syntax.py) — categorize + targeted repair +
mechanical_fix() before verify. Drops parse_error ~13→2 on hard tasks.
- Persistence prompt — inject codex's "keep going until WP proves every goal,
persevere through failures, don't guess." DeepSeek gives up too early.
- Flash→Pro cascade — Flash (cheap) solves the easy ones; escalate residual to
Pro. Route on WP signal. Most passes land on cheap Flash.
- agent + run_eva — for hard proof gaps, let the model self-discover invariant
bounds via EVA. 6. pass@N — exploit weak-model variance (cheap on Flash).
Borrowed from codex (open source: openai/codex, cloned analysis)
apply_patch context-anchored edit format (codex-rs/apply-patch) — anchor edits
to verbatim lines, not line numbers; +/- prefixes keep ACSL backslashes literal
(NO JSON — \forall/\result get corrupted by JSON escaping).- Persistence prompt (codex-rs/core/gpt_5_2_prompt.md).
- Verify-in-loop + update_plan tracking.
Critical gotchas
- Faithfulness is mandatory: a WP pass means nothing if the model deleted the
asserts. Always
check_faithfulness. GLM's 100% WP was 85% cheating.
- Insertion harness hurts non-cheaters: it breaks loop-invariant placement →
parse_error. Use linear for DeepSeek; insertion only for GLM-class cheaters.
- Endpoint matters: GLM coding-plan = 80% empty content; OpenRouter = 0%. Set
high
max_tokens (24000) for reasoning models. See BENCHMARK_METHODOLOGY.md §2.
- Anti-hang: always route LLM calls through
llm_robust.robust_chat (hard
300s deadline). Naive retry hung GLM 34 min.
- Solver dispatch:
SOLVER={codex|deepseek|glm|openrouter} monkey-patches the
chat adapter at import. A standalone runner MUST import solver_dispatch BEFORE
importing codex_adapter_chat, or it won't switch.
Adding a model / endpoint
- Make a
<name>_adapter.py + <name>_adapter_chat.py that delegate to
llm_robust.robust_chat(client, model, history, RETRYABLE, max_tokens=...).
- Add a branch to
solver_dispatch.py.
- Reasoning models: high max_tokens + empty-content retry (see glm_adapter_chat).
- Run:
SOLVER=<name> <KEY>=... python3 bench_parallel.py fmbench_multi -K 5 -w 8 ...
Cost-optimal default
run_fmbench_hybrid.py (Flash→Pro + acsl_syntax + persistence) is the recommended
production path: codex-class results trajectory at mostly-Flash cost. Verify on the
20 hardest tasks (/tmp/glm_locked_sample.json) before scaling.
