ESBMC software model checker integration for Claude Code
npx claudepluginhub esbmc/agent-marketplaceESBMC software model checker integration for Claude Code - verify C, C++, Python, Solidity, and Java/Kotlin programs for bugs, memory safety, undefined behavior, and more
A Claude Code plugin marketplace for ESBMC (Efficient SMT-based Context-Bounded Model Checker) tools.
Formal verification integration for Claude Code. Verify C, C++, Python, Solidity, and Java/Kotlin programs for bugs, memory safety, undefined behavior, and more using ESBMC bounded model checker.
Features:
/verify command for quick verification of source files/audit command for comprehensive security audits with multiple verification passesSee the plugin README for full documentation or the Tutorial for a step-by-step guide.
From within Claude Code:
/plugin marketplace add esbmc/agent-marketplace
/plugin install esbmc-plugin@esbmc-marketplace
If you want to remove the ESBMC agent, you can enter:
/plugin marketplace remove esbmc-marketplace
MIT License - See LICENSE for details.