An RFC for creating an RFC process. :)

.github/PULL_REQUEST_TEMPLATE.md

@@ -7,6 +7,12 @@ Describe Kani's current behavior and how your code changes that behavior. If the
 
 Resolves #ISSUE-NUMBER
 
+### Related RFC:
+
+<!--
+Link to the Tracking RFC issue if this work implements part of an RFC.
+-->
+Optional #ISSUE-NUMBER.
 
 ### Call-outs:
 

.github/workflows/kani.yml

@@ -82,7 +82,7 @@ jobs:
 
       # On one OS only, build the documentation, too.
       - name: Build Documentation
-        run: ./docs/build-docs.sh
+        run: ./scripts/build-docs.sh
 
       # When we're pushed to main branch, only then actually publish the docs.
       - name: Publish Documentation

docs/src/getting-started.md

@@ -12,6 +12,8 @@ Proof harnesses are similar to test harnesses, especially property-based test ha
 
 Kani is currently under active development.
 Releases are published [here](https://github.com/model-checking/kani/releases).
+Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc).
+
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features.
 

rfc/book.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[book]
+title = "Kani RFC Book"
+description = "Design documents for Kani Rust Verifier"
+authors = ["Kani Developers"]
+language = "en"
+multilingual = false
+src = "src"
+
+[output.html]
+site-url = "/kani/rfc/"
+git-repository-url = "https://github.com/model-checking/kani"
+edit-url-template = "https://github.com/model-checking/kani/edit/main/rfc/{path}"
+
+[output.html.playground]
+runnable = false

rfc/src/SUMMARY.md

@@ -0,0 +1,9 @@
+# Kani Rust Verifier - RFCs
+
+[Introduction](./intro.md)
+
+[RFC Template](./template.md)
+
+# Kani RFCs
+
+

rfc/src/intro.md

@@ -0,0 +1,64 @@
+# Introduction
+
+Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. In order to
+integrate feedback from developers and users on future changes to Kani, we decided to follow a light-weight
+"RFC" (request for comments) process.
+
+## When to create an RFC
+
+You should create an RFC in one of two cases:
+
+1. The change you are proposing would be a "one way door": e.g. a change to the public API, a new feature that would be difficult to modify once released, deprecating a feature, etc.
+2. The change you are making has a significant design component, and would benefit from a design review.
+
+Bugs and smaller improvements to existing features do not require an RFC.
+If you are in doubt, feel free to create  a [feature request](https://github.com/model-checking/kani/issues/new?assignees=&labels=&template=feature_request.md) and discuss the next steps in the new issue.
+Your PR reviewer may also request an RFC if your change appears to fall into category 1 or 2.
+
+You do not necessarily need to create an RFC immediately. It is our experience that it is often best to write some "proof of concept" code to test out possible ideas before writing the formal RFC.
+
+## The RFC process
+
+This is the overall workflow for the RFC process:
+
+```toml
+    Create RFC ──> Receive Feedback  ──> Accepted?
+                        │  ∧                  │ Y
+                        ∨  │                  ├───> Implement ───> Test + Feedback ───> Stabilize?
+                       Revise                 │ N                                          │ Y
+                                              └───> Close PR                               ├───> RFC Stable
+                                                                                           │ N
+                                                                                           └───> Remove feature
+```
+
+1. Create an RFC
+   1. Create a tracking issue for your RFC (e.g.: [Issue-1588](https://github.com/model-checking/kani/issues/1588)).
+   2. Start from a fork of the Kani repository.
+   3. Copy the template file ([`rfc/src/template.md`](./template.md)) to `rfc/src/<ID_NUMBER><my-feature>.md`.
+   4. Fill in the details according to the template instructions.
+   5. Submit a pull request.
+2. Build consensus and integrate feedback.
+   1. RFCs should get approved by at least 2 Kani developers.
+   2. Once the RFC has been approved, update the RFC status and merge the PR.
+   3. If the RFC is not approved, close the PR without merging.
+3. Feature implementation.
+   1. Start implementing the new feature in your fork.
+   2. It is OK to implement it incrementally over multiple PRs. Just ensure that every pull request has a testable
+      end-to-end flow and that it is properly tested.
+   3. In the implementation stage, the feature should only be accessible if the user explicitly passes
+      `--enable-unstable` as an argument to Kani.
+   4. Document how to use the feature.
+   5. Keep the RFC up-to-date with the decisions you make during implementation.
+4. Test and Gather Feedback.
+   1. Fix major issues related to the new feature.
+   2. Gather user feedback and make necessary adjustments.
+   3. Add lots of tests.
+5. Stabilization.
+   1. Propose to stabilize the feature when feature is well tested and UX has received positive feedback.
+   2. Create a new PR that removes the `--enable-unstable` guard and that marks the RFC status as "STABLE".
+      1. Make sure the RFC reflects the final implementation and user experience.
+   3. In some cases, we might decide not to incorporate a feature
+      (E.g.: performance degradation, bad user experience, better alternative).
+      In those cases, please update the RFC status to "CANCELLED as per <PR_LINK | ISSUE_LINK>" and remove the code
+      that is no longer relevant.
+   4. Close the tracking issue.

rfc/src/template.md

@@ -0,0 +1,54 @@
+- **Feature Name:** *Fill me with pretty name and a unique ident. E.g: New Feature (`new_feature`)*
+- **Feature Request Issue:** *Link to issue*
+- **RFC PR:** *Link to original PR*
+- **Status:** *One of the following: [Under Review | Unstable | Stable | Cancelled]*
+- **Version:** [0-9]\* *Increment this version whenever you open a new PR to update the RFC (not at every revision).
+  Start with 0.*
+- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
+
+## Summary
+
+Short description of the feature, i.e.: the elevator pitch. What is this feature about?
+
+## User Impact
+
+Why are we doing this? How will this benefit the final user?
+
+ - If this is an API change, how will that impact current users?
+ - For deprecation or breaking changes, how will the transition look like?
+ - If this RFC is related to change in the architecture without major user impact, think about the long term
+impact for user. I.e.: what future work will this enable.
+
+## User Experience
+
+What is the scope of this RFC? Which use cases do you have in mind? Explain how users will interact with it. Also
+please include:
+
+- How would you teach this feature to users? What changes will be required to the user documentation?
+- If the RFC is related to architectural changes and there are no visible changes to UX, please state so.
+
+## Detailed Design
+
+This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind:
+
+- What are the main components that will be modified? (E.g.: changes to `kani-compiler`, `kani-driver`, metadata,
+  installation...)
+- How will they be modified? Any changes to how these components communicate?
+- Will this require any new dependency?
+- What corner cases do you anticipate?
+
+## Rationale and alternatives
+
+- What are the pros and cons of this design?
+- What is the impact of not doing this?
+- What other designs have you considered? Why didn't you choose them?
+
+## Open questions
+
+- Is there any part of the design that you expect to resolve through the RFC process?
+- What kind of user feedback do you expect to gather before stabilization? How will this impact your design?
+
+## Future possibilities
+
+What are natural extensions and possible improvements that you predict for this feature that is out of the
+scope of this RFC? Feel free to brainstorm here.

docs/build-docs.sh → scripts/build-docs.sh

@@ -2,6 +2,10 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# Build all our documentation and place them under book/ directory.
+# The user facing doc is built into book/
+# RFCs are placed under book/rfc/
+
 set -eu
 
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
@@ -20,8 +24,12 @@ fi
 
 # Publish bookrunner report into our documentation
 KANI_DIR=$SCRIPT_DIR/..
+DOCS_DIR=$KANI_DIR/docs
+RFC_DIR=$KANI_DIR/rfc
 HTML_DIR=$KANI_DIR/build/output/latest/html/
 
+cd $DOCS_DIR
+
 if [ -d $HTML_DIR ]; then
     # Litani run is copied into `src` to avoid deletion by `mdbook`
     cp -r $HTML_DIR src/bookrunner/
@@ -38,11 +46,17 @@ else
     echo "WARNING: Could not find the latest bookrunner run."
 fi
 
+echo "Building user documentation..."
 # Build the book into ./book/
 mkdir -p book
-./mdbook build
+mkdir -p book/rfc
+$SCRIPT_DIR/mdbook build
 touch book/.nojekyll
 
+echo "Building RFC book..."
+cd $RFC_DIR
+$SCRIPT_DIR/mdbook build -d $KANI_DIR/docs/book/rfc
+
 # Testing of the code in the documentation is done via the usual
 # ./scripts/kani-regression.sh script. A note on running just the
 # doc tests is in README.md. We don't run them here because