verified-pseudocode-extractor
Extracts human-readable pseudocode from a verified formal artifact (Dafny, Lean, TLA+) while preserving the verified properties as annotations, so the proof-carrying logic can be reimplemented in a production language. Use when porting verified code to an unverified target, when documenting what a formal spec actually does, or when handing a verified algorithm to an implementer.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill verified-pseudocode-extractor90
Quality
88%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
85%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is a strong, well-crafted description for a specialized skill. It excels at specificity and completeness with a clear 'Use when' clause covering multiple scenarios. The main weakness is that trigger terms are heavily technical, which may be appropriate for the target audience but could miss users who phrase requests more casually.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Extracts human-readable pseudocode', 'preserving verified properties as annotations', and specifies source formats (Dafny, Lean, TLA+) with clear purpose (reimplementation in production language). | 3 / 3 |
Completeness | Clearly answers both what (extracts pseudocode from formal artifacts while preserving verified properties) AND when with explicit 'Use when' clause covering three distinct scenarios: porting verified code, documenting formal specs, and handing algorithms to implementers. | 3 / 3 |
Trigger Term Quality | Includes some relevant technical terms (Dafny, Lean, TLA+, pseudocode, formal spec, verified code) but these are specialized jargon. Missing more natural variations users might say like 'convert proof', 'translate formal code', or 'proof to code'. | 2 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification tools (Dafny, Lean, TLA+) specifically. Very unlikely to conflict with general code translation or documentation skills due to the specialized domain focus on proof-carrying logic. | 3 / 3 |
Total | 11 / 12 Passed |
Implementation
92%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a high-quality skill that efficiently teaches pseudocode extraction from verified code. The mapping table provides instant reference, the worked example demonstrates exactly what output should look like, and the 'Do not' section prevents common mistakes. The only minor weakness is that all content is inline rather than using progressive disclosure for the TLA+ variant or extended examples.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude's competence with formal verification languages. No unnecessary explanations of what Dafny/Lean/TLA+ are or how verification works—it jumps straight to actionable mapping tables and examples. | 3 / 3 |
Actionability | Provides a complete worked example with real Dafny code and its corresponding pseudocode output. The mapping table is concrete and copy-paste ready, and the output format template is fully specified. | 3 / 3 |
Workflow Clarity | The workflow is implicit but crystal clear: identify constructs → apply keep/drop rules → annotate inline at point-of-use → format output. The 'Do not' section serves as validation checkpoints for common errors. | 3 / 3 |
Progressive Disclosure | Content is well-organized with clear sections (mapping table, worked example, TLA+ variant, do-nots, output format), but it's a moderately long single file. The reference to 'python-to-dafny-translator' is good, but some content like the TLA+ section could potentially be split out for complex use cases. | 2 / 3 |
Total | 11 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.