Update README (#4291)

Update our README to make it clearer that Kani is useful for *both*
safety and correctness, not mostly safety with correctness on the side.


By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

README.md

@@ -4,13 +4,10 @@
 
 The Kani Rust Verifier is a bit-precise model checker for Rust.
 
-Kani is particularly useful for verifying unsafe code blocks in Rust, where the "[unsafe superpowers](https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers)" are unchecked by the compiler.
-___
-Kani verifies:
- * Memory safety (e.g., null pointer dereferences)
- * User-specified assertions (i.e., `assert!(...)`)
- * The absence of panics (e.g., `unwrap()` on `None` values)
- * The absence of some types of unexpected behavior (e.g., arithmetic overflows)
+Kani is useful for checking both safety and correctness of Rust code.
+- *Safety*: Kani automatically checks for many kinds of [undefined behavior](https://model-checking.github.io/kani/undefined-behaviour.html).
+This makes it particularly useful for verifying unsafe code blocks in Rust, where the "[unsafe superpowers](https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers)" are unchecked by the compiler.
+- *Correctness*: Kani automatically checks panics (e.g. `unwrap()` on `None`), arithmetic overflows, and custom correctness properties, either in the form of assertions (`assert!(...)`) or [function contracts](https://model-checking.github.io/kani/reference/experimental/contracts.html).
 
 ## Installation
 
@@ -28,15 +25,12 @@ See [the installation guide](https://model-checking.github.io/kani/install-guide
 Similar to testing, you write a harness, but with Kani you can check all possible values using `kani::any()`:
 
 ```rust
-use my_crate::{function_under_test, meets_specification, precondition};
+use my_crate::{function_under_test, meets_specification};
 
 #[kani::proof]
 fn check_my_property() {
    // Create a nondeterministic input
-   let input = kani::any();
-
-   // Constrain it according to the function's precondition
-   kani::assume(precondition(input));
+   let input: u8 = kani::any();
 
    // Call the function under verification
    let output = function_under_test(input);
@@ -46,9 +40,8 @@ fn check_my_property() {
 }
 ```
 
-Kani will then try to prove that all valid inputs produce acceptable outputs, without panicking or executing unexpected behavior.
-Otherwise Kani will generate a trace that points to the failure.
-We recommend following [the tutorial](https://model-checking.github.io/kani/kani-tutorial.html) to learn more about how to use Kani.
+Kani will try to prove that all valid inputs produce outputs that satisfy the specification, without panicking or exhibiting unexpected behavior.
+This example is simple; we highly recommend following [the tutorial](https://model-checking.github.io/kani/kani-tutorial.html) to learn more about how to use Kani.
 
 ## GitHub Action
 

docs/src/getting-started.md

@@ -1,11 +1,12 @@
 # Getting started
 
 Kani is an open-source verification tool that uses [model checking](./tool-comparison.md) to analyze Rust programs.
-Kani is particularly useful for verifying unsafe code blocks in Rust, where the "[unsafe superpowers](https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers)" are unchecked by the compiler.
-Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows).
-Kani can also prove custom properties provided in the form of user-specified assertions.
-As Kani uses model checking, Kani will either prove the property, disprove the
-property (with a counterexample), or may run out of resources.
+Kani is useful for checking both safety and correctness of Rust code.
+- *Safety*: Kani automatically checks for many kinds of [undefined behavior](./undefined-behaviour.md).
+This makes it particularly useful for verifying unsafe code blocks in Rust, where the "[unsafe superpowers](https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers)" are unchecked by the compiler.
+- *Correctness*: Kani automatically checks panics (e.g. `unwrap()` on `None`), arithmetic overflows, and custom correctness properties, either in the form of assertions (`assert!(...)`) or [function contracts](https://model-checking.github.io/kani/reference/experimental/contracts.html).
+
+Since Kani uses model checking, Kani will either prove the property, disprove the property (with a counterexample), or may run out of resources.
 
 Kani uses proof harnesses to analyze programs.
 Proof harnesses are similar to test harnesses, especially property-based test harnesses.