Verify your code by chatting▮

AProver is a suite of LLM-driven verification agents. The live demo runs BMC-Agent — Claude generates function specs, CBMC proves or refutes them, the agent classifies counterexamples, and confirmed bugs come back with evidence tiers. Today: C. On the roadmap: Rust (Kani) and beyond.

1 #include <stdint.h>
2 int add(int a, int b) {
3     return a + b;
4 }