<Devsly/>
NotebookLM Watermark Remover
Remove the NotebookLM watermark from PDF slide exports — free, unlimited, and 100% in your browser.
View
NotebookLM Video Watermark Remover
Remove the NotebookLM watermark from every frame of your MP4 and auto-trim the end card — free and unlimited.
View
Gemini Watermark Remover
Remove the Gemini (Veo) sparkle watermark from every frame of your AI-generated MP4 — free and unlimited.
View
MCP https://devsly.io/mcp MCP Tools Best Skills API Docs

Keyboard Shortcuts

Navigation

Quick Search
⌘ / Ctrl + K
Toggle Dark Mode
⌘ / Ctrl + D
Close Dialogs
Esc

Tool Actions

Execute / Process
⌘ / Ctrl + Enter
Clear Input
⌘ / Ctrl + Shift + C
Copy Output
⌘ / Ctrl + Shift + X

Editor

Select All
⌘ / Ctrl + A
Undo
⌘ / Ctrl + Z
Redo
⌘ / Ctrl + Shift + Z

Updated 3mo ago

by younes-io

agent-skills

agentic skills to write TLA+ specs or TLAPS proofs

21 GitHub stars (21)

Steady at 21 stars — no new stars in the 16 days since Sep 30.

  • 2 skills (2 skills found in its SKILL.md files)
  • 0 forks (0 forks)
  • 3mo ago last update (Last updated 3mo ago)

Install

Skills CLI

npx skills add younes-io/agent-skills

Asks which skills and agents to install. Just one: npx skills add younes-io/agent-skills --skill tla-check — add -g for every project.

Claude Code

git clone https://github.com/younes-io/agent-skillscp -r "agent-skills/skills/tla-check" ~/.claude/skills/

Copies the tla-check skill into ~/.claude/skills/ for every project (use .claude/skills/ for one project). Repeat for the other skills listed below.

Plugin

/plugin marketplace add younes-io/agent-skills

Run inside Claude Code if the repository ships a plugin marketplace, then pick plugins from /plugin.

Skills can run code on your machine — read the SKILL.md first.

What it does

In the author's own words, from each skill's SKILL.md.

  • tla-check

    Write and iteratively refine executable TLA+ specs (.tla) and TLC model configs (.cfg) from natural-language system designs; run TLC model checking; summarize pass/fail and counterexamples with explicit assumptions and bounds. Use when asked to design or validate a protocol/state machine, create or edit .tla/.cfg files, run TLC, or interpret TLC failures.

    skills/tla-check/SKILL.md on GitHub (opens in a new tab)
  • tla-proof

    Write and iteratively refine TLA+ theorem proofs in `.tla` modules with TLAPS (`tlapm`); run proof checks and summarize proved vs failed/omitted obligations with explicit assumptions and trust boundaries. Use when asked to create or fix `THEOREM` or `PROOF` blocks, diagnose TLAPS failures, strengthen inductive invariants, prove equivalence, or tune proof structure.

    skills/tla-proof/SKILL.md on GitHub (opens in a new tab)

Review before you install

A skill is a set of instructions and scripts your agent will follow, and it can run code on your machine. Read the SKILL.md and any scripts first — this listing is not a security review.