{"name":"io.github.daedalus/mcp-z3-prover","slug":"daedalus-mcp-z3-prover","title":null,"description":"MCP server exposing Z3 solver API","url":"https://mcp.market/server/daedalus-mcp-z3-prover","rating":null,"grade":"B","score":74,"certified":false,"status":"active","category":"other","tags":[],"presence":{"score":14,"stars":1,"forks":0,"downloads_week":12,"last_push_at":"2026-04-22T14:56:18.000Z","license":"MIT"},"uptime":null,"claimed":false,"transport":"pypi","callable_via_gateway":false,"default_price_micros":0,"repository":"https://github.com/daedalus/mcp-z3-prover","website":null,"version":"0.1.0","remotes":[],"packages":[{"registryType":"pypi","identifier":"mcp-z3-prover","version":"0.1.0","transport":{"type":"stdio"}}],"tools":[{"name":"add_constraint","description":"Add a constraint to the solver. Use variable references like 'bool:x', 'int:y', 'real:z' in expressions.","write_action":false,"price_micros":0,"input_schema":null},{"name":"create_bool_var","description":"Create a Boolean variable with the given name.","write_action":true,"price_micros":0,"input_schema":null},{"name":"create_int_constant","description":"Create an integer constant with the given value.","write_action":true,"price_micros":0,"input_schema":null},{"name":"create_int_var","description":"Create an Integer variable with the given name.","write_action":true,"price_micros":0,"input_schema":null},{"name":"create_real_constant","description":"Create a real constant with the given value.","write_action":true,"price_micros":0,"input_schema":null},{"name":"create_real_var","description":"Create a Real variable with the given name.","write_action":true,"price_micros":0,"input_schema":null},{"name":"get_model_value","description":"Get the value of a variable from the model after solving.","write_action":false,"price_micros":0,"input_schema":null},{"name":"list_variables","description":"List all created variables.","write_action":false,"price_micros":0,"input_schema":null},{"name":"optimize","description":"Solve with optimization objective (maximize or minimize).","write_action":false,"price_micros":0,"input_schema":null},{"name":"reset_solver","description":"Reset the solver state (clear all variables, constraints, and model).","write_action":false,"price_micros":0,"input_schema":null},{"name":"solve","description":"Solve the current problem and return the result.","write_action":false,"price_micros":0,"input_schema":null}],"scan":{"score":74,"grade":"B","scanned_at":"2026-09-27T23:19:45.735Z","report":{"scannerVersion":"0.1.9","scannedAt":"2026-09-27T23:19:45.697Z","components":{"code":{"score":20,"max":25,"notes":["4 source files scanned"]},"reliability":{"score":-1,"max":20,"notes":["no gateway calls yet and no remote to probe"]},"poisoning":{"score":-1,"max":15,"notes":["tools not inspected (local package is not executed); not counted"]},"auth":{"score":12,"max":15,"notes":["local package, no credentials required"]},"maintenance":{"score":8,"max":15,"notes":["last push 158 days ago"]},"identity":{"score":8,"max":10,"notes":["registry namespace matches repository owner","GitHub account older than a year"]}},"findings":[{"id":"exec.eval","severity":"medium","component":"code","title":"eval / new Function used","evidence":"mcp_z3_prover-0.1.0/src/mcp_z3_prover/_core.py: …t_map\": session.constants} result = eval(expr, {\"__builtins__\": {}}, local_vars) …"}],"inputs":{"packages":[{"registryType":"pypi","identifier":"mcp-z3-prover","version":"0.1.0","found":true,"weeklyDownloads":12,"license":"MIT","dependencyCount":20,"publishedAt":"2026-03-28T15:16:07.968314Z","repositoryUrl":"https://github.com/daedalus/mcp-z3-prover"}],"repo":{"found":true,"owner":"daedalus","repo":"mcp-z3-prover","archived":false,"pushedAt":"2026-04-22T14:56:18Z","stars":1,"forks":0,"openIssues":0,"ownerType":"User","ownerAvatarUrl":"https://avatars.githubusercontent.com/u/115175?v=4","ownerCreatedAt":"2009-08-14T02:32:04Z","license":"MIT"},"icon":{"url":"https://avatars.githubusercontent.com/u/115175?v=4&s=128","source":"github"},"presence":{"stars":1,"forks":0,"downloadsWeek":12,"license":"MIT","lastPushAt":"2026-04-22T14:56:18.000Z","score":14}}}},"grade_history":[],"reviews":[]}