Add simplex spec by dnkolegov-ar · Pull Request #3275 · commonwarexyz/monorepo

dnkolegov-ar · 2026-02-28T19:02:28Z

No description provided.

cloudflare-workers-and-pages · 2026-02-28T19:02:35Z

Deploying with Cloudflare Workers

The latest updates on your project. Learn more about integrating Git with Workers.

Status	Name	Latest Commit	Updated (UTC)
✅ Deployment successful! View logs	commonware-mcp	`5309b74`	Mar 04 2026, 04:46 PM

cloudflare-workers-and-pages · 2026-02-28T19:06:29Z

Deploying monorepo with Cloudflare Pages

Latest commit:	`5309b74`
Status:	✅ Deploy successful!
Preview URL:	https://a8b4e908.monorepo-eu0.pages.dev
Branch Preview URL:	https://denis-simplex-quint.monorepo-eu0.pages.dev

View logs

cursor

Cursor Bugbot has reviewed your changes and found 6 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

cursor · 2026-02-28T19:28:14Z

consensus/quint/scripts/invariant.sh

+QUINT_LOGS="./out_inv"
+
+# Default invariants list
+DEFAULT_INVARIANTS="no_proposal_equivocation,agreement,no_vote_equivocation_inv,no_nullification_and_finalization_in_the_same_view,validity,valid_last_finalized,certificates_are_valid_inv,notarized_consistency,safe_finalization"


Missing invariant in default verification list

Medium Severity

DEFAULT_INVARIANTS in invariant.sh is missing finalize_requires_notarization, which is included in all_invariants in replica.qnt. Running invariant.sh without explicitly specifying invariants will skip checking this safety property, meaning it won't be verified in parallel invariant checking workflows.

Additional Locations (1)

consensus/quint/replica.qnt#L1178-L1190

cursor · 2026-02-28T19:28:14Z

consensus/quint/tests/tests_n5f1b1.qnt

+
+    run timeoutBroadcastsNullifyTest = {
+        initWithLeaderAndCertify(
+            Map(0 -> "n0", 1 -> "n0", 2 -> "n1", 3 -> "n2", 4 -> "n3"),


Incomplete leader map missing views 5 and 6

Medium Severity

The leader map in timeoutBroadcastsNullifyTest only covers views 0–4, but VIEWS is 0.to(6) (views 0–6). Entries for views 5 and 6 are missing, which would cause a runtime error if any action tries to look up the leader for those views. Other tests in this file correctly provide all 7 entries.

cursor · 2026-02-28T19:28:14Z

consensus/quint/tests/tests_n5f1b1.qnt

+        val cert = notarization(FIRST_VIEW, "val_b1", Set("n0", "n1", "n2"), "n0")
+
+        initWithLeaderAndCertify(
+            Map(0 -> "n0", 1 -> "n0", 2 -> "n1", 3 -> "n2", 4 -> "n3", 4 -> "n3", 5 -> "n0", 6 -> "n0"),


Duplicate key in leader map literal

Low Severity

The leader map in notarizationCertificateTriggersFinalizeTest has key 4 specified twice (4 -> "n3", 4 -> "n3"). While both entries have the same value so behavior is unchanged, this is a copy-paste error that could mask a missing or incorrect mapping for a different view.

cursor · 2026-02-28T19:28:14Z

consensus/quint/replica.qnt

+    // Check this invariant to see an example of having a quorum of votes.
+    val votes_quorum_example = CORRECT.forall(id => {
+        store_vote.get(id).size() <= M
+    })


Subquorum and quorum examples have identical logic

Low Severity

votes_subquorum_example and votes_quorum_example both use the same threshold <= M. The subquorum example likely intended < M to find a state with fewer votes than a quorum, making these two "examples" indistinguishable.

cursor · 2026-02-28T19:28:14Z

consensus/quint/scripts/smoke.sh

+    "JVM_ARGS=-Xmx40G quint run --invariant=safe main_n6f1b1.qnt --max-samples 20000 --max-steps 50"
+    "JVM_ARGS=-Xmx40G quint verify --invariant=safe main_n6f1b0.qnt --max-steps 7"
+    "./scripts/invariant.sh run ./twins_n6f1b1.qnt 18 --random-transitions"
+    "./scripts/verify.sh random ./main_n6f1b0.qnt safe 10 1 10"


Scripts reference non-existent specification files

Medium Severity

smoke.sh references main_n6f1b1.qnt, main_n6f1b0.qnt, and twins_n6f1b1.qnt, and the makefile repl target references main_n6f0.qnt. None of these files exist in the repository. Running these scripts or the make repl target will fail.

Additional Locations (1)

consensus/quint/makefile#L21-L22

cursor · 2026-02-28T19:28:14Z

consensus/quint/replica.qnt

+            val can_send_nullify = and {
+                not(can_certify(id, cert_block_val)),
+                not(has_sent_nullify(id, cert_view_num)),
+            }


Missing finalize guard allows equivocation in nullify path

Medium Severity

The can_send_nullify guard is missing a not(has_sent_finalize(id, cert_view_num)) check, unlike the symmetric can_send_finalize guard which checks both not(has_sent_finalize(...)) and not(has_sent_nullify(...)). This allows a correct replica to send both finalize and nullify for the same view — when a Byzantine adversary injects a forged notarization certificate for a non-certifiable block in a view where the replica already finalized a different block. The resulting ghost_sent_votes sequence of length 3 would violate votes_seq_correct and the no_vote_equivocation_inv invariant.

This reverts commit 4d5fcf7.

codecov · 2026-03-04T17:48:57Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.00%. Comparing base (1386422) to head (5309b74).
⚠️ Report is 12 commits behind head on main.

@@            Coverage Diff             @@
##             main    #3275      +/-   ##
==========================================
- Coverage   93.86%   93.00%   -0.86%     
==========================================
  Files         419      418       -1     
  Lines      142507   141987     -520     
  Branches        0     3393    +3393     
==========================================
- Hits       133759   132051    -1708     
- Misses       8748     8846      +98     
- Partials        0     1090    +1090

see 205 files with indirect coverage changes

Continue to review full report in Codecov by Sentry.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1386422...5309b74. Read the comment docs.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

dnkolegov-ar force-pushed the denis/simplex-quint branch from fdd47e8 to 45ea60b Compare February 28, 2026 19:06

dnkolegov-ar force-pushed the denis/simplex-quint branch from 45ea60b to 21c58c8 Compare February 28, 2026 19:09

Add quint spec for Simplex

b8d4ab4

dnkolegov-ar force-pushed the denis/simplex-quint branch from 21c58c8 to b8d4ab4 Compare February 28, 2026 19:16

dnkolegov-ar marked this pull request as draft February 28, 2026 19:16

cursor bot reviewed Feb 28, 2026

View reviewed changes

dnkolegov-ar added 22 commits March 2, 2026 13:06

track parents

4bb7c87

fix timeout

48c0e2f

fix parent

c26871f

add more tests

b383560

update Q

f146e78

update invariants

437a48d

update params

b9c9717

fix bug in adb replica

041d9fc

init inv

e6b8633

use option

08993f9

remove empty block

b4471f9

update twins

8669fab

update byzantine vote sender

142d060

fix kinds

54cddbc

fix proposer

20e8727

debug

4d5fcf7

Revert "debug"

bcb74b6

This reverts commit 4d5fcf7.

split screen in smoke

55dda83

help

debe126

fix blunders

dff6efc

fix leader

cb627bc

update quint

c2e18c4

revert quint update

5309b74

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add simplex spec#3275

Add simplex spec#3275
dnkolegov-ar wants to merge 24 commits intomainfrom
denis/simplex-quint

dnkolegov-ar commented Feb 28, 2026

Uh oh!

cloudflare-workers-and-pages bot commented Feb 28, 2026 •

edited

Loading

Uh oh!

cloudflare-workers-and-pages bot commented Feb 28, 2026 •

edited

Loading

Uh oh!

cursor bot left a comment

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

cursor bot Feb 28, 2026

Uh oh!

codecov bot commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

dnkolegov-ar commented Feb 28, 2026

Uh oh!

cloudflare-workers-and-pages bot commented Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Deploying with Cloudflare Workers

Uh oh!

cloudflare-workers-and-pages bot commented Feb 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Deploying monorepo with Cloudflare Pages

Uh oh!

cursor bot left a comment

Choose a reason for hiding this comment

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Missing invariant in default verification list

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Incomplete leader map missing views 5 and 6

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Duplicate key in leader map literal

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Subquorum and quorum examples have identical logic

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Scripts reference non-existent specification files

Uh oh!

cursor bot Feb 28, 2026

Choose a reason for hiding this comment

Missing finalize guard allows equivocation in nullify path

Uh oh!

codecov bot commented Mar 4, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

cloudflare-workers-and-pages bot commented Feb 28, 2026 •

edited

Loading

cloudflare-workers-and-pages bot commented Feb 28, 2026 •

edited

Loading