project-everest/vale

This system is a formal verification toolchain, primarily named Vale, designed to verify low-level code and hardware architectures. It compiles specifications into F* and Dafny, supporting architectures like x86_64 and PowerPC, and includes utilities for build management, documentation, and testing.

This period marks the initial release of the Vale verification tool, establishing the core build system, cross-platform scripts, and essential documentation. It also introduces the Vale compiler to F*, along with supporting tooling for Dafny, Kremlin, and automated release management.

8 changes

This period focused on expanding the Vale compiler's formal verification capabilities to support multiple hardware architectures, specifically x86_64 and PowerPC. The work involved defining architectural specifications, implementing instruction semantics, and creating test suites to ensure correctness across these platforms. Additionally, infrastructure improvements were made to support building and testing within Docker and parsing F* type definitions.

8 changes

This period focused on expanding the project's formal verification capabilities by introducing an interactive Python-based verification tool and migrating documentation to Read the Docs. Concurrently, the codebase added simplified x64 architecture definitions and full PowerPC 64-bit Little-Endian support to enable formal verification for a broader range of hardware targets.

4 changes

project-everest/vale was measured the same way every project in this corpus was: the same rubric, at a pinned commit, with the result published in full. Point the surveyor at a repository you know and see whether you agree with it.