Website updates and fixes

docs/app/layout.tsx

@@ -18,7 +18,7 @@ export const metadata = {
   },
   twitter: {
     card: 'summary_large_image',
-    creator: '@informalsystems',
+    creator: '@quint_lang',
     images: [`${SITE_CONFIG.siteUrl}/og.jpg`],
   },
 }
@@ -37,7 +37,19 @@ const navbar = (
         />
       </svg>
     }
-  />
+  >
+    <a
+      href="https://x.com/quint_lang"
+      target="_blank"
+      rel="noreferrer"
+      aria-label="Quint on X"
+      className="x:text-current"
+    >
+      <svg width="24" height="24" viewBox="0 0 24 24" fill="currentColor">
+        <path d="M18.244 2.25h3.308l-7.227 8.26 8.502 11.24H16.17l-5.214-6.817L4.99 21.75H1.68l7.73-8.835L1.254 2.25H8.08l4.713 6.231zm-1.161 17.52h1.833L7.084 4.126H5.117z" />
+      </svg>
+    </a>
+  </Navbar>
 )
 
 const footer = (

docs/components/ToolCards.tsx

@@ -0,0 +1,48 @@
+const tools = [
+  {
+    title: 'Quint LLM Kit',
+    href: 'https://github.com/informalsystems/quint-llm-kit',
+    description: (
+      <>
+        AI agents and commands that help you generate and iterate on Quint specs.
+        Run <code className="text-sm bg-gray-100 dark:bg-neutral-800 px-1.5 py-0.5 rounded">/spec:next</code> to
+        get guided suggestions at any point in your journey.
+      </>
+    ),
+  },
+  {
+    title: 'Quint Connect',
+    href: 'https://github.com/informalsystems/quint-connect',
+    description:
+      'Model-based testing framework for Rust. Automatically validate your implementation against your Quint spec by replaying generated test traces.',
+  },
+  {
+    title: 'Quint Trace Explorer',
+    href: 'https://github.com/informalsystems/quint-trace-explorer',
+    description:
+      'Terminal UI for navigating execution traces. Highlights state changes to make it easy to understand what has happened.',
+  },
+]
+
+export function ToolCards() {
+  return (
+    <div className="not-prose grid gap-6 mt-8 sm:grid-cols-3">
+      {tools.map((tool) => (
+        <a
+          key={tool.title}
+          href={tool.href}
+          target="_blank"
+          rel="noreferrer"
+          className="group rounded-xl border border-gray-200 dark:border-neutral-700 p-6 transition hover:border-quint-purple hover:shadow-lg"
+        >
+          <h3 className="text-xl font-semibold group-hover:text-quint-purple transition">
+            {tool.title}
+          </h3>
+          <p className="mt-2 text-zinc-600 dark:text-zinc-300">
+            {tool.description}
+          </p>
+        </a>
+      ))}
+    </div>
+  )
+}

docs/components/home/index.tsx

@@ -16,6 +16,7 @@ import { classNames } from './classNames'
 import { ProsOrConsList } from './ProsOrConsList'
 import { ProjectsGridCompact } from './ProjectsGridCompact'
 import { projects } from '../../data/projects'
+import { ToolCards } from '../ToolCards'
 
 const benefits = [
   [
@@ -165,6 +166,13 @@ export function Home() {
             </Link>
           </div>
 
+          <div className="mx-auto max-w-6xl mt-20 mb-8">
+            <h2 className="text-4xl text-center font-bold leading-tight">
+              Try some <span className="text-quint-purple">tools</span> built for Quint
+            </h2>
+            <ToolCards />
+          </div>
+
           <NewsletterSignupBanner />
         </div>
       </section>

docs/content/docs/checking-properties.mdx

@@ -214,7 +214,7 @@ Quint will call Apalache 2-3 times (depending on whether an ordinary invariant w
 
 ### Examples
 
-Check out the blog post [How to write Inductive Invariants](/posts/inductive-invariants) to learn more, and the following examples which include inductive invariants.
+Check out the blog post [How to write Inductive Invariants](/posts/inductive_invariants) to learn more, and the following examples which include inductive invariants.
 - The algorithm from Lamport's Teaching Concurrency paper: [teaching.qnt](https://github.com/informalsystems/quint/blob/main/examples/classic/distributed/TeachingConcurrency/teaching.qnt)
 - Incrementing a shared counter with a mutex: [mutex.qnt](https://github.com/informalsystems/quint/blob/main/examples/classic/distributed/TeachingConcurrency/mutex.qnt)
 - The folklore reliable broadcast protocol explained in the blog post: [reliablebc.qnt](https://github.com/informalsystems/quint/blob/main/examples/classic/distributed/ReliableBroadcast/reliablebc.qnt)

docs/content/docs/getting-started.mdx

@@ -1,5 +1,6 @@
 import { Steps, Tabs, Callout } from 'nextra/components'
 import Image from 'next/image'
+import { ToolCards } from '../../components/ToolCards'
 
 # Getting Started
 
@@ -29,10 +30,14 @@ Welcome to Quint! In this short guide, we'll cover everything from installation
  If you have [Nix](https://nixos.org/) installed, you can obtain a shell with Quint and all its dependencies installed by running:
 
  ```sh
- nix-shell -p quint
+ nix shell "github:NixOS/nixpkgs#quint"
  ```
 
- Note that the release cycle with Nix is slower than with other alternatives, so latest features might not be available.
+ Exiting the shell will remove `quint` from your `PATH`. If you want to keep it, run:
+
+ ```sh
+ nix profile add "github:NixOS/nixpkgs#quint"
+ ```
 
  The Nix package is a great option to use in the CI.
  </Tabs.Tab>
@@ -99,6 +104,10 @@ au BufNewFile,BufReadPost *.qnt runtime syntax/quint.vim
 
 ### Write a specification
 
+<Callout>
+**Prefer AI assistance?** The [Quint LLM Kit ↗](https://github.com/informalsystems/quint-llm-kit) provides Claude Code agents and commands that help you generate Quint specs from existing code or documentation. Run `/spec:next` to get guided suggestions at any point.
+</Callout>
+
 In order to run Quint, we first need a specification. Let's use this simple bank specification, which has a bug.
 
 ```quint
@@ -188,3 +197,7 @@ This will verify all possible executions of up to 10 steps. We can be confident
 </Steps>
 
 That's it! Now that you have the tools and know the workflow, you might want to learn how to write your own specs! Check out the Quint [Lessons](/docs/lessons) and [Examples ↗](https://github.com/informalsystems/quint/tree/main/examples).
+
+## Other tools built for Quint
+
+<ToolCards />

docs/style.css

@@ -57,6 +57,25 @@ dd {
   font-size: 1rem;
 }
 
+/* Purple callouts */
+.nextra-callout.x\:border-orange-100 {
+  border-color: #ddd6fe;
+  background-color: #ede9fe;
+  color: #4c1d95;
+}
+
+:is(html[class~="dark"] .nextra-callout.x\:dark\:border-orange-400\/30) {
+  border-color: rgba(157, 108, 229, 0.3);
+  background-color: rgba(157, 108, 229, 0.2);
+  color: #c4b5fd;
+}
+
+/* Nextra Tabs generates hidden h3 elements for each tab panel, which
+   incorrectly increment the Steps component's counter. Prevent that. */
+.nextra-steps h3[style*="visibility:hidden"] {
+  counter-increment: var(--counter-id) 0;
+}
+
 /* Nextra component is adding the margin twice, so I cancel it here */
 [role="tabpanel"].x\:mt-6 {
   margin-top: -1.5rem !important;