feat: enforce Dafny formatting

.github/workflows/library_format.yml

@@ -0,0 +1,47 @@
+# This workflow performs static analysis checks.
+name: Library format check
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  format_projects:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        library:
+          [
+            DynamoDbEncryption,
+          ]
+        os: [ubuntu-latest]
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ '4.2.0' }}
+
+      - name: Check format of ${{ matrix.library }} Dafny code
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make format_dafny-check