Skip to content

Commit dd5ecd6

Browse files
authored
docs(fv): update README to .conf-based specs and correct run syntax
1 parent 6308fdc commit dd5ecd6

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

fv/README.md

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,29 +13,29 @@ Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/
1313
1414
## Running the verification
1515

16-
The Formal Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options.
16+
The Formal Verification Tool proves specs for contracts, which are defined by per-spec `.conf` files located under `fv/specs/` along with their pre-configured options.
1717

1818
The verification script `./run.js` is used to submit verification jobs to the Certora Verification service.
1919

2020
You can run it from the root of the repository with the following command:
2121

2222
```bash
23-
node fv/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
23+
node fv/run.js [SPEC_NAME | fv/specs/NAME.conf] [--all] [-p N] [-v]
2424
```
2525

2626
Where:
2727

28-
- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided.
29-
- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided.
30-
- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file.
28+
- `SPEC_NAME` is the base name of a configuration file in `fv/specs/` without extension. For example, `AccessControl` maps to `fv/specs/AccessControl.conf`.
29+
- Alternatively, you may pass an explicit path to a `.conf` file under `fv/specs/`.
30+
- Supported script options are `--all`, `--parallel/-p`, and `--verbose/-v`.
3131

3232
> **Note**
3333
> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs.
3434
3535
Example usage:
3636

3737
```bash
38-
node fv/run.js AccessControl # Run the AccessControl spec against every contract implementing it
38+
node fv/run.js AccessControl # Run the AccessControl configuration (fv/specs/AccessControl.conf) using its harness and spec
3939
```
4040

4141
## Adapting to changes in the contracts

0 commit comments

Comments
 (0)