# viperproject/prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.

Repository: https://github.com/viperproject/prusti-dev
Canonical: https://ross.abutalabs.com/products/prusti-dev
Homepage: http://prusti.org
Language: Rust
License: NOASSERTION
License Family: other
Topics: rust, verification, viper, formal-verification
Last push: 2026-08-26T16:13:52+00:00

## Health v2 (maintenance only)
Score: 67/100 (v2, computed 2026-09-02T17:46:02.011165+00:00)
- activity 99, release rhythm 8, longevity 100
- inputs: {"age_days": 2660, "days_push": 7, "days_rel": null, "gap_med": null, "n_releases_24m": 0}
- flags: no_license
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 1806, forks 125 (observed 2026-08-28T04:05:39.068143+00:00)

## What it is
Prusti is a static verifier for Rust that formally proves absence of panics, integer overflows, and other bugs, and checks user-specified contracts such as preconditions, postconditions, and loop invariants. It is built on the Viper verification infrastructure and leverages Rust's ownership type system to simplify specifications.

## Use cases
- formally verify rust code correctness
- prove absence of panics and integer overflows in rust
- check preconditions and postconditions on rust functions
- verify loop invariants in rust programs
- statically analyze rust code for bugs
- specify and check functional contracts in rust

## When to choose
- you need formal correctness guarantees for safety-critical Rust code
- you want to prove absence of panics and overflows beyond what the type system provides
- you are doing research or teaching in program verification with Rust

## When to avoid
- you only need conventional testing or linting rather than formal proofs
- your codebase relies heavily on unsafe Rust, which is largely unsupported
- you need a mature production tool rather than a prototype verifier

## Facets
- artifact type: cli-tool
- maturity: active
- function: testing, developer-tools, parser
- domain: programming-languages, developer-tools
- platform: rust, windows, editor-plugin
- tags: formal-verification, static-analysis, deductive-verification, viper, specification, rust, algorithms, linux, macos

## Member repositories
- viperproject/prusti-dev (main) score 67

## Provenance
- Observed fields: from GitHub, fetched 2026-08-28T04:05:39.068143+00:00.
- Health v2: computed from the inputs above; adoption is never an input.
- Inferred fields (summary, facets, guidance): AI-extracted, prompt v1, taxonomy v1, on 2026-08-30T03:21:32.381457+00:00, confidence not recorded.
  - readme: https://github.com/viperproject/prusti-dev (fetched 2026-08-28T04:05:39.068143+00:00, sha 914d7cfcbef1)
  - homepage: http://prusti.org (fetched 2026-08-29T11:00:38.433038+00:00, sha 9fd1f55457fa)
- Data as of 2026-08-30T08:39:29.467469+00:00.