diff --git a/docs/components/home/ProsOrConsList.tsx b/docs/components/home/ProsOrConsList.tsx
new file mode 100644
index 000000000..38ddc8729
--- /dev/null
+++ b/docs/components/home/ProsOrConsList.tsx
@@ -0,0 +1,53 @@
+import { ComponentProps } from "react";
+import { twMerge } from "tailwind-merge";
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { faCheck, faXmark } from '@fortawesome/free-solid-svg-icons'
+import { classNames } from "./classNames";
+
+interface ProsOrConsListProps extends ComponentProps<"div"> {
+  items: Readonly<string[]>;
+  label: string;
+  type: "pro" | "con";
+}
+
+export function ProsOrConsList({ items, label, type }: ProsOrConsListProps) {
+  const pluralType = `${type}s`;
+
+  return (
+    <div
+      className={twMerge(
+        classNames.prosOrConsContainer,
+        classNames[`${pluralType}Container`]
+      )}
+    >
+      <div
+        className={twMerge(
+          classNames.prosOrConsLabel,
+          classNames[`${pluralType}Label`]
+        )}
+      >
+        {label}
+      </div>
+
+      {items.map((item) => (
+        <div
+          className={twMerge(
+            classNames.proOrConContainer,
+            classNames[`${type}Container`]
+          )}
+          key={item}
+        >
+          <div
+            className={twMerge(
+              classNames.proOrConIcon,
+              classNames[`${pluralType}Icon`]
+            )}
+          >
+            <FontAwesomeIcon icon={type === "pro" ? faCheck : faXmark} />
+          </div>
+          {item}
+        </div>
+      ))}
+    </div>
+  );
+}
diff --git a/docs/components/home/classNames.ts b/docs/components/home/classNames.ts
new file mode 100644
index 000000000..e4258957b
--- /dev/null
+++ b/docs/components/home/classNames.ts
@@ -0,0 +1,87 @@
+export const classNames = {
+  container: `
+    flex
+    flex-col
+    gap-6
+  `,
+
+  benefitContainer: `
+    flex
+    flex-col
+    gap-2
+  `,
+
+  benefitTitle: `
+    text-2xl
+    flex
+    items-center
+    gap-2
+  `,
+
+  benefitIcon: `
+    text-quint-purple
+    w-8
+  `,
+
+  prosAndConsContainer: `
+    flex
+    ml-4
+  `,
+
+  prosOrConsContainer: `
+    px-6
+    py-3
+    flex
+    flex-col
+    gap-2
+    w-full
+  `,
+
+  prosContainer: `
+    bg-quint-purple/10
+    rounded-l-xl
+  `,
+
+  consContainer: `
+    bg-quint-orange/10
+    rounded-r-xl
+  `,
+
+  prosOrConsLabel: `
+    font-bold
+  `,
+
+  prosLabel: `
+    text-quint-purple
+  `,
+
+  consLabel: `
+    text-quint-orange
+  `,
+
+  proOrConContainer: `
+    grid
+    grid-cols-[min-content,auto]
+    gap-2
+    w-full
+  `,
+
+  proContainer: `
+  `,
+
+  conContainer: `
+  `,
+
+  proOrConIcon: `
+    col-start-1
+    col-end-2
+  `,
+
+  proIcon: `
+    text-violet-400
+  `,
+
+  conIcon: `
+    text-amber-400
+  `,
+};
diff --git a/docs/components/home/index.tsx b/docs/components/home/index.tsx
index 2cb2dfd2b..8a660e35d 100644
--- a/docs/components/home/index.tsx
+++ b/docs/components/home/index.tsx
@@ -1,24 +1,49 @@
 import { Code, Pre } from "nextra/components"
 
 import React from "react";
-import { useState } from 'react'
+import { useState, useEffect } from 'react'
 import { useTheme } from 'nextra-theme-docs'
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+import { faCheckCircle } from '@fortawesome/free-solid-svg-icons'
 import CodeSample from './code_sample.mdx'
 import ViolationSample from './violation_sample.mdx'
 
 import Image from 'next/image'
 
+import { classNames } from "./classNames";
+import { ProsOrConsList } from "./ProsOrConsList";
+
+const benefits = [
+  [
+    "Executable",
+    ["Quint", ["checked names and types", "executable"]],
+    ["English & Markdown", ["not checked", "not executuable"]],
+  ],
+  [
+    "Abstract",
+    ["Specification Languages", ["define only what you care about"]],
+    ["Programming Languages", ["define how things happen, in detail"]],
+  ],
+  [
+    "Modern",
+    ["Quint", ["familiar syntax", "CLI and your editor"]],
+    ["Existing Spec Languages", ["math-y syntax", "old GUI tools"]],
+  ],
+] as const;
+
+
 function informalSystemsLogo() {
-    const { resolvedTheme } = useTheme()
-    if (resolvedTheme == "dark") {
-      return (
-        <Image src="/informal-systems-white.png" alt="Informal Systems" width={200} height={200} />
-      );
-    } else {
-      return (
-        <Image src="/informal-systems.png" alt="Informal Systems" width={200} height={200} />
-      );
-  }
+  const { resolvedTheme } = useTheme();
+  const [theme, setTheme] = useState(null);
+    useEffect(() => {
+    setTheme(resolvedTheme);
+  }, [resolvedTheme]);
+
+  return (
+    <a href="https://informal.systems">
+      <Image src={theme == "dark" ? "/informal-systems-white.png" : "/informal-systems.png"} alt="Informal Systems" width={200} height={200} />
+    </a>
+  )
 }
 
 const components = {
@@ -42,41 +67,37 @@ export function Home() {
       <div className="relative px-4 mx-auto max-w-7xl sm:px-6 lg:px-2">
         <h1 className="text-4xl text-center font-bold leading-tight text-inherit sm:text-5xl sm:leading-tight lg:text-6xl lg:leading-tight font-pj">Quint</h1>
         <h2 className="text-quint-purple text-2xl text-center font-bold leading-tight sm:text-2xl sm:leading-tight lg:text-3xl lg:leading-tight font-pj">A modern and executable specification language</h2>
-        <div className="grid grid-cols-1 py-8 gap-y-4 lg:mt-8 lg:items-start lg:grid-cols-2 xl:grid-cols-2">
-          <div className="xl:col-span-1 lg:text-left text-center md:px-16 lg:px-0 xl:pr-20">
-            <h3 className="text-2xl font-bold leading-relaxed">Executable</h3>
-            <ul className="list-inside indent-4">
-              <li>English and Markdown: not checked, not executable</li>
-              <li className="font-bold">Quint: checked names and types, <a className="underline decoration-2 decoration-quint-purple">executable</a></li>
-            </ul>
-            <br />
-
-            <h3 className="text-2xl font-bold leading-relaxed">Specification language</h3>
-            <ul className="list-inside indent-4">
-              <li>Programming languages: define how things happen in detail</li>
-              <li className="font-bold">Specification languages: define only what you <a className="underline decoration-2 decoration-quint-purple">care</a> about</li>
-            </ul>
-            <br />
-
-            <h3 className="text-2xl font-bold leading-relaxed">Modern</h3>
-            <ul className="list-inside indent-4">
-              <li>Existing specification languages: Mathy syntax, old GUI tools</li>
-              <li className="font-bold">Quint: <a className="underline decoration-2 decoration-quint-purple">Familiar</a> syntax, CLI-first, tools for VSCode, Vim and Emacs</li>
-            </ul>
-
-            <a href="/docs/getting-started" title="" className="inline-flex px-8 py-4 mt-8 text-lg font-bold transition-all duration-200 bg-quint-purple text-white rounded sm:mt-10 font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900" role="button">
-              Get started
-            </a>
-
-            <div className="mt-8 mb-8 flex justify-center lg:justify-start">
-              {informalSystemsLogo()}
+        <div className="grid grid-cols-1 py-8 gap-y-4 gap-x-8 lg:mt-8 lg:items-start lg:grid-cols-2 xl:grid-cols-2">
+          <div className="xl:col-span-1">
+            <div className={classNames.container}>
+              {benefits.map(([label, [prosLabel, pros], [consLabel, cons]]) => (
+                <div className={classNames.benefitContainer}>
+                  <h1 className={classNames.benefitTitle}>
+                    <div className={classNames.benefitIcon}>
+                      <FontAwesomeIcon icon={faCheckCircle} />
+                    </div>
+                    {label}
+                  </h1>
+
+                  <div className={classNames.prosAndConsContainer}>
+                    <ProsOrConsList items={pros} label={prosLabel} type="pro" />
+                    <ProsOrConsList items={cons} label={consLabel} type="con" />
+                  </div>
+                </div>
+              ))}
+            </div>
+
+            <div className="mt-4 mb-8 flex justify-center">
+              <a href="/docs/getting-started" title="" className="inline-flex px-8 py-4 mt-8 text-lg font-bold transition-all duration-200 bg-quint-purple text-black rounded sm:mt-10 font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900" role="button">
+                Get started
+              </a>
             </div>
           </div>
 
           <div className="xl:col-span-1 text-lg">
             <CodeSample components={components} />
             <div className="flex justify-center">
-              <button onClick={handleToggleVisibility} className={`transition-all duration-500 ease-out overflow-hidden ${isViolationVisible ? 'hidden' : 'visible'} inline-flex px-4 py-2 font-bold transition-all duration-200 bg-quint-purple text-white rounded font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900`}>
+              <button onClick={handleToggleVisibility} className={`transition-all duration-500 ease-out overflow-hidden ${isViolationVisible ? 'hidden' : 'visible'} inline-flex px-4 py-2 font-bold transition-all duration-200 bg-quint-purple text-black rounded font-pj hover:bg-[#2d0075] hover:text-quint-purple focus:outline-none focus:ring-2 focus:ring-offset-2 focus:ring-gray-900`}>
                 Find bug
               </button>
             </div>
@@ -85,6 +106,10 @@ export function Home() {
             </div>
           </div>
         </div>
+
+        <div className="mt-8 mb-8 flex justify-center">
+          {informalSystemsLogo()}
+        </div>
       </div>
     </section >
   </div >
diff --git a/docs/package-lock.json b/docs/package-lock.json
index e0c3cd8de..a7621b9f5 100644
--- a/docs/package-lock.json
+++ b/docs/package-lock.json
@@ -1,16 +1,20 @@
 {
-  "name": "doc",
+  "name": "docs",
   "lockfileVersion": 3,
   "requires": true,
   "packages": {
     "": {
       "dependencies": {
+        "@fortawesome/fontawesome-svg-core": "^6.5.2",
+        "@fortawesome/free-solid-svg-icons": "^6.5.2",
+        "@fortawesome/react-fontawesome": "^0.2.2",
         "next": "^14.2.4",
         "nextra": "^2.13.4",
         "nextra-theme-docs": "^2.13.4",
         "react": "^18.3.1",
         "react-dom": "^18.3.1",
-        "react-svg": "^16.1.34"
+        "react-svg": "^16.1.34",
+        "tailwind-merge": "2.3.0"
       },
       "devDependencies": {
         "@types/node": "20.14.5",
@@ -48,6 +52,51 @@
       "resolved": "https://registry.npmjs.org/@braintree/sanitize-url/-/sanitize-url-6.0.4.tgz",
       "integrity": "sha512-s3jaWicZd0pkP0jf5ysyHUI/RE7MHos6qlToFcGWXVp+ykHOy77OUMrfbgJ9it2C5bow7OIQwYYaHjk9XlBQ2A=="
     },
+    "node_modules/@fortawesome/fontawesome-common-types": {
+      "version": "6.5.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.2.tgz",
+      "integrity": "sha512-gBxPg3aVO6J0kpfHNILc+NMhXnqHumFxOmjYCFfOiLZfwhnnfhtsdA2hfJlDnj+8PjAs6kKQPenOTKj3Rf7zHw==",
+      "hasInstallScript": true,
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/fontawesome-svg-core": {
+      "version": "6.5.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.5.2.tgz",
+      "integrity": "sha512-5CdaCBGl8Rh9ohNdxeeTMxIj8oc3KNBgIeLMvJosBMdslK/UnEB8rzyDRrbKdL1kDweqBPo4GT9wvnakHWucZw==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.5.2"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/free-solid-svg-icons": {
+      "version": "6.5.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.5.2.tgz",
+      "integrity": "sha512-QWFZYXFE7O1Gr1dTIp+D6UcFUF0qElOnZptpi7PBUMylJh+vFmIedVe1Ir6RM1t2tEQLLSV1k7bR4o92M+uqlw==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.5.2"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/react-fontawesome": {
+      "version": "0.2.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/react-fontawesome/-/react-fontawesome-0.2.2.tgz",
+      "integrity": "sha512-EnkrprPNqI6SXJl//m29hpaNzOp1bruISWaOiRtkMi/xSvHJlzc2j2JAYS7egxt/EbjSNV/k6Xy0AQI6vB2+1g==",
+      "dependencies": {
+        "prop-types": "^15.8.1"
+      },
+      "peerDependencies": {
+        "@fortawesome/fontawesome-svg-core": "~1 || ~6",
+        "react": ">=16.3"
+      }
+    },
     "node_modules/@headlessui/react": {
       "version": "1.7.19",
       "resolved": "https://registry.npmjs.org/@headlessui/react/-/react-1.7.19.tgz",
@@ -5828,6 +5877,18 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/tailwind-merge": {
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/tailwind-merge/-/tailwind-merge-2.3.0.tgz",
+      "integrity": "sha512-vkYrLpIP+lgR0tQCG6AP7zZXCTLc1Lnv/CCRT3BqJ9CZ3ui2++GPaGb1x/ILsINIMSYqqvrpqjUFsMNLlW99EA==",
+      "dependencies": {
+        "@babel/runtime": "^7.24.1"
+      },
+      "funding": {
+        "type": "github",
+        "url": "https://github.com/sponsors/dcastil"
+      }
+    },
     "node_modules/tailwindcss": {
       "version": "3.4.4",
       "resolved": "https://registry.npmjs.org/tailwindcss/-/tailwindcss-3.4.4.tgz",
diff --git a/docs/package.json b/docs/package.json
index 084e2eaa3..ecb9a4e12 100644
--- a/docs/package.json
+++ b/docs/package.json
@@ -1,11 +1,15 @@
 {
   "dependencies": {
+    "@fortawesome/fontawesome-svg-core": "^6.5.2",
+    "@fortawesome/free-solid-svg-icons": "^6.5.2",
+    "@fortawesome/react-fontawesome": "^0.2.2",
     "next": "^14.2.4",
     "nextra": "^2.13.4",
     "nextra-theme-docs": "^2.13.4",
     "react": "^18.3.1",
     "react-dom": "^18.3.1",
-    "react-svg": "^16.1.34"
+    "react-svg": "^16.1.34",
+    "tailwind-merge": "2.3.0"
   },
   "scripts": {
     "dev": "next",
diff --git a/docs/pages/_app.mdx b/docs/pages/_app.mdx
index 4700262ae..af89359b8 100644
--- a/docs/pages/_app.mdx
+++ b/docs/pages/_app.mdx
@@ -1,5 +1,8 @@
 import '../style.css'
+import '@fortawesome/fontawesome-svg-core/styles.css'; // Import the CSS
+import { config } from '@fortawesome/fontawesome-svg-core';
 
 export default function MyApp({ Component, pageProps }) {
+  config.autoAddCss = false;
   return <Component {...pageProps} />
 }
diff --git a/docs/tailwind.config.js b/docs/tailwind.config.js
index 361db4b0b..5b09bc485 100644
--- a/docs/tailwind.config.js
+++ b/docs/tailwind.config.js
@@ -14,6 +14,7 @@ module.exports = {
     extend: {
       colors: {
         'quint-purple': '#9d6ce5',
+        'quint-orange': '#ffab70',
       },
     }
   },
diff --git a/docs/theme.config.jsx b/docs/theme.config.jsx
index 89300eccb..2a3975074 100644
--- a/docs/theme.config.jsx
+++ b/docs/theme.config.jsx
@@ -14,7 +14,7 @@ export default {
       );
     }
   },
-  docsRepositoryBase: 'https://github.com/informalsystems/quint',
+  docsRepositoryBase: 'https://github.com/informalsystems/quint/blob/main/docs',
   project: {
     link: 'https://github.com/informalsystems/quint'
   },