Repository navigation
ci: add Kani formal verification to CI and Copilot setup - #640
Conversation
- Add Kani proof verification job to CI using the official model-checking/kani-github-action@v1 (handles CBMC + toolchain) - Add Kani installation to copilot-setup-steps.yml so agents can run proofs when working on logfwd-core - Add `just kani` recipe for local verification - Document in CONTRIBUTING.md Runs against logfwd-core only (the proven #![no_std] crate with 52+ Kani proofs). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
WalkthroughAdded Kani formal verification tooling and CI steps. A new Possibly related PRs
Comment |
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In @.github/workflows/ci.yml:
- Around line 147-158: The Kani job configuration uses the mutable reference
model-checking/kani-github-action@v1 and lacks a timeout; replace the mutable
tag with the repository's current commit SHA for v1 (i.e., pin
model-checking/kani-github-action@<full-commit-sha>) and add a timeout-minutes
field to the kani job (e.g., timeout-minutes: 30) so the "kani" job and the
"uses" entry reference the pinned SHA and the job will be bounded.
In @.github/workflows/copilot-setup-steps.yml:
- Around line 27-30: Pin the Kani verifier install in the GitHub Actions step
named "Install Kani verifier" by changing the cargo install invocation
(currently "cargo install --locked kani-verifier") to specify the known-good
version (use --version 0.67.0) so the action installs kani-verifier@0.67.0
reproducibly; keep the subsequent "cargo kani setup" step as-is.
In `@CONTRIBUTING.md`:
- Line 77: Update the CONTRIBUTING.md line for the "just kani" entry to add a
prerequisite note that Kani must be installed and configured (or link to the
repository's Kani setup/installation section) before running the command;
specifically update the "just kani" bullet so it reads something like "just kani
— Run Kani formal verification proofs (requires Kani installed/configured; see
[Kani setup])" or add a parenthetical pointing to the setup section.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 7fc16e38-1130-46ab-bae4-8ebb54f520b0
📒 Files selected for processing (4)
.github/workflows/ci.yml.github/workflows/copilot-setup-steps.ymlCONTRIBUTING.mdjustfile
| kani: | ||
| name: Kani proofs | ||
| if: github.event_name == 'push' || github.event.pull_request.draft == false | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
|
|
||
| - name: Run Kani verification | ||
| uses: model-checking/kani-github-action@v1 | ||
| with: | ||
| args: -p logfwd-core | ||
|
|
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Resolve the current v1 tag commit so you can pin it explicitly.
git ls-remote https://github.com/model-checking/kani-github-action refs/tags/v1Repository: strawgate/memagent
Length of output: 44
🏁 Script executed:
# Check if the workflow file exists and view the relevant lines
if [ -f ".github/workflows/ci.yml" ]; then
echo "=== Lines 147-158 of .github/workflows/ci.yml ==="
sed -n '147,158p' ".github/workflows/ci.yml"
else
echo ".github/workflows/ci.yml not found"
fiRepository: strawgate/memagent
Length of output: 427
🌐 Web query:
kani-github-action v1 release commit SHA model-checking
💡 Result:
The kani-github-action is the official GitHub Action for running the Kani Rust Verifier (a model checker for Rust) in CI pipelines. It is hosted at https://github.com/model-checking/kani-github-action. v1 appears to refer to the default branch (named "v1"), which is used in documentation examples like "uses: model-checking/kani-github-action@v1". When referenced without a specific tag (e.g., @v1), GitHub Actions uses the commit SHA of the default branch at the time of workflow execution. No explicit "v1 release" or specific v1.0.0 tag/commit SHA was found in search results. The repository has 28 releases, with the latest being v1.1 (released 2024-01-10). The repo was created on 2022-10-14, with the action announced around late 2022. The Kani project issue for creating the action was closed on Sep 6, 2022. To obtain the exact current commit SHA for @v1: 1. Visit https://github.com/model-checking/kani-github-action/tree/v1 2. The SHA is shown next to the branch name (e.g., abc1234). 3. For pinning, use "uses: model-checking/kani-github-action@v1#" (recommended for security). Kani itself is for model-checking Rust code for safety and correctness properties, automatically detecting panics, overflows, etc., using bit-precise verification.
Citations:
- 1: https://github.com/model-checking/kani-github-action
- 2: https://model-checking.github.io/kani/install-github-ci.html
- 3: https://model-checking.github.io/kani-verifier-blog/2022/12/21/easily-verify-your-rust-in-ci-with-kani.html
- 4: https://github.com/model-checking/kani/milestone/13?closed=1
🏁 Script executed:
# Try alternative approaches to find the tag info
curl -s "https://api.github.com/repos/model-checking/kani-github-action/releases/tags/v1" | jq -r '.target_commitish, .tag_name, .published_at' 2>/dev/null || echo "Could not fetch tag info"Repository: strawgate/memagent
Length of output: 86
Pin Kani action to commit SHA and add job timeout.
The workflow references model-checking/kani-github-action@v1 (a mutable branch), which drifts with each run and introduces supply-chain risk. Model-checking jobs can run indefinitely without a timeout, consuming CI minutes unexpectedly. Pin to a full commit SHA and add timeout-minutes.
Suggested fix
kani:
name: Kani proofs
if: github.event_name == 'push' || github.event.pull_request.draft == false
runs-on: ubuntu-latest
+ timeout-minutes: 30
steps:
- uses: actions/checkout@v4
- name: Run Kani verification
- uses: model-checking/kani-github-action@v1
+ uses: model-checking/kani-github-action@<commit-sha>
with:
args: -p logfwd-coreResolve the current v1 branch HEAD at: https://github.com/model-checking/kani-github-action/tree/v1
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In @.github/workflows/ci.yml around lines 147 - 158, The Kani job configuration
uses the mutable reference model-checking/kani-github-action@v1 and lacks a
timeout; replace the mutable tag with the repository's current commit SHA for v1
(i.e., pin model-checking/kani-github-action@<full-commit-sha>) and add a
timeout-minutes field to the kani job (e.g., timeout-minutes: 30) so the "kani"
job and the "uses" entry reference the pinned SHA and the job will be bounded.
| - name: Install Kani verifier | ||
| run: | | ||
| cargo install --locked kani-verifier | ||
| cargo kani setup |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Verify current published versions before choosing a pin.
curl -s https://crates.io/api/v1/crates/kani-verifier | jq -r '.crate.max_stable_version, .versions[0].num'Repository: strawgate/memagent
Length of output: 75
🏁 Script executed:
# Check if file exists and inspect the specific lines
if [ -f ".github/workflows/copilot-setup-steps.yml" ]; then
echo "=== File exists ==="
echo "=== Lines 25-32 (context around 27-30) ==="
sed -n '25,32p' ".github/workflows/copilot-setup-steps.yml"
else
echo "File not found at .github/workflows/copilot-setup-steps.yml"
find . -name "copilot-setup-steps.yml" 2>/dev/null
fiRepository: strawgate/memagent
Length of output: 275
🏁 Script executed:
# Verify the structure of the workflow to understand context
head -50 ".github/workflows/copilot-setup-steps.yml" 2>/dev/null || echo "Cannot read file"Repository: strawgate/memagent
Length of output: 762
Pin kani-verifier version to keep setup reproducible.
Line 29 installs unpinned kani-verifier, which can break unexpectedly when upstream releases change behavior. Pin a known-good version and update intentionally. Current stable version is 0.67.0.
Suggested change
- name: Install Kani verifier
run: |
- cargo install --locked kani-verifier
+ cargo install --locked kani-verifier --version 0.67.0
cargo kani setup📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| - name: Install Kani verifier | |
| run: | | |
| cargo install --locked kani-verifier | |
| cargo kani setup | |
| - name: Install Kani verifier | |
| run: | | |
| cargo install --locked kani-verifier --version 0.67.0 | |
| cargo kani setup |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In @.github/workflows/copilot-setup-steps.yml around lines 27 - 30, Pin the Kani
verifier install in the GitHub Actions step named "Install Kani verifier" by
changing the cargo install invocation (currently "cargo install --locked
kani-verifier") to specify the known-good version (use --version 0.67.0) so the
action installs kani-verifier@0.67.0 reproducibly; keep the subsequent "cargo
kani setup" step as-is.
There was a problem hiding this comment.
♻️ Duplicate comments (1)
.github/workflows/ci.yml (1)
147-160:⚠️ Potential issue | 🟠 MajorPin the Kani action SHA and bound job runtime.
Line 155 uses a mutable action ref (
@v1), and thekanijob has no timeout. This leaves supply-chain drift risk and unbounded CI runtime.Suggested fix
kani: name: Kani proofs if: github.event_name == 'push' || github.event.pull_request.draft == false runs-on: ubuntu-latest + timeout-minutes: 30 steps: - uses: actions/checkout@v4 - name: Run Kani verification - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@<full-v1-head-sha> with: args: -p logfwd-core env: RUSTC_WRAPPER: ""#!/bin/bash set -euo pipefail echo "== Resolve current v1 head SHA ==" git ls-remote https://github.com/model-checking/kani-github-action refs/heads/v1 echo echo "== Current Kani job block ==" sed -n '147,170p' .github/workflows/ci.yml echo echo "== Verify action ref and timeout presence ==" rg -n 'model-checking/kani-github-action@|^\s*timeout-minutes:' .github/workflows/ci.yml🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In @.github/workflows/ci.yml around lines 147 - 160, The Kani job uses an unpinned action ref and lacks a runtime bound; replace the mutable uses entry "model-checking/kani-github-action@v1" in the kani job with a fixed commit SHA (the repo HEAD SHA for v1) and add a timeout-minutes setting under the kani job definition (e.g., timeout-minutes: 30) so the workflow is pinned and the job runtime is bounded; update the uses value and add the timeout-minutes key near the runs-on/steps block for the kani job.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In @.github/workflows/ci.yml:
- Around line 147-160: The Kani job uses an unpinned action ref and lacks a
runtime bound; replace the mutable uses entry
"model-checking/kani-github-action@v1" in the kani job with a fixed commit SHA
(the repo HEAD SHA for v1) and add a timeout-minutes setting under the kani job
definition (e.g., timeout-minutes: 30) so the workflow is pinned and the job
runtime is bounded; update the uses value and add the timeout-minutes key near
the runs-on/steps block for the kani job.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: a61a379c-caf0-4293-9145-caca803fa786
📒 Files selected for processing (1)
.github/workflows/ci.yml
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The constant 80_763_609_600_000_000_000 exceeded u64::MAX (18.4e18), causing a compilation error. Also tightened the year guard from 2554 to 2553, since 2554-12-31T23:59:59.999999999Z overflows u64 nanos. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
crates/logfwd-core/src/otlp.rs (1)
1007-1010:⚠️ Potential issue | 🔴 CriticalFix overflowing
u64literal in compositional proof bound.The literal
80_763_609_600_000_000_000exceedsu64::MAXand blocks Kani compilation. The parser accepts years up to 2554 (line 245), so the bound must compute max nanoseconds for that year rather than use a hardcoded literal.Suggested fix
- const MAX_NANOS: u64 = 80_763_609_600_000_000_000; - assert!(nanos <= MAX_NANOS); + // Bound using the parser's own max accepted year. + let max_days = days_from_civil(2554, 12, 31) as u64; + let max_nanos = (((max_days as u128 * 86_400u128) + 86_399u128) * 1_000_000_000u128 + + 999_999_999u128) as u64; + assert!(nanos <= max_nanos);🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@crates/logfwd-core/src/otlp.rs` around lines 1007 - 1010, The hardcoded MAX_NANOS constant (80_763_609_600_000_000_000) overflows u64 and breaks Kani; replace the literal in otlp.rs with a computed bound instead: define a YEAR_MAX = 2554 (or reuse the existing year bound) and compute max nanoseconds by calculating the seconds between the epoch and YEAR_MAX and multiplying by 1_000_000_000 using a wider intermediate (e.g., u128 or checked_mul) and then cast/assert to u64; update the const MAX_NANOS definition and keep the assert!(nanos <= MAX_NANOS) check intact.
♻️ Duplicate comments (2)
.github/workflows/ci.yml (1)
155-157:⚠️ Potential issue | 🟠 MajorPin Kani GitHub Action to a full commit SHA.
Using
@v1is mutable; pinning the exact commit makes CI deterministic and reduces supply-chain risk.Suggested change
- uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@<full-commit-sha>#!/bin/bash set -euo pipefail git ls-remote https://github.com/model-checking/kani-github-action refs/tags/v1🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In @.github/workflows/ci.yml around lines 155 - 157, The workflow step named "Run Kani verification" currently uses the mutable tag model-checking/kani-github-action@v1; replace that with the action pinned to a full commit SHA (model-checking/kani-github-action@<full-commit-sha>) so the CI is deterministic and supply-chain safe—obtain the exact commit SHA for the v1 tag (e.g., via git ls-remote or the action repo tags) and update the uses field in the "Run Kani verification" job accordingly..github/workflows/copilot-setup-steps.yml (1)
27-30:⚠️ Potential issue | 🟠 MajorPin
kani-verifierto a fixed version for reproducible setup.Line 29 installs a mutable latest version, which can break Copilot flows unexpectedly across runs.
Suggested change
- cargo install --locked kani-verifier + cargo install --locked kani-verifier --version <known-good-version>#!/bin/bash set -euo pipefail curl -s https://crates.io/api/v1/crates/kani-verifier | jq -r '.crate.max_stable_version'🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In @.github/workflows/copilot-setup-steps.yml around lines 27 - 30, The workflow step named "Install Kani verifier" currently installs the latest kani-verifier which is non-reproducible; update the step to install a pinned version instead (e.g., use cargo install --locked kani-verifier --version "<KANI_VERSION>" or read a KANI_VERSION env var) so the install command in that step and the associated RUSTC_WRAPPER="" cargo kani setup call use a fixed, documented version; ensure KANI_VERSION is defined in the workflow or replaced with the chosen semver string.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Outside diff comments:
In `@crates/logfwd-core/src/otlp.rs`:
- Around line 1007-1010: The hardcoded MAX_NANOS constant
(80_763_609_600_000_000_000) overflows u64 and breaks Kani; replace the literal
in otlp.rs with a computed bound instead: define a YEAR_MAX = 2554 (or reuse the
existing year bound) and compute max nanoseconds by calculating the seconds
between the epoch and YEAR_MAX and multiplying by 1_000_000_000 using a wider
intermediate (e.g., u128 or checked_mul) and then cast/assert to u64; update the
const MAX_NANOS definition and keep the assert!(nanos <= MAX_NANOS) check
intact.
---
Duplicate comments:
In @.github/workflows/ci.yml:
- Around line 155-157: The workflow step named "Run Kani verification" currently
uses the mutable tag model-checking/kani-github-action@v1; replace that with the
action pinned to a full commit SHA
(model-checking/kani-github-action@<full-commit-sha>) so the CI is deterministic
and supply-chain safe—obtain the exact commit SHA for the v1 tag (e.g., via git
ls-remote or the action repo tags) and update the uses field in the "Run Kani
verification" job accordingly.
In @.github/workflows/copilot-setup-steps.yml:
- Around line 27-30: The workflow step named "Install Kani verifier" currently
installs the latest kani-verifier which is non-reproducible; update the step to
install a pinned version instead (e.g., use cargo install --locked kani-verifier
--version "<KANI_VERSION>" or read a KANI_VERSION env var) so the install
command in that step and the associated RUSTC_WRAPPER="" cargo kani setup call
use a fixed, documented version; ensure KANI_VERSION is defined in the workflow
or replaced with the chosen semver string.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 86a47056-6025-4de2-a561-9d05f1ce6eae
📒 Files selected for processing (7)
.github/workflows/ci.yml.github/workflows/copilot-setup-steps.ymlCONTRIBUTING.mdcrates/logfwd-core/src/byte_search.rscrates/logfwd-core/src/otlp.rscrates/logfwd-core/src/pipeline/lifecycle.rsjustfile
💤 Files with no reviewable changes (1)
- crates/logfwd-core/src/byte_search.rs
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
crates/logfwd-core/src/otlp.rs (1)
964-983:⚠️ Potential issue | 🔴 CriticalEnable
function-contractsflag in Kani invocations to unblock#[kani::proof_for_contract(...)]proofs.Five
#[kani::proof_for_contract]harnesses are present (crates/logfwd-core/src/otlp.rs, structural.rs), but CI fails because the-Z function-contractsunstable flag is not enabled. Add the flag to:
.github/workflows/ci.ymlkani job: changeargs: -p logfwd-coretoargs: -p logfwd-core -Z function-contractsjustfilekani target: changecargo kani -p logfwd-coretocargo kani -p logfwd-core -Z function-contracts🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@crates/logfwd-core/src/otlp.rs` around lines 964 - 983, The Kani harnesses using #[kani::proof_for_contract(...)] (e.g., proofs for parse_4digits, parse_2digits, days_from_civil and others) require the unstable -Z function-contracts flag; update the CI kani invocation and the local just/Kani target to include that flag so those proofs run: modify the Kani command used in the GitHub Actions kani job (the args that currently run -p logfwd-core) to add -Z function-contracts, and likewise update the justfile kani target (the cargo kani -p logfwd-core command) to pass -Z function-contracts so proof_for_contract harnesses are enabled during verification.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Outside diff comments:
In `@crates/logfwd-core/src/otlp.rs`:
- Around line 964-983: The Kani harnesses using #[kani::proof_for_contract(...)]
(e.g., proofs for parse_4digits, parse_2digits, days_from_civil and others)
require the unstable -Z function-contracts flag; update the CI kani invocation
and the local just/Kani target to include that flag so those proofs run: modify
the Kani command used in the GitHub Actions kani job (the args that currently
run -p logfwd-core) to add -Z function-contracts, and likewise update the
justfile kani target (the cargo kani -p logfwd-core command) to pass -Z
function-contracts so proof_for_contract harnesses are enabled during
verification.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: d58266d6-b33a-415b-88cb-033545beab6a
📒 Files selected for processing (1)
crates/logfwd-core/src/otlp.rs
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
♻️ Duplicate comments (1)
.github/workflows/ci.yml (1)
156-156:⚠️ Potential issue | 🟠 MajorPin the Kani action to a full commit SHA (mutable tag still used).
Line [156] still references
@v1, which is mutable and can drift between runs. Keep the timeout, but pinuses:to an immutable commit SHA.Suggested fix
- - name: Run Kani verification - uses: model-checking/kani-github-action@v1 + - name: Run Kani verification + uses: model-checking/kani-github-action@<full-commit-sha>#!/bin/bash set -euo pipefail # 1) Verify workflow still uses mutable `@v1` sed -n '147,161p' .github/workflows/ci.yml # 2) Resolve current commit for the v1 ref (for pinning) git ls-remote https://github.com/model-checking/kani-github-action refs/heads/v1 refs/tags/v1Expected result:
- Step 1 shows
uses: model-checking/kani-github-action@v1.- Step 2 returns a 40-char SHA that you can pin in
uses: ...@<sha>.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In @.github/workflows/ci.yml at line 156, Replace the mutable tag on the Kani action usage by pinning the `uses: model-checking/kani-github-action@v1` entry to the repository's immutable commit SHA: resolve the current 40-character SHA for the v1 ref (e.g., via `git ls-remote` against the action repo) and update the `uses:` value to `model-checking/kani-github-action@<commit-sha>` while leaving the existing timeout and other step settings unchanged.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In @.github/workflows/ci.yml:
- Line 156: Replace the mutable tag on the Kani action usage by pinning the
`uses: model-checking/kani-github-action@v1` entry to the repository's immutable
commit SHA: resolve the current 40-character SHA for the v1 ref (e.g., via `git
ls-remote` against the action repo) and update the `uses:` value to
`model-checking/kani-github-action@<commit-sha>` while leaving the existing
timeout and other step settings unchanged.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 54a6b348-fd67-4c15-a7e7-5e4240d001fb
📒 Files selected for processing (2)
.github/workflows/ci.ymljustfile
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Summary
model-checking/kani-github-action@v1(handles CBMC + toolchain automatically)copilot-setup-steps.ymlso Copilot agents can runcargo kaniwhen working on proofsjust kanirecipe for local verification of logfwd-core proofsjust kanicommandRuns against
logfwd-coreonly (the proven#![no_std]crate with 52+ Kani proofs).Test plan
just kaniworks locally (requires Kani installed)🤖 Generated with Claude Code