The following directories contain Vale and related tools:
- tools/Vale/src: Vale
- tools/Vale/test: test files for Vale
- tools/Dafny: Dafny binaries built from https://github.com/Microsoft/dafny
- tools/Kremlin: Interface to Kremlin
The following directories contain library code verified by Dafny and Vale:
- dafny/specs/lib and dafny/code/lib: general-purpose libraries for Dafny
- dafny/specs/arch and dafny/code/arch: definitions of assembly language architectures (x86, x64, ARM)
- dafny/code/test: test files for libraries and architecture code
Files in dafny/specs are specification files that are part of the trusted computing base. Files in dafny/code contain verified code that is not part of the trusted computing base. Files in dafny/specs should not depend on files in dafny/code.
Building Vale will create the following additional directories; all files generated by the build should be in these directories:
- obj
- bin