# This is B3

B3 is an _intermediate verification language_ (IVL). It is used to prescribe proof obligations,
primarily those of interest in an automated deductive verifier for a source programming language.

B3 is an open-source project on [github](https://github.com/dafny-lang/b3).


```{toctree}
:maxdepth: 2
:caption: Contents:
motivation
examples
syntax
top-level-decls
statements
expressions
semantics
```