add links to docs (#294)

README.md

@@ -1,13 +1,20 @@
 # Cedar Specification
 
-This repository contains the formalization of Cedar and infrastructure for performing differential randomized testing (DRT) between the formalization and Rust production implementation available in [cedar](https://github.com/cedar-policy/cedar).
+This repository contains the formalization of Cedar and infrastructure for performing differential randomized testing (DRT) between the formalization and Rust production implementation available in [`cedar`](https://github.com/cedar-policy/cedar).
+
+You can learn more about our formalization efforts in the following blog posts:
+
+* [How we built Cedar with automated reasoning and differential testing](https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing)
+* [Lean Into Verified Software Development](https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/)
 
 ## Repository Structure
 
 * [`cedar-lean`](./cedar-lean) contains the Lean formalization of, and proofs about, Cedar.
 * [`cedar-drt`](./cedar-drt) contains code for fuzzing, property-based testing, and differential testing of Cedar.
 * [`cedar-policy-generators`](./cedar-policy-generators) contains code for generating schemas, entities, policies, and requests using the [arbitrary](https://docs.rs/arbitrary/latest/arbitrary/index.html#) crate.
 
+See the README in each directory for more information.
+
 ## Build
 
 ### Lean formalization and proofs

cedar-lean/README.md

@@ -2,6 +2,8 @@
 
 This folder contains the Lean formalization of, and proofs about, Cedar.
 
+Auto-generated documentation is available at <https://cedar-policy.github.io/cedar-spec/docs/>.
+
 ## Setup
 
 Follow [these instructions](https://leanprover.github.io/lean4/doc/setup.html) to set up Lean and install the VS Code plugin.