[BryanFRD]

Stacked on #1379 (preMajor). Merge that one first.

ferrflow migrate --from release-please now produces a config that releases the project it came from. Before, it read neither extra-files nor the pre-major flags and said nothing about it.

Mapped

• extra-files:
  • generic (and plain strings) → txt with a selector on the x-release-please-version line (optional v outside the capture)
  • toml with $.package.version / $.workspace.package.version on a Cargo.toml → toml
  • json with $.version → json
  • anything else is listed under "Review manually" with the exact entry. Nothing is dropped silently
• bump-minor-pre-major → preMajor.breaking: minor, bump-patch-for-minor-pre-major → preMajor.feat: patch, each on its own, on the workspace when every package agrees
• autoMergeReleases: false, because release-please never merges its own release PR
• updateLockfiles: true when a versioned file has a lockfile
• package name: package-name, component, root package.json name, directory name, then app. The directory-name fallback applies to every migrator
• the output only contains non-default keys (all migrators). A round-trip test reloads every migrator fixture and checks it equals the migrated config
• the "release-type has no file mapping" warning only fires when the package really ends up with no versioned files

The x-release-please-start-version / x-release-please-end block form is not mapped and gets a warning.

Example

A release-please config for an invented Neovim plugin (go release type, two generic marker files, a Cargo workspace version, both pre-major flags) is a test fixture. Output:

{
  "workspace": {
    "preMajor": { "breaking": "minor", "feat": "patch" },
    "releaseCommitMode": "pr",
    "autoMergeReleases": false,
    "update_lockfiles": true
  },
  "package": [{
    "name": "quillmark.nvim",
    "path": ".",
    "versionedFiles": [
      { "path": "lua/quillmark/version.lua", "format": "txt", "selector": "v?(\\d+\\.\\d+\\.\\d+(?:[-+][0-9A-Za-z][0-9A-Za-z.+-]*)?)[^\\n]*x-release-please-version" },
      { "path": "README.md", "format": "txt", "selector": "..." },
      { "path": "Cargo.toml", "format": "toml" }
    ],
    "changelog": "CHANGELOG.md"
  }]
}

The selector tests run through the real txt reader/writer on the fixture's two marker lines: they read 0.5.0, and a write to 0.6.0 replaces only the version.

Closes #1375

[ferrfleet-interne]

Changes requested. The code review approved, but formal verification found a counterexample: the generic extra-files selector rewrites only the first line carrying x-release-please-version, where release-please rewrites every such line.

Blocking

• major, src/config/migrate/release_please/extra_files.rs:8 (GENERIC_MARKER_SELECTOR) with src/formats/txt.rs (select_span): select_span takes the first regex match only. A file with two marked lines keeps the second on the old version after a release, and nothing reports it. Minimal case: a = "0.5.0" # x-release-please-version and b = "0.5.0" # x-release-please-version. Writing 0.6.0 changes only the first. The migration report warns about the start/end block form only. Either support multi-line rewrites for this selector, or at least warn in the report that only the first marked line is updated.

Other findings

• minor, src/config/migrate/tests.rs:530: the emitted ferrflow.json writes update_lockfiles in snake_case, while the README and the report say updateLockfiles. update_lockfiles is missing from CAMEL_CASE_KEYS in src/config/format.rs (update_dependents, defer_publish and manifest_file have the same gap). Both spellings load through the serde alias, so nothing breaks at runtime. The avante test pins the inconsistency by asserting json["workspace"]["update_lockfiles"]. Add the keys, then assert updateLockfiles.
• suggestion, src/config/migrate/prune.rs:31: to_pretty_json repeats the camel-casing, pretty-printing and trailing newline of JsonFormat::serialize, so the two can drift. Add a Value-level helper in format.rs and call it from both.
• suggestion, src/config/migrate/release_please.rs:258: the generic-file warning does not mention the x-release-please-major, -minor and -patch markers, which are silently left unmanaged. Name them in the warning.

The review found the extra-files, pre-major and auto-merge mapping correct and well tested, and the round-trip test shows the pruned output reloads to the same config.

Formal verification

Property	Result
apply_pre_major: hoisting or per-package placement never changes effective_pre_major (1 to 3 packages, 1110 assignments)	tested, exhaustive
pre_major_rules: package flag overrides top-level, minor maps to breaking: minor, patch to feat: patch, nothing else set (81 combinations)	tested, exhaustive
Pruned ferrflow.json reloads to the migrated Config, pre-major matches flags, autoMergeReleases false, no duplicate versioned files (512 seeded configs)	tested
Any extra-files entry migrates without panic and is named in a warning if unmapped (512 random values)	tested
One marked line among unmarked lines: read and write touch only that version (512 files)	tested
Writing a version rewrites every marked line	counterexample (above)

Not verified:

• The Kani harnesses were not run. Kani 0.68.0 hits an internal compiler error on the crate (kani-compiler/src/intrinsics.rs:243), so the same properties were checked by exhaustive enumeration. The proposed CI job would fail the same way, and the kani-github-action reference needs pinning to a commit SHA.
• The selector, extra-files mapping and emit round-trip were covered by seeded randomized tests, which are tests and not proofs.
• Behaviour on x-release-please-major/minor/patch markers and the start/end block form was not tested.
• enable_lockfile_updates and default_package_name/current_dir_name were not verified (thin glue over Manifest::from_manifest_filename and the cwd).

3 harnesses (Kani proofs, exhaustive checks, randomized properties), not yet in the PR

src/config/migrate/release_please/kani_proofs.rs (declared with #[cfg(kani)] mod kani_proofs;): 3 proofs covering placement for 1 and 3 packages and flag precedence.

//! Kani harnesses for the release-please pre-major mapping.
//!
//! Run with `cargo kani --harness release_please`.

use super::*;
use crate::config::types::{PreMajorBump, PreMajorRules};

fn any_bump() -> Option<PreMajorBump> {
    match kani::any::<u8>() % 3 {
        0 => None,
        1 => Some(PreMajorBump::Minor),
        _ => Some(PreMajorBump::Patch),
    }
}

fn any_rules() -> Option<PreMajorRules> {
    if kani::any() {
        Some(PreMajorRules {
            breaking: any_bump(),
            feat: any_bump(),
        })
    } else {
        None
    }
}

fn any_flag() -> Option<bool> {
    if kani::any() { Some(kani::any()) } else { None }
}

/// Whatever mix of per-package rules the migrator computed, placing them
/// (hoisted to the workspace or written per package) never changes the rule
/// a package actually resolves to through `effective_pre_major`.
fn placement_preserves_effective_rules<const N: usize>() {
    let rules: [Option<PreMajorRules>; N] = core::array::from_fn(|_| any_rules());
    let mut packages: Vec<PackageConfig> = (0..N).map(|_| PackageConfig::default()).collect();
    let mut workspace = WorkspaceConfig::default();

    apply_pre_major(&mut packages, &rules, &mut workspace);

    for (package, rule) in packages.iter().zip(rules.iter()) {
        assert_eq!(package.effective_pre_major(&workspace), *rule);
    }
}

#[kani::proof]
#[kani::unwind(4)]
fn release_please_pre_major_placement_one_package() {
    placement_preserves_effective_rules::<1>();
}

#[kani::proof]
#[kani::unwind(4)]
fn release_please_pre_major_placement_three_packages() {
    placement_preserves_effective_rules::<3>();
}

/// `bump-minor-pre-major` maps to `breaking: minor` and
/// `bump-patch-for-minor-pre-major` to `feat: patch`, a package-level flag
/// (even `false`) wins over the top-level one, and no other rule is invented.
#[kani::proof]
#[kani::unwind(2)]
fn release_please_pre_major_flag_precedence() {
    let entry = PackageEntry {
        bump_minor_pre_major: any_flag(),
        bump_patch_for_minor_pre_major: any_flag(),
        ..PackageEntry::default()
    };
    let rp = ReleasePleaseConfig {
        bump_minor_pre_major: any_flag(),
        bump_patch_for_minor_pre_major: any_flag(),
        ..ReleasePleaseConfig::default()
    };
    let mut report = MigrationReport::default();

    let got = pre_major_rules(".", &entry, &rp, &mut report);

    let minor = entry
        .bump_minor_pre_major
        .unwrap_or(rp.bump_minor_pre_major.unwrap_or(false));
    let patch = entry
        .bump_patch_for_minor_pre_major
        .unwrap_or(rp.bump_patch_for_minor_pre_major.unwrap_or(false));
    if !minor && !patch {
        assert!(got.is_none());
    } else {
        let got = got.expect("a set flag must produce rules");
        assert_eq!(got.breaking == Some(PreMajorBump::Minor), minor);
        assert_eq!(got.feat == Some(PreMajorBump::Patch), patch);
        assert!(got.breaking != Some(PreMajorBump::Patch));
        assert!(got.feat != Some(PreMajorBump::Minor));
    }
}

src/config/migrate/release_please/verify_exhaustive.rs (declared with #[cfg(test)] mod verify_exhaustive;): the same properties by enumeration.

//! Exhaustive checks of the release-please pre-major mapping over its whole
//! finite input domain (the same properties as `kani_proofs.rs`, enumerated
//! instead of model-checked).

use super::*;
use crate::config::types::{PreMajorBump, PreMajorRules};

const BUMPS: [Option<PreMajorBump>; 3] = [None, Some(PreMajorBump::Minor), Some(PreMajorBump::Patch)];
const FLAGS: [Option<bool>; 3] = [None, Some(false), Some(true)];

fn all_rules() -> Vec<Option<PreMajorRules>> {
    let mut out = vec![None];
    for breaking in BUMPS {
        for feat in BUMPS {
            out.push(Some(PreMajorRules { breaking, feat }));
        }
    }
    out
}

/// For every assignment of rules to 1..=3 packages, placing them never
/// changes the rule each package resolves to through `effective_pre_major`.
#[test]
fn pre_major_placement_preserves_effective_rules_exhaustively() {
    let domain = all_rules();
    for n in 1..=3usize {
        let mut idx = vec![0usize; n];
        loop {
            let rules: Vec<_> = idx.iter().map(|&i| domain[i]).collect();
            let mut packages: Vec<PackageConfig> = (0..n).map(|_| PackageConfig::default()).collect();
            let mut workspace = WorkspaceConfig::default();
            apply_pre_major(&mut packages, &rules, &mut workspace);
            for (package, rule) in packages.iter().zip(&rules) {
                assert_eq!(package.effective_pre_major(&workspace), *rule, "{rules:?}");
            }
            let mut k = 0;
            while k < n && idx[k] + 1 == domain.len() {
                idx[k] = 0;
                k += 1;
            }
            if k == n {
                break;
            }
            idx[k] += 1;
        }
    }
}

/// Every combination of top-level and package-level flags: the package flag
/// (even `false`) wins, minor maps to `breaking: minor`, patch to
/// `feat: patch`, and nothing else is set.
#[test]
fn pre_major_flag_precedence_exhaustively() {
    for pm in FLAGS {
        for pp in FLAGS {
            for tm in FLAGS {
                for tp in FLAGS {
                    let entry = PackageEntry {
                        bump_minor_pre_major: pm,
                        bump_patch_for_minor_pre_major: pp,
                        ..PackageEntry::default()
                    };
                    let rp = ReleasePleaseConfig {
                        bump_minor_pre_major: tm,
                        bump_patch_for_minor_pre_major: tp,
                        ..ReleasePleaseConfig::default()
                    };
                    let got = pre_major_rules(".", &entry, &rp, &mut MigrationReport::default());
                    let minor = pm.unwrap_or(tm.unwrap_or(false));
                    let patch = pp.unwrap_or(tp.unwrap_or(false));
                    let want = PreMajorRules {
                        breaking: minor.then_some(PreMajorBump::Minor),
                        feat: patch.then_some(PreMajorBump::Patch),
                    };
                    let want = (minor || patch).then_some(want);
                    assert_eq!(got, want, "{pm:?} {pp:?} {tm:?} {tp:?}");
                }
            }
        }
    }
}

src/config/migrate/verify_props.rs (declared with #[cfg(test)] mod verify_props; in src/config/migrate.rs): seeded randomized properties. generic_selector_rewrites_every_marked_line is the one that fails.

//! Randomized property tests for `ferrflow migrate --from release-please`.
//!
//! These are not proofs: each property is checked on a fixed number of
//! inputs drawn from a seeded PRNG, so a failure is reproducible from the
//! seed printed in the assertion message.

use super::{Migration, MigrationReport, Source, emit, release_please};
use crate::config::Config;
use crate::config::format::{ConfigFileFormat, format_handler};
use crate::config::types::{PreMajorBump, PreMajorRules};
use crate::formats::VersionFile;
use crate::formats::txt::TxtVersionFile;
use serde_json::{Value, json};
use std::path::PathBuf;

const CASES: u64 = 512;

struct Rng(u64);

impl Rng {
    fn new(seed: u64) -> Self {
        Rng(seed.wrapping_mul(0x9E37_79B9_7F4A_7C15) | 1)
    }
    fn next(&mut self) -> u64 {
        let mut x = self.0;
        x ^= x << 13;
        x ^= x >> 7;
        x ^= x << 17;
        self.0 = x;
        x
    }
    fn below(&mut self, n: u64) -> u64 {
        self.next() % n
    }
    fn bool(&mut self) -> bool {
        self.below(2) == 0
    }
    fn pick<'a, T>(&mut self, items: &'a [T]) -> &'a T {
        &items[self.below(items.len() as u64) as usize]
    }
}

fn version(rng: &mut Rng) -> String {
    let core = format!("{}.{}.{}", rng.below(30), rng.below(30), rng.below(30));
    match rng.below(4) {
        0 => format!("{core}-rc.{}", rng.below(9)),
        1 => format!("{core}-beta"),
        _ => core,
    }
}

fn marker_line(rng: &mut Rng, v: &str) -> String {
    let (open, close) = *rng.pick(&[
        ("return \"", "\""),
        ("    version='v", "'"),
        ("VERSION = ", ""),
        ("version: v", ""),
        ("  \"version\": \"", "\","),
    ]);
    let tail = *rng.pick(&[" -- ", " # ", "  // keep in sync ", " <!-- "]);
    format!("{open}{v}{close}{tail}x-release-please-version")
}

fn plain_line(rng: &mut Rng) -> String {
    match rng.below(4) {
        0 => format!("local dep = \"{}\"", version(rng)),
        1 => "```lua".to_string(),
        2 => String::new(),
        _ => format!("see https://example.com/v{}", version(rng)),
    }
}

fn generic_selector() -> String {
    let (config, _) =
        release_please::build(r#"{"packages": {".": {"release-type": "simple", "extra-files": ["f"]}}}"#)
            .unwrap();
    config.packages[0]
        .versioned_files
        .iter()
        .find_map(|vf| vf.selector.clone())
        .expect("generic extra file carries a selector")
}

/// On a file with one `x-release-please-version` line among unmarked lines,
/// the generated selector reads that line's version, and writing a new
/// version changes that line's version and nothing else in the file.
#[test]
fn generic_selector_reads_and_rewrites_only_the_marked_version() {
    let selector = generic_selector();
    let dir = tempfile::tempdir().unwrap();
    for seed in 0..CASES {
        let mut rng = Rng::new(seed);
        let old = version(&mut rng);
        let new = version(&mut rng);
        let marker_at = rng.below(4) as usize;
        let mut lines: Vec<String> = (0..4).map(|_| plain_line(&mut rng)).collect();
        let marked = marker_line(&mut rng, &old);
        lines.insert(marker_at, marked.clone());
        let file = dir.path().join(format!("f{seed}"));
        std::fs::write(&file, lines.join("\n") + "\n").unwrap();

        let read = TxtVersionFile
            .read_version_with_selector(&file, Some(&selector))
            .unwrap();
        assert_eq!(read, old, "seed {seed}");

        TxtVersionFile
            .write_version_with_selector(&file, &new, Some(&selector))
            .unwrap();
        lines[marker_at] = marked.replacen(&old, &new, 1);
        assert_eq!(
            std::fs::read_to_string(&file).unwrap(),
            lines.join("\n") + "\n",
            "seed {seed}"
        );
    }
}

/// release-please's generic updater rewrites the version on every line that
/// carries `x-release-please-version`. The migrated config must do the same,
/// or a release leaves some marked lines on the old version.
#[test]
fn generic_selector_rewrites_every_marked_line() {
    let selector = generic_selector();
    let dir = tempfile::tempdir().unwrap();
    for seed in 0..CASES {
        let mut rng = Rng::new(seed);
        let old = version(&mut rng);
        let new = version(&mut rng);
        let lines = [
            marker_line(&mut rng, &old),
            plain_line(&mut rng),
            marker_line(&mut rng, &old),
        ];
        let file = dir.path().join(format!("f{seed}"));
        std::fs::write(&file, lines.join("\n") + "\n").unwrap();

        TxtVersionFile
            .write_version_with_selector(&file, &new, Some(&selector))
            .unwrap();
        let written = std::fs::read_to_string(&file).unwrap();
        for line in written.lines().filter(|l| l.contains("x-release-please-version")) {
            assert!(
                line.contains(&new) && !line.contains(&old) || old == new,
                "seed {seed}: marked line left on {old} after writing {new}: {line:?}\n{written}"
            );
        }
    }
}

const RELEASE_TYPES: &[&str] = &["node", "rust", "python", "go", "simple", "java", "ruby"];
const PATHS: &[&str] = &[".", "a", "crates/core", "packages/web", "svc/"];

fn extra_file(rng: &mut Rng) -> Value {
    rng.pick(&[
        json!("README.md"),
        json!("/README.md"),
        json!({"type": "generic", "path": "lua/version.lua"}),
        json!({"type": "toml", "path": "Cargo.toml", "jsonpath": "$.package.version"}),
        json!({"type": "toml", "path": "Cargo.toml", "jsonpath": "$.workspace.package.version"}),
        json!({"type": "toml", "path": "pyproject.toml", "jsonpath": "$.project.version"}),
        json!({"type": "json", "path": "package.json", "jsonpath": "$.version"}),
        json!({"type": "json", "path": "manifest.json", "jsonpath": "$.meta.version"}),
        json!({"type": "yaml", "path": "chart.yaml", "jsonpath": "$.version"}),
        json!({"type": "generic"}),
        json!(7),
    ])
    .clone()
}

fn flag(rng: &mut Rng) -> Option<bool> {
    match rng.below(3) {
        0 => None,
        1 => Some(true),
        _ => Some(false),
    }
}

fn put_flags(obj: &mut serde_json::Map<String, Value>, minor: Option<bool>, patch: Option<bool>) {
    if let Some(m) = minor {
        obj.insert("bump-minor-pre-major".into(), json!(m));
    }
    if let Some(p) = patch {
        obj.insert("bump-patch-for-minor-pre-major".into(), json!(p));
    }
}

struct Generated {
    raw: String,
    /// Expected (bump-minor-pre-major, bump-patch-for-minor-pre-major) per
    /// package path, after package-over-top-level precedence.
    flags: std::collections::BTreeMap<String, (bool, bool)>,
}

fn release_please_config(rng: &mut Rng) -> Generated {
    let mut root = serde_json::Map::new();
    let (top_minor, top_patch) = (flag(rng), flag(rng));
    put_flags(&mut root, top_minor, top_patch);
    if rng.bool() {
        root.insert("include-component-in-tag".into(), json!(true));
    }
    if rng.below(4) == 0 {
        root.insert("release-type".into(), json!(rng.pick(RELEASE_TYPES)));
    }
    let mut packages = serde_json::Map::new();
    let mut flags = std::collections::BTreeMap::new();
    let count = rng.below(4);
    for _ in 0..count {
        let path = *rng.pick(PATHS);
        if packages.contains_key(path) {
            continue;
        }
        let mut pkg = serde_json::Map::new();
        pkg.insert("release-type".into(), json!(rng.pick(RELEASE_TYPES)));
        if rng.bool() {
            pkg.insert("component".into(), json!(format!("c{}", rng.below(5))));
        }
        let extras: Vec<Value> = (0..rng.below(4)).map(|_| extra_file(rng)).collect();
        if !extras.is_empty() {
            pkg.insert("extra-files".into(), Value::Array(extras));
        }
        let (m, p) = (flag(rng), flag(rng));
        put_flags(&mut pkg, m, p);
        flags.insert(
            path.to_string(),
            (
                m.or(top_minor).unwrap_or(false),
                p.or(top_patch).unwrap_or(false),
            ),
        );
        packages.insert(path.to_string(), Value::Object(pkg));
    }
    if packages.is_empty() {
        flags.insert(
            ".".to_string(),
            (top_minor.unwrap_or(false), top_patch.unwrap_or(false)),
        );
    } else {
        root.insert("packages".into(), Value::Object(packages));
    }
    Generated {
        raw: Value::Object(root).to_string(),
        flags,
    }
}

fn build_in_tempdir(raw: &str) -> (Config, MigrationReport) {
    let dir = tempfile::tempdir().unwrap();
    let _guard = crate::test_utils::CWD_LOCK
        .lock()
        .unwrap_or_else(|e| e.into_inner());
    let saved = std::env::current_dir().unwrap();
    std::env::set_current_dir(dir.path()).unwrap();
    let built = release_please::build(raw);
    std::env::set_current_dir(saved).unwrap();
    built.unwrap()
}

/// For any release-please config: the emitted ferrflow.json (with defaults
/// pruned) loads back to exactly the config the migrator built, every
/// package resolves to the pre-major rules its flags ask for, and no
/// versioned file is listed twice for the same package.
#[test]
fn release_please_migration_round_trips_and_keeps_pre_major_semantics() {
    for seed in 0..CASES {
        let mut rng = Rng::new(seed);
        let generated = release_please_config(&mut rng);
        let (config, report) = build_in_tempdir(&generated.raw);
        let ctx = format!("seed {seed}: {}", generated.raw);

        assert_eq!(config.packages.len(), generated.flags.len(), "{ctx}");
        for package in &config.packages {
            let (minor, patch) = generated.flags[&package.path];
            let expected = PreMajorRules {
                breaking: minor.then_some(PreMajorBump::Minor),
                feat: patch.then_some(PreMajorBump::Patch),
            };
            let expected = (expected != PreMajorRules::default()).then_some(expected);
            assert_eq!(
                package.effective_pre_major(&config.workspace),
                expected,
                "{ctx}: package {}",
                package.path
            );
            for (i, vf) in package.versioned_files.iter().enumerate() {
                assert!(
                    !package.versioned_files[..i].contains(vf),
                    "{ctx}: {} listed twice",
                    vf.path
                );
            }
        }
        assert!(!config.workspace.auto_merge_releases, "{ctx}");

        let migration = Migration::new(
            Source::ReleasePlease,
            PathBuf::from("release-please-config.json"),
            config,
            report,
        );
        let out = tempfile::tempdir().unwrap();
        let (_, content) = emit(&migration, out.path(), true).unwrap();
        let reloaded = format_handler(ConfigFileFormat::Json)
            .parse(&content)
            .unwrap_or_else(|e| panic!("{ctx}: emitted config does not load: {e:#}\n{content}"));
        assert_eq!(
            serde_json::to_value(&reloaded).unwrap(),
            serde_json::to_value(&migration.config).unwrap(),
            "{ctx}: reloaded config differs\n{content}"
        );
    }
}

fn arbitrary_json(rng: &mut Rng, depth: u32) -> Value {
    match rng.below(if depth == 0 { 4 } else { 6 }) {
        0 => Value::Null,
        1 => json!(rng.bool()),
        2 => json!(rng.next() as i64),
        3 => json!(*rng.pick(&["", "/", "//x", "a/../b", "Cargo.toml", "generic", "$.version"])),
        4 => Value::Array((0..rng.below(3)).map(|_| arbitrary_json(rng, depth - 1)).collect()),
        _ => {
            let mut map = serde_json::Map::new();
            for _ in 0..rng.below(4) {
                let key = *rng.pick(&["type", "path", "jsonpath", "xpath", "glob"]);
                map.insert(key.to_string(), arbitrary_json(rng, depth - 1));
            }
            Value::Object(map)
        }
    }
}

/// Any `extra-files` entry, however malformed, migrates without panicking,
/// and an entry the migrator cannot express is named verbatim under
/// warnings instead of being dropped silently.
#[test]
fn arbitrary_extra_files_never_panic_and_are_never_dropped_silently() {
    for seed in 0..CASES {
        let mut rng = Rng::new(seed);
        let entry = arbitrary_json(&mut rng, 3);
        let raw = json!({"packages": {"pkg": {"release-type": "simple", "extra-files": [entry]}}})
            .to_string();
        let (config, report) = build_in_tempdir(&raw);
        let mapped = config.packages[0].versioned_files.len() > 1
            || report.mapped.iter().any(|m| m.contains("already covered"));
        let warned = report.warnings.iter().any(|w| w.contains(&entry.to_string()));
        assert!(mapped || warned, "seed {seed}: {entry} neither mapped nor reported");
    }
}

Also proposed: .github/workflows/verify.yml running model-checking/kani-github-action@v1 with --lib --harness release_please on PRs touching src/config/migrate/**. It would fail on the Kani ICE above until that is fixed, and the action needs SHA pinning.