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 and cryptographic code verified by Dafny and Vale:
- src/lib: general-purpose libraries for Dafny
- src/arch: definitions of assembly language architectures (x86, x64, ARM)
- src/crypto: verified cryptographic code
- src/test: test files for libraries, architecture code, and cryptography code
Dafny files with a suffix .s.dfy are specification files that are part of the trusted computing base. Dafny files with a suffix .i.dfy and Vale files contain verified code that is not part of the trusted computing base.
Building Vale will create the following additional directories; all files generated by the build should be in these directories:
- obj
- bin