diff --git a/flake.lock b/flake.lock
index 7802641..3354709 100644
--- a/flake.lock
+++ b/flake.lock
@@ -44,11 +44,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1774274588,
-        "narHash": "sha256-dnHvv5EMUgTzGZmA+3diYjQU2O6BEpGLEOgJ1Qe9LaY=",
+        "lastModified": 1771744638,
+        "narHash": "sha256-EDLi+YAsEEAmMeZe1v6GccuGRbCkpSZp/+A6g+pivR8=",
         "owner": "nix-community",
         "repo": "home-manager",
-        "rev": "cf9686ba26f5ef788226843bc31fda4cf72e373b",
+        "rev": "cb6c151f5c9db4df0b69d06894dc8484de1f16a0",
         "type": "github"
       },
       "original": {
@@ -66,11 +66,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1773876229,
-        "narHash": "sha256-ncup+eYqHABZzBgwfQzxOXWHIcjN4kkZl9QTb4cgNm8=",
+        "lastModified": 1771243101,
+        "narHash": "sha256-p/qTbQU5wQEqbKWF8M0bZWuryUCrPsWrJB0GlNF1k6M=",
         "owner": "nix-community",
         "repo": "NixOS-WSL",
-        "rev": "381bc12a25d49c6b798f98ab33a8d951ec54659b",
+        "rev": "6d52ea6d66cb333c611c7b0e16dd24a05c9263e7",
         "type": "github"
       },
       "original": {
@@ -82,11 +82,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1774244481,
-        "narHash": "sha256-4XfMXU0DjN83o6HWZoKG9PegCvKvIhNUnRUI19vzTcQ=",
+        "lastModified": 1771714954,
+        "narHash": "sha256-nhZJPnBavtu40/L2aqpljrfUNb2rxmWTmSjK2c9UKds=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "4590696c8693fea477850fe379a01544293ca4e2",
+        "rev": "afbbf774e2087c3d734266c22f96fca2e78d3620",
         "type": "github"
       },
       "original": {
diff --git a/home/cli.nix b/home/cli.nix
index a91e159..03d5e2c 100644
--- a/home/cli.nix
+++ b/home/cli.nix
@@ -29,7 +29,7 @@
       "o" = "xdg-open";
       "update" = "sudo nixos-rebuild switch --flake ~/dev/nixos";
       "rm" = "rm -i";
-      "ls" = "eza --git-ignore -ls type";
+      "ls" = "eza";
     };
 
     stateVersion = "25.11";
diff --git a/home/graphical.nix b/home/graphical.nix
index ba0d7b3..8d863ad 100644
--- a/home/graphical.nix
+++ b/home/graphical.nix
@@ -15,7 +15,6 @@
         mattermost-desktop
         nerd-fonts.adwaita-mono
         newsflash
-        proton-pass
         protonmail-bridge-gui
         signal-desktop
         texliveFull
@@ -32,7 +31,6 @@
         rounded-window-corners-reborn
         runcat
         tray-icons-reloaded
-        useless-gaps
         window-centering
       ]);
 
diff --git a/home/packages/helix/default.nix b/home/packages/helix/default.nix
index 6fe6d74..cff82e7 100644
--- a/home/packages/helix/default.nix
+++ b/home/packages/helix/default.nix
@@ -18,32 +18,28 @@ in
       keys.insert.j.k = "normal_mode";
     };
     languages = {
-      language-server = {
-        tinymist = {
-          config.exportPdf = "onSave";
-          config.outputPath = "$root/$dir/out/$name";
-        };
-        scls = {
-          command = "simple-completion-language-server";
-          config.feature_words = false;
-          config.feature_snippets = true;
-          config.snippets_first = true;
-          config.snippets_inline_by_word_tail = false;
-          config.feature_unicode_input = true;
-          config.feature_paths = false;
-          config.feature_citations = false;
-          environment.RUST_LOG = "info,simple-completion-language-server=info";
-          environment.LOG_FILE = "/tmp/completion.log";
-        };
-        ocamllsp = {
-          command = "ocamllsp";
-          args = [ "--fallback-read-dot-merlin" ];
-        };
-        menhir-lsp.command = "menhir-lsp";
-        dafny-lsp = {
-          command = "dafny";
-          args = [ "server" ];
-        };
+      language-server.tinymist = {
+        config.exportPdf = "onSave";
+        config.outputPath = "$root/$dir/out/$name";
+      };
+      language-server.scls = {
+        command = "simple-completion-language-server";
+        config.feature_words = false;
+        config.feature_snippets = true;
+        config.snippets_first = true;
+        config.snippets_inline_by_word_tail = false;
+        config.feature_unicode_input = true;
+        config.feature_paths = false;
+        config.feature_citations = false;
+        environment.RUST_LOG = "info,simple-completion-language-server=info";
+        environment.LOG_FILE = "/tmp/completion.log";
+      };
+      language-server.ocamllsp = {
+        command = "ocamllsp";
+        args = [ "--fallback-read-dot-merlin" ];
+      };
+      language-server.menhir-lsp = {
+        command = "menhir-lsp";
       };
       language = [
         {
@@ -62,28 +58,6 @@ in
           ];
           scope = "source.menhir";
         }
-        {
-          name = "ocaml";
-          language-servers = [
-            "scls"
-            "ocamllsp"
-          ];
-        }
-        {
-          name = "dafny";
-          file-types = [ "dfy" ];
-          language-servers = [ "dafny-lsp" ];
-          scope = "source.dafny";
-        }
-        {
-          name = "zelus";
-          file-types = [
-            "zli"
-            "zls"
-          ];
-          language-servers = [ "scls" ];
-          scope = "source.ocaml";
-        }
       ];
       grammar = [
         {
diff --git a/shells/why3-dev/flake.nix b/shells/why3-dev/flake.nix
index 017cb55..06ebb8a 100644
--- a/shells/why3-dev/flake.nix
+++ b/shells/why3-dev/flake.nix
@@ -13,10 +13,7 @@
     {
       devShells."${system}".default =
         let
-          pkgs = import nixpkgs {
-            inherit system;
-            config.allowUnfree = true;
-          };
+          pkgs = import nixpkgs { inherit system; };
           menhir-lsp = pkgs.callPackage ./menhir-lsp.nix (pkgs // pkgs.ocamlPackages);
         in
         pkgs.mkShell {
@@ -24,20 +21,18 @@
             # Build elements
             autoconf
             ocaml
+            ocamlPackages.ocaml-lsp
             ocamlPackages.findlib
             ocamlPackages.menhir
             ocamlPackages.menhirLib
             ocamlPackages.zarith
             ocamlPackages.lablgtk3
             ocamlPackages.lablgtk3-sourceview3
-            ocamlPackages.camlzip
 
-            # Provers
-            alt-ergo
+            # Available provers
+            # alt-ergo
             cvc5
             z3
-            # Development tooling
-            ocamlPackages.ocaml-lsp
             menhir-lsp
           ];
         };