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:
/verifycommand for quick verification of source files/auditcommand for comprehensive security audits with multiple verification passes- Verification skill that triggers automatically when discussing code verification topics
- Reference documentation, examples, and utility scripts
See 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
- ESBMC installed and available in your PATH
- Claude Code CLI installed
MIT License - See LICENSE for details.