hodd-rust

What problem does it solve?

This skill provides a rigorous, multi-layered validation framework for Rust projects, especially those involving unsafe code, concurrency, or critical safety requirements. It integrates type-driven, spec-first, proof-driven, and design-by-contract paradigms to eliminate bugs and ensure correctness at compile-time and runtime.

Core Features & Use Cases

• Multi-Paradigm Validation: Combines Rust's type system, Flux refined types, Quint specifications, Kani model checking, Lean 4 proofs, and contracts crate for comprehensive verification.
• Unsafe Code & Concurrency Validation: Utilizes Miri for runtime Undefined Behavior (UB) detection and Loom for exhaustive concurrency testing.
• Strict Validation-First Workflow: Enforces planning and verification before and during implementation, reducing costly post-development debugging.
• Use Case: Develop a high-performance, lock-free data structure in Rust. This skill ensures its memory safety, thread safety, and algorithmic correctness through a combination of formal methods and specialized testing tools.

Quick Start

Use the hodd-rust skill to develop a concurrent counter system in Rust, ensuring it is free of data races and deadlocks. The agent will guide you through the validation-first Rust development workflow.