Conversation
Use is_none_or instead of map_or for clarity, reformat code. Assisted-by: OpenCode (Claude Sonnet 4)
Add bounded model checking proofs using Kani to verify key invariants: - skip_if_zero_or_none: correctly identifies values to skip serializing - set_fds/get_fds: round-trip property holds for all message types - get_fds: returns 0 when fds field is None Also adds: - GitHub Actions workflow job to run Kani proofs in CI - Justfile with common development commands including kani targets Kani is a bounded model checker that mathematically proves these properties hold for all possible inputs within bounds, providing stronger guarantees than traditional testing. Assisted-by: OpenCode (Claude Sonnet 4)
Points to Microsoft's Rust devcontainer image for VS Code/Codespaces. Assisted-by: OpenCode (Claude Sonnet 4)
The proofs using JsonRpcRequest/Response with kani::any() caused combinatorial explosion in Kani's bounded model checking due to the complexity of serde_json::Value types. Simplify to focus on verifiable properties: - skip_if_zero_or_none: 3 proofs covering None, Some(0), Some(n>0) - get_fds: 2 proofs covering None and Some(n) cases These 5 proofs now complete successfully in ~0.02s each. Assisted-by: OpenCode (Claude Sonnet 4)
Replace separate toolchain installation with devcontainers/ci action that runs inside the same devcontainer image used for local development. This ensures CI and local builds use identical environments. Both jobs now delegate to Justfile targets: - ci job: runs `just ci` (fmt check, clippy, tests) - kani job: runs `just kani` (formal verification proofs) Also updates .devcontainer.json to use bootc-dev/devenv-debian image which includes Kani, cargo-nextest, and other development tools. Assisted-by: OpenCode (Claude Sonnet 4)
|
My opinion, expressed here: If one is using LLMs to assist in code generation, Rust is a really great choice just as a baseline - the strong type system, good tools etc. But it's also one of the only industrial languages to make it easy (like this, with Kani and others) to dip one's toes into formal methods/proofs of correctness. For the record: I'm for sure not a Kani expert, but it really did just work to prompt something like "look at this project and find places we can apply proofs of correctness with Kani". That led into a side quest of the problem of reproducing the proofs locally because Kani pins to an arbitrary Rust toolchain, and so as others know I'm trying to build on devcontainers for reproducible environments, hence bootc-dev/infra@d6f12dd added a reproducible Kani install into our devcontainer. Then a key thing is to ensure GHA uses our devcontainer as is done here. And combined: easy to hack on, reproducible formally proved correct Rust (of course, just a small subset of this repo, but I'm looking forward to doing more). |
1 participant
No description provided.