SNNV
====

.. raw:: html

   <div class="hero-banner">
     <h1>SNNV</h1>
     <p>Sound set-based robustness verification for first-to-fire (F2F) Leaky
        Integrate-and-Fire spiking neural networks. The spiking star set separates
        temporal spike patterns from affine propagation, enabling star-set
        reachability without exhaustive latency enumeration.</p>
     <div class="hero-badges">
       <span class="hero-badge">Python 3.10+</span>
       <span class="hero-badge">PyTorch / snnTorch</span>
       <span class="hero-badge">Star-set reachability</span>
       <span class="hero-badge">HiGHS LP</span>
       <span class="hero-badge">MNIST / F-MNIST / CIFAR-10 / GTSRB</span>
     </div>
   </div>

   <div class="feature-grid">
     <a class="feature-card" href="core_idea.html">
       <div class="feature-card-icon icon-blue">
         <svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="10"/><line x1="12" y1="8" x2="12" y2="12"/><line x1="12" y1="16" x2="12.01" y2="16"/></svg>
       </div>
       <div class="feature-card-title">The Core Idea</div>
       <div class="feature-card-desc">Why SNN verification is hard, and the spiking-star insight that makes it tractable.</div>
     </a>
     <a class="feature-card" href="spike_star.html">
       <div class="feature-card-icon icon-purple">
         <svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><polygon points="12 2 2 7 12 12 22 7 12 2"/><polyline points="2 17 12 22 22 17"/><polyline points="2 12 12 17 22 12"/></svg>
       </div>
       <div class="feature-card-title">How Spike Star Works</div>
       <div class="feature-card-desc">Generalized star sets, F2F encoding, spike patterns, effective synapses, affine propagation, adaptive latency splitting.</div>
     </a>
     <a class="feature-card" href="playground.html">
       <div class="feature-card-icon icon-orange">
         <svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M12 20h9"/><path d="M16.5 3.5a2.12 2.12 0 0 1 3 3L7 19l-4 1 1-4z"/></svg>
       </div>
       <div class="feature-card-title">Interactive Playground</div>
       <div class="feature-card-desc">Drag the input star (box or zonotope); watch the latency cells, membrane envelopes, score enclosure, and robustness verdict update live.</div>
     </a>
     <a class="feature-card" href="results.html">
       <div class="feature-card-icon icon-green">
         <svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><line x1="18" y1="20" x2="18" y2="10"/><line x1="12" y1="20" x2="12" y2="4"/><line x1="6" y1="20" x2="6" y2="14"/><line x1="2" y1="20" x2="22" y2="20"/></svg>
       </div>
       <div class="feature-card-title">Benchmark Results</div>
       <div class="feature-card-desc">Per-case browser over MNIST / Fashion-MNIST / CIFAR-10 / GTSRB, with SMT-baseline comparison.</div>
     </a>
     <a class="feature-card" href="setup.html">
       <div class="feature-card-icon icon-blue">
         <svg viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><polyline points="16 18 22 12 16 6"/><polyline points="8 6 2 12 8 18"/></svg>
       </div>
       <div class="feature-card-title">Getting Started</div>
       <div class="feature-card-desc">Install with uv and run the first-to-fire reachability demo.</div>
     </a>
   </div>

.. toctree::
   :hidden:
   :maxdepth: 1

   core_idea
   spike_star
   playground
   results
   setup