发布 Creusot 0.1 • creusot-rs/creusot

Creusot Overview: Creusot is the first official version of a verification tool for safe Rust programs. It allows proving Rust programs' behavior formally by annotating code with contracts using SMT solvers. It's best for verifying data-structures or algorithm implementations and not for systems with heavy outside world interaction or concurrency. Notable projects using it include CreuSAT and Sprout.
Getting Started: Users should check the README.
Cargo Integration: The cargo creusot binary simplifies crate verification. cargo creusot setup helps manage installations and can install provers like CVC4, CVC5, and Z3. 'External' prover versions can be provided via the --external flag.
Supported Language Features:
- Basic language constructs: All control flow syntax and borrowing (including mutable borrows) are supported.
- Traits: Supports traits with associated methods and constants, trait bounds involving associated types, but not GATs or trait objects.
- Closures: Supports most closures like FnOnce, FnMut, Fn, and move closures. Async closures are not supported.
- Iterators: Provides extensive support for iterators and iterator chains.
Unsupported Language Features:
- Async: Does not support async code, generators, or coroutines.
- Unsafe: Cannot verify code using raw pointers.
- Trait Objects: Does not support trait object reasoning.
- HRTB & GATs: Advanced features like Higher-Ranked Trait Bounds or Generic Associated Types are not supported.
Specification Language: Pearlite:
- Contracts & Assertions: Provides several forms like #[requires(..)], #[ensures(..)], #[variant(..)], #[invariant(..)], proof_assert!(..), and #[trusted].
- Pearlite Expressions: A total, functional language with syntax similar to Rust, including quantifiers, the @ operator, and the ^ final operator.
- Logical Types: Provides types like Int, Seq<T>, FSet<T>, and Map<A, B>.
- Predicates and Logical functions: Users can define their own functions and predicates with contracts.
- Ghost code: Supports snapshots for reasoning about state evolution in loops.
- Trait laws & Refinements: Enforces trait laws and allows refining trait bounds.
- Closure Contracts: Contracts of closures can mention captured variables and use old(..) function.
- Type Invariants: Enforces type invariants by implementing the Invariant trait.
- Extern Specs: Allows assuming outside functions satisfy a contract and refine trait bounds.
creusot-contracts: Part of the creusot-contracts crate with extern specs for Rust standard library and useful logical functions, types, and traits.
Conclusion: Thanks for interest. Many small contributions are unlisted. Future releases aim to be more frequent. Thanks to contributors like Yusuke Matsushita, Sarek Skotam, etc.