List all available Atelier B projects

Get detailed information about an Atelier B project

List all components (machines, refinements, implementations) in a project

Typecheck a B component to verify syntax and type correctness

B0 check a B component to verify it is B0 compliant (required before C code generation)

Generate proof obligations for a B component

Run automatic prover on a B component. Force levels: 0-3 (auto), 10-13 (forced), -1 (fast), -2 (replay)

Get proof status of a component or entire project

List B source files in the workspace. Supports filtering by project and extension (.mch, .ref, .imp, .erf, etc.)

Read the content of a B source file (.mch, .ref, .imp, etc.), C code (.c, .h), or Makefile from the workspace. Content is returned verbatim. For a .pmi file, a 'po_labels' list names the proof obligation each entry of its flat theories (ProofState, MethodList, PassList) belongs to; those entries carry no operation name of their own, so do not try to infer it from their position.

Write or update the content of a B source file (.mch, .ref, .imp, etc.), C code (.c, .h), or Makefile in the workspace. Creates a backup by default.

Get the directory structure of a B project showing files and subdirectories

Create a new Atelier B project in the workspace with bdp, lang, and src subdirectories

Add a new B component (machine, refinement, or implementation) to a project. Creates the file in src/ with a template and registers it with Atelier B.

Remove a component from an Atelier B project. Optionally delete the source file from disk.

Remove an Atelier B project. WARNING: If delete_files is true, permanently deletes all project files!

Generate C code for a single B component (implementation or basic machine). Output goes to lang/c directory.

Generate C code for a complete B project from a toplevel component. Output goes to lang/c directory.