B3

B3 is an intermediate verification language (IVL). Like other IVLs (for example, Boogie 2, Why3, and Viper), B3 provides a natural way to express proof obligations that arise in deductive program verification. More generally, a translation from a programming language into B3 can capture the semantics of that language.

B3 improves on Boogie 2 in two major ways:

• The B3 language is streamlined for the kinds of encoding tasks that the Dafny-to-Boogie translation developed over the course of 15+ years. For example, B3 has check statements ("check and forget"), injective modifiers for function parameters, and various "breadcrumbs" that can be used to report detailed error messags.

• The B3 verifier is designed, from the ground up, with proof stability in mind. For example, the verifier uses symbolic execution without joins, so the "then" and "else" branches of a conditional statement are never considered together. Any temporary names introduced in that process are generated independently for the two branches. Also, the verifier introduces types, functions, and axioms into the verification context lazily. This reduces the size of the proof context, which experience shows has a positive effect on proof stability.

B3 is implemented in Dafny, so its code is verified (up to the given specifications). The build scripts compile the B3 tool to both .NET and Java. Internally, B3 makes calls to an SMT solver; currently, Z3 and CVC5 are supported.

View and build

To view and edit the sources, open this folder with VS Code.

To manage the project from the command line, see the Makefile. For example, to verify the code, run

make verify

You'll need Dafny version 4.11.

Run

After successfully running make build (which calls dafny build src/dfyconfig.toml --output bin/b3), you can run B3 like

>  bin/b3 verify MyProgram.b3

(for example, try test/verifier/basics.b3 as the MyProgram.b3).

If you want to link to B3 from your own program verifier, you may prefer to create a B3 AST directly, rather than calling B3 as a separate process. The Makefile has targets for building B3 for both .NET (the default) and Java. (Dafny has compilers to also target languages, too. To use any of them, you need to implement class OSProcess for that language.) To run B3 under the JVM, build it with make build-java and then do

>  CLASSPATH=target/java/bin/b3.jar java b3 verify MyProgram.b3

B3 supports Z3 and CVC5 as its underlying SMT engine. Select between the two with --z3 (default) or --cvc5.

B3 documentation

The main documentation for B3 is its language reference language, This is B3.

The original B3 concept document gives some thinking and motivation. Note, however, that the language has evolved, so the concept document does not always describe what is implemented.

Other documents for B3 contributors are available in the doc folder.

Tests

The B3 test suite depends on LLVM lit and OutputCheck. Install them by using the following command and run the test suite by make lit.

brew install pipx
pipx install lit==18.1.8
pipx install OutputCheck

Tool stages

• Parser: input characters -> raw AST -- RawAst.WellFormed says whether or not raw AST is well-formed, but doesn't give good error messages
• Resolver: raw AST -> resolved AST -- generates a good error message if RawAst.WellFormed does not hold -- ensures Ast.WellFormed
• TypeChecker: operates on a well-formed resolved AST -- check if AST is type correct -- ensures TypeCorrect
• StaticConsistency: operates on a well-formed resolved AST -- statically enforce additional consistency conditions
• Verifier: resolved AST -> calls to RSolver.{Extend,Prove}
• Semantics: gives co-inductive big-step semantics for raw AST (note, this file is being rewritten to incorporate new features and to apply to the resolved AST)