Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
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
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ prevent entire categories of bugs. The language's goal is ...

[![CI](https://github.com/berkeleynerd/safe/actions/workflows/ci.yml/badge.svg)](https://github.com/berkeleynerd/safe/actions/workflows/ci.yml)
![Spec version](https://img.shields.io/badge/spec-v0.1_working_draft-blue)
![Proved fixtures](https://img.shields.io/badge/proved_fixtures-262-brightgreen)
![Proved fixtures](https://img.shields.io/badge/proved_fixtures-263-brightgreen)

The current toolchain compiles it through
Ada/SPARK-oriented artifacts. The user-facing goal is not to preserve Ada
Expand Down Expand Up @@ -150,7 +150,7 @@ itself.
Two independent evidence channels back the safety claims:

**Emitted proof corpus.** The blocking emitted-proof inventory currently covers
262 fixtures with 4 explicit exclusions and 0 uncovered fixtures: 3 frontend
263 fixtures with 4 explicit exclusions and 0 uncovered fixtures: 3 frontend
spec exclusions and 1 intentional tooling-reject fixture. No compiling
runtime-regression fixture remains outside the emitted proof lane. These
fixtures are emitted as Ada/SPARK and verified by GNATprove through the
Expand All @@ -163,11 +163,11 @@ proved, 1 Silver VC justified, and 0 unproved. Its 16 templates account for

| Metric | Value |
|--------|-------|
| Proved emitted fixtures | 262 (4 exclusions: 3 spec, 1 tooling, 0 runtime proof gaps; 0 uncovered) |
| Proved emitted fixtures | 263 (4 exclusions: 3 spec, 1 tooling, 0 runtime proof gaps; 0 uncovered) |
| Companion template VCs | 553 total (414 proved, 1 justified, 0 unproved, 138 flow passed) |
| Companion templates | 16 templates, 315 template checks |
| Tracked proof assumptions | [13](companion/assumptions.yaml) (12 open, 1 resolved) |
| Test corpus | 650 `.safe` files (positive, negative, build, concurrency, interfaces, embedded, emitted-shape) |
| Test corpus | 651 `.safe` files (positive, negative, build, concurrency, interfaces, embedded, emitted-shape) |
| Embedded evidence lane | STM32F4 / Jorvik / Renode (blocking in CI) |
| Compiler size | ~73K LOC Ada across 75 source files |
| Emitter size | ~26K LOC Ada across 14 emitter source files |
Expand Down
Loading
Loading