microsoft / qsharp-verifier

Formal Verification for Q#

This repository contains Q* (pronounced Q-star), a tool for formally verifying quantum programs written in Q#. It is implemented as a library for F* and is currently in the prototype stage of development. Its goal is to allow Q# developers to formally reason about their programs, providing stronger correctness guarantees than testing and leading to higher-quality Q# code.

This code in this repository loosely corresponds to the vision outlined in Ch. 5 of Kesha Hietala's dissertation.

Directory

• qstar/examples: Examples and demos of using Q* and the Q#-to-Q* translator.
• qstar/src: Q* library code, written in F*. See the README in that directory for more information.
• qstar/translator: Plugin for the Q# compiler to automatically translate Q# programs into Q* instructions.

Requirements

Install F* and .NET.

If building F* from source, we recommend using the everest script from Project Everest:

./everest check
./everest FStar make

Demo

You can convert the Examples.qs file into Q* instruction trees by running dotnet build from the qstar/examples directory. This will produce an F* file in qstar/examples/obj/QStar. A prettified excerpt from the output is in Demo.fst. You should be able to typecheck this file in F* (e.g., by copying it into the qstar/src directory and running make), indicating that our Q# definitions satisfy basic well-formedness properties. Proofs about the semantics of the example programs are in DemoProofs.fst.

Contributing

This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.opensource.microsoft.com.

When you submit a pull request, a CLA bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., status check, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact [email protected] with any additional questions or comments.

Trademarks

This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft trademarks or logos is subject to and must follow Microsoft's Trademark & Brand Guidelines. Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. Any use of third-party trademarks or logos are subject to those third-party's policies.