Next Generation
Bounded Model Checker

Pushing boundaries of BMC: modern, convenient, efficient, and free solution for multiagent systems.

🚀 Public release coming soon in 2026

Multi-Agent Model Lifecycle

Create, run, and verify multi-agent BMC models — all in one place

Define multi-agent systems, configure bounded reachability and safety properties, then run verification jobs with a single click. Track every version of your models, roll back changes, and catch deadlocks, violations, and counterexamples before they reach production.

Drivetrain Error

Charging

Ready

Visual Collaboration

Edit models visually and collaborate in real time

Build and refine your models using an interactive graph-based GUI — no manual syntax required. Share models with teammates, co-edit state graphs and transitions together, and maintain a full audit trail of every change across your organisation.

v1.3

main

Live

Edit

API & Integrations

Plug BMC verification into any language or toolchain

Use the REST API to submit models, trigger verification runs, and retrieve results from Python, Java, Go, or any other language. Integrate BMC checks into CI pipelines, automated test suites, or custom research workflows — without ever leaving your existing tooling.

Interleaving Semantics

Every possible ordering, verified

All agents run concurrently, and BMC explores every possible ordering of their steps. No race condition or deadlock hides in an unlikely schedule.

Running

Waiting

Blocked

Ready

Developer-first

Models as code, results in seconds

Define multi-agent systems in YAML or build them programmatically via the SDK. Run bounded model checking with a single API call.

func runBMC() {
    client := nextbmc.NewClient()

    model, _ := client.Models.Create(bmc.ModelInput{
        Name: "train-tunnel",
        Agents: []bmc.Agent{
            {
                Name:    "Train1",
                Initial: "approaching",
                Transitions: []bmc.Transition{
                    {From: "approaching", To: "in_tunnel",  Guard:  "semaphore == free"},
                    {From: "in_tunnel",   To: "leaving",    Action: "semaphore = occupied"},
                    {From: "leaving",     To: "approaching", Action: "semaphore = free"},
                },
            },
            {Name: "Train2" /* same transitions */},
        },
        Properties: []bmc.Property{
            {
                Name:    "mutual_exclusion",
                Type:    bmc.Always,
                Formula: "!(Train1 == in_tunnel && Train2 == in_tunnel)",
            },
        },
    })
}

No proprietary language: Unlike other BMC tools, there is no custom DSL to learn. Models are plain YAML or JSON — formats your whole stack already speaks.
YAML & JSON import / export: Round-trip your models freely. Export to JSON for programmatic manipulation, re-import YAML from version control with zero friction.
SDK for every language: Official clients for Go, Python, Java, and more. One REST API as the universal fallback — integrate from any environment.
Proof certificates: Every passing check produces a signed certificate. Every failure ships a full counterexample trace for immediate diagnosis.

Are you ready to push the boundaries?

Create model in convenient GUI, run bounded model checking in seconds, and get a proof or a counterexample trace — no setup, no custom language, no surprises.

Do you want more? Check what we can offer