Anodized – catch Rust runtime bugs at compile time
20 hours ago
- #specification
- #verification
- #Rust
- Anodized is a system for enforcing complex specifications in Rust without altering the language or toolchain, working on stable Rust.
- It uses the #[spec] attribute to define preconditions (requires), postconditions (ensures), and invariants (maintains) as standard Rust boolean expressions.
- Annotations are parsed and validated on every build, with runtime checks out of the box, and future support for fuzzing and static analysis planned.
- Anodized aims to improve interoperability across Rust verification tools by serving as a common layer, avoiding duplication of specification efforts.
- It supports multiple runtime behaviors like check-and-panic, check-and-print, and no-check, configurable via Cargo.toml features and #[cfg] attributes.
- Specifications can capture entry-time values (captures) and bind return values (binds), including destructuring for complex postconditions.
- Anodized differentiates from similar tools by focusing on ergonomics and a unified attribute, with a vision for ecosystem-wide integration.