| name | discover-systems-theory |
| description | Automatically discover eBPF, compiler, programming language theory, information retrieval, and formal verification skills when working with kernel tracing, parsers, type systems, Z3, Lean, or theorem proving |
| license | MIT |
| metadata | {"author":"rand","version":"4.0"} |
| compatibility | {"claude-code":">=1.0.0"} |
Systems Theory & Language Design Skills Discovery
When This Skill Activates
- eBPF, kernel tracing, XDP, kprobes, BPF
- Compilers, parsers, interpreters, AST, bytecode
- Type systems, type theory, programming language design
- LLVM, IR, SSA, code generation, optimization passes
- Information retrieval, search, ranking, vector search
- Formal verification, theorem proving, model checking
- SAT, SMT, Z3, Lean, constraint solving
Available Skills (32 total)
eBPF (4 skills)
- ebpf-fundamentals - eBPF programs, verifier, maps
- ebpf-networking - XDP, TC, socket filtering
- ebpf-security-monitoring - LSM hooks, syscall tracing
- ebpf-tracing-observability - kprobes, tracepoints, profiling
Information Retrieval (5 skills)
- ir-search-fundamentals - Indexing, tokenization, TF-IDF, BM25
- ir-query-understanding - Query parsing, expansion, intent
- ir-ranking-reranking - Learning to rank, cross-encoders
- ir-vector-search - Embeddings, ANN, HNSW, FAISS
- ir-recommendation-systems - Collaborative/content-based filtering
Programming Language Theory (13 skills)
- type-systems - Type theory, inference, polymorphism
- lambda-calculus - Lambda calculus, reduction, Church encodings
- curry-howard - Propositions as types, proofs as programs
- dependent-types - Dependent types, refinement types
- operational-semantics - Small-step, big-step semantics
- program-verification - Hoare logic, invariants, correctness
- structure-editors - Structural editing, projectional editors
- hazelnut-calculus - Hazelnut typed holes calculus
- live-programming-holes - Live programming with typed holes
- typed-holes-foundations - Typed holes theory and foundations
- typed-holes-interaction - Interactive typed hole filling
- typed-holes-llm - LLM-powered typed hole completion
- typed-holes-semantics - Typed holes formal semantics
Formal Methods (10 skills)
- z3-solver-basics - Z3 SMT solver, constraints, assertions
- sat-solving-strategies - SAT solving, DPLL, CDCL
- smt-theory-applications - SMT theories, bitvectors, arrays
- lean-proof-basics - Lean 4 basics, tactics, terms
- lean-tactics - Advanced Lean tactics and automation
- lean-theorem-proving - Theorem proving patterns in Lean
- lean-mathlib4 - Mathlib4 library usage
- csp-modeling - Constraint satisfaction problems
- constraint-propagation - Arc consistency, propagation
- backtracking-search - Backtracking, branch and bound
Load Full Category Details
Read ../ebpf/INDEX.md
Read ../ir/INDEX.md
Read ../plt/INDEX.md
Read ../formal/INDEX.md
Progressive Loading
- Level 1: This gateway loads automatically (~70 lines)
- Level 2: Load category INDEX.md for full skill listings
- Level 3: Load specific skills as needed
