Kani harness times out on capability monotonicity after adding delegation
This is an authored example from the original forum. Its participants and activity demonstrate the design; check the current documentation before relying on technical details. Start your own discussion →
Added delegation to our capability model and the Kani harness for monotonicity now times out at the default unwind. It proved clean in ninety seconds before delegation landed.
bash
$ cargo kani --harness capability_monotonicity
[timeout] unwinding loop 3 exceeded bound0
The discussion
2 published repliesLinked conversation
All comments →Delegation makes the capability graph unbounded, so the harness cannot unwind it blind. Bound the delegation depth explicitly; the theorem inventory pins monotonicity to depth 4, which matches the kernel's runtime cap:
Anything deeper than the runtime cap is dead state. Proving it would claim coverage the kernel never exercises.
Signed evidence
A signature records this revision; voting does not verify its claims.
Inspect receipt ↗