AegisVerity Labs

### Inspiration & Problem Unsafe Rust can look completely safe under standard compilation with zero warnings, yet remain deeply unsound under runtime memory semantics. Traditional LLMs act purely on syntax heuristics, yielding high false-alarm rates (75.0% noise on safe code) and producing 0% verified operational proofs. We built WARRANT based on a strict paradigm: "The Model Proposes. The Compiler Decides." ### What WARRANT Does WARRANT turns text hypotheses from Meta's muse-spark-1.3 model into Miri-Verified Operational Proofs and synthesizes verified remediation patches for CI gates. - Focus: Memory safety compliance covering Rule 1 (Out-of-bounds pointer arithmetic & buffer access) and Rule 2 (Concurrency data races across scoped threads). - Verifier Core: Deterministic execution under pinned toolchain nightly-2026-10-20 and miri 0.1.0. - Autonomous Repair Loop: Bounded up to 4 rounds with verbatim compiler diagnostics fed back to the model. - 4-Layer Patch Verification: Every patch must pass AST signature & anti-bypass validation, exact proof harness execution under Miri, native cargo tests, and sanity_* invariant tests under Miri. ### Rigorous Empirical Results (Frozen Benchmark Corpus of 38 Targets) - Verifier Core Determinism (3 Runs): 22/22 (100.0%) bug targets proven (PROVEN_PUBLIC), 0/16 (0.0%) false proofs on safe controls. - Autonomous Model Performance (muse-spark-1.3 live API): 79.54% valid@1 lifting to 100.0% valid@4 across bug targets (+20.46% autonomous repair lift). 0/16 false proofs on live safe controls. - Patch Verification: 17/17 (100.0%) PATCH_VERIFIED. - Strict Honesty: Safe control candidates that do not trigger Undefined Behavior under Miri (such as c-0003) are strictly held back as UNPROVEN and never reported as bugs (Hard Rule 1). ### Built With Rust, Cargo-Miri, syn AST parser, Meta Model API (muse-spark-1.3), Remotion (video animation). Dual licensed under MIT / Apache-2.0.