What to watch for

These are failure modes of any formal flow, agentic or not. Bitlevel is built to surface them rather than hide them, but you should know what they look like.

Overconstraint and vacuity

An overconstrained environment proves things about a design that cannot happen; a vacuous property never actually applied. Both produce a reassuring green result that means nothing.

• Ask for the overconstraint audit rather than assuming it happened.
• Treat vacuous_pass and uncoverable as red flags, not passes. The agent runs vacuity checks automatically and flags them, but read the flags.
• Ask that constraints be written as modeling code with intent recorded, not bare assumes — it is what makes an audit possible later.

Bounded vs. unbounded

"No failure found" is meaningless without a depth. Every clean bounded result Bitlevel reports carries the bound it reached — bounded_pass to cycle N. That number is the result. If you need a proof, say so; the convergence loop (helpers, reductions, case splits, induction, IC3) is how you get one, and when it cannot close, the agent tells you what is blocking.

Checker quality

A converging proof of a weak property is worse than an inconclusive proof of a strong one, because it looks finished. Mutation analysis is the check on this: it injects faults and reports which ones the checkers catch. The gaps are the point of the output. Ask for it before sign-off, and any time a property closed suspiciously easily.

Inferred intent

When there is no spec and the agent infers intent from the RTL, a plausible-looking but wrong checker is the most likely failure. Read the stated assumptions it lists before trusting the result, and correct them — it will rebuild the checkers.

Practical things

• Approval prompts block long runs. If you walk away from a session, make sure the agent is not waiting on a Do you want to proceed? — or switch to auto mode for that session.
• Use tmux. A dropped SSH connection kills an unprotected session and whatever run it was driving.
• Machine resources. Formal is CPU- and memory-hungry. --workers scales throughput; the agent sets it, but a run that seems idle on a large box is usually one that was left at the default.

Support

If at any point you need help, reach your Voltai deployment contacts. Include the instance name, the project directory, and — if a run misbehaved — the out/results.json and the .bitlevel.log from that run; they contain the exact commands and engine output.

Happy verification.