diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7e14dfd7ff3072248ca5b9b640d5a926663f0df3..b86b0826b80d70a8319d3501b2ee27e4aaea8c5c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -57,6 +57,14 @@ wp-qualif:
    - nix
   allow_failure: true
 
+aorai-prove:
+  stage: tests
+  script:
+   - nix/frama-ci.sh build -A frama-c.aorai-prove
+  tags:
+   - nix
+  allow_failure: true
+
 genassigns:
   stage: tests
   script:
diff --git a/nix/default.nix b/nix/default.nix
index b3e6929a292d9f526fabea47f1ded55b933450e4..7a4cc5ffedbd16e8cc5fd638ca7131c6d5ffe7ee 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -187,6 +187,36 @@ rec {
         '';
   };
 
+  aorai-prove = mk_deriv {
+        name = "frama-c-aorai-prove";
+        buildInputs = mk_buildInputs { opamPackages = [
+                    { name = "alt-ergo"; constraint = "=2.0.0"; }
+               ]; };
+        build_dir = main.build_dir;
+        src = main.build_dir + "/dir.tar";
+        sourceRoot = ".";
+        postUnpack = ''
+               find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "test_config*" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
+        '';
+        configurePhase = ''
+           true
+        '';
+
+        buildPhase = ''
+          make clean_share_link
+          make create_share_link
+          mkdir home
+          HOME=$(pwd)/home
+          why3 config --full-config
+          make src/plugins/aorai/tests/ptests_config
+          make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
+        '';
+
+        installPhase = ''
+          true
+        '';
+  };
+
   e-acsl-tests-dev = mk_deriv {
         name = "frama-c-e-acsl-tests-dev";
         buildInputs = mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };