seqra/formal-spec

Latest recorded source activity: October 19, 2026 at 21:45

SkillsMP catalog refreshed: October 29, 2026 at 18:30

skills collected: 1

GitHub stars: 1
GitHub forks: 0

Install with an AI assistant

Copy this prompt into the AI assistant you're using.

Follow https://skillsmp.com/skill-install/prompt.md to install Agent Skills from https://github.com/seqra/formal-spec.

Repository README

Repository README source: README.md

Read the source README

Expand full README

# formal-spec <p align="center"> <img src="assets/cover.svg" alt="formal-spec: Spec-as-code" width="960"> </p> A skill that gives coding agents a structured way to reason before implementing. Write a model and an independent specification. State the proof obligations that connect them and prove them in Lean. Then derive tests and implement through TDD. Use it for behavior where mistakes could harm users, data, money, or access. Proofs cover the model and its assumptions; tests check the implementation. <p align="center"> <img src="assets/workflow.svg" alt="Spec-as-code: specify the behavior, prove the model, derive tests, implement through TDD." width="960"> </p> Install: ```sh npx skills add seqra/formal-spec ``` Then ask your agent: **“Work proof-first on this change.”** [Skill](skill/SKILL.md) · [Workflow](skill/references/workflow.md) · [Examples](demo/README.md) Apache-2.0. See [LICENSE](LICENSE).

Loading the repository README…

Posts

See all →

Aleksandr Misonizhnik

@seqradevOct 23, 2026 06:39 UTC

Skill release postCoordinate agent tasks

Post summary

formal-spec makes an agent reason through formal methods: model the behavior, write an independent spec and proof obligations, check them in Lean, then derive tests and implement through TDD.

Original post

View Skill details · formal-spec/skill

Skills in this repository

classification pending

skill

occupation

description

updated

formal-spec

unclassified

Structure agent reasoning about consequential behavior with a model, independent specification, proof obligations, and Lean proofs, then derive tests and implement through TDD. Skip cosmetic changes.

2026-10-19

Showing 1 of 1 collected skill.