# Verus attributes for executable code The `#[verus_spec]` attribute macro can help add Verus specifications and proofs to existing executable code without sacrificing readability. ## When to use `#[verus_spec]` instead of the `verus!` macro The default way to write Verus code is by using the `verus!` macro. However, using `verus!` to embed specifications and proofs directly in executable code may not always be ideal for production settings. This is particularly true when developers want to integrate verification into an existing Rust project and aim to: 1. Minimize changes to executable code — avoid modifying function APIs to include tracked or ghost arguments, and preserve native Rust syntax for maintainability. 2. Adopt verification incrementally — apply Verus gradually to a large, existing codebase without requiring a full rewrite of the function APIs. 3. Maintain readability — ensure the verified code remains clean and understandable for developers who are not familiar with Verus or want to ignore verification-related annotations. 4. Optimize dependency management — use Verus components (`verus_builtin`, `verus_builtin_macros`, and `vstd`) in a modular way, allowing projects to define custom stub macros and control Verus dependencies via feature flags. ## Adding specifications to a function Use `#[verus_spec(requires ... ensures ...)]` to attach a specification to a function signature. Here is an example: ```rust {{#include ../../../../examples/guide/exec_attr.rs:verus_spec}} ``` ## Adding verification hints Use `#[verus_verify(...)]` to provide hints to the verifier to mark a function as `external`, `external_body`, `spinoff_prover`, or specify a different resource limit via `rlimit(amount)`. In addition, you can create a dual mode (spec + exec) function via the [`verus_verify(dual_spec)`](exec_to_spec.md) attribute, which will attempt to generate a spec function from an executable function. ## Adding proofs inside functions When a function has the `#[verus_spec(...)]` att…