From 772dcbd206ebadf76af472bf596f5c92706a5914 Mon Sep 17 00:00:00 2001
From: Aristotelis Papanis <aristotelis.papanis@blocksense.network>
Date: Thu, 23 Oct 2025 17:22:14 +0300
Subject: [PATCH] chore(docs): Updated docs

---
 formal_verification_docs/src/SUMMARY.md       |  21 +--
 .../src/blocksense_noir.md                    |   2 +-
 .../getting_started.md                        |  99 -------------
 .../noir_formal_verification/limitations.md   | 132 ------------------
 .../specifications/README.md                  |   5 -
 .../specifications/ghost_functions.md         |  12 --
 .../specifications/recursion_and_loops.md     |  29 ----
 .../src/unconstrained_support.md              |   1 +
 .../README.md                                 |  13 +-
 .../additional_features.md                    |  18 +--
 .../src/verno/getting_started.md              | 103 ++++++++++++++
 .../src/verno/limitations.md                  |  94 +++++++++++++
 .../specification_syntax.md                   |  72 +++++++---
 .../src/verno/specifications/README.md        |   5 +
 .../verno/specifications/ghost_functions.md   |  38 +++++
 .../specifications/pre_and_postconditions.md  |  37 ++---
 .../specifications/quantifiers.md             |  26 ++--
 .../specifications/recursion_and_loops.md     |  30 ++++
 .../src/verno/unconstrained_support.md        |  72 ++++++++++
 19 files changed, 458 insertions(+), 351 deletions(-)
 delete mode 100644 formal_verification_docs/src/noir_formal_verification/getting_started.md
 delete mode 100644 formal_verification_docs/src/noir_formal_verification/limitations.md
 delete mode 100644 formal_verification_docs/src/noir_formal_verification/specifications/README.md
 delete mode 100644 formal_verification_docs/src/noir_formal_verification/specifications/ghost_functions.md
 delete mode 100644 formal_verification_docs/src/noir_formal_verification/specifications/recursion_and_loops.md
 create mode 100644 formal_verification_docs/src/unconstrained_support.md
 rename formal_verification_docs/src/{noir_formal_verification => verno}/README.md (52%)
 rename formal_verification_docs/src/{noir_formal_verification => verno}/additional_features.md (72%)
 create mode 100644 formal_verification_docs/src/verno/getting_started.md
 create mode 100644 formal_verification_docs/src/verno/limitations.md
 rename formal_verification_docs/src/{noir_formal_verification => verno}/specification_syntax.md (51%)
 create mode 100644 formal_verification_docs/src/verno/specifications/README.md
 create mode 100644 formal_verification_docs/src/verno/specifications/ghost_functions.md
 rename formal_verification_docs/src/{noir_formal_verification => verno}/specifications/pre_and_postconditions.md (65%)
 rename formal_verification_docs/src/{noir_formal_verification => verno}/specifications/quantifiers.md (70%)
 create mode 100644 formal_verification_docs/src/verno/specifications/recursion_and_loops.md
 create mode 100644 formal_verification_docs/src/verno/unconstrained_support.md

diff --git a/formal_verification_docs/src/SUMMARY.md b/formal_verification_docs/src/SUMMARY.md
index a6fadc19fb2..9e34fca7fd1 100644
--- a/formal_verification_docs/src/SUMMARY.md
+++ b/formal_verification_docs/src/SUMMARY.md
@@ -1,16 +1,17 @@
 # Summary
 
 - [Blocksense Noir](./blocksense_noir.md)
-- [Noir Formal Verification](./noir_formal_verification/README.md)
-  - [Getting Started](./noir_formal_verification/getting_started.md)
-  - [Specifications](./noir_formal_verification/specifications/README.md)
-    - [Pre- and Postconditions](./noir_formal_verification/specifications/pre_and_postconditions.md)
-    - [Quantifiers](./noir_formal_verification/specifications/quantifiers.md)
-    - [Ghost Functions](./noir_formal_verification/specifications/ghost_functions.md)
-    - [Recursion and Loops](./noir_formal_verification/specifications/recursion_and_loops.md)
-  - [Additional Features](./noir_formal_verification/additional_features.md)
-  - [Specification Syntax](./noir_formal_verification/specification_syntax.md)
-  - [Limitations](./noir_formal_verification/limitations.md)
+- [Verno](./verno/README.md)
+  - [Getting Started](./verno/getting_started.md)
+  - [Specifications](./verno/specifications/README.md)
+    - [Pre- and Postconditions](./verno/specifications/pre_and_postconditions.md)
+    - [Quantifiers](./verno/specifications/quantifiers.md)
+    - [Ghost Functions](./verno/specifications/ghost_functions.md)
+    - [Recursion and Loops](./verno/specifications/recursion_and_loops.md)
+  - [Additional Features](./verno/additional_features.md)
+  - [Unconstrained Noir Support](./verno/unconstrained_support.md)
+  - [Specification Syntax](./verno/specification_syntax.md)
+  - [Limitations](./verno/limitations.md)
 - [Noir PLONKY2 Backend](./noir_plonky2_backend/README.md)
   - [Getting Started](./noir_plonky2_backend/getting_started.md)
 - [Noir Tracer](./noir_tracer/README.md)
diff --git a/formal_verification_docs/src/blocksense_noir.md b/formal_verification_docs/src/blocksense_noir.md
index 2d51d2c135f..33016359ac7 100644
--- a/formal_verification_docs/src/blocksense_noir.md
+++ b/formal_verification_docs/src/blocksense_noir.md
@@ -4,7 +4,7 @@ At Blocksense, we’ve enhanced the Noir programming language and compiler with
 
   1. [Noir time-travel debugging](./noir_tracer) in the [CodeTracer](https://github.com/metacraft-labs/codetracer) environment;
    
-  2. [formal verification](./noir_formal_verification) of Noir circuits, based on the Z3 SMT solver and the IR language of the [Verus project](https://github.com/verus-lang/verus); and
+  2. [Formal verification](./verno) of Noir circuits, based on the Z3 SMT solver and the IR language of the [Verus project](https://github.com/verus-lang/verus); and
    
   3. [Noir compilation support](./noir_plonky2_backend) for the PLONKY2 proof system.
     
diff --git a/formal_verification_docs/src/noir_formal_verification/getting_started.md b/formal_verification_docs/src/noir_formal_verification/getting_started.md
deleted file mode 100644
index 9259650dfaa..00000000000
--- a/formal_verification_docs/src/noir_formal_verification/getting_started.md
+++ /dev/null
@@ -1,99 +0,0 @@
-# Getting Started
-
-## Installation
-<div class="warning">  
-NOTE: This installation requires more than 20GBs of drive memory.  
-</div>  
-
-First, fetch the source code from our [Noir Github fork](https://github.com/blocksense-network/noir):
-
-```bash
-git clone https://github.com/blocksense-network/noir.git -b formal-verification
-```
-
-* Nix-powered machines with `direnv` only need to do:
-
-    ```bash
-    cd noir
-    direnv allow
-    cargo build
-    ```
-
-* Nix-powered machines without `direnv` have to do the following:
-
-    ```bash
-    cd noir
-    nix develop
-    cargo build
-    export PATH=$PATH:$PWD/target/debug
-    ```
-
-* For other systems, you will need to have `rustup` installed. Follow those instructions:
-
-    ```bash
-    git clone https://github.com/blocksense-network/Venir.git
-
-    pushd Venir
-    export RUSTC_BOOTSTRAP=1
-    cargo build
-    export LD_LIBRARY_PATH="${HOME}/.rustup/toolchains/1.76.0-x86_64-unknown-linux-gnu/lib:${LD_LIBRARY_PATH}"
-    export PATH=$PATH:$PWD/target/debug
-    popd
-
-    pushd noir
-    mkdir lib
-    popd
-
-    git clone https://github.com/Aristotelis2002/verus-lib.git
-    
-    pushd verus-lib/source/
-    pushd tools
-    ./get-z3.sh
-    export VERUS_Z3_PATH=$PWD/z3
-    popd
-    export RUSTC_BOOTSTRAP=1
-    export VERUS_IN_VARGO=1
-    export RUSTFLAGS="--cfg proc_macro_span --cfg verus_keep_ghost --cfg span_locations"
-    cargo build
-    cargo run -p vstd_build -- ./target/debug/
-    cp ./target/debug/vstd.vir ../../noir/lib/
-    popd
-
-    pushd noir
-    cargo build
-    export PATH=$PATH:$PWD/target/debug
-    ```
-
-If you encounter any issues, refer to our [Github discussions](https://github.com/blocksense-network/noir/issues). If it's not listed, don't hesitate to report it—we're happy to assist
-
-## Running Noir FV
-
-Let's first create a Noir project in a new directory:
-
-```bash
-nargo new my_project
-cd my_project
-```
-
-Now, let's try running Noir FV on the following simple Noir program. Copy the following in `src/main.nr`:
-
-```rust,ignore
-#[requires(x >= 100)]
-#[ensures(result >= 20)]
-fn main(x: u32) -> pub u32 {
-    let y = x / 5;
-    y
-}
-```
-
-To formally verify the code run the following command while inside of the project directory:
-
-```bash
-nargo fv
-```
-
-If the verification is successful, you should see the following output:
-
-```
-Verification successful!
-```
diff --git a/formal_verification_docs/src/noir_formal_verification/limitations.md b/formal_verification_docs/src/noir_formal_verification/limitations.md
deleted file mode 100644
index 820c89574d6..00000000000
--- a/formal_verification_docs/src/noir_formal_verification/limitations.md
+++ /dev/null
@@ -1,132 +0,0 @@
-# Limitations
-
-As a prototype, Noir FV has certain limitations and does not yet support some features of Noir. The following features are currently unsupported:
-* **Mutable references** as function parameters
-* **Lambda functions**
-* **Standard library functions**
-* **Unconstrained functions**
-* **Vectors** (`Vec<T>`)
-* **Optional types** (`Option<T>`)
-
-These limitations may change as Noir FV evolves.
-
-These examples show the errors produced when using unsupported features in Noir FV.
-
-## Mutable Reference Parameters
-```rust,ignore
-fn main() {
-    let mut x = 5;
-    nullify(&mut x);
-    assert(x == 0);
-}
-
-fn nullify(x: &mut u32) {
-  *x = 0;
-}
-```
-Output after running `nargo fv`:
-```
-Error: Verification crashed!
-```
-
-## Lambda Functions
-```rust,ignore
-#[ensures(result == x / 2)]
-fn main(x: u32) -> pub u32 {
-  let divide_by_2 = |val| val / 2; // Lambda function
-  divide_by_2(x)
-}
-```
-Output:
-```
-error: postcondition not satisfied
-  ┌─ src/main.nr:1:11
-  │
-1 │ #[ensures(result == x / 2)]
-  │           ---------------- failed this postcondition
-  │
-
-Error: Verification failed!
-```
-
-## Standard Library Functions
-```rust,ignore
-#[requires(x.lt(y))]
-#[ensures(result == x)]
-fn main(x: Field, y: pub Field) -> pub Field {
-    if x.lt(y) {
-      x
-    } else {
-      y
-    }
-}
-```
-Output:
-```
-The application panicked (crashed).
-Message:  called `Option::unwrap()` on a `None` value
-```
-
-## Unconstrained Functions
-```rust,ignore
-#[requires(num < 100000)]
-#[ensures(result == num + 1)]
-fn main(num: u32) -> pub u32 {
-    let out = unsafe { 
-        increment(num) 
-    };
-    out
-}
-#[requires(num < 100000)]
-#[enusres(result == num + 1)]
-unconstrained fn increment(num: u32) -> u32 {
-    if num > 100000 {
-      0
-    } else {
-      num + 1
-    }
-}
-```
-Output:
-```
-The application panicked (crashed).
-Message:  internal error: entered unreachable code
-```
-## Vectors
-```rust,ignore
-fn main(x: Field, y: pub Field) {
-  let mut vector: Vec<Field> = Vec::new();
-  for i in 0..5 {
-    vector.push(i as Field);
-  }
-  assert(vector.len() == 5);
-}
-```
-Output:
-```
-The application panicked (crashed).
-Message:  internal error: entered unreachable code
-```
-
-## Optional Types
-```rust,ignore
-fn main() {
-    let none: Option<u32> = Option::none();
-    assert(none.is_none());
-    let some = Option::some(3);
-    assert(some.unwrap() == 3);
-}
-```
-Output:
-```
-error: assertion failed
-  ┌─ src/main.nr:5:12
-  │
-5 │     assert(some.unwrap() == 3);
-  │            ------------------- assertion failed
-  │
-
-Error: Verification failed!
-```
-
-Although some of these examples may seem easy to support we have decided to focus on completing our prototype sooner so we can get early feedback on the features that we think matter the most.
diff --git a/formal_verification_docs/src/noir_formal_verification/specifications/README.md b/formal_verification_docs/src/noir_formal_verification/specifications/README.md
deleted file mode 100644
index 05580bb5693..00000000000
--- a/formal_verification_docs/src/noir_formal_verification/specifications/README.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Specifications
-
-Noir FV programs contain **specifications** (in the form of annotations) above all functions to define the intended behavior of the code. These specifications include **preconditions**, **postconditions** and **assertions**. Specifications are a form of *ghost code* — instructions that appear in the Noir program for verification purposes, but are not included in the compiled executable.
-
-This chapter covers the syntax and usage of these specifications through basic examples of preconditions, postconditions, and assertions.
diff --git a/formal_verification_docs/src/noir_formal_verification/specifications/ghost_functions.md b/formal_verification_docs/src/noir_formal_verification/specifications/ghost_functions.md
deleted file mode 100644
index 2559905771e..00000000000
--- a/formal_verification_docs/src/noir_formal_verification/specifications/ghost_functions.md
+++ /dev/null
@@ -1,12 +0,0 @@
-# Ghost Functions
-In many formal verification systems, there is a strict separation between code for mathematical proofs and for execution.
-Some systems, like **Verus**, introduce explicit "ghost functions"—special functions used purely for proofs and omitted from compiled code.
-Others, like **Prusti**, allow calling regular functions inside specifications without requiring them to be ghost functions.
-
-**Noir FV does not have ghost functions**. Instead, we prioritize executable code while ensuring that functions used in specifications are **pure**—they must have no side effects and always return the same output for the same input.
-
-The traditional approach of using ghost functions, proofs, and lemmas has its benefits, especially for reasoning about complex systems like distributed systems.
-However, it also has drawbacks, such as reduced code reusability and increased mathematical complexity, which can make the verification process less user-friendly.
-
-With Noir FV, we take a different path—focusing on executable code and usability.
-Our approach simplifies formal verification, making it more intuitive without compromising rigorous correctness guarantees.
\ No newline at end of file
diff --git a/formal_verification_docs/src/noir_formal_verification/specifications/recursion_and_loops.md b/formal_verification_docs/src/noir_formal_verification/specifications/recursion_and_loops.md
deleted file mode 100644
index 2c1f79e9651..00000000000
--- a/formal_verification_docs/src/noir_formal_verification/specifications/recursion_and_loops.md
+++ /dev/null
@@ -1,29 +0,0 @@
-# Recursion and loops
-
-Noir FV streamlines formal verification by eliminating the need for [loop invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html) and [termination proofs](https://verus-lang.github.io/verus/guide/recursion.html).  
-Unlike traditional frameworks that rely on techniques like induction, decrease clauses, and invariants to prove correctness for recursive functions and loops, constrained Noir avoids these complexities altogether.
-
-## Why?
-
-   1. **No Recursion** – Noir does not support recursion, eliminating the need for termination proofs.
-   2. **Bounded Loops** – All loops in constrained Noir have fixed bounds, meaning they always terminate.
-
-## Example: Verifying a Loop
-
-The following Noir function increments `sum` in a loop and successfully verifies **without needing invariants**:
-```rust,ignore
-#[requires((0 <= x) & (x <= y) 
-    & (y < 1000000))] // Prevent overflow when adding numbers
-fn main(x: u32, y: u32) {
-    let mut sum = y;
-    for i in 0..100 {
-        sum += x;
-    }
-    assert(sum >= y);
-}
-```
-Since `sum` is always increasing and `x` is non-negative, the assertion `sum >= y` holds for all valid inputs. Noir FV can verify this automatically without requiring additional annotations.
-
-### Recursion
-
-In Noir FV you *can* prove statements for recursive functions but this is not beneficial because programs with recursion **can not** be built by the standard Noir compiler.
diff --git a/formal_verification_docs/src/unconstrained_support.md b/formal_verification_docs/src/unconstrained_support.md
new file mode 100644
index 00000000000..38745158652
--- /dev/null
+++ b/formal_verification_docs/src/unconstrained_support.md
@@ -0,0 +1 @@
+# Unconstrained Noir Support
diff --git a/formal_verification_docs/src/noir_formal_verification/README.md b/formal_verification_docs/src/verno/README.md
similarity index 52%
rename from formal_verification_docs/src/noir_formal_verification/README.md
rename to formal_verification_docs/src/verno/README.md
index 96b76102b6e..2a1d7299f68 100644
--- a/formal_verification_docs/src/noir_formal_verification/README.md
+++ b/formal_verification_docs/src/verno/README.md
@@ -1,16 +1,15 @@
-# Noir FV overview
+# Verno Overview
 
-We at Blocksense have created a tool for verifying the correctness of code written in Noir. Building upon Microsoft's open-source verification framework Verus, we're able to prove functional correctness of constrained code, before it is ever ran! Noir FV introduces no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable code will always satisfy some user-provided specifications for all possible inputs.  
-
-Constrained Noir is not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness) which simplifies proof writing. Noir’s deterministic nature eliminates the need for complex clauses which appear in other formal verification systems (like [invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html?#loop-invariants) and [decrease clauses](https://verus-lang.github.io/verus/guide/reference-decreases.html?#the-decreases-measure)). Alongside the absence of a heap, we see Noir as a strong candidate for formal verification.
+Verno is a tool for verifying the correctness of code written in Noir, built by Metacraft-labs. Building upon Microsoft's open-source verification framework Verus, we're able to prove functional correctness of constrained code, before it is ever run. Verno introduces no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable code will always satisfy some user-provided specifications for all possible inputs.
 
+Constrained Noir is not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness) which simplifies proof writing. Many loops verify automatically thanks to determinism and fixed bounds, yet Verno also supports richer constructs—such as [loop invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html?#loop-invariants) and [decrease clauses](https://verus-lang.github.io/verus/guide/reference-decreases.html?#the-decreases-measure)—when the program logic requires them. Alongside the absence of a heap, we see Noir as a strong candidate for formal verification.
 
 # This guide
 
-Noir FV reuses Noir's syntax and type system to express specifications for executable code. Basic proficiency with the language is assumed by this guide. Noir's documentation can be found [here](https://noir-lang.org/docs).
+Verno reuses Noir's syntax and type system to express specifications for executable code. Basic proficiency with the language is assumed by this guide. Noir's documentation can be found [here](https://noir-lang.org/docs).
 
-Code specification needs to be written according to a number of predetermined rules, using clauses like `forall` and `requires`. Of course, you'll also need to grasp and conform to the required rigor for creating, what is effectively, a mathematical proof. It can be challenging to prove that a Noir function satisfies its postconditions (its ensures clauses) or that a call to a function satisfies the function’s preconditions (its requires clauses). 
+Code specification needs to be written according to a number of predetermined rules, using clauses like `forall` and `requires`. Of course, you'll also need to grasp and conform to the required rigor for creating, what is effectively, a mathematical proof. It can be challenging to prove that a Noir function satisfies its postconditions (its ensures clauses) or that a call to a function satisfies the function’s preconditions (its requires clauses).
 
 Therefore, this guide’s tutorial will walk you through the various concepts and techniques, starting with relatively simple concepts (e.g., basic properties about integers), progressing to moderately difficult challenges, and eventually covering advanced topics like proofs about arrays using `forall` and `exists`.
 
-All of these proofs are supported by an automated theorem prover (specifically, Z3, a satisfiability-modulo-theories solver, or “SMT solver” for short). The SMT solver will often be able to prove simple properties, such as basic properties about booleans or integer arithmetic, with no additional help from the programmer. However, more complex proofs often require effort from both the programmer and the SMT solver. Therefore, this guide will also help you understand the strengths and limitations of SMT solving, and give advice on how to fill in the parts of proofs that SMT solvers cannot handle automatically.
+All of these proofs are supported by an automated theorem prover (specifically, Z3, a satisfiability-modulo-theories solver, or “SMT solver” for short). The SMT solver will often be able to prove simple properties, such as basic properties about booleans or integer arithmetic, with no additional help from the programmer. However, more complex proofs often require effort from both the programmer and the SMT solver. Therefore, this guide will also help you understand the strengths and limitations of SMT solving, and give advice on how to fill in the parts of proofs that SMT solvers cannot handle automatically.
\ No newline at end of file
diff --git a/formal_verification_docs/src/noir_formal_verification/additional_features.md b/formal_verification_docs/src/verno/additional_features.md
similarity index 72%
rename from formal_verification_docs/src/noir_formal_verification/additional_features.md
rename to formal_verification_docs/src/verno/additional_features.md
index b9389c089cd..588080d3449 100644
--- a/formal_verification_docs/src/noir_formal_verification/additional_features.md
+++ b/formal_verification_docs/src/verno/additional_features.md
@@ -1,6 +1,6 @@
 # Additional Features
 
-Noir FV supports formal verification for **structures**, **tuples**, and **generic functions**, enabling proofs for more complex data types and abstractions.
+Verno supports formal verification for **structures**, **tuples**, and **generic functions**, enabling proofs for more complex data types and abstractions.
 These features are seamless—no additional syntax, complex attributes, or overhead is required.
 
 ## Verifying Structs
@@ -16,9 +16,9 @@ struct Student {
 }
 
 // Returns true if the student qualifies for the scholarship 
-#[requires(student.grade <= MAX_GRADE)] // Max possible grade
-#[ensures(student.grade >= MIN_GRADE ==> result == true)]
-#[ensures(student.grade < MIN_GRADE ==> result == false)]
+#['requires(student.grade <= MAX_GRADE)] // Max possible grade
+#['ensures(student.grade >= MIN_GRADE ==> result == true)]
+#['ensures(student.grade < MIN_GRADE ==> result == false)]
 fn main(student: Student) -> pub bool{
     student.grade >= MIN_GRADE
 }
@@ -40,7 +40,7 @@ struct NamedAccount {
 }
 
 impl BankAccount for NamedAccount {
-  #[ensures(result == self.amount as u64)]
+  #['ensures(result == self.amount as u64)]
   fn get_amount(self) -> u64 {
     self.amount as u64
   }
@@ -52,22 +52,22 @@ struct AnonymousAccount {
 }
 
 impl BankAccount for AnonymousAccount {
-  #[ensures(result == self.amount as u64)]
+  #['ensures(result == self.amount as u64)]
   fn get_amount(self) -> u64 {
     self.amount as u64
   }
 }
 
-#[ensures(result == (first_account.amount as u64 + second_account.amount as u64) )]
+#['ensures(result == (first_account.amount as u64 + second_account.amount as u64) )]
 fn main(first_account: NamedAccount, second_account: AnonymousAccount) -> pub u64 {
   sum_accounts(first_account, second_account)
 }
 
-#[ensures(result == first.get_amount() + second.get_amount())]
+#['ensures(result == first.get_amount() + second.get_amount())]
 fn sum_accounts<T, U>(first: T, second: U) -> pub u64 
 where T: BankAccount,
       U: BankAccount,
 {
   first.get_amount() + second.get_amount()
 }
-```
\ No newline at end of file
+```
diff --git a/formal_verification_docs/src/verno/getting_started.md b/formal_verification_docs/src/verno/getting_started.md
new file mode 100644
index 00000000000..537300fb1aa
--- /dev/null
+++ b/formal_verification_docs/src/verno/getting_started.md
@@ -0,0 +1,103 @@
+# Getting Started with Verno
+
+Welcome to Verno! This guide will walk you through the installation process and show you how to run Verno to formally verify your Noir programs.
+
+## Installation
+
+### Prerequisites
+
+Before you begin, you need to have the Rust programming language and its package manager, Cargo, installed on your system.
+
+We recommend using [rustup](https://rustup.rs/) to install and manage your Rust versions. This project includes a `rust-toolchain.toml` file, and `rustup` will automatically download and use the correct Rust toolchain for you.
+
+### 1. Clone the Repository
+
+First, clone the Verno repository from GitHub:
+
+```bash
+git clone https://github.com/blocksense-network/verno.git
+cd verno
+```
+
+### 2. Set up the Environment
+
+You have two options for setting up the development environment: using Nix or by running the provided shell scripts.
+
+#### Option A: With Nix
+
+If you have the [Nix package manager](https://nixos.org/download.html) installed, you can easily set up a development environment by running:
+
+```bash
+nix develop
+```
+
+This command will create a shell with all the necessary dependencies for Verno.
+
+#### Option B: Without Nix
+
+If you don't have Nix, you can set up the environment by running the following shell scripts from the root of the repository:
+
+```bash
+./get_verus_std.sh
+./venir_build.sh
+```
+
+These scripts will download and build the required dependencies. Please follow any instructions printed by the scripts.
+
+### 3. Build and Test
+
+Once your environment is set up, you can build Verno using Cargo:
+
+```bash
+cargo build
+```
+
+To ensure everything is working correctly, run the test suite:
+
+```bash
+cargo test
+```
+
+If all tests pass, you have successfully installed Verno!
+
+## Running Verno
+
+Let's first create a Noir project in a new directory:
+
+```bash
+nargo new my_project
+cd my_project
+```
+
+If you have `nargo` in your path or have set up the environment variable `NARGO_PATH` to contain the path to your `nargo` binary, you can actually run the following commands instead for creating a Noir project.
+
+
+```bash
+verno new my_project
+cd my_project
+```
+
+Verno supports proxying commands to `nargo`.
+
+Now, let's try running Verno on the following simple Noir program. Copy the following in `src/main.nr`:
+
+```rust,ignore
+#['requires(x >= 100)]
+#['ensures(result >= 20)]
+fn main(x: u32) -> pub u32 {
+    let y = x / 5;
+    y
+}
+```
+
+To formally verify the code run the following command while inside of the project directory:
+
+```bash
+verno formal-verify
+```
+
+If the verification is successful, you should see the following output:
+
+```
+Verification successful!
+```
\ No newline at end of file
diff --git a/formal_verification_docs/src/verno/limitations.md b/formal_verification_docs/src/verno/limitations.md
new file mode 100644
index 00000000000..36be639df24
--- /dev/null
+++ b/formal_verification_docs/src/verno/limitations.md
@@ -0,0 +1,94 @@
+# Limitations
+
+Verno still omits a handful of Noir features. The following constructs remain unsupported today:
+
+* **Lambda functions**
+* **Standard library functions** that rely on runtime helpers beyond the formal-verification shim
+* **Vectors** (`Vec<T>`)
+* **Optional types** (`Option<T>`)
+
+These limitations may change as the toolchain evolves, so check this page when upgrading to a new release. The examples below illustrate the current verifier behaviour when the unsupported features are used.
+
+## Lambda Functions
+```rust,ignore
+#['ensures(result == x / 2)]
+fn main(x: u32) -> pub u32 {
+    let divide_by_2 = |val| val / 2; // Lambda function
+    divide_by_2(x)
+}
+```
+Output:
+```
+error: postcondition not satisfied
+  ┌─ src/main.nr:1:11
+  │
+1 │ #['ensures(result == x / 2)]
+  │           ---------------- failed this postcondition
+  │
+
+Error: Verification failed!
+```
+
+## Standard Library Functions
+```rust,ignore
+#['requires(x.lt(y))]
+#['ensures(result == x)]
+fn main(x: Field, y: pub Field) -> pub Field {
+    if x.lt(y) {
+        x
+    } else {
+        y
+    }
+}
+```
+Output:
+```
+The application panicked (crashed).
+Message:  called `Option::unwrap()` on a `None` value
+```
+
+## Vectors
+```rust,ignore
+fn main(x: Field, y: pub Field) {
+    let mut vector: Vec<Field> = Vec::new();
+    for i in 0..5 {
+        vector.push(i as Field);
+    }
+    assert(vector.len() == 5);
+}
+```
+Output:
+```
+The application panicked (crashed).
+Message:  internal error: entered unreachable code
+```
+
+## Optional Types
+```rust,ignore
+fn main() {
+    let none: Option<u32> = Option::none();
+    assert(none.is_none());
+    let some = Option::some(3);
+    assert(some.unwrap() == 3);
+}
+```
+Output:
+```
+error: assertion failed
+  ┌─ src/main.nr:5:12
+  │
+5 │     assert(some.unwrap() == 3);
+  │            ------------------- assertion failed
+  │
+
+Error: Verification failed!
+```
+
+## Recently Lifted Limitations
+
+Two previously missing capabilities are now available:
+
+- **Mutable references** are supported as function parameters. When writing specifications against mutable borrows, use `fv_std::old()` to refer to the incoming value (see the ghost functions guide for examples).
+- **Unconstrained Noir functions** participate in verification, provided their bodies introduce the right `#[requires]`/`#[ensures]` contracts and loop annotations (`invariant`, `decreases`, etc.). The dedicated *Unconstrained Noir Support* page outlines the required proof obligations.
+
+Although some of the unsupported features above might appear straightforward, we continue to prioritize end-to-end verification of core Noir programs before expanding the surface area further.
diff --git a/formal_verification_docs/src/noir_formal_verification/specification_syntax.md b/formal_verification_docs/src/verno/specification_syntax.md
similarity index 51%
rename from formal_verification_docs/src/noir_formal_verification/specification_syntax.md
rename to formal_verification_docs/src/verno/specification_syntax.md
index ecc68fdd52a..8ab6d1a2e84 100644
--- a/formal_verification_docs/src/noir_formal_verification/specification_syntax.md
+++ b/formal_verification_docs/src/verno/specification_syntax.md
@@ -1,28 +1,30 @@
 # Specification syntax
 
-Noir FV specifications are a superset of Noir's Boolean expressions. The key extensions are summarized below:
+Verno specifications are a superset of Noir's Boolean expressions. The key extensions are summarized below:
 
 | Syntax | Meaning |
 | ------ | ------- |
-| [`result`](specs_grammar.md#result-variable) | Return value of the function |
-| [`... ==> ...`](annotations/quantifiers.md#logical-implication) | Right implication |
-| [`forall(...)`](annotations/quantifiers.md#forall) | Universal quantifier |
-| [`exists(...)`](annotations/quantifiers.md#exists) | Existential quantifier |
+| [`result`](#result-variable) | Return value of the function |
+| [`... ==> ...`](specifications/quantifiers.md#logical-implication) | Right implication |
+| [`forall(...)`](specifications/quantifiers.md#forall) | Universal quantifier |
+| [`exists(...)`](specifications/quantifiers.md#exists) | Existential quantifier |
+| [`old(expr)`](#old-helper) | Value of `expr` at function/loop entry |
+| [`#['ghost]`](specifications/ghost_functions.md) | Declares a ghost-only helper |
 
 ## `result` Variable
 
-In Noir FV, the special variable `result` refers to the return value of a function. It can only be used in **postconditions** (`ensures` annotations) and must not be used as a regular function parameter name.
+In Verno, the special variable `result` refers to the return value of a function. It can only be used in **postconditions** (`ensures` annotations) and must not be used as a regular function parameter name.
 
 Here is an example for returning an integer:
 ```rust,ignore
-#[ensures(result == 8)]
+#['ensures(result == 8)]
 fn eight() -> i32 {
     8
 }
 ```
 And an example for returning a tuple and accessing individual fields:
 ```rust,ignore
-#[ensures((result.0 / -2 == result.1.0 as i32) & (result.1.1 == 0))]
+#['ensures((result.0 / -2 == result.1.0 as i32) & (result.1.1 == 0))]
 fn main() -> pub (i32, (u32, u32)) {
     (-8, (4, 0))
 }
@@ -36,15 +38,15 @@ One implication of this is the need for additional parentheses to ensure the cor
 
 ## Type Checking in Annotations
 
-Noir FV enforces type checking within annotation expressions. While this ensures consistency, it may sometimes produce errors that seem unintuitive, especially to users familiar with other formal verification systems.
+Verno enforces type checking within annotation expressions. While this ensures consistency, it may sometimes produce errors that seem unintuitive, especially to users familiar with other formal verification systems.
 
 In some cases, you may need to add explicit type casts to satisfy the type checker. When doing so, always prefer **upcasting** (from smaller integer type to larger one) rather than **downcasting** (from larger integer type to smaller one), as downcasting can result in loss of information, leading to incorrect verification results. While downcasting may allow the type checker to accept an expression, it can introduce unintended behavior that prevents the verifier from proving correctness.
 
 ### Example: Why Upcasting is Necessary
 Consider the following function::
 ```rust,ignore
-#[requires(x >= y)]
-#[ensures(result == y + 1)]
+#['requires(x >= y)]
+#['ensures(result == y + 1)]
 fn main(x: u16, y: u32) -> pub u32 {
     y + 1
 }
@@ -54,7 +56,7 @@ Attempting to verify this code results in a type error:
 error: Integers must have the same bit width LHS is 16, RHS is 32
   ┌─ src/main.nr:1:12
   │
-1 │ #[requires(x >= y)]
+1 │ #['requires(x >= y)]
   │            -----
   │
 
@@ -62,8 +64,8 @@ Error: Aborting due to 1 previous error
 ```
 To fix the error, we might attempt a downcast, converting `y` to `u16`:
 ```rust,ignore
-#[requires(x >= y as u16)]
-#[ensures(result == y + 1)]
+#['requires(x >= y as u16)]
+#['ensures(result == y + 1)]
 fn main(x: u16, y: u32) -> pub u32 {
     y + 1
 }
@@ -84,13 +86,47 @@ This failure is expected. If `y` were `max(u32) = 4,294,967,295`, downcasting it
 
 Instead of downcasting `y`, the correct approach is to **upcast** `x` to match `y`'s bit width::
 ```rust,ignore
-#[requires(x as u32 >= y)]
-#[ensures(result == y + 1)]
+#['requires(x as u32 >= y)]
+#['ensures(result == y + 1)]
 fn main(x: u16, y: u32) -> pub u32 {
     y + 1
 }
 ```
-After running `nargo fv`:
+After running `verno formal-verify`:
 ```
 Verification successful!
-```
\ No newline at end of file
+```
+## `old` Helper
+
+The `old(expr)` helper refers to the value of an expression at the start of a function (inside `ensures`) or at the start of each loop iteration (inside an `invariant`). This is particularly useful when specifying the behaviour of mutable references.
+
+```rust,ignore
+use fv_std::old;
+
+#['requires(*old(counter) < u32::MAX)]
+#['ensures(*counter == *old(counter) + 1)]
+fn bump(counter: &mut u32) {
+    *counter += 1;
+}
+```
+
+The `old` value is read-only: you can use it in specifications, but not assign to it.
+
+## Ghost Functions
+
+Functions annotated with `#['ghost]` are excluded from the compiled circuit and exist solely for specifications. They keep proof-oriented helpers separate from executable code.
+
+```rust,ignore
+#['ghost]
+fn is_power_of_2(x: i32) -> bool {
+    x > 0 & ((x & (x - 1)) == 0)
+}
+
+#['requires(is_power_of_2(x) & is_power_of_2(y))]
+#['ensures(is_power_of_2(result))]
+fn multiply_powers_of_2(x: i32, y: i32) -> pub i32 {
+    x * y
+}
+```
+
+Ghost helpers can call other ghost code and appear freely inside `requires`/`ensures` clauses.
diff --git a/formal_verification_docs/src/verno/specifications/README.md b/formal_verification_docs/src/verno/specifications/README.md
new file mode 100644
index 00000000000..00eee6f2b5a
--- /dev/null
+++ b/formal_verification_docs/src/verno/specifications/README.md
@@ -0,0 +1,5 @@
+# Specifications
+
+Verno programs contain **specifications** (in the form of annotations) above all functions to define the intended behavior of the code. These specifications include **preconditions**, **postconditions** and **assertions**. Specifications are a form of *ghost code* — instructions that appear in the Noir program for verification purposes, but are not included in the compiled executable.
+
+This chapter covers the syntax and usage of these specifications through basic examples of preconditions, postconditions, and assertions.
diff --git a/formal_verification_docs/src/verno/specifications/ghost_functions.md b/formal_verification_docs/src/verno/specifications/ghost_functions.md
new file mode 100644
index 00000000000..28a2b718b2b
--- /dev/null
+++ b/formal_verification_docs/src/verno/specifications/ghost_functions.md
@@ -0,0 +1,38 @@
+# Ghost Functions
+In many formal verification systems, there is a strict separation between code for mathematical proofs and for execution.
+Some systems, like **Verus**, introduce explicit "ghost functions"—special functions used purely for proofs and omitted from compiled code.
+Others, like **Prusti**, allow calling regular functions inside specifications without requiring them to be ghost functions.
+
+**Verno supports ghost functions**.
+
+A function can be marked as `#['ghost]` to indicate that it is only for use in specifications. Ghost functions are not compiled to ACIR and do not affect the final program, so they can be used to write verification logic that would be too expensive or impossible to run in a real execution.
+
+This is useful for defining helper functions for your specifications that are not part of the program's core logic.
+
+### Example from Test Suite
+
+The project's test suite includes several examples of ghost functions. While most are minimal, the following example, adapted from the `is_power_of_2` test, is the most illustrative.
+
+It uses a ghost function to define a reusable check, which keeps the specifications for the main logic clean and readable.
+
+```rust,ignore
+#['ghost]
+fn is_power_of_2(x: i32) -> bool {
+  if x <= 0 {
+      false
+    } else {
+      (x & (x - 1)) == 0
+    }
+}
+
+#['requires(is_power_of_2(x))]
+#['requires(is_power_of_2(y))]
+#['ensures(is_power_of_2(result))]
+fn multiply_powers_of_2(x: i32, y: i32) -> pub i32 {
+    x * y
+}
+```
+In this example, `is_power_of_2` is a ghost function used in the `requires` and `ensures` annotations to verify the `multiply_powers_of_2` function. The `is_power_of_2` function itself is not part of the compiled program. This helps to keep the specification of `multiply_powers_of_2` clean and readable.
+The traditional approach of using ghost functions, proofs, and lemmas has its benefits, especially for reasoning about complex systems like distributed systems.
+However, it also has drawbacks, such as reduced code reusability and increased mathematical complexity, which can make the verification process less user-friendly.
+
diff --git a/formal_verification_docs/src/noir_formal_verification/specifications/pre_and_postconditions.md b/formal_verification_docs/src/verno/specifications/pre_and_postconditions.md
similarity index 65%
rename from formal_verification_docs/src/noir_formal_verification/specifications/pre_and_postconditions.md
rename to formal_verification_docs/src/verno/specifications/pre_and_postconditions.md
index eabd1fd799e..c46ca80280b 100644
--- a/formal_verification_docs/src/noir_formal_verification/specifications/pre_and_postconditions.md
+++ b/formal_verification_docs/src/verno/specifications/pre_and_postconditions.md
@@ -10,7 +10,12 @@ fn main(x1: i8) -> pub i8 {
 }
 ```
 
-If we run `nargo fv` to verify the code we will get the following output:
+If we run `verno formal-verify` to verify the code we will get the following output:
+
+```admonish tip
+You can use the shorter alias `verno fv` instead of `verno formal-verify`.
+```
+
 ```
 error: possible arithmetic underflow/overflow
   ┌─ src/main.nr:2:14
@@ -21,11 +26,11 @@ error: possible arithmetic underflow/overflow
 
 Error: Verification failed!
 ```
-Noir FV cannot prove that the result of `x1 + x1` fits in an `i8` value, i.e. is in the range `-128`…`127`. For example, if `x1` were `100`, then `x1 + x1` would be `200`, which exceeds `127`. We need to make sure that the argument `x1` stays within a safe range.
+Verno cannot prove that the result of `x1 + x1` fits in an `i8` value, i.e. is in the range `-128`…`127`. For example, if `x1` were `100`, then `x1 + x1` would be `200`, which exceeds `127`. We need to make sure that the argument `x1` stays within a safe range.
 
 We can do this by adding preconditions (also known as `requires` annotations) to `main` specifying which values for `x1` are allowed. Preconditions are written using Noir's [attributes](https://noir-lang.org/docs/noir/concepts/functions#attributes) syntax and they have a boolean body expression which can utilize the function's arguments:
 ```rust,ignore
-#[requires(-64 <= x1 & x1 < 64)]
+#['requires(-64 <= x1 & x1 < 64)]
 fn main(x1: i8) -> pub i8 {
     let x2 = x1 + x1;
     x2 + x2 
@@ -45,7 +50,7 @@ Error: Verification failed!
 ```
 If we want both `x1 + x1` and `x2 + x2` to succeed, we need a stricter bound on `x1`:
 ```rust,ignore
-#[requires(-32 <= x1 & x1 < 32)]
+#['requires(-32 <= x1 & x1 < 32)]
 fn main(x1: i8) -> pub i8 {
     let x2 = x1 + x1;
     x2 + x2 
@@ -59,12 +64,12 @@ fn main() {
     let n = quadruple(40);
 }
 ```
-For this call Noir FV reports an error, since `40` is not less than `32`:
+For this call Verno reports an error, since `40` is not less than `32`:
 ```
 error: precondition not satisfied
   ┌─ src/main.nr:1:12
   │
-1 │ #[requires(-32 <= x1 & x1 < 32)]
+1 │ #['requires(-32 <= x1 & x1 < 32)]
   │            -------------------- failed precondition
   │
 
@@ -85,7 +90,7 @@ fn main() {
     assert(n == 40);
 }
 ```
-Although `quadruple(10)` does return `40`, Noir FV nevertheless reports an error:
+Although `quadruple(10)` does return `40`, Verno nevertheless reports an error:
 ```
 error: assertion failed
    ┌─ src/main.nr:10:12
@@ -96,23 +101,23 @@ error: assertion failed
 
 Error: Verification failed!
 ```
-The error occurs because, even though `quadruple` multiplies its argument by `4`, `quadruple` doesn’t publicize this fact to the other functions in the program. To do this, we can add postconditions (`ensures` annotations) to `quadruple` specifying some properties of `quadruple`’s return value. In Noir FV, the return value is referred with the variable name `result`:
+The error occurs because, even though `quadruple` multiplies its argument by `4`, `quadruple` doesn’t publicize this fact to the other functions in the program. To do this, we can add postconditions (`ensures` annotations) to `quadruple` specifying some properties of `quadruple`’s return value. In Verno, the return value is referred with the variable name `result`:
 ```rust,ignore
-#[requires(-32 <= x1 & x1 < 32)]
-#[ensures(result == 4 * x1)]
+#['requires(-32 <= x1 & x1 < 32)]
+#['ensures(result == 4 * x1)]
 fn quadruple(x1: i8) -> pub i8 {
     let x2 = x1 + x1;
     x2 + x2 
 }
 ```
-With this postcondition, Noir FV can now prove that `quadruple` behaves as intended. When `main` calls quadruple, the SMT solver uses the postcondition to verify the assertion `n == 40`.
+With this postcondition, Verno can now prove that `quadruple` behaves as intended. When `main` calls quadruple, the SMT solver uses the postcondition to verify the assertion `n == 40`.
 ### Modular Verification
-Preconditions and postconditions enable modular verification, a key feature of Noir FV. This approach establishes a clear contract between functions:
-1. When `main` calls `quadruple`, Noir FV checks that the arguments satisfy `quadruple`’s preconditions.
-2. When verifying `quadruple`’s body, Noir FV assumes the preconditions hold and ensures the postconditions are satisfied.
-3. When verifying `main`, Noir FV relies on `quadruple`’s postconditions without needing to inspect its implementation.
+Preconditions and postconditions enable modular verification, a key feature of Verno. This approach establishes a clear contract between functions:
+1. When `main` calls `quadruple`, Verno checks that the arguments satisfy `quadruple`’s preconditions.
+2. When verifying `quadruple`’s body, Verno assumes the preconditions hold and ensures the postconditions are satisfied.
+3. When verifying `main`, Verno relies on `quadruple`’s postconditions without needing to inspect its implementation.
 
 This modularity breaks verification into smaller, manageable pieces, making it more efficient than verifying the entire program at once. However, writing precise preconditions and postconditions requires effort. For large programs, you’ll likely spend significant time crafting these specifications to ensure correctness.
 
 ### Assert and SMT Solvers
-During verification with `nargo fv`, the `assert` keyword is used to make local requests to the SMT solver (Z3) to prove a specific fact. Importantly, Noir's `assert` behaves differently depending on whether you’re running `nargo fv` (verification) or `nargo execute` (execution). 
+During verification with `verno formal-verify`, the `assert` keyword is used to make local requests to the SMT solver (Z3) to prove a specific fact. Importantly, Noir's `assert` behaves differently depending on whether you’re running `verno formal-verify` (verification) or `nargo execute` (execution). 
diff --git a/formal_verification_docs/src/noir_formal_verification/specifications/quantifiers.md b/formal_verification_docs/src/verno/specifications/quantifiers.md
similarity index 70%
rename from formal_verification_docs/src/noir_formal_verification/specifications/quantifiers.md
rename to formal_verification_docs/src/verno/specifications/quantifiers.md
index dec19b0b454..f2470bfa466 100644
--- a/formal_verification_docs/src/noir_formal_verification/specifications/quantifiers.md
+++ b/formal_verification_docs/src/verno/specifications/quantifiers.md
@@ -1,7 +1,7 @@
 # Quantifiers
 ## Logical implication
 
-To improve readability, Noir FV supports the *implication* operator `==>`. The expression `a ==> b` (reads as “a implies b”) is logically equivalent to `!a | b`.
+To improve readability, Verno supports the *implication* operator `==>`. The expression `a ==> b` (reads as “a implies b”) is logically equivalent to `!a | b`.
 
 For example, the expression:
 
@@ -27,10 +27,10 @@ fn is_power_of_2(x: i32) -> bool {
     }
 }
 
-#[requires(is_power_of_2(arr[0]))]
-#[requires(is_power_of_2(arr[1]))]
-#[requires(is_power_of_2(arr[2]))]
-#[ensures(is_power_of_2(result))]
+#['requires(is_power_of_2(arr[0]))]
+#['requires(is_power_of_2(arr[1]))]
+#['requires(is_power_of_2(arr[2]))]
+#['ensures(is_power_of_2(result))]
 fn main(arr: [i32; 3]) -> pub i32 {
     arr[1]
 }
@@ -38,7 +38,7 @@ fn main(arr: [i32; 3]) -> pub i32 {
 
 However, this approach doesn't scale well for larger arrays.
 
-Fortunately, Noir FV and SMT solvers support the [universal(`forall`) and existential(`exists`) quantifiers](https://en.wikipedia.org/wiki/Quantifier_(logic)), which we can think of as infinite conjunctions or disjunctions:
+Fortunately, Verno and SMT solvers support the [universal(`forall`) and existential(`exists`) quantifiers](https://en.wikipedia.org/wiki/Quantifier_(logic)), which we can think of as infinite conjunctions or disjunctions:
 
 ```
 forall(|i| f(i)) = ... f(-2) & f(-1) & f(0) & f(1) & f(2) & ...
@@ -49,11 +49,11 @@ By default the bound variables (`i` in `forall|i|`) are of type `int`, represent
 With quantifiers, it's much more convenient to write a specification about all elements of an array:
 
 ```rust,ignore
-#[requires(
+#['requires(
     forall(|i|
      (0 <= i) & (i < 3) ==> is_power_of_2(arr[i])
     ))]
-#[ensures(is_power_of_2(result))]
+#['ensures(is_power_of_2(result))]
 fn main(arr: [i32; 3]) -> pub i32 {
     arr[1]
 }
@@ -66,13 +66,13 @@ fn main(arr: [i32; 3]) -> pub i32 {
 The following example demonstrates how `exists` successfully finds a witness
 
 ```rust,ignore
-#[requires(is_power_of_2(arr[0]))] // Potential witness
-#[requires(!is_power_of_2(arr[1]))]
-#[requires(is_power_of_2(arr[2]))] // Potential witness
-#[ensures(exists(|i| (0 <= i) & (i < 3) ==> is_power_of_2(result[i])))] // i is going to be either 0 or 2
+#['requires(is_power_of_2(arr[0]))] // Potential witness
+#['requires(!is_power_of_2(arr[1]))]
+#['requires(is_power_of_2(arr[2]))] // Potential witness
+#['ensures(exists(|i| (0 <= i) & (i < 3) ==> is_power_of_2(result[i])))] // i is going to be either 0 or 2
 fn main(arr: [i32; 3]) -> pub [i32; 3] {
     arr
 }
 ```
 
-This verification succeeds because at least one element (`arr[0]` or `arr[2]`) is a power of 2, allowing `exists` to identify a witness.
\ No newline at end of file
+This verification succeeds because at least one element (`arr[0]` or `arr[2]`) is a power of 2, allowing `exists` to identify a witness.
diff --git a/formal_verification_docs/src/verno/specifications/recursion_and_loops.md b/formal_verification_docs/src/verno/specifications/recursion_and_loops.md
new file mode 100644
index 00000000000..d7d963988f2
--- /dev/null
+++ b/formal_verification_docs/src/verno/specifications/recursion_and_loops.md
@@ -0,0 +1,30 @@
+# Recursion and loops
+
+Constrained Noir keeps many loop proofs lightweight thanks to fixed bounds and deterministic control flow. As a result, simple patterns often verify without extra annotations. When additional reasoning is required, Verno now supports explicit [loop invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html) and [decreases clauses](https://verus-lang.github.io/verus/guide/reference-decreases.html?#the-decreases-measure) via helpers in `fv_std`.
+
+## Why do simple loops verify easily?
+
+   1. **No recursion in constrained Noir** – Since recursion is disallowed in the constrained subset, termination proofs rarely come up.
+   2. **Bounded loops** – Loop bounds are explicit, so even without decreases clauses the verifier can reason about termination.
+
+When you step outside these patterns—e.g. working with `unconstrained fn`, ghost helpers, or more precise arithmetic—you can attach invariants and decreases clauses just like in other verification systems. See the [Unconstrained Noir Support](../unconstrained_support.md) guide for a full example.
+
+## Example: Verifying a loop
+
+The following Noir function increments `sum` in a loop and already verifies without extra annotations:
+```rust,ignore
+#['requires((0 <= x) & (x <= y) 
+    & (y < 1000000))] // Prevent overflow when adding numbers
+fn main(x: u32, y: u32) {
+    let mut sum = y;
+    for i in 0..100 {
+        sum += x;
+    }
+    assert(sum >= y);
+}
+```
+Since `sum` is always increasing and `x` is non-negative, the assertion `sum >= y` holds for all valid inputs. If you strengthen the postconditions or need to expose intermediate facts, add `invariant(...)` clauses (and `decreases(...)` when necessary) to the loop body.
+
+### Recursion
+
+In Verno you *can* prove statements for recursive functions but this is not beneficial because programs with recursion **can not** be built by the standard Noir compiler.
diff --git a/formal_verification_docs/src/verno/unconstrained_support.md b/formal_verification_docs/src/verno/unconstrained_support.md
new file mode 100644
index 00000000000..857c2a45858
--- /dev/null
+++ b/formal_verification_docs/src/verno/unconstrained_support.md
@@ -0,0 +1,72 @@
+# Unconstrained Noir Support
+
+Verno now handles Noir programs that mix `unconstrained fn` bodies with specification annotations. This unlocks verification for idiomatic Noir code that performs side-effecting computation while remaining compatible with Noir's `unconstrained` execution model.
+
+The key ingredients for a successful proof are:
+
+1. Add the usual `#[requires(...)]` / `#[ensures(...)]` contracts to your functions, even if the function is marked `unconstrained`.
+2. Annotate loops with `invariant(...)` (to preserve safety properties) and `decreases(...)` (to prove termination) from `fv_std`.
+3. When mutating state through references, use `fv_std::old()` so specifications can refer to the pre-state.
+
+The snippet below demonstrates the pattern on a simple accumulator:
+
+```rust
+use fv_std::{decreases, invariant, old};
+
+#['ensures(result == slice_sum(arr, 0))]
+unconstrained fn sum_array(arr: [u32; 8]) -> u32 {
+    let mut acc = 0;
+    let mut idx = 0;
+
+    while idx < 8 {
+        invariant(idx <= 8);
+        invariant(acc == slice_sum(arr, idx));
+        decreases(8 - idx);
+
+        acc += arr[idx];
+        idx += 1;
+    }
+
+    acc
+}
+
+#['requires(*old(out) == 0)]
+#['ensures(*out == slice_sum(arr, 0))]
+fn write_sum(out: &mut u32, arr: [u32; 8]) {
+    let total = sum_array(arr);
+    *out = total;
+}
+
+#['ghost]
+fn slice_sum(arr: [u32; 8], start: u32) -> u32 {
+    let mut sum = 0;
+    let mut i = start;
+    while i < 8 {
+        invariant(start <= i & i <= 8);
+        invariant(sum == arr[start..i].sum());
+        decreases(8 - i);
+
+        sum += arr[i];
+        i += 1;
+    }
+    sum
+}
+```
+
+This example showcases each of the supported ingredients:
+
+- `sum_array` is `unconstrained`, yet its behaviour is described with a postcondition and loop obligations.
+- Each `while` loop supplies both `invariant` and `decreases` clauses from `fv_std`.
+- The `write_sum` wrapper uses `fv_std::old()` to relate the mutable reference `out` to its pre-state, an ability now supported across the toolchain.
+
+### When to fall back to assumptions
+
+If a proof step requires a fact that Noir's arithmetic reasoning cannot derive automatically (for example, wide integer bounds), it is acceptable to introduce an `fv_std::assume(condition)` inside the loop. Use assumptions sparingly, and prefer strengthening invariants when possible.
+
+### Summary
+
+- Every `unconstrained fn` may be verified as long as it carries contracts.
+- Loops must provide invariants and decreases clauses so the verifier can reason about safety and termination.
+- Mutable references are fully interoperable with `fv_std::old()` and can appear in both constrained and unconstrained contexts.
+
+See the `test_programs/formal_verify_success` fixtures (e.g. `verus_requires_ensures`, `verus_assorted_demo`) for concrete, compilable examples of these techniques in action.