fstarverifier

Invocation

This skill is used when:

• Verifying F* (.fst) or interface (.fsti) files
• Debugging verification failures
• Checking proof completeness

Core Operations

Basic Verification

# Verify a single file
fstar.exe Module.fst

# With Pulse extension
fstar.exe --include <PULSE_HOME>/out/lib/pulse Module.fst

# With include paths
fstar.exe --include <PULSE_HOME>/out/lib/pulse --include path/to/lib Module.fst