specreview

Name: specreview
Availability: InStock
Author: FStarLang

Review F* and Pulse specifications for weak or missing correctness guarantees.

8|4|Updated Mar 25, 2026

Search Tags:#verification #postconditions #specification review #pulse #fstar #interface audit

Ready to run

npx skills add https://github.com/FStarLang/proof-copilot --skill specreview

💬 Prompt for ChatGPT / Claude Chat▼

Please help me install this Agent Skill.
Skill: specreview
Source: https://github.com/FStarLang/proof-copilot/tree/main/plugins/proof-copilot/skills/specreview
Command: npx skills add https://github.com/FStarLang/proof-copilot --skill specreview

SYSTEM DOCUMENTATION & REQUIREMENTS

What problem does it solve?

This Skill helps you review F* and Pulse specifications so they prove real functional correctness instead of only type safety or shallow structural properties.

Core Features & Use Cases

Postcondition Auditing: Check whether exported functions expose meaningful requires and ensures clauses.
Specification Strength Review: Detect weak postconditions that do not connect implementations to their pure models.
Interface Verification: Inspect .fsti files to confirm callers can rely on the documented correctness properties.
Use Case: If a sorting function only guarantees a sorted result, this Skill helps you strengthen the spec so it also proves the output is a permutation of the input.

Quick Start

Ask the specreview skill to audit this F* module’s interface and point out any weak or missing specifications.

Frequently Asked Questions about specreview

High-intent search queries and answers about installing and using this skill.

FAQPage Schema

How do I review F* specifications for weak postconditions?▼

Weak postconditions in F* specifications are detected by auditing exported functions to ensure requires and ensures clauses connect implementations to pure models, proving functional correctness beyond shallow type safety.

What is a specification strength review in Pulse?▼

A specification strength review in Pulse evaluates whether exported functions expose meaningful preconditions and postconditions, ensuring caller-usable spec-level properties prove functional correctness rather than just structural properties.

How do I audit F* interface files for missing correctness guarantees?▼

Auditing F* interface files for missing correctness guarantees involves inspecting .fsti files to confirm callers can rely on documented properties and that exported preconditions and strong postconditions are present.

Can I check implementation-to-specification consistency in verified F* codebases?▼

Yes, you can check implementation-to-specification consistency in verified F* codebases by reviewing whether specifications prove real functional correctness and applying postcondition analysis to detect weak or missing guarantees.

When do I need to strengthen F* specs beyond type safety?▼

You need to strengthen F* specs beyond type safety when a function's postcondition only guarantees shallow structural properties, such as a sorting function proving a sorted result without proving it is a permutation of the input.

What are the limitations of relying on type safety instead of F* postconditions?▼

Relying on type safety instead of F* postconditions limits verified codebases to shallow structural properties, failing to prove real functional correctness or provide caller-usable spec-level properties for interface audits.