PAL is a verification framework that lets you write C and prove it correct.
You annotate standard C code with contracts -- preconditions, postconditions,
loop invariants, ownership disciplines -- using macros from pal.h, and PAL
handles the rest: it transpiles the annotated source into
Pulse (a separation-logic-based
verification language built on F*),
where the proofs are discharged automatically by the type checker.
The result is a single C codebase that both compiles with any standard C
compiler and carries machine-checked correctness proofs. When C2PULSE is
not defined, all annotations vanish -- the code is plain C.
#include "pal.h"
void swap(int *x, int *y)
_ensures(*y == _old(*x) && *x == _old(*y))
{
int tmp = *y;
*y = *x;
*x = tmp;
}The _ensures annotation states the postcondition: after swap returns,
the values are exchanged. PAL translates this into a Pulse function whose
type encodes that contract. F*/Pulse type-checks the generated code -- if
it passes, the implementation satisfies the spec. More availabe at examples/.
| What | Version | Why |
|---|---|---|
| Clang / LLVM | 20.x (CI uses llvm.sh 20, currently 20.1.8) |
libclang parses C |
| LLVM dev headers | 20.x | llvm-config, libclang-cpp20-dev, libclang-20-dev |
| g++ | recent | builds the C++ FFI (cpp/impl.cpp) |
| Rust | 2024 edition | compiles the PAL binary |
| F*/Pulse | nightly 2026-06-04 | verifies generated .fst output |
These are the same steps CI runs
(see .github/workflows/ci.yml):
# Clang 20 + LLVM dev packages
wget https://apt.llvm.org/llvm.sh
chmod +x llvm.sh
sudo ./llvm.sh 20
sudo apt update
sudo apt install -y clang-20 libclang-cpp20-dev g++ clang-tools-20 libclang-20-dev
# F*/Pulse nightly (pinned to the version CI uses)
./opt/install-fstar.sh --link-dir /usr/local/bin
# Rust (skip if already installed)
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | shllvm-config (or llvm-config-20) must be on PATH -- the build script
calls it to find LLVM libraries.
make # Rust binary + Pulse support library
make test -j8 # translate every test case, verify with F*
cd test/swap && make # one test
cargo run -- --print-ir test/swap/swap.c # just the IR82 test directories, each a C file that PAL translates and F*/Pulse
verifies. Create a new one with ./test/new.sh my_test.
cargo run -- -o out/ myfile.c # emit .fst files
cargo run -- --print-ir myfile.c # dump IR, no files written
cargo run -- --time-passes -o out/ myfile.c # per-pass timingpal [OPTIONS] <FILES>...
-o, --outdir <DIR> where to write .fst output
-I <PATH> extra include search paths
--print-ir print IR and exit
--time-passes show per-pass timing
-q, --quiet suppress diagnostics on stderr
--tmpdir <DIR> directory for intermediates
Detailed references live in doc/:
| Document | Covers |
|---|---|
| Surface syntax | Full annotation reference: contracts, ownership, refinements, ghost code, Pulse interop |
| Structs | What PAL emits per struct and union: generated types, predicates, fold/unfold, field projections |
| Internals | Pipeline passes, IR design, Zngur FFI, diagnostics, output structure, Pulse support library |
| doc/README.md | Documentation index: how to write specs, how C data is modeled in Pulse |