Document zerocopy's design ethos.

README.md

@@ -86,6 +86,31 @@ for network parsing.
 
 [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html
 
+## Zerocopy's Ethos
+
+Much like cryptographic primitives, `unsafe` Rust is a fractal of
+security-critical subtleties. Absent hundreds of engineering hours of expert
+scruitiny, `unsafe` can silently introduce undefined behavior into your
+codebase. We have invested those engineering hours so you don't need to.
+
+We strive to ensure that that Zerocopy code is sound under Rust's current
+memory model, and *any future memory model*. We ensure this by:
+- **...not 'guessing' about Rust's semantics.**
+  We annotate `unsafe` with a precise rationale for its soundness that
+  quotes a relevant section of the Rust's official documentation. When
+  Rust's documented semantics are unclear, we work with the Rust Operational
+  Semantics Team to clarify Rust's documentation.
+- **...rigorously testing our implementation.**
+  We run tests using [Miri], ensuring that Zerocopy is sound across a wide
+  array of supported target platforms of varying endianness and pointer
+  width, and across both current and experimental memory models of Rust.
+- **...formally proving the correctness of our implementation.**
+  We apply formal verification tools like [Kani][kani] to prove Zerocopy's
+  correctness.
+
+[Miri]: https://github.com/rust-lang/miri
+[Kani]: https://github.com/model-checking/kani
+
 ## Disclaimer
 
 Disclaimer: Zerocopy is not an officially supported Google product.

src/lib.rs

@@ -84,6 +84,31 @@
 //!   may be removed at any point in the future.
 //!
 //! [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html
+//!
+//! # Zerocopy's Ethos
+//!
+//! Much like cryptographic primitives, `unsafe` Rust is a fractal of
+//! security-critical subtleties. Absent hundreds of engineering hours of expert
+//! scruitiny, `unsafe` can silently introduce undefined behavior into your
+//! codebase. We have invested those engineering hours so you don't need to.
+//!
+//! We strive to ensure that that Zerocopy code is sound under Rust's current
+//! memory model, and *any future memory model*. We ensure this by:
+//! - **...not 'guessing' about Rust's semantics.**   
+//!   We annotate `unsafe` with a precise rationale for its soundness that
+//!   quotes a relevant section of the Rust's official documentation. When
+//!   Rust's documented semantics are unclear, we work with the Rust Operational
+//!   Semantics Team to clarify Rust's documentation.
+//! - **...rigorously testing our implementation.**   
+//!   We run tests using [Miri], ensuring that Zerocopy is sound across a wide
+//!   array of supported target platforms of varying endianness and pointer
+//!   width, and across both current and experimental memory models of Rust.
+//! - **...formally proving the correctness of our implementation.**   
+//!   We apply formal verification tools like [Kani][kani] to prove Zerocopy's
+//!   correctness.
+//!
+//! [Miri]: https://github.com/rust-lang/miri
+//! [Kani]: https://github.com/model-checking/kani
 
 // Sometimes we want to use lints which were added after our MSRV.
 // `unknown_lints` is `warn` by default and we deny warnings in CI, so without