# Formal Verification

Formal Verification is a Linty scan engine that provides additional rules based on formal verification. These advanced
rules help you detect bugs and vulnerabilities, improving the reliability and security of your IPs.

BugFinder is available as part of [Linty Ultra](https://linty-services.com/pricing).

## Workflow

1. Generate and run formal checks directly in VS Code with
   the [Linty Formal Verification](https://marketplace.visualstudio.com/items?itemName=LintyServices.linty-formal-verification)
   extension.
2. Save these formal checks in your project repository (default location: `.linty/formal`; this can be updated via the
   `sonar.hdl.formal.paths` property).
3. Integrate these formal checks into your continuous integration workflow. First, activate the formal verification
   rules tagged as <a href="https://demo.linty-services.com/coding_rules?languages=hdl&tags=formal">formal</a> in your
   quality profiles. Then, run a [Linty scan](./scan.md).

## Custom Formal Checks

You can embed your own formal checks based on [SymbiYosys](https://symbiyosys.readthedocs.io/en/latest/) into Linty. To
do so, for each check:

1. Create a rule from
   the <a href="https://demo.linty-services.com/coding_rules?open=hdlformal%3AHDL2999&rule_key=hdlformal%3AHDL2999">
   Linty formal check template</a> and activate it in your quality profiles.
2. Get the ID of the rule you just created.
3. Add the following line at the top of your formal check `.sby` file: `# Linty check ID: my_rule`. Replace `my_rule`
   with the ID of the rule you just created (everything after `hdlformal`).
4. Store the `.sby` file in your project repository (default location: `.linty/formal`; this can be updated via the
   `sonar.hdl.formal.paths` property).