From 92569f68d287640c74607671e8a332c8d0769d7a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 17 Aug 2026 19:26:54 -0400 Subject: [PATCH 1/5] Add citation metadata for the Kani ASE 2026 paper Add a `CITATION.cff` (CFF 1.2.0) whose `preferred-citation` points at the ASE '26 paper, so GitHub's "Cite this repository" button emits the paper rather than a bare software reference, and add a "Citing Kani" section to the README with the ACM Reference Format and a ready-to-paste BibTeX entry. Validated with `cffconvert --validate` (schema 1.2.0) and rendered with `ruby-cff` (the library behind GitHub's citation widget). --- CITATION.cff | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 32 ++++++++++++++++++++++ 2 files changed, 107 insertions(+) create mode 100644 CITATION.cff diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 000000000000..83f02f8c1c2a --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,75 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +cff-version: 1.2.0 +title: Kani Rust Verifier +message: >- + If you use Kani in your research, please cite the ASE 2026 paper listed under + `preferred-citation`. +type: software +authors: + - name: The Kani Contributors +abstract: >- + Kani is a bit-precise model checker for Rust. It verifies both safety + (undefined behavior) and correctness (panics, arithmetic overflow, and + user-defined properties expressed as assertions or function contracts) of Rust + programs, including unsafe code. +repository-code: https://github.com/model-checking/kani +url: https://model-checking.github.io/kani/ +license: + - Apache-2.0 + - MIT +keywords: + - rust + - model checking + - formal verification + - program analysis + - undefined behavior +preferred-citation: + type: conference-paper + title: "Kani: A Model Checker for Rust" + authors: + - given-names: Rémi + family-names: Delmas + - given-names: Zyad + family-names: Hassan + - given-names: Qinheping + family-names: Hu + - given-names: Rahul + family-names: Kumar + - given-names: Felipe R. + family-names: Monteiro + - given-names: Thanh + family-names: Nguyen + - given-names: Adrián + family-names: Palacios + - given-names: Celina + family-names: Val + - given-names: Michael + family-names: Tautschnig + - given-names: Justus + family-names: Adam + - given-names: Daniel + family-names: Schwartz-Narbonne + - given-names: Carolyn + family-names: Zech + collection-title: >- + Proceedings of the 41st IEEE/ACM International Conference on Automated + Software Engineering (ASE '26) + collection-type: proceedings + conference: + name: >- + 41st IEEE/ACM International Conference on Automated Software Engineering + city: Munich + country: DE + date-start: '2026-10-12' + date-end: '2026-10-16' + publisher: + name: Association for Computing Machinery + city: New York + region: NY + country: US + year: 2026 + month: 10 + pages: 13 + doi: 10.1145/3832783.3834499 + url: https://doi.org/10.1145/3832783.3834499 diff --git a/README.md b/README.md index 4459d5aa25e1..d65d12aae435 100644 --- a/README.md +++ b/README.md @@ -50,6 +50,38 @@ Use Kani in your CI with `model-checking/kani-github-action@VERSION`. See the book](https://model-checking.github.io/kani/install-github-ci.html) for details. +## Citing Kani + +If you use Kani in your research, please cite our ASE 2026 paper. + +ACM Reference Format: + +> Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, and Carolyn Zech. 2026. Kani: A Model Checker for Rust. In *Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE '26), October 12–16, 2026, Munich, Germany*. ACM, New York, NY, USA, 13 pages. + +BibTeX: + +```bibtex +@inproceedings{kani-ase-2026, + author = {Delmas, R{\'e}mi and Hassan, Zyad and Hu, Qinheping and Kumar, Rahul and + Monteiro, Felipe R. and Nguyen, Thanh and Palacios, Adri{\'a}n and + Val, Celina and Tautschnig, Michael and Adam, Justus and + Schwartz-Narbonne, Daniel and Zech, Carolyn}, + title = {{Kani}: A Model Checker for {Rust}}, + year = {2026}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/3832783.3834499}, + doi = {10.1145/3832783.3834499}, + booktitle = {Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering}, + numpages = {13}, + location = {Munich, Germany}, + series = {ASE '26} +} +``` + +The same citation is available in machine-readable form in [CITATION.cff](CITATION.cff), +which powers GitHub's *Cite this repository* button. + ## Security See [SECURITY](https://github.com/model-checking/kani/security/policy) for more information. From 14a372e550d575a7a838f537d52cace23e21d5bc Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 17 Aug 2026 19:27:05 -0400 Subject: [PATCH 2/5] Remove VSTTE 2024 paper sources The LaTeX sources for the VSTTE 2024 short paper were checked in but are not built by anything in the repository, and the paper itself is now published. The ASE 2026 paper is the citation of record, so point people at it via `CITATION.cff` and the README instead of carrying paper sources here. The sources remain available in the git history. Also drop the now-empty `papers/` entry from the AGENTS.md repository layout table. --- AGENTS.md | 1 - papers/vstte2024/README.md | 1 - papers/vstte2024/paper.bib | 135 ----------------------------- papers/vstte2024/paper.tex | 172 ------------------------------------- 4 files changed, 309 deletions(-) delete mode 100644 papers/vstte2024/README.md delete mode 100644 papers/vstte2024/paper.bib delete mode 100644 papers/vstte2024/paper.tex diff --git a/AGENTS.md b/AGENTS.md index 26c101e18698..19997c23609f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -45,7 +45,6 @@ Kani uses [CBMC](https://github.com/diffblue/cbmc) as its underlying verificatio |-----------|-------------| | `docs/` | User and developer documentation (built with mdBook) | | `rfc/` | Request for Comments documents for design decisions | -| `papers/` | Academic papers related to Kani | ## Build and Development Commands diff --git a/papers/vstte2024/README.md b/papers/vstte2024/README.md deleted file mode 100644 index 568b501138b5..000000000000 --- a/papers/vstte2024/README.md +++ /dev/null @@ -1 +0,0 @@ -This contains the contents for a short paper at VSTTE2024. In order to build this, please download the LLNCS style file available at https://resource-cms.springernature.com/springer-cms/rest/v1/content/19238648/data/v8, unpack the resulting llncs.zip, and use standard LaTeX tools to build the paper. \ No newline at end of file diff --git a/papers/vstte2024/paper.bib b/papers/vstte2024/paper.bib deleted file mode 100644 index dafdbc98cbb2..000000000000 --- a/papers/vstte2024/paper.bib +++ /dev/null @@ -1,135 +0,0 @@ -% Copyright Kani Contributors -% SPDX-License-Identifier: Apache-2.0 OR MIT - -\begin{paper}{8} -@inproceedings{verus-sys, - author = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan}, - booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)}, - code = {https://github.com/verus-lang/verus}, - month = {November}, - title = {Verus: A Practical Foundation for Systems Verification}, - year = {2024} -} - -@inproceedings{denis2022creusot, - title={Creusot: a foundry for the deductive verification of {R}ust programs}, - author={Denis, Xavier and Jourdan, Jacques-Henri and March{'e}, Claude}, - booktitle={International Conference on Formal Engineering Methods}, - pages={90--105}, - year={2022}, - organization={Springer} -} - -@inproceedings{astrauskas2022prusti, - title={The {P}rusti project: Formal verification for {R}ust}, - author={Astrauskas, Vytautas and B{\'\i}l{\`y}, Aurel and Fiala, Jon{\'a}{\v{s}} and Grannan, Zachary and Matheja, Christoph and M{\"u}ller, Peter and Poli, Federico and Summers, Alexander J}, - booktitle={NASA Formal Methods Symposium}, - pages={88--108}, - year={2022}, - organization={Springer} -} - -@inproceedings{vanhattum2022verifying, - title={Verifying dynamic trait objects in {R}ust}, - author={VanHattum, Alexa and Schwartz-Narbonne, Daniel and Chong, Nathan and Sampson, Adrian}, - booktitle={Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice}, - pages={321--330}, - year={2022} -} - -@manual{superPower, - title = {Unsafe Rust}, - url = {https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html}, - author = {Rust Documentation} -} - -@inproceedings{li2021mirchecker, - title={MirChecker: detecting bugs in {R}ust programs via static analysis}, - author={Li, Zhuohua and Wang, Jincheng and Sun, Mingshen and Lui, John CS}, - booktitle={Proceedings of the 2021 ACM SIGSAC conference on computer and communications security}, - pages={2183--2196}, - year={2021} -} - -@manual{stringChallenge, - title = {Memory Safety of String}, - year = {2024}, - author = {Zyad Hassan}, - url = {https://model-checking.github.io/verify-rust-std/challenges/0010-string.html} -} - -@manual{anderson20medium, - title = {The Rust Compilation Model Calamity}, - year = {2020}, - url = {https://pingcap.medium.com/the-rust-compilation-model-calamity-1a8ce781cf6cb}, - author = {Brian Anderson} -} - -@article{matsakis2014rust, - title={The rust language}, - author={Matsakis, Nicholas D and Klock, Felix S}, - journal={ACM SIGAda Ada Letters}, - volume={34}, - number={3}, - pages={103--104}, - year={2014}, - publisher={ACM New York, NY, USA} -} - -@manual{challenge, - title = {Memory Safety of String}, - url = {https://github.com/model-checking/verify-rust-std/issues/61}, - author = {Zyad Hassan}, - year = {2024} -} - -@manual{solution, - title = {char and ascii{\_}char contracts}, - url = {https://github.com/model-checking/verify-rust-std/pull/48}, - year = {2024}, - author = {Carolyn Zech} -} - -@manual{rustAndroid, - title = {The Impact of Rust on Security Development}, - year = {2024}, - url = {https://www.riscure.com/the-impact-of-rust-on-security-development}, - author = {Christiaan Biesterbosch and Valeria Vatolina} -} -@manual{liam2022android, - title = {How Google is using Rust to reduce memory safety vulnerabilities in Android}, - year = {2020}, - url = {https://www.zdnet.com/article/google-after-using-rust-we-slashed-android-memory-safety-vulnerabilities/}, - author = {Liam Tung} -} - -@article{jung2017rustbelt, - title={RustBelt: Securing the foundations of the Rust programming language}, - author={Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek}, - journal={Proceedings of the ACM on Programming Languages}, - volume={2}, - number={POPL}, - pages={1--34}, - year={2017}, - publisher={ACM New York, NY, USA} -} - -@article{ayoun2024hybrid, - title={A hybrid approach to semi-automated Rust verification}, - author={Ayoun, Sacha-{\'E}lie and Denis, Xavier and Maksimovi{\'c}, Petar and Gardner, Philippa}, - journal={arXiv preprint arXiv:2403.15122}, - year={2024} -} - -@article{ho2022aeneas, - title={Aeneas: Rust verification by functional translation}, - author={Ho, Son and Protzenko, Jonathan}, - journal={Proceedings of the ACM on Programming Languages}, - volume={6}, - number={ICFP}, - pages={711--741}, - year={2022}, - publisher={ACM New York, NY, USA} -} - -\end{thebibliography} \ No newline at end of file diff --git a/papers/vstte2024/paper.tex b/papers/vstte2024/paper.tex deleted file mode 100644 index a523bbf1de5b..000000000000 --- a/papers/vstte2024/paper.tex +++ /dev/null @@ -1,172 +0,0 @@ -% Copyright Kani Contributors -% SPDX-License-Identifier: Apache-2.0 OR MIT - -\documentclass[runningheads]{llncs} -% -\usepackage[T1]{fontenc} -\usepackage{graphicx} -\usepackage{amsmath,amsfonts} -\usepackage{hyperref} -\usepackage{listings} -\usepackage{xcolor} -\usepackage{color} -\usepackage{listings} -\definecolor{GrayCodeBlock}{RGB}{241,241,241} -\definecolor{BlackText}{RGB}{110,107,94} -\definecolor{RedTypename}{RGB}{182,86,17} -\definecolor{GreenString}{RGB}{96,172,57} -\definecolor{PurpleKeyword}{RGB}{184,84,212} -\definecolor{GrayComment}{RGB}{170,170,170} -\definecolor{GoldDocumentation}{RGB}{180,165,45} -\lstdefinelanguage{rust} -{ - columns=fullflexible, - keepspaces=true, - frame=single, - framesep=0pt, - framerule=0pt, - framexleftmargin=4pt, - framexrightmargin=4pt, - framextopmargin=5pt, - framexbottommargin=3pt, - xleftmargin=4pt, - xrightmargin=4pt, - backgroundcolor=\color{GrayCodeBlock}, - basicstyle=\ttfamily\color{BlackText}, - keywords={ - true,false, - unsafe,async,await,move, - use,pub,crate,super,self,mod, - struct,enum,fn,const,static,let,mut,ref,type,impl,dyn,trait,where,as, - break,continue,if,else,while,for,loop,match,return,yield,in - }, - keywordstyle=\color{PurpleKeyword}, - ndkeywords={ - bool,u8,u16,u32,u64,u128,i8,i16,i32,i64,i128,char,str, - Self,Option,Some,None,Result,Ok,Err,String,Box,Vec,Rc,Arc,Cell,RefCell,HashMap,BTreeMap, - macro_rules - }, - ndkeywordstyle=\color{RedTypename}, - comment=[l][\color{GrayComment}\slshape]{//}, - morecomment=[s][\color{GrayComment}\slshape]{/*}{*/}, - morecomment=[l][\color{GoldDocumentation}\slshape]{///}, - morecomment=[s][\color{GoldDocumentation}\slshape]{/*!}{*/}, - morecomment=[l][\color{GoldDocumentation}\slshape]{//!}, - morecomment=[s][\color{RedTypename}]{\#![}{]}, - morecomment=[s][\color{RedTypename}]{\#[}{]}, - stringstyle=\color{GreenString}, - string=[b]" -} - -\begin{document} -% -\title{Verifying the Rust Standard Library} -%\titlerunning{Verifying the Rust} - -\author{ -Rahul Kumar \and -Celina Val \and -Felipe Monteiro \and -Michael Tautschnig \and -Zyad Hassan \and -Qinheping Hu \and -Adrian Palacios \and -Remi Delmas \and -Jaisurya Nanduri \and -Felix Klock \and -Justus Adam \and -Carolyn Zech \and -Artem Agvanian -} -% -\authorrunning{R. Kumar et al.} - -\institute{Amazon Web Services, USA\\ \url{https://aws.amazon.com/} -} - -\maketitle - -\begin{abstract} -The Rust programming language is growing fast and seeing increased adoption due to performance and speed-of-development benefits. It provides strong compile-time guarantees along with blazing performance and an active community of support. The Rust language has experienced steady growth in the last few years with a total developer size of close to 3M developers. Several large projects such as Servo, TiKV, and the Rust compiler itself are in the millions of lines of code. Although Rust provides strong safety guarantees for \texttt{safe} code, the story with \texttt{unsafe} code is incomplete. In this short paper, we motivate the case for verifying the Rust standard library and how we are approaching this endeavor. We describe our effort to verify the Rust standard library via a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges open to all. - -\keywords{Rust \and standard library \and verification \and formal methods \and safe -\and unsafe \and memory safety \and correctness \and challenge} -\end{abstract} - -\section{Rust} - -Rust~\cite{matsakis2014rust} is a modern programming language designed to enable developers to efficiently create high performance reliable systems. Rust delivers high performance because it does not use a garbage collector. Combined with a powerful type system that enforces ownership of memory wherein memory can be shared or mutable, but never both. This helps avoid data-races and memory errors, thereby reducing the trade-off between high-level safety guarantees and low-level controls -- a highly desired property of programming languages. Unlike C/C++, the Rust language aims to minimize undefined behavior statically by employing a strong type system and an \textit{extensible} ownership model for memory. - -The extensible model of ownership relies on the simple (yet difficult) principle of enforcing that an object can be accessed by multiple aliases/references only for read purposes. To write to an object, there can only be one reference to it at any given time. Such a principle in practice eliminates significant amounts of memory-related errors~\cite{rustAndroid}. In spite of the great benefits in practice, this principle tends to be restrictive for a certain subset of implementations that are too low-level or require very specific types of synchronization. As a result, the Rust language introduced the \texttt{unsafe} keyword. When used, the compiler may not be able to prove the memory safety rules that are enforced on \texttt{safe} code blocks. Alias tracking is not performed for raw pointers which can only be used in \texttt{unsafe} code blocks, which enables developers to perform actions that would be rejected by the compiler in \texttt{safe} code blocks. This is also referred to as \textit{superpowers}~\cite{superPower} of \texttt{unsafe} code blocks. Examples of these superpowers include dereferencing a raw pointer, calling an unsafe function or method, and accessing fields of unions etc. A clear side-effect of this choice is that most if not all memory related errors in the code are due to the \texttt{unsafe} code blocks introduced by the developer. - -Rust developers use \textit{encapsulation} as a common design pattern to mask unsafe code blocks. The safe abstractions allow \texttt{unsafe} code blocks to be limited in number and not leak into all parts of the codebase. The Rust standard library itself has widespread use of \texttt{unsafe} code blocks, with almost 5.5K \texttt{unsafe} functions and 4.8K \texttt{unsafe} code blocks. In the last 3 years, 40 soundness issues have been filed in the Rust standard library along with 17 reported CVEs, even with the extensive testing and usage of the library. The onus of proving the safety and correctness of these \texttt{unsafe} code blocks is on the developers. Some such efforts have been made, but there is still a lot of ground to cover~\cite{jung2017rustbelt}. - -Verifying the Rust standard library is important and rewarding along multiple dimensions such as improving Rust, creating better verification tools, and enabling a safer ecosystem. Given the size and scope of this exercise, we believe doing this in isolation would be expensive and counter-productive. Ergo, we believe that motivating the community and creating a unified crowd-sourced effort is the desirable method, which we hope to catalyze via our proposed effort. - - -\section{Rust Verification Landscape} - -A common misconception Rust developers have is that they are producing \texttt{safe} memory-safe code by simply using Rust as their development language. To counter this, there have been significant efforts to create tools and techniques that enable verification of Rust code. Here we list (alphabetically) some tools: - -\begin{itemize} - - \item \textbf{Creusot}~\cite{denis2022creusot} is a Rust verifier that also employs deductive-style verification for \texttt{safe} Rust code. Creusot also introduces \textbf{Pearlite} - a specification language for specifying function and loop contracts. - - \item \textbf{Gillian-Rust}~\cite{ayoun2024hybrid} is a separation logic based hybrid verification tool for Rust programs with support for \texttt{unsafe} code. Gillian-Rust is also linked to Creusot, but does in certain cases require manual intervention. - - \item \textbf{Kani}~\cite{vanhattum2022verifying} uses bounded model checking to verify generic memory safety properties and user specified assertions. Kani supports both \texttt{unsafe} and \texttt{safe} code, but cannot guarantee unbounded verification in all cases. - - \item \textbf{Prusti}~\cite{astrauskas2022prusti} employs deductive verification to prove functional correctness of \texttt{safe} Rust code. Specifically, it targets certain type of \textit{panics} and allows users to specify properties of interest. - - \item \textbf{Verus}~\cite{verus-sys} is an SMT-based tool used to verify Rust code and can support \texttt{unsafe} in certain situations such as the use of raw pointers and unsafe cells. - - \item There are several other tools which are in the related space, but we do not list them here explicitly. -\end{itemize} - -\section{Verifying the Rust Standard Library} - -We are proposing the creation of a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges. Each challenge describes the goal and the success criteria. Currently, we are focusing on doing verification for memory-safety. The challenges are open to anyone. This effort aims to be \textit{tool agnostic} to facilitate the introduction of verification solutions into the Rust mainline and making verification an integral part of the Rust ecosystem. Towards this, we have been working with the Rust language team to introduce function and loop contracts into the Rust mainline and have created a fork of the Rust standard library repository \url{https://github.com/model-checking/verify-rust-std/} wherein all solutions to challenges and verification artifacts are stored. Challenges can come in various flavors: 1/ specifying contracts for a part of the Rust standard library, 2/ specify and verify a part of the Rust standard library, and 3/ introduce new tools/techniques to verify parts of the Rust standard library. The repository provides templates for introducing new challenges, new tools, and instructions on how to submit solutions to challenges. To date, we have over 20 students, academics, and researchers engaging. - -As part of this effort, we are also creating challenges. For example, we have created a challenge to verify the String library in the standard library~\cite{stringChallenge}. In this challenge, the goal is to verify the memory safety of \texttt{std::string::String} and prove the absence of undefined behavior (UB). Even though the majority of \texttt{String} methods are safe, many of them are safe abstractions over unsafe code. For instance, the insert method is implemented as follows : -\begin{lstlisting}[language=rust, caption=Unsafe usage in String, frame=single, numbers=left] - pub fn insert(&mut self, idx: usize, ch: char) { - assert!(self.is_char_boundary(idx)); - let mut bits = [0; 4]; - let bits = ch.encode_utf8(&mut bits).as_bytes(); - - unsafe { - self.insert_bytes(idx, bits); - } - } -\end{lstlisting} - -The goal also specifies the \textit{success criteria} that must be met for the solution to be reviewed and merged into the CI pipeline. -\begin{lstlisting}[caption=Success criteria for the String challenge.,frame=single] -Verify the memory safety of all public functions that are -safe abstractions over unsafe code: - unbounded: from_utf16le, from_utf16le_lossy, - from_utf16be, from_utf16be_lossy, - remove_matches, insert_str, - split_off, replace_range, retain - others: pop, remove, insert, drain, leak, - into_boxed_str -Ones marked as unbounded must be verified for any -string/slice length. -\end{lstlisting} - -Example of a solution for a challenge can be found in~\cite{solution}. This particular solution introduces new contracts for \texttt{char} and \texttt{ascii\_char}. The contracts are also verified using Kani. - -\noindent \textbf{Our call to action} to you is to come and be a part of this effort and contribute by solving challenges, introducing new challenges, introducing new tools, or helping review and refine the current processes! - -\begin{credits} -\subsubsection{\ackname} We would like to thank all the academic partners that have helped us shape challenges, started contributing to challenges, and provide invaluable advice throughout the process of jump starting this initiative. We also would like to thank Niko Matsakis, Byron Cook, and Kurt Kufeld for their support and leadership. -\end{credits} - -% -% Bibliography -% -\bibliographystyle{splncs04} -\bibliography{paper} - - -\end{document} From 87e445fe5a8c0fa56f7e6b0012e8304450555987 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 17 Aug 2026 19:27:51 -0400 Subject: [PATCH 3/5] Remove unused favicon.ico Added alongside the logo in #1157 but never referenced. The documentation site is built by `scripts/build-docs.sh` and published from `docs/book/`, so a repository-root icon never reaches it; mdBook takes its favicon from `theme/favicon.{png,svg}`, which this repository does not override. It is also absent from the `include` list in `Cargo.toml`, so it is not packaged into the `kani-verifier` crate, and GitHub does not use repository-root icons. --- favicon.ico | Bin 15086 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 favicon.ico diff --git a/favicon.ico b/favicon.ico deleted file mode 100644 index d2bf13219274dbe14bae89c9775360ef69f631d5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 15086 zcmeHO30PG1+Mi*7+4tql*=B~pExmr%c~eB2b4Yt-eUqN+c3F9F@;Hk?0)W=|IW%Vg4dfEDAJ28B`Gs#7*A2u6l0r|9}6o zGa#198#I*3>pB05Baq5y2Vk43tv*Uu_Ihso7~`w_I>=`-{}-_Mv|P{{6I? zmtWEA!beM`oF4pYSnJaLLHrRxr|a4GPvGBQtquuMt3yN37bH`iFAYu2+Uwx5z;Ew2 zNNua-vz1QU8Nq0HXKbBYt78R~>Y4xLnblV~I^}{)ZfjV_>ZG{XV*cc-V0)fGSz?!y zXQScmSUbN>FdB!>dW81sRK;X`cXF^TPhjb!Tt9!2rB0PA3u`r9UUBdT%Xnt(IkdqW z^!+E>xlIDbwOi~bB75qOxx^wpV_ldPY&$2Aaga{@12k%>j0*CT1P0c&Q%Qgy&CzK` z9enm3jizG{lkuGiLHq&1#%(OsYC8|EZ98=>2l>#^!R`6Y&hEUSRJJ54JHTxEXg0?z zzogUsvtM1>GZ+TW;h04N=6*?_lx|O36ASFzHo zS%01GwV6D-L@=8pwxC>~M$`EvJGZ+qh|ew4>3W1epzeL24EjOQPTNVr&Sl=l8pK&G zi9`mK1lunNPTN_$|Gp4=^ar!)y@d)@gMo5+qjnn2i{13P*TZ$1@S!?w|F^W-mtIjQ zo3@bnOUXDT_jOYBLafuhJjBL+^J}o}H1^KOdHAHGsl@H1KdWWhMm%e(ia-39O4Y74 zO?`IJ#(gbVshBGU{hM11`Zs;~+owF1v33mmhw+{R|ycJK#EgZQHr zLHv(G5Pt%9PMM9}af78(j!@>96rHZmVCcY(YEAo>A)mvsj_+chPc#|dn`5OWUnPAp z^xPX7O_#1(ZTCT_PujhvQnd|zILG&ukeH04Qk}NrLa_ZmxGxZXDmZ3-1#OK7|J#IM ztV2EfRopi#?*dSA->AI3pD&~SkvlBCtcaoGF|Jh=uC{GIq3!do_Q`siP4BOk$$~pr z%;QdQ%reOAVV{Gu2d&+GjC)>S4VoJbBPN)QAI`RzKK_YkQ-vVgA@Ft$H{qG^dA$xd z8P81@uXcWiz*uKPMn?;1yA1v0>Gl0HRH~NqXlue*GA5o`S16a)Z|~vf5vg3S@Ao0k zY`R|0{tNmiJk*6}UuDU-3viB(3oJ7SdoaBMd#}XK?YRZ4^1GeeiuVi3u~+9xB!22g zdIM+TXUNIVHbB3_ zs(h>q_6pa=Vvf!s^YZw6y(XTkzb}A%`k~yQ4}b45xR>j7ectAnq>DVeyps32%9!eW z)$JKN@kl_RimU4wq%zKKHjP^d%u@`kQ*1Jg%mjY>IoN&?;~;zJ&lm?;gTr^AyXv$C zuoa$VtY2jl{lT-FE<;|D`f8=J)iV}zWD;~}0nuN7&N%X+?)a=~CT@K|*4V-Cs~~%q^rcpJ?Bd0T z&z~w)tBwr)d9lSDaTHiP*k>X4OMjWXek0(Z(KPktcF3k{PX0K?l3%$lL?3&`RMTD~ z?>)SF%Kid9b_RHGS0Q6vl&#l?Pc)k%mXZ17n3d-qhJB2NA!D4jBLZcPS^_q`=e@?E zh{YnMLh-le=xeCOG;s|}F9Dv}R0tctnDiS=FpZ6zo6ER~&i)1R@e1P>+++_u}MzbQNdssT&FWb z8f(x{6hKj(-lr^a*A_91VzyC=rGO%=N4s7*e*!*F>+NtTC(P%Wk z_~HvGlP6ETJ$m%i^AyFvqgi!1gP2wwI&@fNw+|?Pu4B*q5yJ=X4hw4=fwePKm3r_m zsgw=2TBhc5OtK)CH@?sJA(z){#xZF(80&)b0fFkE2e)?b*Oo0?_G;3kNqOtmt%aPN zgB5S$@|37wzy1s3#*RH3GdV^WJ2qZev0}B5oU}}sH+ODH-#&eaPr&3U`w$A>!H6W_ zJ3*^`^**~*r|mJ0V-^GJEh^IM`^KOxpKIx>k9KX_c8Z92zi`&9S;GE(`-*z>cUD2pZHh>cr?v%gNDtzLc~EVAgtE7X4SQ$KoH^@9j2Q7g+E$SE8#Zk4 zO471rg`Z8ERvsMe6jUmepx5h#+}vDY`}XY>8Q*+U7BObbZWOH*&M_M!XTzq09X@n4 zX}|K4!>9A9o!bd}mdFUA@5-%q?b^M!dE>^C1@q^Z zMMg#nef#zm!o$Obf`S5J-P*NxcJA0wIw?Bp4C>e)(zfff#XKQ_$TY}=yS_8n`ENV8 z?|*aKP~P~Yz>Nc`gbcBy_UFu-kCrW4ya7Iowrtu|lAfMkk&}}n{F0w9?90j$Qj(KO zzsuZNK4$djBdGIGY%iBLY=Hg0h3tR5u79MbA1n1mu3LwC^X~aw03DcJ0vT6Z{q1Si zMU_fL)A+c!^M?-|D#1Dwrz9trB_}17txQiZIk10!(WVU>?sV`_`)m z89dBnibybhDK>_@M;jC_0prQ*`w3;iCOnS*2ejBvcF^KKzi=>8x(o`suW<^@BV=9mF52Ah?n6 z5ybBkcrIO_sL9#brFzmo`2W3T{;#`qrPUf$s8+Xoz83uYDxwYz4V@Sl8~fAhRjZ0N zZQM|jv~=mML2tg9gEMjE`t|F=(xpo;JpJ_315nvDr|?yEgY64@$%8M*ejvYL@59dl zf5f*a>#~JuYUWY555co%yeYA(kHIEQhc9E?7rvOQ03^s<30nj>7KUyA!$1)712gn(d{V*h9N-tJTlC<`Z~h8uT)-7a5;7 z@9r@Zzm(HUIv?`H!`lt; za}K_s5#vZF@ToN8nKgO$@1YymZ^z1v#zC9mXFAL=srd>;Eqm0PPd-sC-ERy-#K91k9#<2zj7!-k0n_Z!3(#)WLYa;xrm+qD2WFGS&FL&Mo_E{`fG=8ea#wtGq z1Zs_tO_L#$E&!{-m%6XqZ2BNwCU=mOiYIzWW$e?y0@*fp<1M!gukyVU9~{ADuvs?1 zC(;QWOY6|N1ah^ZUe|Z9**N|SgMRo|3PqzoLiYG;G%tj~=dqN?IuhTobKe$l%-5&! zE}6uP{3MTrTk0^>CsNekKR`_@l#QD~MmLAO%c50ZnC^*m_TSWq;JQSj`)DC~gZI^G zOT5NT67+&lL16MTC+lbBGZ235igJ2$}5&wF`o*l170>;W?Agp9CQfG!xT7 zXda=`N(z*9GZN3>t2l&ogdu=NgI5&8RYi$Vao`TceK$|5R@Nvg{Fhu(nNtG25TsN- z?XtW7Y_{O*vLnWyV=+&vQ(XOV`PAzMHZkajwUa9v(l++nQ}9{FKW>{Ci$SmdR||#W ze;%6SKwA=HcxK~CxjZ-+c`DoCUra;)cl`&C!V68!m;l{(5;_OF_raIhIJOIHk((yt zm>x8hu$-~ZJs_3RF1zr-HGO}T%FH^%qW8mJy&3U7l}g=)!93tp`Mwm&zneK`#bL@k zc@F%OGi~g;GK1lbxBVpIN3oSfdVTL_ZS4A+&|L$8@1KPpI|?k|3#)k;@`J6GhPl58 z|M4uuD{jGeeT!!{@4Z zG~`$8xC#7H%roh?kcaWQ_c&|%tyXtnfa$jdyJ8=;?YBBFu*tZ+cL;W-Ei)rP-wc!* zYTWl;yvShV%y7pi9<}c(Ua;SCf#-s}+OP2^@=`b}HEkYZCB^sq4y)SqZA1I|?%osF z193HW>iz(G`<+mnkNw!A=O|0e9LS(EWIt8yGhgl3=3N1DVRq!HHEn8&(TKE~m(cf` ziyZxRhCx5D1y~ZpSJn{g5MyV*`w{s}s4EeK#p0x1-dqcjJw)5??*}f`p>uH*aoF%p0BBaP_w16yKkk8$*htqMg` zlJDiZ5Ibd|?@n7S)5mz;`Jzuf)yUboQ|H~$(TSJ)_8t6pQl?Ft=1qF{?z^^2mytyu zefYu2!Grt9aGbG5T?HS1cgUdYTJ0-$QI=vvkk0~rqO(}b4#E41w=5rolyEWz6^_MNC2``a8 z;Dc9MEtAt6{7&rAEw`bkr)xA_edY#W{IW@tCjBceE-u_`HV1a?+9ho9qD8lQA$CJi zl(2B&0wHtfPGQ!UUmlXn8(+@L`N9`TCK&voqB!AemM?2ovttgPSC(o(k8s~7$e<`aHf zA|E_+d_%A?TlWB$84=r_gz-YQdGri?S#-)to>`S=HjN)xt*_cX296v#^37elzP&j1 zqg7==9Er1g`gY4I#FNiK$2yTqVFNGw+~46t=1-LXcLHB^Lypz+#6R-LSDQA&COqG9 zp$iM#+y8ZvJCPv?aOaDfO=Ek)w{@H7J3L1^W)MBIt1BU0fz(gxsy~ zqmJv9#NXc^xmisurpW_fgY^ywls}SR8Zz!F=~Fa3@5_Ee{b+mrI2&DA9qtx8+#TB7 zJW<2kVoBjog;UCM3ngV!1WB31eP0j@(a~a|7c}J@W9TTdDYGao(B& zvowQ!$in8ADV6P|(8IluGx8Pkx~Ec>X=Iu_ml$u17lHAKPV(^J z!I0$4{tO=0d<~r9nq%k!9p+;OY;qSqh5y;eGt0Zzcdprr`0=hF{@{^%j(=Zwa5=Cy z_br00{1(PO1pQ5c4_`}JCbh)8Eyn*R-HjQ9hPJVf8Wpj5)Tr@od-occ{MK7zevSP! zeu`SHa;+DcH~1c6D9cpX%^T)HZz6wq=NG`0E`L7`ID~LC1RAn<9`OcWv}R;J$mR7drm_>L;j+L3lAqG z#6L@!m;Ntg;TFW6enI&@$UFU!%oEWMz`1dxeeWy0e}DaZ@4nkOHulpFX=$lRq3tt| z2iwScT!F6rCWfQe3<|bgD6+GAlkk5QK}uDt8f8(N))RU+ZJbp`))@P$05(Z)V0M{} z&HNO$$TsX}hj-uJzmZqTF;pt%>J)NBk0WNgwh#Vi#U+CbhM_X-^`{Znw0YO@{%tf2 zHM8`JaM%h1a8B>qBE+{@g!^(Ce6A(%g96>&B>qvH;6tF>v8p>z+D>lFzBW%JT6_!l K1>zGGiT)3E5~aZa From 5af61b1f5eca12941390d08b3b21927d51d0691f Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 17 Aug 2026 19:37:55 -0400 Subject: [PATCH 4/5] Remove orphaned bundle-test Dockerfiles These were built by the `TestAlternativePlatforms` job of `release.yml`, which was removed in #3744 when Ubuntu 18.04 and AL2 support was dropped. That PR deleted only the 18.04 Dockerfile and left the other six behind, so nothing in the repository has referenced them since November 2024. They are also stale: two still install `kani-verifier` from crates.io rather than the bundle under test, and the NixOS one carries a workaround for #1246. Installing a release bundle is now covered natively by the `TestBundle` job across the macOS and Ubuntu runners, without Docker. Only `Dockerfile.bundle-release-24-04` remains, which builds the image published to GHCR on release. --- scripts/ci/Dockerfile.bundle-test-al2 | 19 --------- scripts/ci/Dockerfile.bundle-test-nixos | 41 ------------------- .../ci/Dockerfile.bundle-test-ubuntu-20-04 | 20 --------- .../Dockerfile.bundle-test-ubuntu-20-04-alt | 22 ---------- .../ci/Dockerfile.bundle-test-ubuntu-22-04 | 20 --------- .../ci/Dockerfile.bundle-test-ubuntu-24-04 | 20 --------- 6 files changed, 142 deletions(-) delete mode 100644 scripts/ci/Dockerfile.bundle-test-al2 delete mode 100644 scripts/ci/Dockerfile.bundle-test-nixos delete mode 100644 scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 delete mode 100644 scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt delete mode 100644 scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 delete mode 100644 scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 diff --git a/scripts/ci/Dockerfile.bundle-test-al2 b/scripts/ci/Dockerfile.bundle-test-al2 deleted file mode 100644 index 4e18f2165e90..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-al2 +++ /dev/null @@ -1,19 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM amazonlinux:2 -RUN yum install -y gcc curl tar gzip && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -#RUN cargo install --path ./kani-verifier -#RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz -RUN cargo install kani-verifier -RUN cargo-kani setup diff --git a/scripts/ci/Dockerfile.bundle-test-nixos b/scripts/ci/Dockerfile.bundle-test-nixos deleted file mode 100644 index 2bbeb8ceee18..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-nixos +++ /dev/null @@ -1,41 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM nixos/nix -RUN nix-channel --update -WORKDIR /tmp/kani -RUN echo $' \n\ -with import {}; \n\ -mkShell { \n\ - packages = [ \n\ - curl \n\ - gcc \n\ - patchelf \n\ - rustup \n\ - ]; \n\ -}' >> ./default.nix -# we need to switch to nix-shell to get proper support for e.g. pip -SHELL ["nix-shell", "--command"] -ENTRYPOINT ["nix-shell"] -RUN rustup toolchain add stable -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz - -# Temporary hack: nix-shell causes problems when trying to run these with 'docker run' -# like we do for other tests, so we've imported these into the dockerfile for now -# until everything can be replaced with 'self-test': -# https://github.com/model-checking/kani/issues/1246 -RUN cargo kani --version -RUN (cd /tmp/kani/tests/cargo-kani/simple-lib && cargo kani) -RUN (cd /tmp/kani/tests/cargo-kani/simple-visualize && cargo kani) -RUN (cd /tmp/kani/tests/cargo-kani/build-rs-works && cargo kani) -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 deleted file mode 100644 index f81af91f6f52..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:20.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-*.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt deleted file mode 100644 index 35bc522b651f..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt +++ /dev/null @@ -1,22 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle -# using an alternative install path * - -FROM ubuntu:20.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true \ - KANI_HOME="/tmp" -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-*.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 deleted file mode 100644 index f7dd23e1233d..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:22.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 deleted file mode 100644 index 1b85fd2e0b58..000000000000 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 +++ /dev/null @@ -1,20 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Note: this file is intended only for testing the kani release bundle - -FROM ubuntu:24.04 -ENV DEBIAN_FRONTEND=noninteractive \ - DEBCONF_NONINTERACTIVE_SEEN=true -RUN apt-get update && \ - apt-get install -y curl build-essential && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y -ENV PATH="/root/.cargo/bin:${PATH}" - -WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ -# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier -RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz From c44dc15a377cf30912c5230092d349ae2602cde7 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 17 Aug 2026 19:38:30 -0400 Subject: [PATCH 5/5] Document the CI helpers in scripts/ci Add a README explaining what `Dockerfile.bundle-release-24-04` is for: it builds the `ghcr.io/model-checking/kani-ubuntu-24.04` image published by the `Package Docker` job on release tags. Because it installs Kani from the release bundle and the packaged `kani-verifier` crate, it cannot be built from a clean checkout, so record the two artifacts it expects in the build context and the commands that produce them. Also note that the root `.dockerignore` exists for this build, that bundle installation is tested natively by `TestBundle` rather than through Docker, and that `run-copyright-check.sh` depends on GNU `xargs`. --- scripts/ci/README.md | 45 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 scripts/ci/README.md diff --git a/scripts/ci/README.md b/scripts/ci/README.md new file mode 100644 index 000000000000..0bbc92c36fd4 --- /dev/null +++ b/scripts/ci/README.md @@ -0,0 +1,45 @@ +# CI helpers + +Helper scripts and container definitions used by the GitHub Actions workflows in +[`.github/workflows/`](../../.github/workflows). Nothing here is part of a normal +local build. + +## `Dockerfile.bundle-release-24-04` + +Builds the container image published for each Kani release, +`ghcr.io/model-checking/kani-ubuntu-24.04:` (also tagged `latest`). + +It is used by the `Package Docker` job in +[`release.yml`](../../.github/workflows/release.yml), which runs only on pushes of a +`kani-*` tag. That job produces the release artifacts first, then builds this image +with the repository root as the build context — so the root +[`.dockerignore`](../../.dockerignore) is what keeps `.git`, `firecracker/`, and +`target/{debug,release}` out of the uploaded context — and pushes the result to GHCR. + +Because it installs Kani *from those artifacts* rather than from source, it cannot be +built from a clean checkout. Two things must already exist in the build context: + +| Path in the build context | Produced by | +|---------------------------|-------------| +| `kani--x86_64-unknown-linux-gnu.tar.gz` | `cargo bundle` | +| `target/package/kani-verifier-/` | `cargo package -p kani-verifier` | + +To reproduce the release image locally: + +```bash +cargo bundle +cargo package -p kani-verifier +docker build -t kani-ubuntu-24.04 -f scripts/ci/Dockerfile.bundle-release-24-04 . +``` + +Note that installing a release bundle is *not* tested through Docker. The `TestBundle` +job in `release.yml` does that natively across the macOS and Ubuntu runners it supports. + +## Copyright check + +`run-copyright-check.sh` runs `copyright_check.py` over every tracked file that does not +match a pattern in `copyright-exclude`, requiring the two-line header described in +[`docs/src/conventions.md`](../../docs/src/conventions.md). It runs in the +`format-check` workflow. + +The script uses `xargs -d`, which is GNU-only, so it does not run as-is on macOS.