Skip to content

fix: target Kani proofs to wsc package with bounded unwind#65

Merged
avrabe merged 2 commits intomainfrom
fix/kani-targeted-proofs
Mar 21, 2026
Merged

fix: target Kani proofs to wsc package with bounded unwind#65
avrabe merged 2 commits intomainfrom
fix/kani-targeted-proofs

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Mar 21, 2026

Summary

cargo kani --tests was running against the full workspace and timing out. Fix:

  • Target just wsc library: cargo kani -p wsc
  • Add --default-unwind 4 for bounded model checking
  • Add --output-format terse for cleaner logs
  • Add timeout-minutes: 30 safety limit

Test plan

  • Kani BMC job completes within 30 minutes
  • All 19 proof harnesses pass

🤖 Generated with Claude Code

avrabe and others added 2 commits March 21, 2026 16:13
cargo kani --tests on the full workspace was timing out. Target
just the wsc library with --default-unwind 4 and 30-min timeout.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
340 artifacts across 23 types. Provides agent context for
artifact types, commands, and traceability rules.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@avrabe avrabe merged commit 423e011 into main Mar 21, 2026
11 checks passed
@avrabe avrabe deleted the fix/kani-targeted-proofs branch March 21, 2026 15:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant