Kani verification for build_adjacency with tests and tooling#186

Merged

leynos merged 21 commits intomainfrom

kani-verify-build-adjacency-w7ihby

Apr 13, 2026

Commits on Apr 12, 2026

docs(execplans): add execution plan for Kani verification of build_adjacency

leynos
and
devboxerhub[bot]
committed
feat(decomposition_advice): add Kani verification and test coverage for build_adjacency

leynos
and
devboxerhub[bot]
committed
fix(tests): correct crate name in decomposition_adjacency_behaviour

leynos
and
claude
committed
style(tests): fix import ordering in decomposition_adjacency_behaviour

leynos
and
claude
committed
fix(kani): address code review feedback

leynos
and
claude
committed
refactor(kani): extract symbolic setup into shared helper

leynos
and
claude
committed
refactor: address inline code review comments

leynos
and
claude
committed
docs(kani): correct run-kani.sh default behavior description

leynos
and
claude
committed
docs(kani): add bounded model checking section to developers guide

leynos
and
claude
committed
style: add comma before coordinating conjunction 'so'

leynos
and
claude
committed
style(docs): conform developers guide to style rules

leynos
and
claude
committed
docs(kani): address PR review findings

leynos
and
claude
committed
feat(decomposition_advice): add Kani harness to exclude spurious edges

leynos
and
devboxerhub[bot]
committed
docs: align Kani execplan with shipped bounds
leynos
committed
refactor(community_kani,scripts): use constructor for SimilarityEdge and improve shell script robustness

leynos
and
devboxerhub[bot]
committed
style(decomposition_advice): use assert_eq! instead of assert! for adjacency length check

leynos
and
devboxerhub[bot]
committed
chore(build,kani,test_support): improve kani install script and enhance test safety checks

leynos
and
devboxerhub[bot]
committed
feat(test_support/decomposition_adjacency): add structured validation errors to adjacency_report

leynos
and
devboxerhub[bot]
committed
docs(test_support/decomposition): update docs and examples for adjacency_report error handling

leynos
and
devboxerhub[bot]
committed
refactor(decomposition_advice): use helper functions in adjacency verification proof

leynos
and
devboxerhub[bot]
committed
docs(developers-guide,scripts): add usage instructions for Kani install and run scripts

leynos
and
devboxerhub[bot]
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Kani verification for build_adjacency with tests and tooling#186

Kani verification for build_adjacency with tests and tooling#186
leynos merged 21 commits intomainfrom
kani-verify-build-adjacency-w7ihby

Commits on Apr 12, 2026

docs(execplans): add execution plan for Kani verification of build_adjacency

feat(decomposition_advice): add Kani verification and test coverage for build_adjacency

fix(tests): correct crate name in decomposition_adjacency_behaviour

style(tests): fix import ordering in decomposition_adjacency_behaviour

fix(kani): address code review feedback

refactor(kani): extract symbolic setup into shared helper

refactor: address inline code review comments

docs(kani): correct run-kani.sh default behavior description

docs(kani): add bounded model checking section to developers guide

style: add comma before coordinating conjunction 'so'

style(docs): conform developers guide to style rules

docs(kani): address PR review findings

feat(decomposition_advice): add Kani harness to exclude spurious edges

docs: align Kani execplan with shipped bounds

refactor(community_kani,scripts): use constructor for SimilarityEdge and improve shell script robustness

style(decomposition_advice): use assert_eq! instead of assert! for adjacency length check

chore(build,kani,test_support): improve kani install script and enhance test safety checks

feat(test_support/decomposition_adjacency): add structured validation errors to adjacency_report

docs(test_support/decomposition): update docs and examples for adjacency_report error handling

refactor(decomposition_advice): use helper functions in adjacency verification proof

docs(developers-guide,scripts): add usage instructions for Kani install and run scripts