fix(proof-crate-gen): improve generated README content

- Remove 'do not edit by hand' — users own the README after first gen
- Replace raw verifier commands with elicitation prove --kani/--creusot/--verus --csv
- Add Contents table summarising the three generated backend directories
- Update elicit_proofs/README.md to match

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: crumplecup

crates/elicit_proofs/README.md

@@ -1,18 +1,31 @@
 # elicit_proofs
 
-> **Auto-generated** — do not edit by hand.
-> Regenerate with `elicitation generate proof-crate`.
-
 Kani, Creusot, and Verus proof harnesses for [`elicit_server`],
-produced by [elicitation](https://crates.io/crates/elicitation).
+generated by [elicitation](https://crates.io/crates/elicitation).
+
+This README was scaffolded on first generation and can be freely edited —
+subsequent runs of `elicitation generate proof-crate` will not overwrite it.
+
+## Contents
+
+| Directory | Description |
+|-----------|-------------|
+| `src/kani/generated/` | Kani proof harnesses, one per VSM transition |
+| `src/creusot/generated/` | Creusot logic predicates and extern specs |
+| `src/verus/generated/` | Verus proof harnesses |
 
-## Verifiers
+## Running proofs
 
-| Backend  | Feature flag | Run command                       |
-|----------|-------------|-----------------------------------|
-| Kani     | `kani`      | `cargo kani`                      |
-| Creusot  | `creusot`   | `cargo creusot prove`             |
-| Verus    | `verus`     | `verus src/lib.rs`                |
+```sh
+# Kani
+elicitation prove --kani --csv
+
+# Creusot
+elicitation prove --creusot --csv
+
+# Verus
+elicitation prove --verus --csv
+```
 
 ## Regenerating
 

crates/elicitation/src/cli/generate/proof_crate_gen.rs

@@ -726,19 +726,32 @@ fn render_readme(proof_name: &str, primary_source: &str) -> String {
     format!(
         r#"# {proof_name}
 
-> **Auto-generated** — do not edit by hand.
-> Regenerate with `elicitation generate proof-crate`.
-
 Kani, Creusot, and Verus proof harnesses for [`{primary_source}`],
-produced by [elicitation](https://crates.io/crates/elicitation).
+generated by [elicitation](https://crates.io/crates/elicitation).
+
+This README was scaffolded on first generation and can be freely edited —
+subsequent runs of `elicitation generate proof-crate` will not overwrite it.
+
+## Contents
 
-## Verifiers
+| Directory | Description |
+|-----------|-------------|
+| `src/kani/generated/` | Kani proof harnesses, one per VSM transition |
+| `src/creusot/generated/` | Creusot logic predicates and extern specs |
+| `src/verus/generated/` | Verus proof harnesses |
+
+## Running proofs
+
+```sh
+# Kani
+elicitation prove --kani --csv
 
-| Backend  | Feature flag | Run command                       |
-|----------|-------------|-----------------------------------|
-| Kani     | `kani`      | `cargo kani`                      |
-| Creusot  | `creusot`   | `cargo creusot prove`             |
-| Verus    | `verus`     | `verus src/lib.rs`                |
+# Creusot
+elicitation prove --creusot --csv
+
+# Verus
+elicitation prove --verus --csv
+```
 
 ## Regenerating
 
@@ -751,6 +764,9 @@ elicitation generate proof-crate \
 "#
     )
 }
+"#
+    )
+}
 
 
 /// return the names of any external crates that appear in `workspace_deps` but