To start using the P Verifier, you must install P along with the verification dependencies (UCLID5 and an SMT solver like Z3). Detailed installation instructions are available[here](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/install-pverifier.md); simple usage instructions are available[here](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/using-pverifier.md).

To start using the P Verifier, you must install P along with the verification dependencies (UCLID5 and an SMT solver like Z3). Detailed installation instructions are available[here](install-pverifier.md); simple usage instructions are available[here](using-pverifier.md).

To help you get acquainted with the new verification features, we have prepared a comprehensive tutorial that walks you through the formal verification of a simplified two-phase commit (2PC) protocol. This tutorial covers the key concepts and steps of using the verification backend. You can find the tutorial[here](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/twophasecommitverification.md).

To help you get acquainted with the new verification features, we have prepared a comprehensive tutorial that walks you through the formal verification of a simplified two-phase commit (2PC) protocol. This tutorial covers the key concepts and steps of using the verification backend. You can find the tutorial[here](twophasecommitverification.md).

!!! tip ""

**We recommend that you start with the[Tutorials](tutsoutline.md) to get familiar with

**We recommend that you start with the[Tutorials](../../tutsoutline.md) to get familiar with

the P language and its tool chain.**

??? note "PVerifier Extension Top Level Declarations Grammar"

Before moving forward, we assume that you have successfully installed

the[PVerifier](install-pverifier.md).

In this section, we provide an overview of the steps involved in verifying a P program using the[two-phase commit](../tutorial/twophasecommit.md) example in Tutorials.

In this section, we provide an overview of the steps involved in verifying a P program using the[two-phase commit](../../tutorial/twophasecommit.md) example in Tutorials.

??? info "Get the Two-Phase Commit Example Locally"

We will use the[TwoPhaseCommit](https://github.com/p-org/P/tree/master/Tutorial/2_TwoPhaseCommit) example from Tutorial folder in P repository to describe the process of verifying a P program. Please clone the P repo and navigate to the

1. Configure your project to use PVerifier as the target in your`.pproj` file

2. Compile the project using the P compiler

This process follows the same workflow described in[Using P](../../getstarted/usingp.md), except that we specify`PVerifier` as the backend instead of other targets like`CSharp` or`Java`.

This process follows the same workflow described in[Using P](../../getstarted/usingP.md), except that we specify`PVerifier` as the backend instead of other targets like`CSharp` or`Java`.

-P Exhaustive Mode:advanced/pex.md

-PVerifier:

-Announcement:advanced/PVerifierLanguageExtensions/announcement.md

-Outline:advanced/PVerifierLanguageExtensions/outline.md

-Installation:advanced/PVerifierLanguageExtensions/install-pverifier.md

-Using PVerifier:advanced/PVerifierLanguageExtensions/using-pverifier.md

-Pure Functions:advanced/PVerifierLanguageExtensions/pure.md

-Init Conditions:advanced/PVerifierLanguageExtensions/init-condition.md

-Specifications:advanced/PVerifierLanguageExtensions/specification.md

-Lemmas and Proofs:advanced/PVerifierLanguageExtensions/proof.md

-Two Phase Commit Verification:advanced/PVerifierLanguageExtensions/twophasecommitverification.md

-Language Manual:

-P Program (Outline):manualoutline.md

-P DataTypes:manual/datatypes.md