Updates for README.md (model-checking#1010)

* Updates for `README.md`

* Address comments

* Use lowercase in bullet list

README.md

@@ -1,19 +1,16 @@
 # Kani Rust Verifier
 
-The Kani Rust Verifier aims to be a bit-precise model-checker for Rust.
-Kani ensures that unsafe Rust code is actually safe, and verifies that safe Rust code will not panic at runtime.
+The Kani Rust Verifier is a bit-precise model checker for Rust.
 
-## Installing Kani
+Kani verifies:
+ * memory safety -- even in unsafe Rust code
+ * user-specified assertions
+ * absence of panics
+ * checks for some classes of undefined behavior
 
-Until an official release is out, you can [read documentation on how to check out and build Kani yourself](https://model-checking.github.io/kani/install-guide.html).
+## Installation
 
-## What can Kani do?
-
-Our documentation covers:
-
-* [Comparison with other tools](https://model-checking.github.io/kani/tool-comparison.html)
-* [Failures that Kani can spot](https://model-checking.github.io/kani/tutorial-kinds-of-failure.html)
-* [Kani's current limitations](https://model-checking.github.io/kani/limitations.html)
+Kani must currently be built from source. See [the installation guide](https://model-checking.github.io/kani/install-guide.html) for more details.
 
 ## How does Kani work?
 
@@ -24,30 +21,34 @@ use my_crate::{function_under_test, is_valid, meets_specification};
 
 #[kani::proof]
 fn check_my_property() {
+   // Create a nondeterministic input
    let input = kani::any();
+   // Constrain it to represent valid values
    kani::assume(is_valid(input));
+   // Call the function under verification
    let output = function_under_test(input);
+   // Check that it meets the specification
    assert!(meets_specification(input, output));
 }
 ```
 
-Kani will then prove that all valid inputs will produce acceptable outputs, without panicking or executing undefined behavior.
-You can learn more about how to use Kani [by following the Kani tutorial](https://model-checking.github.io/kani/kani-tutorial.html).
+Kani will then prove that all valid inputs produce acceptable outputs, without panicking or executing undefined behavior.
+We recommend following [the tutorial](https://model-checking.github.io/kani/kani-tutorial.html) to learn more about how to use Kani.
 
 ## Security
 See [SECURITY](https://github.com/model-checking/kani/security/policy) for more information.
 
-## Developer guide
-See [Kani developer documentation](https://model-checking.github.io/kani/dev-documentation.html).
+## Contributing
+If you are interested in contributing to Kani, please take a look at [the developer documentation](https://model-checking.github.io/kani/dev-documentation.html).
 
 ## License
 ### Kani
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 
 See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details.
 
-### Rust compiler
-Kani contains code from the Rust compiler.
-The rust compiler is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
+### Rust
+Kani contains code from the Rust project.
+Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
 
 See [the Rust repository](https://github.com/rust-lang/rust) for details.