# VmMemory verification

The default build imports every `*/Spec.lean` module here; each states its exact
contracts and preconditions. The root Makefile lists the extracted functions.
Specifications that call into the kernel assume the system-call contracts in
[Syscalls/Linux.lean](../Syscalls/Linux.lean).

Not verified:
- Guest-memory access, descriptor cloning, formatting, and serialization.
- `FileBackedMappingParameters::open`, modeled by an opaque result.

See the root README for [build and extraction](../README.md#build-and-extraction)
and the [trust boundary](../README.md#trust-boundary).