prove

Point formal at its own Rust and come back with proved properties. You are not here to change the Rust.

Target for this run: $ARGUMENTS — if that is empty, take the first entry under "Where to aim" that has no properties yet. One target per run. Stop when it is done rather than moving on; a long run costs more than two short ones and reviews worse.

Read README.md §"Driving formal from an agent" and CLAUDE.md first. The guide served over HTTP is the authority on the workflow — this file only says what is already done, what to aim at, and what not to break.

What already exists

formal.properties.json holds three properties, all against rust/formal-core/src/proof_cache.rs, with their Lean in proofs/: normalise_code/length_non_increasing, framed/shifting_a_boundary_changes_the_payload, normalise_formal/word_operators_respect_boundaries. Two of the three were written after formal found a real cache-key collision. Do not restate them.

Everything else in the workspace is unproved.

Running it

The binary is not on PATH, so the README's bare formal … will not work. From rust/:

cargo run --bin formal -- status                # expect: mathlib oleans built, sandbox bubblewrap
cargo run --bin formal -- serve --background    # returns once /health answers; no-op if already up
cargo run --bin formal -- stop

It serves on http://127.0.0.1:1337.

The loop

GET  /guide                      the workflow and the spec-file schema
GET  /guide/extract              how to find pure functions and properties
POST /session {"spec_file": "<absolute path to formal.properties.json>"}
GET  /guide/formalize            Lean 4 conventions for stating a property
GET  /guide/tactics              read before writing a proof, not after it fails
POST /session/{id}/check         {"proofs": {"<id>": "<lean>"}}

spec_file must be absolute — the server's working directory is not yours. /guide/{topic} takes exactly extract, formalize, tactics.