michael-denyer/agent-formal-verify/formal-verify

Formal verify

Model individual protocols or sequential invariants. Map counter-examples to events and locations in the source code. Before reporting a pass, confirm that each checked property detects a relevant mutation and that its checker passes.

Choose tools according to the target:

Prefer Kani when the function is Rust and its inputs and loops can be bounded, because it checks the production function directly. Use Lean when the property must hold for every size or the code is not Rust.

A thread protocol that depends on arithmetic such as slot = item mod window needs both tools. Use TLA+ for the interleavings with the arithmetic as a constant, and Lean for the arithmetic.

Use the tool the user names. When the table gives another tool for part of the target, report what the named tool leaves unchecked.

1. Pick the targets

Search with rg for pthread_cond, pthread_mutex, atomic_, std::condition_variable, sync.Cond, chan, select, asyncio.Condition, Semaphore, atexit and setjmp. Also search for protocol state names such as ready, stop, done, finished, pending, inflight, head, tail and exiting. Classify each hit:

• Model hand-written protocols, including hand-overs, bounded pipelines, queues with ordered output, shutdown, cleanup, retry and lease loops.
• Leave data-parallel loops over disjoint indices to ThreadSanitizer or the language's race detector, and say so in the reply.
• For library-owned channels or executors, model the calling code.
• Use Lean for arithmetic the protocol or output depends on. Examples include slot and splice indices, window bounds, sizes computed and checked differently, and encoder round trips. Search for %, - 1, + 1, >>, overlap, splice and offset near the protocol's data.

For Rust functions, also search for unsafe, as u32, as usize, checked_, wrapping_, unwrap(, slicing and %. Record each function's input ranges, loop bounds and assumptions for a Kani target.

Write a table with one row per target before modelling. A protocol and the arithmetic it depends on are separate targets. For a protocol, record its threads, shared variables, every wait and what wakes it, terminal states such as joined or closed, and resources whose ownership moves. Include slots, buffers, file handles and resources that close frees. For a Lean target, record the functions, their integer types and the property. Start with waits that have no escape, resources freed by two paths, and errors raised on a different thread from the one that reports them. Read the whole source file for each target so the model follows the code.

2. Prepare the tools

Prepare tools after picking targets and before launching agents. The helpers are in this skill's scripts/ directory. Stay in the target repository and run each helper with bash and its absolute path. Pass absolute paths to models and matrices. Tool setup describes the pins, caches and environment settings.

• When a target needs Kani, run bash <skill-dir>/scripts/setup.sh rust. Copy the Kani template into a verification crate only when it helps add harnesses that call the production function.
• When a target needs TLA+, run bash <skill-dir>/scripts/setup.sh tla.
• When a target needs Lean, every Lean model in the repository shares one Lake project. If the repository has none, copy lakefile.toml, lake-manifest.json and lean-toolchain from <skill-dir>/examples/lean-template/ to lean/ in the target repository, once. Then run bash <skill-dir>/scripts/setup.sh lean <absolute-model-project-path>.

Require a successful exit and a READY line from each command. A helper that cannot run prints UNAVAILABLE and exits 3. Report it as "not checked" with its remedy. It is neither a pass nor a failure of the model. A check that ran and failed exits 1; usage errors exit 2. The setup helper reuses ready tools and installs a missing Lean pin, so the user does not need to rerun /agent-formal-verify:setup when a target or pin changes. Keep the installed skill files read-only and copy templates into the target repository.

If a system prerequisite such as Java or elan is missing, use the setup skill to prepare it within the user's installation constraints and existing authorization. Report any prerequisite that cannot be prepared. If java on PATH has no runtime, set JAVA to a working JDK's java binary for the setup helper and the matrix runner.

The helpers:

• The setup helper, `scripts/setup.sh`, verifies the pinned TLC JAR and is the only helper that installs a Lean toolchain.
• The matrix runner, `scripts/tlc-matrix.sh`, runs TLC with a matrix of constants and prints one PASS or FAIL per run with its state count, then a SUMMARY line with the totals. A failing run prints its error trace reduced by `scripts/tlc-trace.py` to the variables each step changed. Copy `examples/tla-template/` to start a spec and its matrix.
• The Lean checker, `scripts/lean-check.sh`, builds every .lean file in the pinned Lake project and audits every declaration of every built module. It fails on a build error, a sorry, a declaration that rests on an axiom beyond propext, Classical.choice and Quot.sound, or a .lean file that no Lake library owns. Use --freeze before the file names to record statement types and definition bodies in each model's .statements file before proving it. Freezing permits sorry and reports FROZEN, not a proof PASS. Later checks enforce those records and permit proof changes and added declarations. Given file names after the project, it checks only those files. Copy `examples/lean-template/Model/BoundedQueue.lean` to start a model.
• The Rust checker, `scripts/kani-check.sh`, runs the pinned Kani on the crate's proof harnesses. It reports each harness's unwind bound and check count, rejects failed checks and unsatisfied cover conditions, and prints concrete playback tests when available. Copy `examples/kani-template/` for a bounded-queue example.
• The mutation runner, `scripts/mutate.py`, takes a model's <Name>.mutations file and applies each listed bug to a temporary copy of the model. It prints DETECTED or MISSED per mutation with what failed, UNCOVERED for a TLA+ property or Kani harness that no mutation targets, and a SUMMARY line. All three templates include a mutations file.

3. Model one target per agent

Spawn one agent per target, in parallel when supported. Use the host runtime's agent tools and follow the user's model configuration when selecting agents. An agent does not see this skill. Its brief contains:

• the target's row from the table, with its source files and line ranges;
• the model's name, <Name>, and for a Lean target the absolute path of the Lake project, or for Kani the absolute path of the crate;
• the absolute path of this skill's directory as <skill-dir>, and any JAVA setting;
• the instruction to read <skill-dir>/references/tla-brief.md for a protocol, <skill-dir>/references/lean-brief.md for arithmetic, or <skill-dir>/references/rust-brief.md for a Rust function, in full and to follow it.

Name the brief file and leave its text out of the prompt. The TLA+ brief, the Lean brief and the Rust brief hold the modelling requirements, the files to write, the commands to run and what to report. If delegation is unavailable, read the brief for each target and model the targets yourself, one at a time.

An agent writes only its own files, tla/<Name>.tla, .matrix and .mutations, lean/Model/<Name>.lean, .mutations and .statements, or the assigned Rust harness and .mutations files in a separate crate, so parallel agents share none. When Rust agents have reported, run the Rust checker on each crate. When the Lean agents have reported, run the Lean checker on the whole project, without a file name. An existing Lean project keeps its layout and must pin Lean 4.20.0 or later.

4. Read the counter-example back into the code

For a closed Lean proof, compare the model's printed differential vectors with the production function in the repository's native test framework. Report the agreement count and integer widths. Claim that the proof describes the code only after this comparison agrees, or state beside the verdict that the vectors were not run.

For each violation, in this order:

1. Read the reduced trace that the matrix runner prints under the FAIL line, the inputs that Lean's bounded search prints, or Kani's failed check and playback inputs. Map each step to a code event and source line.
2. Check reachability against the real constants and callers. If a violation occurs at Slots=1 while the code ships Slots=4, decide whether the trace needs the smaller count or can also occur at the shipped one. Report the first as safe only while the count stays at the shipped value, and the second as a reachable bug. Keep the boundary configuration in the matrix either way.
3. Reproduce a reachable trace with a deterministic test, a ThreadSanitizer or race-detector run, or a stress loop using the trace's counts. Hooks, a small slot count or barriers can force the interleaving. If no practical reproduction exists, report that limitation and the model configuration that demonstrates the violation. Concrete inputs from Lean or Kani always allow a unit test. If it passes on the production code, correct the model or harness and rerun.
4. Change code only when the user asked for fixes. Otherwise report the trace, the reproduction and the proposed fix, and stop here. The model then describes the code as written, so its failing check is the record of the bug. Do not reword the property to pass, prove its negation or add runs that expect failure. Mutations for a failing property wait for the fix.
5. Fix only a violation that shipped settings can reach, and only with a reproduction from step 3 unless none is practical. Report the rest. Apply the smallest fix that prevents the trace, update the model to match, and rerun its matrix, the Lean checker or the Rust checker, then its mutations and any reproducing test. Keep the model and code change together.
6. When the user asked for commits or pull requests, use one PR per bug. Include the model, its mutations file, the fix and any reproducing test. In the description, name the theorem, #guard, TLC property or Kani harness that failed, and say when no test reproduces the bug. Write the rest as the Reply section says.

5. Keep the proof, and record each result once