Skip to content

D16: formal verification spike (Kani)#167

Open
DammyAji wants to merge 1 commit into
Dgetsylver:mainfrom
DammyAji:d16-formal-verification-spike
Open

D16: formal verification spike (Kani)#167
DammyAji wants to merge 1 commit into
Dgetsylver:mainfrom
DammyAji:d16-formal-verification-spike

Conversation

@DammyAji
Copy link
Copy Markdown

  • Add kani-verify/ standalone crate with 6 proof harnesses for D9 invariants
  • Document I1 (geometric series) as blocked with rationale
  • Add CI job (.github/workflows/kani.yml) triggered on leverage.rs changes
  • Add HTML report at kani-verify/report/index.html

Closes #57

Summary

Related Issue

Closes #

Checks

  • I read the contribution guide.
  • I kept this pull request scoped to the linked issue.
  • I ran the relevant local checks or explained why they were skipped.
  • For Drips wave issues, I claimed the issue before opening this pull request.

Notes for Reviewers

- Add kani-verify/ standalone crate with 6 proof harnesses for D9 invariants
- Document I1 (geometric series) as blocked with rationale
- Add CI job (.github/workflows/kani.yml) triggered on leverage.rs changes
- Add HTML report at kani-verify/report/index.html

Closes Dgetsylver#57
@drips-wave
Copy link
Copy Markdown

drips-wave Bot commented May 29, 2026

@DammyAji Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits

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.

D16: Formal verification spike (kani / prusti)

1 participant