From f7148e576980095c63af3704399f72843841722e Mon Sep 17 00:00:00 2001 From: Copilot Date: Mon, 8 Jun 2026 17:11:33 +0000 Subject: [PATCH 1/3] =?UTF-8?q?README:=20note=20Copilot-assisted=20refresh?= =?UTF-8?q?=20=E2=80=94=20~10x=20faster=20verify=20and=20assume=20cleanup?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Update the prominent 'READ before using the code' notice to reflect that verismo now builds and verifies against the latest Verus toolchain after a Copilot-assisted refresh. Highlights: - ~10x faster verification (CI now ~3min) - dropped assume() workarounds / unsound proofs originally added around older Verus bugs Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index d45dad7..1b5ae6c 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,10 @@ This repo includes the code for VeriSMo project. # 🗞️ READ before using the code -* The code here is a research prototype we built between 2022-2024 and will not be able to work with latest verus toolchain. We currently have no active plans to refactor it for newer versions; +* The code here is a research prototype we built between 2022-2024. With assistance from GitHub Copilot, it has been brought back up to date with the latest Verus toolchain. +* Recent improvements (Copilot-assisted refresh, mid-2026): + * **~10× faster verification**: CI now finishes the full proof in ~3 minutes (previously ~30 minutes). + * **Soundness cleanup**: dropped a number of `assume()` workarounds and unsound proofs that had been added to work around bugs in older Verus. * While our approach outperforms traditional OS verification methods, it may still not achieve optimal performance in Verus due to limited proof engineering efforts. * We recommend using this repository as a reference to explore what is possible for low-level verified code (rust-based kernel). For production or ongoing development, please refer to the [Verus project](https://github.com/verus-lang/verus) for the latest features and tooling. From 8bc0646bb344ba92a91b834c2f772f2455aefa7b Mon Sep 17 00:00:00 2001 From: Copilot Date: Mon, 8 Jun 2026 17:13:09 +0000 Subject: [PATCH 2/3] README: split News from 'READ before using' and drop inconsistent claims - Hoist Copilot-assisted refresh into a top-level News section. - Drop the 'may still not achieve optimal performance / limited proof engineering' bullet (inconsistent with the 10x speedup News). - Drop 'due to the old style of Verus code' qualifier (no longer accurate after the toolchain refresh). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- README.md | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 1b5ae6c..eedcadb 100644 --- a/README.md +++ b/README.md @@ -2,16 +2,18 @@ This repo includes the code for VeriSMo project. +# 📰 News + +* **mid-2026 — Copilot-assisted refresh**: verismo now builds and verifies against the latest Verus toolchain. + * **~10× faster verification**: CI finishes the full proof in ~3 minutes (previously ~30 minutes). + * **Soundness cleanup**: dropped `assume()` workarounds and unsound proofs that had been added to work around bugs in older Verus. + # 🗞️ READ before using the code -* The code here is a research prototype we built between 2022-2024. With assistance from GitHub Copilot, it has been brought back up to date with the latest Verus toolchain. -* Recent improvements (Copilot-assisted refresh, mid-2026): - * **~10× faster verification**: CI now finishes the full proof in ~3 minutes (previously ~30 minutes). - * **Soundness cleanup**: dropped a number of `assume()` workarounds and unsound proofs that had been added to work around bugs in older Verus. -* While our approach outperforms traditional OS verification methods, it may still not achieve optimal performance in Verus due to limited proof engineering efforts. +* The code here is a research prototype originally built between 2022-2024. * We recommend using this repository as a reference to explore what is possible for low-level verified code (rust-based kernel). For production or ongoing development, please refer to the [Verus project](https://github.com/verus-lang/verus) for the latest features and tooling. -* The current implementation does not fully separate executable code from specification/proof code due to the old style of Verus code. However, we are actively exploring incremental verification of real-world systems. For example, [COCONUT-SVSM](https://github.com/coconut-svsm/svsm) is the first open-source project that successfully integrated Verus-based verification into an existing codebase without a full rewrite. You could expect it as a more developer-friendly Rust code with a better verification performance in the future. +* The current implementation does not fully separate executable code from specification/proof code. We are actively exploring incremental verification of real-world systems. For example, [COCONUT-SVSM](https://github.com/coconut-svsm/svsm) is the first open-source project that successfully integrated Verus-based verification into an existing codebase without a full rewrite. You could expect it as a more developer-friendly Rust code with a better verification performance in the future. ## Files 📁 From 053f13c0b455ae8b7f90af0b74cc474395def25a Mon Sep 17 00:00:00 2001 From: Copilot Date: Mon, 8 Jun 2026 17:19:44 +0000 Subject: [PATCH 3/3] Update readme --- README.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index eedcadb..3479ee8 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ This repo includes the code for VeriSMo project. # 🗞️ READ before using the code -* The code here is a research prototype originally built between 2022-2024. +* The code here is a research prototype originally built between 2022-2024; The build and verification still work in this project. However it may not work with current HyperV due to ABI mismatch. The steps to run it in a VM is not tested in recent release; * We recommend using this repository as a reference to explore what is possible for low-level verified code (rust-based kernel). For production or ongoing development, please refer to the [Verus project](https://github.com/verus-lang/verus) for the latest features and tooling. * The current implementation does not fully separate executable code from specification/proof code. We are actively exploring incremental verification of real-world systems. For example, [COCONUT-SVSM](https://github.com/coconut-svsm/svsm) is the first open-source project that successfully integrated Verus-based verification into an existing codebase without a full rewrite. You could expect it as a more developer-friendly Rust code with a better verification performance in the future. @@ -57,23 +57,23 @@ Now, run verification checks and build the binary. Run ``` -make verify -``` - -or - -``` -cd source/verismo_main; cargo verify --release; +cd source; cargo verus focus --release; ``` ### b. To verify a single module, which is useful for development: + ``` -cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release; +cd source; cargo verus focus --release -- --verify-module security::monitor ``` ### c. Understand results: -A fully verified result should have "verified": 2138, "errors": 0, +A fully verified result should have + +``` +verification results:: 852 verified, 0 errors +verification results:: 1280 verified, 0 errors +``` ### d. Build without verification 🛠️ @@ -87,7 +87,7 @@ make debugbuild or ``` -cd source/verismo_main; cargo build --feature noverify --release; +cd source/verismo_main; cargo verus build -- --no-verify; ``` ## 4. Create VM image (skip if you run `make` or `make verify`)