feat(stealth-registry): add Kani formal verification for top 3 invariants (#108) - #146

Merged

truthixify merged 19 commits into

wraith-protocol:developfrom

Michvista:feat/kani-stealth-registry-invariants

Aug 4, 2026

Commits on Jul 26, 2026

feat(stealth-registry): add Kani formal verification for top 3 invariants (#108)
Michvista
committed
299e6a1

Commits on Jul 30, 2026

fix(stealth-registry): make kani mock no_std-compatible
Michvista
committed
f023526

Commits on Aug 4, 2026

fix(stealth-registry): resolve kani std + fmt CI failures
Michvista
committed
0385079
fix(stealth-registry): gate DataKey behind cfg(not(kani)) to fix type conflict
Michvista
committed
3dc5c36
fix(stealth-registry): add missing kani imports and apply canonical rustfmt
Michvista
committed
0a1a93c
fix(stealth-registry): gate Cargo.toml dependencies under cfg(not(kani))
Michvista
committed
f578ae6
fix(stealth-registry): add extern crate std under cfg(kani) and restore Cargo.toml
Michvista
committed
33cd8ac
fix(stealth-registry): optimize kani symbolic execution and match exact rustfmt layout
Michvista
committed
018314e
fix(stealth-registry): add extern crate declarations inside mock_sdk.rs under cfg(kani)
Michvista
committed
9c37da6
fix(stealth-registry): format remove_keys parameter list across multiple lines
Michvista
committed
f7b5b75
fix(ci): normalize all stellar workspace files to LF line endings
Michvista
committed
761cd84
fix(ci): re-index entire stellar/ tree with LF endings via .gitattributes
Michvista
committed
e1217d8
fix(stealth-registry): gate soroban-sdk and wraith-metrics under cfg(not(kani)) in Cargo.toml
Michvista
committed
57a19fe
revert: undo mass CRLF normalization - only keep stealth-registry changes
Michvista
committed
2e284d1
fix(stealth-registry): apply exact rustfmt layout and fix Kani type annotation
Michvista
committed
9c64244
fix(stealth-registry): suppress unused_imports warning for kani mock_sdk use block
Michvista
committed
4fbda59
perf(stealth-registry): eliminate dynamic symbolic loops in kani proofs to prevent timeout explosion
Michvista
committed
5d3266e
fix(stealth-registry): tighten kani proofs and mock arithmetic
Michvista
committed
5020874
fix(stealth-registry): remove kani unwind from register proof
Michvista
committed
72669a6