AGENT SKILL

component-sync-specs

Ensure a component implementation is synchronized with its specifications.

01 前言 Front Matter

name: component-sync-specs
description: Ensure a component implementation is synchronized with its specifications.

For each component identified in $ARGUMENTS, run the following:

Synchronize Spin/Promela models with current source code and re-verify

Create a new Spin/Promela formal verification model for a system property

Install the Creusot Rust verification tool

Prepare an existing Cargo project to use Creusot formal verification

Add Coq 8.20 as an additional prover to an existing Creusot installation, for verification conditions that SMT solvers cannot discharge

Formally verify a component's properties with Creusot and annotate its interface definitions