SharpProof checks C# contracts and effects. Add SharpProof to an SDK-style project and build to run the analyzer and full verification automatically.
This is a preview and very, very likely (read: does) have many bugs. The way I would use this project is, if SharpProof claims there is an issue, then get your AI tool of choice to use it as a guide for a test case to prove that that specific test case fails. Proven is conditional on the modeled language subset and recorded assumptions. Refuted requires a replayable violation. Unknown is an accountable result, not success. See semantics and coverage and limits.
Run all repository lint, spelling, package compatibility, and link checks with one Docker command:
docker compose run --rm --build lintIt builds the pinned toolchain and lint tools automatically, writes reports under
artifacts/lint, and exits nonzero if a check fails. For host Git worktrees, use
pwsh -File eng/scripts/Invoke-SharpProof.ps1 lint. See quality gates
for scope and individual checks.
The standard setup is dotnet add package SharpProof using your configured feed, or this one reference with no SharpProof configuration properties:
<ItemGroup>
<PackageReference Include="SharpProof" Version="1.0.0-preview.1" />
</ItemGroup>It restores the contract API, analyzer, worker, and pinned native solver automatically and defaults to strict verification. Keep the standard reference without PrivateAssets="all" so application contract dependencies propagate. The internal dependency graph remains version-matched; no separate installation is needed.
| Package | Purpose |
|---|---|
SharpProof.Attributes |
Application contract API and IntelliSense XML; targets netstandard2.0 |
SharpProof |
Standard complete entrypoint: automatically restores the API, analyzer, build tasks, worker and pinned native solver |
SharpProof.Verifier |
Compatibility entrypoint and implementation payload for analysis and verification |
Full verification covers six native OS/architecture combinations: Windows, macOS, and glibc Linux, each on x64 and ARM64, plus the canonical Linux container, within the host and filesystem support matrix. Windows solver payloads include the C++ runtime statically, so no separate Visual C++ redistributable installation is needed. Linux requires a compatible glibc distribution and native runtime dependencies; musl remains unsupported. Repository development commands run in the canonical container. An explicit advisory/off profile opts out of default strict verification.
The standard setup requires .NET SDK 10.0.100 or newer and its .NET 10 runtime, independently of the application's target framework. Explicit portable-only advisory analysis retains its separate SDK 9.0.300+/Roslyn 4.14 minimum; that older host cannot run the default verifier. The canonical image supplies the pinned SDK.
The consumer application can retain a compatible older target framework. For setup diagnostics, run pwsh -File eng/scripts/Invoke-SharpProof.ps1 doctor -Target path/to/Consumer.csproj -Format Json from this checkout; it evaluates a trusted project without restore/build and identifies missing assets or configuration. A doctor pass does not execute a proof.
See older frameworks, Windows, and Visual Studio for the modern-host application-target matrix, the Windows MSBuild 18+ task-host integration, explicit advisory-only MSBuild 17.14 behavior, and deployment/interactive-IDE qualification limits.
The checked-in package version is 1.0.0-preview.1. Use packed local artifacts to evaluate this checkout; package availability on a public feed is not implied.
using SharpProof.Attributes;
public static class Calculator
{
public static long Increment(long value)
{
Contract.Requires(value >= 0 && value < long.MaxValue);
Contract.Ensures(Contract.Result<long>() == Contract.Old(value) + 1);
return checked(value + 1);
}
}Contract clauses belong in a contiguous method prologue. They express static conditions and are normally removed by the C# compiler. Do not define SHARPPROOF_CONTRACTS: SharpProof has no runtime contract-checking mode.
Start with the single-reference setup and your first proof. Project templates generate the standard setup or an explicit portable-only alternative using this checkout's package version. Follow incremental adoption for an existing repository and upgrades when changing versions. See public API for the full contract surface.
The configuration reference covers selection, IDE behavior, report paths, specification packs, budgets, and caching. Use verification evidence to interpret a run and the language reference to investigate particular C# constructs.
The developer tools guide covers workspace templates, preview-first project initialization, setup/evidence reports in text/JSON/Markdown, exact-base CI comparison, relocatable NUnit regression export, and optional editor scaffolding. These matching preview packages require a configured feed; this checkout does not imply public package availability.
From the repository root, with Docker Compose v2 and Linux containers:
docker compose build tooling
docker compose run --rm tooling test -Target src/SharpProof.Analyzer.Tests/SharpProof.Analyzer.Tests.csproj -TestFilter FullyQualifiedName~DocumentationSnippetTests
docker compose run --rm tooling pr
pr runs Release build and PR semantic/package gates. Coverage, corpus, fuzzing, and security have separate commands; see the container command reference. Finite tasks copy source into private container workspaces and export artifacts. Run repository .NET, PowerShell, packaging, and acceptance commands there.
- Read claim outcomes, reasons, assumptions, and vacuity in worker records. Diagnostic silence alone does not prove anything.
- Compare portable diagnostics with diagnostic examples. Analyzer and worker results have different scopes.
- Inspect typed Unknown reasons before adjusting a budget or changing a contract.
- Review trusted boundaries and API specifications as assumptions. Suppression affects reporting, not evidence.
- Loops, calls, exceptions, and heap operations have modeled cases and conservative limits; language admission does not guarantee a proof.
The documentation index links the current guides, implementation references, and validation fixtures. Contributing describes development standards. Report vulnerabilities through the security policy.
The development workflows guide connects repository changes to the relevant container commands and CI evidence.
Releases use the three-package graph and tag-gated consumer checks described in the release process.