Convert a Rust target into minimally modified Verus-compatible code using an explicit verification command. Use when migrating a specific file and iterating until the verification command succeeds.
Standardmäßig ist der Prompt ausgewählt, der zuerst die Quelle prüft. Sie können zu einem direkten Befehl wechseln oder eine lokale Kopie herunterladen.
Quelldateien prüfen
Lesen Sie SKILL.md und alle von SkillsMP angezeigten Begleitdateien, bevor Sie sich für eine Installation entscheiden.
Mit Codex oder Claude installieren Kopieren Sie diesen Prompt, fügen Sie ihn in Codex, Claude oder einen anderen Assistant ein und lassen Sie die Skill-Seite prüfen und installieren.
Ein direkter Befehl überspringt den Prüf-Prompt. Prüfen Sie die Quelle, bevor Sie ihn ausführen.
Convert a Rust target into minimally modified Verus-compatible code using an explicit verification command. Use when migrating a specific file and iterating until the verification command succeeds.
license
MIT
compatibility
Requires Codex CLI and a working Verus verification command.
metadata
{"author":"kverus","version":"1.0"}
Convert Rust code into minimally modified Verus-compatible code for one explicit target file and verification command.
If either target or verify is missing, ask for the missing value and stop.
Shared Verus References
If migration requires Verus syntax, modes, ghost/tracked values, atomic ghost code, loop invariants, or tokenized state-machine rules, read the relevant reference under ../kverus-common/references/ before editing.
Objective
Convert the Rust code in target into Verus-compatible code with the smallest possible set of edits such that:
the code is syntactically accepted by Verus
the verification command succeeds
the original source structure is preserved as much as possible
the result is suitable as a future proof-ready baseline, even if it is not fully proved now
The goal is not to fully verify semantic correctness. The goal is only to make the code pass at the syntax, compatibility, and front-end acceptance level.
Required Workflow
Before making large edits:
inspect the target code and its immediate dependencies
make a short plan
edit incrementally
run the verification command after meaningful changes
use the error messages to guide the next minimal repair step
Avoid broad rewrites up front.
Hard Constraints
A. In-place edits only
Edit the code at the original location whenever possible.
Do not comment out an entire function, impl, or module and rewrite a replacement elsewhere if a local replacement is sufficient.
B. Preserve original Rust code locally
For each modified or unsupported construct, preserve the original Rust code as a nearby comment at the same location whenever feasible.
// let lock = self.lock.fetch_add(READER, Acquire);letlock = ...
C. No fake placeholders
Do not introduce any new:
unimplemented!()
panic!()
loop {}
D. Minimality
Only change code that is necessary for:
the requested target
its minimal dependency closure
Do not refactor unrelated code.
E. Preserve structure
Preserve as much as possible:
item order
function order
impl and block structure
source locality
nearby comments
Avoid large structural rewrites.
Transformation Rules
Rule 1: Attribute-first executable verification
Prefer #[verus_spec] for executable functions and supported annotations on
their loops, preserving native Rust signatures and bodies. Use verus! for
spec/proof declarations, external specifications, and constructs unsupported by
the active attribute syntax.
Keep use statements outside verus! unless required by syntax.
Rule 2: #[verifier::external_body]
Add #[verifier::external_body] to functions whose bodies should be skipped during proof checking.
Use this as the default strategy unless it prevents syntactic acceptance.
Rule 3: Unsupported Rust features
If Verus does not support a Rust feature or syntax fragment:
keep the original code as a nearby comment when feasible
rewrite only the unsupported fragment
keep the rewritten code at the same location
Rule 4: Compile-failed Rust
If the original Rust code does not compile, still convert it into the closest Verus-compatible form using minimal edits.
Rule 5: Dependencies
If the target relies on other code, minimally adapt only the necessary dependencies.
If a required dependency is commented out, uncomment only the minimum necessary portion.
Do not expand edits beyond the smallest dependency closure needed to pass the verification command.
Edit Priority Policy
When multiple repair strategies exist, prefer them in the following order:
local syntax-preserving edits
adding #[verifier::external_body]
rewriting unsupported expressions or type fragments
minimally adapting direct dependencies
broader edits only as a last resort
Validation Loop
Use this workflow:
inspect code
make a short plan
apply minimal edits
run verify
inspect errors
apply the smallest necessary repair
repeat until success or a real blocker remains
Failure Policy
If the verification command cannot succeed without violating the constraints:
stop at the smallest blocking point
do not fabricate behavior
do not introduce placeholders
report the blocking location precisely
Output Expectations
Perform the edits in the workspace when allowed.
Return the modified code with local commented preservation of original Rust constructs near modified locations whenever feasible, including any necessary minimal dependency edits.
Do not add long explanations unless the user asks for them.
Domain-Specific Guidance
Atomic operations
For operations such as:
fetch_add
fetch_sub
compare_exchange
prefer atomic_with_ghost! when required by Verus compatibility.
