Wybe 0.0.5

.NET 9.0 This package targets .NET 9.0. The package is compatible with this framework or higher. 
dotnet add package Wybe --version 0.0.5
                    


                    

                
NuGet\Install-Package Wybe -Version 0.0.5
This command is intended to be used within the Package Manager Console in Visual Studio, as it uses the NuGet module's version of Install-Package. 
<PackageReference Include="Wybe" Version="0.0.5" />
For projects that support PackageReference, copy this XML node into the project file to reference the package. 
<PackageVersion Include="Wybe" Version="0.0.5" />
                    


                            Directory.Packages.props
                        

                    

                
<PackageReference Include="Wybe" />
                    


                            Project file
For projects that support Central Package Management (CPM), copy this XML node into the solution Directory.Packages.props file to version the package. 
paket add Wybe --version 0.0.5
                    


                    

                
#r "nuget: Wybe, 0.0.5"
#r directive can be used in F# Interactive and Polyglot Notebooks. Copy this into the interactive tool or source code of the script to reference the package. 
#:package Wybe@0.0.5
#:package directive can be used in C# file-based apps starting in .NET 10 preview 4. Copy this into a .cs file before any lines of code to reference the package. 
#addin nuget:?package=Wybe&version=0.0.5
                    


                            Install as a Cake Addin
                        

                    

                
#tool nuget:?package=Wybe&version=0.0.5
                    


                            Install as a Cake Tool

Wybe

Wybe

A theorem prover embedded in F#'s computation expressions, using Z3 under the hood

Features and progress

Installation instructions

  • Install the dotnet 9 CLI
  • Clone this repository locally

Example workflow

  1. create a Rust file with functions and declare their properties as assertions in the source code. We will be using the example functions in example_functions.rs

  2. extract proof obligations to an F# script, in this case example_functions.fsx

    cd wybe/experiments
dotnet run --project ../Tool/Tool.fsproj -- -e example_functions.rs

  3. complete the necessary steps to prove all the theorems in example_functions.fsx, i.e. if checking a proof fails then more detailed calculations and hints must be provided.

  4. check the proofs in example_functions.fsx

    dotnet fsi example_functions.fsx

  5. if the output indicates success, you have formally verified all declared properties of the Rust functions in example_functions.rs.

  6. add more functions to example_functions.rs or modify existing ones

  7. continue extracting proof obligations, completing and checking the proofs

Note: once the Wybe CLI is published as a NuGet package and installed, you can simply run wybe -e example_functions.rs to extract proof obligations and wybe -c example_functions.fsx to check proofs.

Example proof

Double Negation

Product Compatible and additional computed target framework versions.
.NET net9.0 is compatible.  net9.0-android was computed.  net9.0-browser was computed.  net9.0-ios was computed.  net9.0-maccatalyst was computed.  net9.0-macos was computed.  net9.0-tvos was computed.  net9.0-windows was computed.  net10.0 was computed.  net10.0-android was computed.  net10.0-browser was computed.  net10.0-ios was computed.  net10.0-maccatalyst was computed.  net10.0-macos was computed.  net10.0-tvos was computed.  net10.0-windows was computed. 
Compatible target framework(s)
Included target framework(s) (in package)
Learn more about Target Frameworks and .NET Standard.

NuGet packages

This package is not used by any NuGet packages.

GitHub repositories

This package is not used by any popular GitHub repositories.

Version Downloads Last Updated
0.0.5 115 5/23/2025
0.0.4 145 5/22/2025
0.0.3 172 5/16/2025
0.0.2 182 5/16/2025
0.0.1 231 5/14/2025