skills.rest
OutlineDriven
OutlineDrivenOFFICIAL
Explore all skills by this author →
GitHub

hodd-rust

Validates Rust code with formal methods and specialized testing tools.

34|Updated Nov 17, 2025
Search Tags:#type safety#concurrency#formal verification#Rust#Kani#Miri#Loom#unsafe code
One-click install
npx skills add https://github.com/OutlineDriven/odin-claude-plugin --skill hodd-rust
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: hodd-rust
Source: https://github.com/OutlineDriven/odin-claude-plugin/tree/main/skills/hodd-rust
Command: npx skills add https://github.com/OutlineDriven/odin-claude-plugin --skill hodd-rust

SYSTEM DOCUMENTATION & REQUIREMENTS

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.