Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 45 additions & 0 deletions .github/workflows/seal-core.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
name: SEAL-Core

on:
push:
pull_request:

jobs:
fstar-verification:
runs-on: ubuntu-latest

env:
FSTAR_VERSION: v2026.03.24

steps:
- name: Check out repository
uses: actions/checkout@v4

- name: Install host packages
run: |
set -euo pipefail
sudo apt-get update
sudo apt-get install -y ca-certificates curl git gzip make tar

- name: Install F*
run: |
set -euo pipefail
mkdir -p "$RUNNER_TEMP/fstar-bin"
curl -fsSL https://aka.ms/install-fstar \
| bash -s -- \
--release \
--version "$FSTAR_VERSION" \
--dest "$RUNNER_TEMP/fstar" \
--link-dir "$RUNNER_TEMP/fstar-bin"
echo "$RUNNER_TEMP/fstar-bin" >> "$GITHUB_PATH"

- name: Check F* version
run: fstar.exe --version

- name: Verify SEAL-Core
run: |
set -euo pipefail
make toolchain
make verify
make test
git diff --check
11 changes: 11 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,17 @@ make verify
make test
```

## CI

```sh
make verify
make test
```

GitHub Actions verifies the F* authority model on push and pull request.

C extraction remains deferred until a compatible KaRaMeL toolchain is pinned.

## Current Prototype

SEAL-Core v0 models a small fail-closed authority gate in F*. The gate evaluates a subject operation against a capability set, evidence state, and transition receipt state.
Expand Down
Loading