Skip to content

content(projects): add witness as the 4th Verify tool #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Apr 28, 2026
Merged

content(projects): add witness as the 4th Verify tool #41

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
11 changes: 8 additions & 3 deletions templates/projects.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,10 @@ <h1 class="section-heading">{{ section.title }}</h1>
<span class="face-tool__name">Lean 4</span>
<span class="face-tool__desc">scheduling theory</span>
</a>
<a href="https://github.com/pulseengine/witness" class="face-tool" rel="noopener">
<span class="face-tool__name">witness</span>
<span class="face-tool__desc">MC/DC on Wasm IR</span>
</a>
</div>
<div class="face-divider"></div>
<div class="face-edge">
Expand Down Expand Up @@ -215,13 +219,14 @@ <h3 style="color:#22d3ee">Build — the pipeline</h3>
</div>

<div class="cube-detail__panel" data-detail="verify" style="display:none">
<h3 style="color:#4ade80">Verify — three independent proof paths across everything</h3>
<p><strong>Verus</strong> proves Rust code via SMT/Z3 — preconditions, postconditions, invariants on every public function. <strong>Rocq</strong> machine-checks abstract invariants that hold regardless of implementation. <strong>Lean 4</strong> proves scheduling theory — priority inheritance, deadline guarantees, starvation freedom.</p>
<p>These are not limited to one tool. Every component in the ecosystem — meld, loom, synth, kiln, gale, relay, wohl — carries formal verification. Three independent paths run in CI on every commit.</p>
<h3 style="color:#4ade80">Verify — three proof paths and the empirical coverage cell</h3>
<p><strong>Verus</strong> proves Rust code via SMT/Z3 — preconditions, postconditions, invariants on every public function. <strong>Rocq</strong> machine-checks abstract invariants that hold regardless of implementation. <strong>Lean 4</strong> proves scheduling theory — priority inheritance, deadline guarantees, starvation freedom. <strong>witness</strong> measures branch / MC/DC coverage at the post-compile WebAssembly level — the empirical counterpart that closes the §FM.6.7(f) / structural-coverage cell DO-178C, ISO 26262 Part 6 Table 12, and IEC 61508 Annex C expect.</p>
<p>These are not limited to one tool. Every component in the ecosystem — meld, loom, synth, kiln, gale, relay, wohl — carries formal verification. Four independent verification paths run in CI on every commit: three proof, one coverage.</p>
<div class="cube-detail__links">
<a href="https://github.com/pulseengine/rules_verus" rel="noopener">rules_verus</a>
<a href="https://github.com/pulseengine/rules_rocq_rust" rel="noopener">rules_rocq_rust</a>
<a href="https://github.com/pulseengine/rules_lean" rel="noopener">rules_lean</a>
<a href="https://github.com/pulseengine/witness" rel="noopener">witness</a>
<a href="https://github.com/pulseengine/gale" rel="noopener">gale</a>
</div>
</div>
Expand Down
Loading