Add --export-json for structured verification results
#4472
Conversation
…o add runner results
…n-handler # Conflicts: # kani-driver/src/main.rs
…schedule the schema for harness metadada util func.
…kani-output into feat/json-handler
…s_runner.rs to minimize dependency
This reverts commit a2e7757.
|
Thank you for your suggestion! We discussed with Rajath about this and user can opt in using the flag so hopefully nothing will be broken. |
fix: update cbmc for minimal changes, delete redundant changes
- Implement MCP server to integrate Kani with AI assistants - Add tools: verify_rust_project, verify_unsafe_code, explain_kani_failure, generate_kani_harness - Add Kani output parser - Enable Amazon Q to run Kani verification via MCP protocol
Update: MCP Integration with Amazon Q CLI
Revert "Update: MCP Integration with Amazon Q CLI"
Feat/json handler copyright check
ci: fix copyright and clippy check
|
Thanks for adding this feature. This has been longstanding! I would recommend putting this feature under an unstable flag (see https://model-checking.github.io/kani/rfc/rfcs/0006-unstable-api.html) for some time until we ensure the json schema won't change. |
|
Would it make sense to use a standard JSON schema format such as https://json-schema.org/ along with a standard validator, e.g. https://python-jsonschema.readthedocs.io/en/stable/validate/? |
|
|
||
| Several edge cases need consideration: | ||
|
|
||
| **CBMC output parsing**: We extract CBMC statistics using regex patterns. If CBMC's output format changes in future versions, parsing may fail. To handle this gracefully, we can omit CBMC statistics in the json schema. |
There was a problem hiding this comment.
It's likely more robust to use CBMC's --json-ui option (https://diffblue.github.io/cbmc/man/cbmc.html).
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Thank you for reviewing this and for the suggestion. |
6 participants
Add opt-in JSON export (--export-json ) to emit structured verification results (metadata, per-harness outcomes, CBMC stats).
Improves Kani by enabling reliable machine-readable output for external tools and applications.
Context: Current output is human-readable only, which blocks robust automation and integrations.
Manual tests:
• Run cargo kani --export-json out.json
• With multiple harnesses: counts in summary match executed harnesses.
Resolves #2572
Resolves #2636
Resolves #2574
Resolves #2562
Resolves #1194
Resolves #1219
Resolves #1045
Resolves #598
Resolves #3357
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.